Isabelle theorem prover
|
|
The Isabelle theorem prover an interactive theorem proving framework, a successor of the HOL theorem prover.
Example taken from a theory file
subsection{*Inductive definition of the even numbers*}
consts Ev :: "nat set" | Ev of type set of naturals
inductive Ev | Inductive definition, two cases
intros
ZeroI: "0 : Ev"
Add2I: "n : Ev ==> Suc(Suc n) : Ev"
text{* Using the introduction rules: *}
lemma "Suc(Suc(Suc(Suc 0))) \<in> Ev" | four belongs to Ev
apply(rule Add2I) | proof
apply(rule Add2I)
apply(rule ZeroI)
done
text{*A simple inductive proof: *}
lemma "n:Ev ==> n+n : Ev" | 2n is even if n is even
apply(erule Ev.induct) | induction
apply(simp) | simplification
apply(rule Ev.ZeroI)
apply(simp)
apply(rule Ev.Add2I)
apply(rule Ev.Add2I)
apply(assumption)
done
External link
- Isabelle website (http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html)
See also: theorem prover.