src/HOL/UNITY/Guar.thy
 changeset 13819 78f5885b76a9 parent 13812 91713a1915ee child 14112 95d51043d2a3
1.1 --- a/src/HOL/UNITY/Guar.thy	Sun Feb 16 12:16:07 2003 +0100
1.2 +++ b/src/HOL/UNITY/Guar.thy	Sun Feb 16 12:17:40 2003 +0100
1.3 @@ -32,21 +32,21 @@
1.4      case, proving equivalence with Chandy and Sanders's n-ary definitions*)
1.6    ex_prop  :: "'a program set => bool"
1.7 -   "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F Join G) \<in> X"
1.8 +   "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F\<squnion>G) \<in> X"
1.10    strict_ex_prop  :: "'a program set => bool"
1.11 -   "strict_ex_prop X == \<forall>F G.  F ok G --> (F \<in> X | G \<in> X) = (F Join G \<in> X)"
1.12 +   "strict_ex_prop X == \<forall>F G.  F ok G --> (F \<in> X | G \<in> X) = (F\<squnion>G \<in> X)"
1.14    uv_prop  :: "'a program set => bool"
1.15 -   "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F Join G) \<in> X)"
1.16 +   "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F\<squnion>G) \<in> X)"
1.18    strict_uv_prop  :: "'a program set => bool"
1.19     "strict_uv_prop X ==
1.20 -      SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F Join G \<in> X))"
1.21 +      SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F\<squnion>G \<in> X))"
1.23    guar :: "['a program set, 'a program set] => 'a program set"
1.24            (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
1.25 -   "X guarantees Y == {F. \<forall>G. F ok G --> F Join G \<in> X --> F Join G \<in> Y}"
1.26 +   "X guarantees Y == {F. \<forall>G. F ok G --> F\<squnion>G \<in> X --> F\<squnion>G \<in> Y}"
1.29    (* Weakest guarantees *)
1.30 @@ -64,8 +64,8 @@
1.31    refines :: "['a program, 'a program, 'a program set] => bool"
1.32  			("(3_ refines _ wrt _)" [10,10,10] 10)
1.33    "G refines F wrt X ==
1.34 -     \<forall>H. (F ok H  & G ok H & F Join H \<in> welldef \<inter> X) -->
1.35 -         (G Join H \<in> welldef \<inter> X)"
1.36 +     \<forall>H. (F ok H  & G ok H & F\<squnion>H \<in> welldef \<inter> X) -->
1.37 +         (G\<squnion>H \<in> welldef \<inter> X)"
1.39    iso_refines :: "['a program, 'a program, 'a program set] => bool"
1.40                                ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
1.41 @@ -146,19 +146,19 @@
1.42  (*** guarantees ***)
1.44  lemma guaranteesI:
1.45 -     "(!!G. [| F ok G; F Join G \<in> X |] ==> F Join G \<in> Y)
1.46 +     "(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y)
1.47        ==> F \<in> X guarantees Y"
1.48  by (simp add: guar_def component_def)
1.50  lemma guaranteesD:
1.51 -     "[| F \<in> X guarantees Y;  F ok G;  F Join G \<in> X |]
1.52 -      ==> F Join G \<in> Y"
1.53 +     "[| F \<in> X guarantees Y;  F ok G;  F\<squnion>G \<in> X |]
1.54 +      ==> F\<squnion>G \<in> Y"
1.55  by (unfold guar_def component_def, blast)
1.57  (*This version of guaranteesD matches more easily in the conclusion
1.58    The major premise can no longer be  F \<subseteq> H since we need to reason about G*)
1.59  lemma component_guaranteesD:
1.60 -     "[| F \<in> X guarantees Y;  F Join G = H;  H \<in> X;  F ok G |]
1.61 +     "[| F \<in> X guarantees Y;  F\<squnion>G = H;  H \<in> X;  F ok G |]
1.62        ==> H \<in> Y"
1.63  by (unfold guar_def, blast)
1.65 @@ -263,24 +263,24 @@
1.67  lemma guarantees_Join_Int:
1.68      "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]
1.69 -     ==> F Join G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
1.70 +     ==> F\<squnion>G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
1.71  apply (unfold guar_def)
1.72  apply (simp (no_asm))
1.73  apply safe
1.74  apply (simp add: Join_assoc)
1.75 -apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
1.76 +apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
1.77  apply (simp add: ok_commute)
1.78  apply (simp (no_asm_simp) add: Join_ac)
1.79  done
1.81  lemma guarantees_Join_Un:
1.82      "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]
1.83 -     ==> F Join G \<in> (U \<union> X) guarantees (V \<union> Y)"
1.84 +     ==> F\<squnion>G \<in> (U \<union> X) guarantees (V \<union> Y)"
1.85  apply (unfold guar_def)
1.86  apply (simp (no_asm))
1.87  apply safe
1.88  apply (simp add: Join_assoc)
1.89 -apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
1.90 +apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
1.91  apply (simp add: ok_commute)
1.92  apply (simp (no_asm_simp) add: Join_ac)
1.93  done
1.94 @@ -291,7 +291,7 @@
1.95  apply (unfold guar_def, auto)
1.96  apply (drule bspec, assumption)
1.97  apply (rename_tac "i")
1.98 -apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
1.99 +apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
1.100  apply (auto intro: OK_imp_ok
1.101              simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
1.102  done
1.103 @@ -302,7 +302,7 @@
1.104  apply (unfold guar_def, auto)
1.105  apply (drule bspec, assumption)
1.106  apply (rename_tac "i")
1.107 -apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
1.108 +apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
1.109  apply (auto intro: OK_imp_ok
1.110              simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
1.111  done
1.112 @@ -311,7 +311,7 @@
1.113  (*** guarantees laws for breaking down the program, by lcp ***)
1.115  lemma guarantees_Join_I1:
1.116 -     "[| F \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
1.117 +     "[| F \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
1.118  apply (unfold guar_def)
1.119  apply (simp (no_asm))
1.120  apply safe
1.121 @@ -319,7 +319,7 @@
1.122  done
1.124  lemma guarantees_Join_I2:
1.125 -     "[| G \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
1.126 +     "[| G \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
1.127  apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
1.128  apply (blast intro: guarantees_Join_I1)
1.129  done
1.130 @@ -328,17 +328,17 @@
1.131       "[| i \<in> I;  F i \<in> X guarantees Y;  OK I F |]
1.132        ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
1.133  apply (unfold guar_def, clarify)
1.134 -apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
1.135 +apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
1.136  apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
1.137  done
1.140  (*** well-definedness ***)
1.142 -lemma Join_welldef_D1: "F Join G \<in> welldef ==> F \<in> welldef"
1.143 +lemma Join_welldef_D1: "F\<squnion>G \<in> welldef ==> F \<in> welldef"
1.144  by (unfold welldef_def, auto)
1.146 -lemma Join_welldef_D2: "F Join G \<in> welldef ==> G \<in> welldef"
1.147 +lemma Join_welldef_D2: "F\<squnion>G \<in> welldef ==> G \<in> welldef"
1.148  by (unfold welldef_def, auto)
1.150  (*** refinement ***)
1.151 @@ -356,13 +356,13 @@
1.153  lemma strict_ex_refine_lemma:
1.154       "strict_ex_prop X
1.155 -      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X)
1.156 +      ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X)
1.157                = (F \<in> X --> G \<in> X)"
1.158  by (unfold strict_ex_prop_def, auto)
1.160  lemma strict_ex_refine_lemma_v:
1.161       "strict_ex_prop X
1.162 -      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =
1.163 +      ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =
1.164            (F \<in> welldef \<inter> X --> G \<in> X)"
1.165  apply (unfold strict_ex_prop_def, safe)
1.166  apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
1.167 @@ -371,7 +371,7 @@
1.169  lemma ex_refinement_thm:
1.170       "[| strict_ex_prop X;
1.171 -         \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X --> G Join H \<in> welldef |]
1.172 +         \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> G\<squnion>H \<in> welldef |]
1.173        ==> (G refines F wrt X) = (G iso_refines F wrt X)"
1.174  apply (rule_tac x = SKIP in allE, assumption)
1.175  apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
1.176 @@ -380,12 +380,12 @@
1.178  lemma strict_uv_refine_lemma:
1.179       "strict_uv_prop X ==>
1.180 -      (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X) = (F \<in> X --> G \<in> X)"
1.181 +      (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = (F \<in> X --> G \<in> X)"
1.182  by (unfold strict_uv_prop_def, blast)
1.184  lemma strict_uv_refine_lemma_v:
1.185       "strict_uv_prop X
1.186 -      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =
1.187 +      ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =
1.188            (F \<in> welldef \<inter> X --> G \<in> X)"
1.189  apply (unfold strict_uv_prop_def, safe)
1.190  apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
1.191 @@ -394,8 +394,8 @@
1.193  lemma uv_refinement_thm:
1.194       "[| strict_uv_prop X;
1.195 -         \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X -->
1.196 -             G Join H \<in> welldef |]
1.197 +         \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X -->
1.198 +             G\<squnion>H \<in> welldef |]
1.199        ==> (G refines F wrt X) = (G iso_refines F wrt X)"
1.200  apply (rule_tac x = SKIP in allE, assumption)
1.201  apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
1.202 @@ -458,15 +458,15 @@
1.203  by (unfold wx_def, auto)
1.205  (* Proposition 6 *)
1.206 -lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G \<in> X})"
1.207 +lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F\<squnion>G \<in> X})"
1.208  apply (unfold ex_prop_def, safe)
1.209 -apply (drule_tac x = "G Join Ga" in spec)
1.210 +apply (drule_tac x = "G\<squnion>Ga" in spec)
1.211  apply (force simp add: ok_Join_iff1 Join_assoc)
1.212 -apply (drule_tac x = "F Join Ga" in spec)
1.213 +apply (drule_tac x = "F\<squnion>Ga" in spec)
1.214  apply (simp (no_asm_use) add: ok_Join_iff1)
1.215  apply safe
1.216  apply (simp (no_asm_simp) add: ok_commute)
1.217 -apply (subgoal_tac "F Join G = G Join F")
1.218 +apply (subgoal_tac "F\<squnion>G = G\<squnion>F")
1.219  apply (simp (no_asm_simp) add: Join_assoc)
1.220  apply (simp (no_asm) add: Join_commute)
1.221  done
1.222 @@ -474,15 +474,15 @@
1.223  (* Equivalence with the other definition of wx *)
1.225  lemma wx_equiv:
1.226 - "wx X = {F. \<forall>G. F ok G --> (F Join G):X}"
1.227 + "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G):X}"
1.229  apply (unfold wx_def, safe)
1.230  apply (simp (no_asm_use) add: ex_prop_def)
1.231  apply (drule_tac x = x in spec)
1.232  apply (drule_tac x = G in spec)
1.233 -apply (frule_tac c = "x Join G" in subsetD, safe)
1.234 +apply (frule_tac c = "x\<squnion>G" in subsetD, safe)
1.235  apply (simp (no_asm))
1.236 -apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G \<in> X}" in exI, safe)
1.237 +apply (rule_tac x = "{F. \<forall>G. F ok G --> F\<squnion>G \<in> X}" in exI, safe)
1.238  apply (rule_tac  wx'_ex_prop)
1.239  apply (rotate_tac 1)
1.240  apply (drule_tac x = SKIP in spec, auto)