# Theory Even

Up to index of Isabelle/HOL/TLA

theory Even
imports State
`(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL    Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>                 Stephan Merz <Stephan.Merz at loria.fr>    Year:        2011    Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>*)header {* A simple illustrative example  *}theory Evenimports State begintext{*  A trivial example illustrating invariant proofs in the logic, and how  Isabelle/HOL can help with specification. It proves that @{text x} is  always even in a program where @{text x} is initialized as 0 and  always incremented by 2.*}inductive_set  Even :: "nat set"where  even_zero: "0 ∈ Even"| even_step: "n ∈ Even ==> Suc (Suc n) ∈ Even"locale Program =  fixes x :: "state => nat"  and init :: "temporal"  and act :: "temporal"  and phi :: "temporal"  defines "init ≡ TEMP \$x = # 0"  and "act ≡ TEMP x` = Suc<Suc<\$x>>"  and "phi ≡ TEMP init ∧ \<box>[act]_x"lemma (in Program) stutinvprog: "STUTINV phi"  by (auto simp: phi_def init_def act_def stutinvs nstutinvs)lemma  (in Program) inveven: "\<turnstile> phi --> \<box>(\$x ∈ # Even)"  unfolding phi_defproof (rule invmono)  show "\<turnstile> init --> \$x ∈ #Even"    by (auto simp: init_def even_zero)next  show "|~ \$x ∈ #Even ∧ [act]_x --> o(\$x ∈ #Even)"    by (auto simp: act_def even_step tla_defs)qedend`