## [f01853]: thys / TLA / Even.thy  Maximize  Restore  History

### 50 lines (40 with data), 1.5 kB

 ``` 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49``` ```(* Title: A Definitional Encoding of TLA in Isabelle/HOL Authors: Gudmund Grov Stephan Merz Year: 2011 Maintainer: Gudmund Grov *) 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: "init \ TEMP \$x = # 0" and act : "act \ TEMP x` = Suc>" and phi: "phi \ TEMP init \ \[act]_x" lemma (in Program) stutinvprog: "STUTINV phi" by (auto simp: phi init act stutinvs nstutinvs) lemma (in Program) inveven: "\ phi \ \(\$x \ # Even)" unfolding phi 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 ```