src/HOL/UNITY/Constrains.thy
changeset 13812 91713a1915ee
parent 13805 3786b2fd6808
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/UNITY/Constrains.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Constrains.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4  subsection{*traces and reachable*}
     1.5  
     1.6  lemma reachable_equiv_traces:
     1.7 -     "reachable F = {s. \<exists>evs. (s,evs): traces (Init F) (Acts F)}"
     1.8 +     "reachable F = {s. \<exists>evs. (s,evs) \<in> traces (Init F) (Acts F)}"
     1.9  apply safe
    1.10  apply (erule_tac [2] traces.induct)
    1.11  apply (erule reachable.induct)
    1.12 @@ -392,4 +392,35 @@
    1.13    used by Always_Int_I) *)
    1.14  lemmas Always_thin = thin_rl [of "F \<in> Always A", standard]
    1.15  
    1.16 +
    1.17 +subsection{*Totalize*}
    1.18 +
    1.19 +lemma reachable_imp_reachable_tot:
    1.20 +      "s \<in> reachable F ==> s \<in> reachable (totalize F)"
    1.21 +apply (erule reachable.induct)
    1.22 + apply (rule reachable.Init) 
    1.23 + apply simp 
    1.24 +apply (rule_tac act = "totalize_act act" in reachable.Acts) 
    1.25 +apply (auto simp add: totalize_act_def) 
    1.26 +done
    1.27 +
    1.28 +lemma reachable_tot_imp_reachable:
    1.29 +      "s \<in> reachable (totalize F) ==> s \<in> reachable F"
    1.30 +apply (erule reachable.induct)
    1.31 + apply (rule reachable.Init, simp) 
    1.32 +apply (force simp add: totalize_act_def intro: reachable.Acts) 
    1.33 +done
    1.34 +
    1.35 +lemma reachable_tot_eq [simp]: "reachable (totalize F) = reachable F"
    1.36 +by (blast intro: reachable_imp_reachable_tot reachable_tot_imp_reachable) 
    1.37 +
    1.38 +lemma totalize_Constrains_iff [simp]: "(totalize F \<in> A Co B) = (F \<in> A Co B)"
    1.39 +by (simp add: Constrains_def) 
    1.40 +
    1.41 +lemma totalize_Stable_iff [simp]: "(totalize F \<in> Stable A) = (F \<in> Stable A)"
    1.42 +by (simp add: Stable_def)
    1.43 +
    1.44 +lemma totalize_Always_iff [simp]: "(totalize F \<in> Always A) = (F \<in> Always A)"
    1.45 +by (simp add: Always_def)
    1.46 +
    1.47  end