6.5.1 Lemma

This handy little rule allows one to use proofs one has already done. The premises don’t have to match exactly, but they must be of the same form. Aris will check for each symbol it recognizes (connectives, quantifiers, parentheses, comma, and identity). These symbols must match exactly. Aris will then check that the sentences match the correct form, or rather that they appear in the correct order.

For example, if you already did a proof of the form:

• A <-> B
• A
• ——–
• B

And want to reuse it, then your reference sentences must be in the form ‘A’ <-> ‘B’, and ‘A’. In general, they do not have to be in that order, however. Then, your conclusion must be the second half of the biconditional.

This is where Isar interoperability comes in. Instead of selecting a previous Aris proof, a .thy file can be used. Aris will attempt to translate it into a form that it can use, using most of the keywords as references, and the lemmas and theorems as goals. These are the sentences that can be proved. For more information, see Isabelle/Isar.