Science Fair Project Encyclopedia
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
See also: theorem prover.
10-26-2009 08:16:03
The contents of this article is licensed from www.wikipedia.org under the GNU Free Documentation License. Click here to see the transparent copy and copyright details
The contents of this article is licensed from www.wikipedia.org under the GNU Free Documentation License. Click here to see the transparent copy and copyright details