Proving in Isabelle

Isabelle supports both forwards and backwards proof, though we focus on backwards proof (described previously on page ). The state of such a proof is represented by a set of premises (known as subgoals) that would imply the conclusion (known as the final goal):

$$[ \phi_1, \dots, \phi_n ]\Longrightarrow \phi$$

Where $[\phi_1,\cdots,\phi_n]$ are the premises and $\phi$ is the conclusion.

The initial state of a proof is the assertion:

$$[ \phi ]\Longrightarrow \phi$$

Successive proof states are reached by removing one of the premises, and replacing with it an equivalent set of premises. Functions that map one premise to zero or more different premises are referred to as tactics.

Premises that are axioms of the logic, or previously proven theorems may be removed from the set of subgoals, since they do not need to be proven.

The proof is complete when the set of subgoals has been reduced to the empty set, ie the proof state has been reduced to:

$$[ ]\Longrightarrow \phi$$

Some theorem proving systems show the full structure of the proof tree as it is built (for example Fred [18]), however Isabelle only informs the user of what the contents of the leaf nodes are, not their position in the tree structure. This may have the benefit that identical nodes are proven only once. This proof structure will be mirrored in the user interface.