Cheat Sheet for the Isabelle/HOL Theorem Prover in ProofGeneral

Rule Application Methods

To apply a method (i.e. do a proof step):

        apply method

Consider the following rule R, which in Isabelle looks like [| P1; ...; Pn |] ==> Q

        P1 ... Pn

To iterate over possible instantiations when applying a method, use:


To specify an instantiation, use the method (we similarly have erule_tac, drule_tac and frule_tac):

        rule_tac ?x="foo" and ?y="bar" and ?z="fish" in R

To direct one of these methods to subgoal number i:

        rule_tac [i] R

To limit the number of displayed subgoals, use pr n. Use prefer or defer to change ordering of subgoals.

Use + and ? and | to compose methods. Use by to apply the given method, then apply assumption then end the proof:

        by (drule mp, (assumption|arith))+?

Useful Rules

Variables are either bound or free ('?' qualifiers are omitted). If you can see question marks or boxes then probably your font does not support the required mathematical symbols (try this one instead).

For all
allI: (⋀x. P x) ⟹ ∀x. P x
allE: ⟦∀x. P x; P xR⟧ ⟹ R
spec: x. P xP x
exI: P x ⟹ ∃x. P x
exE: ⟦∃x. P x; ⋀x. P xQ⟧ ⟹ Q
impI: (PQ) ⟹ PQ
impE: PQ; P; QR⟧ ⟹ R
mp: PQ; P⟧ ⟹ Q
conjI: P; Q⟧ ⟹ PQ
conjE: PQ; ⟦P; Q⟧ ⟹ R⟧ ⟹ R
disjI1: PPQ
disjI2: QPQ
disjE: PQ; PR; QR⟧ ⟹ R
Int_lower1: ABA
Int_lower2: ABB
Un_upper1: AAB
Un_upper2: BAB
subset_trans: AB; BC⟧ ⟹ AC
CollectD: a ∈ {x. P x} ⟹ P a
ssubst: t = s; P s⟧ ⟹ P t
notnotD: ¬¬PP

Acknowledgements and Links

Some of this text is stolen from the Isabelle tutorial.

Valid HTML

Back to front page