src/HOL/UNITY/Union.thy
changeset 13812 91713a1915ee
parent 13805 3786b2fd6808
child 13819 78f5885b76a9
     1.1 --- a/src/HOL/UNITY/Union.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Union.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4    SKIP :: "'a program"
     1.5      "SKIP == mk_program (UNIV, {}, UNIV)"
     1.6  
     1.7 -  (*Characterizes safety properties.  Used with specifying AllowedActs*)
     1.8 +  (*Characterizes safety properties.  Used with specifying Allowed*)
     1.9    safety_prop :: "'a program set => bool"
    1.10      "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
    1.11  
    1.12 @@ -316,10 +316,10 @@
    1.13  subsection{*the ok and OK relations*}
    1.14  
    1.15  lemma ok_SKIP1 [iff]: "SKIP ok F"
    1.16 -by (auto simp add: ok_def)
    1.17 +by (simp add: ok_def)
    1.18  
    1.19  lemma ok_SKIP2 [iff]: "F ok SKIP"
    1.20 -by (auto simp add: ok_def)
    1.21 +by (simp add: ok_def)
    1.22  
    1.23  lemma ok_Join_commute:
    1.24       "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))"
    1.25 @@ -332,7 +332,8 @@
    1.26  
    1.27  lemma ok_iff_OK:
    1.28       "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"
    1.29 -by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb all_conj_distrib eq_commute, blast)
    1.30 +by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb
    1.31 +              all_conj_distrib eq_commute,   blast)
    1.32  
    1.33  lemma ok_Join_iff1 [iff]: "F ok (G Join H) = (F ok G & F ok H)"
    1.34  by (auto simp add: ok_def)
    1.35 @@ -374,7 +375,7 @@
    1.36  lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F i \<in> Allowed(F j))"
    1.37  by (auto simp add: OK_iff_ok ok_iff_Allowed)
    1.38  
    1.39 -subsection{*@{text safety_prop}, for reasoning about
    1.40 +subsection{*@{term safety_prop}, for reasoning about
    1.41   given instances of "ok"*}
    1.42  
    1.43  lemma safety_prop_Acts_iff:
    1.44 @@ -389,11 +390,6 @@
    1.45       "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X"
    1.46  by (simp add: Allowed_def safety_prop_Acts_iff)
    1.47  
    1.48 -lemma def_prg_Allowed:
    1.49 -     "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]  
    1.50 -      ==> Allowed F = X"
    1.51 -by (simp add: Allowed_eq)
    1.52 -
    1.53  (*For safety_prop to hold, the property must be satisfiable!*)
    1.54  lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \<subseteq> B)"
    1.55  by (simp add: safety_prop_def constrains_def, blast)
    1.56 @@ -413,9 +409,35 @@
    1.57       "(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)"
    1.58  by (auto simp add: safety_prop_def, blast)
    1.59  
    1.60 +lemma def_prg_Allowed:
    1.61 +     "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]  
    1.62 +      ==> Allowed F = X"
    1.63 +by (simp add: Allowed_eq)
    1.64 +
    1.65 +lemma Allowed_totalize [simp]: "Allowed (totalize F) = Allowed F"
    1.66 +by (simp add: Allowed_def) 
    1.67 +
    1.68 +lemma def_total_prg_Allowed:
    1.69 +     "[| F == mk_total_program (init, acts, UNION X Acts) ; safety_prop X |]  
    1.70 +      ==> Allowed F = X"
    1.71 +by (simp add: mk_total_program_def def_prg_Allowed) 
    1.72 +
    1.73  lemma def_UNION_ok_iff:
    1.74       "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]  
    1.75        ==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
    1.76  by (auto simp add: ok_def safety_prop_Acts_iff)
    1.77  
    1.78 +text{*The union of two total programs is total.*}
    1.79 +lemma totalize_Join: "totalize F Join totalize G = totalize (F Join G)"
    1.80 +by (simp add: program_equalityI totalize_def Join_def image_Un)
    1.81 +
    1.82 +lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F Join G)"
    1.83 +by (simp add: all_total_def, blast)
    1.84 +
    1.85 +lemma totalize_JN: "(\<Squnion>i \<in> I. totalize (F i)) = totalize(\<Squnion>i \<in> I. F i)"
    1.86 +by (simp add: program_equalityI totalize_def JOIN_def image_UN)
    1.87 +
    1.88 +lemma all_total_JN: "(!!i. i\<in>I ==> all_total (F i)) ==> all_total(\<Squnion>i\<in>I. F i)"
    1.89 +by (simp add: all_total_iff_totalize totalize_JN [symmetric])
    1.90 +
    1.91  end