Isabelle 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))) \ 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 

• Isabelle website

<< Previous Word Browser Next >>
caerleon chalk figures in the united kingdom tamara de lempicka self publishing muskingum river harbor defenses of manila and subic bays fort mills philippine division ovulation vowel shift patriarch ephiphanius of constantinople	louis ii of france katie hnida chain days of wine and roses marcello mastroianni divorce, italian style dana scott this sporting life clean programming language scalar field hud (movie)	uniqueness type cat ballou formal methods the spy who came in from the cold the pawnbroker hol theorem prover douglas dunn oskar werner carl czerny alan arkin herb ritts	cool hand luke cliff robertson edge of sanity lcf theorem prover charly the heart is a lonely hunter computer program analysis alan bates the fixer ron moody emigration