src/HOL/TLA/Init.thy
changeset 21624 6f79647cf536
parent 17309 c43ed29bd197
child 26304 02fbd0e7954a
     1.1 --- a/src/HOL/TLA/Init.thy	Fri Dec 01 17:22:33 2006 +0100
     1.2 +++ b/src/HOL/TLA/Init.thy	Sat Dec 02 02:52:02 2006 +0100
     1.3 @@ -4,9 +4,6 @@
     1.4      Author:      Stephan Merz
     1.5      Copyright:   1998 University of Munich
     1.6  
     1.7 -    Theory Name: Init
     1.8 -    Logic Image: HOL
     1.9 -
    1.10  Introduces type of temporal formulas. Defines interface between
    1.11  temporal formulas and its "subformulas" (state predicates and actions).
    1.12  *)
    1.13 @@ -43,6 +40,40 @@
    1.14    fw_stp_def:  "first_world == st1"
    1.15    fw_act_def:  "first_world == %sigma. (st1 sigma, st2 sigma)"
    1.16  
    1.17 -ML {* use_legacy_bindings (the_context ()) *}
    1.18 +lemma const_simps [int_rewrite, simp]:
    1.19 +  "|- (Init #True) = #True"
    1.20 +  "|- (Init #False) = #False"
    1.21 +  by (auto simp: Init_def)
    1.22 +
    1.23 +lemma Init_simps [int_rewrite]:
    1.24 +  "!!F. |- (Init ~F) = (~ Init F)"
    1.25 +  "|- (Init (P --> Q)) = (Init P --> Init Q)"
    1.26 +  "|- (Init (P & Q)) = (Init P & Init Q)"
    1.27 +  "|- (Init (P | Q)) = (Init P | Init Q)"
    1.28 +  "|- (Init (P = Q)) = ((Init P) = (Init Q))"
    1.29 +  "|- (Init (!x. F x)) = (!x. (Init F x))"
    1.30 +  "|- (Init (? x. F x)) = (? x. (Init F x))"
    1.31 +  "|- (Init (?! x. F x)) = (?! x. (Init F x))"
    1.32 +  by (auto simp: Init_def)
    1.33 +
    1.34 +lemma Init_stp_act: "|- (Init $P) = (Init P)"
    1.35 +  by (auto simp add: Init_def fw_act_def fw_stp_def)
    1.36 +
    1.37 +lemmas Init_simps = Init_stp_act [int_rewrite] Init_simps
    1.38 +lemmas Init_stp_act_rev = Init_stp_act [int_rewrite, symmetric]
    1.39 +
    1.40 +lemma Init_temp: "|- (Init F) = F"
    1.41 +  by (auto simp add: Init_def fw_temp_def)
    1.42 +
    1.43 +lemmas Init_simps = Init_temp [int_rewrite] Init_simps
    1.44 +
    1.45 +(* Trivial instances of the definitions that avoid introducing lambda expressions. *)
    1.46 +lemma Init_stp: "(sigma |= Init P) = P (st1 sigma)"
    1.47 +  by (simp add: Init_def fw_stp_def)
    1.48 +
    1.49 +lemma Init_act: "(sigma |= Init A) = A (st1 sigma, st2 sigma)"
    1.50 +  by (simp add: Init_def fw_act_def)
    1.51 +
    1.52 +lemmas Init_defs = Init_stp Init_act Init_temp [int_use]
    1.53  
    1.54  end