Theory Even

(*  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 Even
imports State 
begin

text{*
  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_def
proof (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)
qed


end