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>
*)

section ‹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 ‹x› is
  always even in a program where ‹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 ∧ □[act]_x"

lemma (in Program) stutinvprog: "STUTINV phi"
  by (auto simp: phi_def init_def act_def stutinvs nstutinvs)

lemma  (in Program) inveven: "⊢ phi ⟶ □($x ∈ # Even)"
  unfolding phi_def
proof (rule invmono)
  show "⊢ init ⟶ $x ∈ #Even"
    by (auto simp: init_def even_zero)
next
  show "|~ $x ∈ #Even ∧ [act]_x ⟶ ○($x ∈ #Even)"
    by (auto simp: act_def even_step tla_defs)
qed


end