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.5  
     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.9  
    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.13  
    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.17  
    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.22  
    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.27    
    1.28  
    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.38  
    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.43  
    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.49  
    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.56  
    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.64  
    1.65 @@ -263,24 +263,24 @@
    1.66  
    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.80  
    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.114  
   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.123  
   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.138  
   1.139  
   1.140  (*** well-definedness ***)
   1.141  
   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.145  
   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.149  
   1.150  (*** refinement ***)
   1.151 @@ -356,13 +356,13 @@
   1.152  
   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.159  
   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.168  
   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.177  
   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.183  
   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.192  
   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.204  
   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.224  
   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.228  
   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 [2] wx'_ex_prop)
   1.239  apply (rotate_tac 1)
   1.240  apply (drule_tac x = SKIP in spec, auto)