src/HOL/UNITY/Project.thy
changeset 13819 78f5885b76a9
parent 13812 91713a1915ee
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/UNITY/Project.thy	Sun Feb 16 12:16:07 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Project.thy	Sun Feb 16 12:17:40 2003 +0100
     1.3 @@ -16,13 +16,13 @@
     1.4    projecting :: "['c program => 'c set, 'a*'b => 'c, 
     1.5  		  'a program, 'c program set, 'a program set] => bool"
     1.6      "projecting C h F X' X ==
     1.7 -       \<forall>G. extend h F Join G \<in> X' --> F Join project h (C G) G \<in> X"
     1.8 +       \<forall>G. extend h F\<squnion>G \<in> X' --> F\<squnion>project h (C G) G \<in> X"
     1.9  
    1.10    extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
    1.11  		 'c program set, 'a program set] => bool"
    1.12      "extending C h F Y' Y ==
    1.13 -       \<forall>G. extend h F  ok G --> F Join project h (C G) G \<in> Y
    1.14 -	      --> extend h F Join G \<in> Y'"
    1.15 +       \<forall>G. extend h F  ok G --> F\<squnion>project h (C G) G \<in> Y
    1.16 +	      --> extend h F\<squnion>G \<in> Y'"
    1.17  
    1.18    subset_closed :: "'a set set => bool"
    1.19      "subset_closed U == \<forall>A \<in> U. Pow A \<subseteq> U"  
    1.20 @@ -44,11 +44,11 @@
    1.21  apply (blast dest: stable_constrains_Int intro: constrains_weaken)
    1.22  done
    1.23  
    1.24 -(*Generalizes project_constrains to the program F Join project h C G
    1.25 +(*Generalizes project_constrains to the program F\<squnion>project h C G
    1.26    useful with guarantees reasoning*)
    1.27  lemma (in Extend) Join_project_constrains:
    1.28 -     "(F Join project h C G \<in> A co B)  =   
    1.29 -        (extend h F Join G \<in> (C \<inter> extend_set h A) co (extend_set h B) &   
    1.30 +     "(F\<squnion>project h C G \<in> A co B)  =   
    1.31 +        (extend h F\<squnion>G \<in> (C \<inter> extend_set h A) co (extend_set h B) &   
    1.32           F \<in> A co B)"
    1.33  apply (simp (no_asm) add: project_constrains)
    1.34  apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken] 
    1.35 @@ -58,9 +58,9 @@
    1.36  (*The condition is required to prove the left-to-right direction
    1.37    could weaken it to G \<in> (C \<inter> extend_set h A) co C*)
    1.38  lemma (in Extend) Join_project_stable: 
    1.39 -     "extend h F Join G \<in> stable C  
    1.40 -      ==> (F Join project h C G \<in> stable A)  =   
    1.41 -          (extend h F Join G \<in> stable (C \<inter> extend_set h A) &   
    1.42 +     "extend h F\<squnion>G \<in> stable C  
    1.43 +      ==> (F\<squnion>project h C G \<in> stable A)  =   
    1.44 +          (extend h F\<squnion>G \<in> stable (C \<inter> extend_set h A) &   
    1.45             F \<in> stable A)"
    1.46  apply (unfold stable_def)
    1.47  apply (simp only: Join_project_constrains)
    1.48 @@ -69,23 +69,23 @@
    1.49  
    1.50  (*For using project_guarantees in particular cases*)
    1.51  lemma (in Extend) project_constrains_I:
    1.52 -     "extend h F Join G \<in> extend_set h A co extend_set h B  
    1.53 -      ==> F Join project h C G \<in> A co B"
    1.54 +     "extend h F\<squnion>G \<in> extend_set h A co extend_set h B  
    1.55 +      ==> F\<squnion>project h C G \<in> A co B"
    1.56  apply (simp add: project_constrains extend_constrains)
    1.57  apply (blast intro: constrains_weaken dest: constrains_imp_subset)
    1.58  done
    1.59  
    1.60  lemma (in Extend) project_increasing_I: 
    1.61 -     "extend h F Join G \<in> increasing (func o f)  
    1.62 -      ==> F Join project h C G \<in> increasing func"
    1.63 +     "extend h F\<squnion>G \<in> increasing (func o f)  
    1.64 +      ==> F\<squnion>project h C G \<in> increasing func"
    1.65  apply (unfold increasing_def stable_def)
    1.66  apply (simp del: Join_constrains
    1.67              add: project_constrains_I extend_set_eq_Collect)
    1.68  done
    1.69  
    1.70  lemma (in Extend) Join_project_increasing:
    1.71 -     "(F Join project h UNIV G \<in> increasing func)  =   
    1.72 -      (extend h F Join G \<in> increasing (func o f))"
    1.73 +     "(F\<squnion>project h UNIV G \<in> increasing func)  =   
    1.74 +      (extend h F\<squnion>G \<in> increasing (func o f))"
    1.75  apply (rule iffI)
    1.76  apply (erule_tac [2] project_increasing_I)
    1.77  apply (simp del: Join_stable
    1.78 @@ -95,8 +95,8 @@
    1.79  
    1.80  (*The UNIV argument is essential*)
    1.81  lemma (in Extend) project_constrains_D:
    1.82 -     "F Join project h UNIV G \<in> A co B  
    1.83 -      ==> extend h F Join G \<in> extend_set h A co extend_set h B"
    1.84 +     "F\<squnion>project h UNIV G \<in> A co B  
    1.85 +      ==> extend h F\<squnion>G \<in> extend_set h A co extend_set h B"
    1.86  by (simp add: project_constrains extend_constrains)
    1.87  
    1.88  
    1.89 @@ -204,9 +204,9 @@
    1.90  
    1.91  (*In practice, C = reachable(...): the inclusion is equality*)
    1.92  lemma (in Extend) reachable_imp_reachable_project:
    1.93 -     "[| reachable (extend h F Join G) \<subseteq> C;   
    1.94 -         z \<in> reachable (extend h F Join G) |]  
    1.95 -      ==> f z \<in> reachable (F Join project h C G)"
    1.96 +     "[| reachable (extend h F\<squnion>G) \<subseteq> C;   
    1.97 +         z \<in> reachable (extend h F\<squnion>G) |]  
    1.98 +      ==> f z \<in> reachable (F\<squnion>project h C G)"
    1.99  apply (erule reachable.induct)
   1.100  apply (force intro!: reachable.Init simp add: split_extended_all, auto)
   1.101   apply (rule_tac act = x in reachable.Acts)
   1.102 @@ -217,8 +217,8 @@
   1.103  done
   1.104  
   1.105  lemma (in Extend) project_Constrains_D: 
   1.106 -     "F Join project h (reachable (extend h F Join G)) G \<in> A Co B   
   1.107 -      ==> extend h F Join G \<in> (extend_set h A) Co (extend_set h B)"
   1.108 +     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B   
   1.109 +      ==> extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)"
   1.110  apply (unfold Constrains_def)
   1.111  apply (simp del: Join_constrains
   1.112              add: Join_project_constrains, clarify)
   1.113 @@ -227,22 +227,22 @@
   1.114  done
   1.115  
   1.116  lemma (in Extend) project_Stable_D: 
   1.117 -     "F Join project h (reachable (extend h F Join G)) G \<in> Stable A   
   1.118 -      ==> extend h F Join G \<in> Stable (extend_set h A)"
   1.119 +     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A   
   1.120 +      ==> extend h F\<squnion>G \<in> Stable (extend_set h A)"
   1.121  apply (unfold Stable_def)
   1.122  apply (simp (no_asm_simp) add: project_Constrains_D)
   1.123  done
   1.124  
   1.125  lemma (in Extend) project_Always_D: 
   1.126 -     "F Join project h (reachable (extend h F Join G)) G \<in> Always A   
   1.127 -      ==> extend h F Join G \<in> Always (extend_set h A)"
   1.128 +     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A   
   1.129 +      ==> extend h F\<squnion>G \<in> Always (extend_set h A)"
   1.130  apply (unfold Always_def)
   1.131  apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
   1.132  done
   1.133  
   1.134  lemma (in Extend) project_Increasing_D: 
   1.135 -     "F Join project h (reachable (extend h F Join G)) G \<in> Increasing func   
   1.136 -      ==> extend h F Join G \<in> Increasing (func o f)"
   1.137 +     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func   
   1.138 +      ==> extend h F\<squnion>G \<in> Increasing (func o f)"
   1.139  apply (unfold Increasing_def, auto)
   1.140  apply (subst extend_set_eq_Collect [symmetric])
   1.141  apply (simp (no_asm_simp) add: project_Stable_D)
   1.142 @@ -253,9 +253,9 @@
   1.143  
   1.144  (*In practice, C = reachable(...): the inclusion is equality*)
   1.145  lemma (in Extend) reachable_project_imp_reachable:
   1.146 -     "[| C \<subseteq> reachable(extend h F Join G);    
   1.147 -         x \<in> reachable (F Join project h C G) |]  
   1.148 -      ==> \<exists>y. h(x,y) \<in> reachable (extend h F Join G)"
   1.149 +     "[| C \<subseteq> reachable(extend h F\<squnion>G);    
   1.150 +         x \<in> reachable (F\<squnion>project h C G) |]  
   1.151 +      ==> \<exists>y. h(x,y) \<in> reachable (extend h F\<squnion>G)"
   1.152  apply (erule reachable.induct)
   1.153  apply  (force intro: reachable.Init)
   1.154  apply (auto simp add: project_act_def)
   1.155 @@ -263,22 +263,22 @@
   1.156  done
   1.157  
   1.158  lemma (in Extend) project_set_reachable_extend_eq:
   1.159 -     "project_set h (reachable (extend h F Join G)) =  
   1.160 -      reachable (F Join project h (reachable (extend h F Join G)) G)"
   1.161 +     "project_set h (reachable (extend h F\<squnion>G)) =  
   1.162 +      reachable (F\<squnion>project h (reachable (extend h F\<squnion>G)) G)"
   1.163  by (auto dest: subset_refl [THEN reachable_imp_reachable_project] 
   1.164                 subset_refl [THEN reachable_project_imp_reachable])
   1.165  
   1.166  (*UNUSED*)
   1.167  lemma (in Extend) reachable_extend_Join_subset:
   1.168 -     "reachable (extend h F Join G) \<subseteq> C   
   1.169 -      ==> reachable (extend h F Join G) \<subseteq>  
   1.170 -          extend_set h (reachable (F Join project h C G))"
   1.171 +     "reachable (extend h F\<squnion>G) \<subseteq> C   
   1.172 +      ==> reachable (extend h F\<squnion>G) \<subseteq>  
   1.173 +          extend_set h (reachable (F\<squnion>project h C G))"
   1.174  apply (auto dest: reachable_imp_reachable_project)
   1.175  done
   1.176  
   1.177  lemma (in Extend) project_Constrains_I: 
   1.178 -     "extend h F Join G \<in> (extend_set h A) Co (extend_set h B)   
   1.179 -      ==> F Join project h (reachable (extend h F Join G)) G \<in> A Co B"
   1.180 +     "extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)   
   1.181 +      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B"
   1.182  apply (unfold Constrains_def)
   1.183  apply (simp del: Join_constrains
   1.184              add: Join_project_constrains extend_set_Int_distrib)
   1.185 @@ -291,43 +291,43 @@
   1.186  done
   1.187  
   1.188  lemma (in Extend) project_Stable_I: 
   1.189 -     "extend h F Join G \<in> Stable (extend_set h A)   
   1.190 -      ==> F Join project h (reachable (extend h F Join G)) G \<in> Stable A"
   1.191 +     "extend h F\<squnion>G \<in> Stable (extend_set h A)   
   1.192 +      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A"
   1.193  apply (unfold Stable_def)
   1.194  apply (simp (no_asm_simp) add: project_Constrains_I)
   1.195  done
   1.196  
   1.197  lemma (in Extend) project_Always_I: 
   1.198 -     "extend h F Join G \<in> Always (extend_set h A)   
   1.199 -      ==> F Join project h (reachable (extend h F Join G)) G \<in> Always A"
   1.200 +     "extend h F\<squnion>G \<in> Always (extend_set h A)   
   1.201 +      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A"
   1.202  apply (unfold Always_def)
   1.203  apply (auto simp add: project_Stable_I)
   1.204  apply (unfold extend_set_def, blast)
   1.205  done
   1.206  
   1.207  lemma (in Extend) project_Increasing_I: 
   1.208 -    "extend h F Join G \<in> Increasing (func o f)   
   1.209 -     ==> F Join project h (reachable (extend h F Join G)) G \<in> Increasing func"
   1.210 +    "extend h F\<squnion>G \<in> Increasing (func o f)   
   1.211 +     ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func"
   1.212  apply (unfold Increasing_def, auto)
   1.213  apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
   1.214  done
   1.215  
   1.216  lemma (in Extend) project_Constrains:
   1.217 -     "(F Join project h (reachable (extend h F Join G)) G \<in> A Co B)  =   
   1.218 -      (extend h F Join G \<in> (extend_set h A) Co (extend_set h B))"
   1.219 +     "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B)  =   
   1.220 +      (extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B))"
   1.221  apply (blast intro: project_Constrains_I project_Constrains_D)
   1.222  done
   1.223  
   1.224  lemma (in Extend) project_Stable: 
   1.225 -     "(F Join project h (reachable (extend h F Join G)) G \<in> Stable A)  =   
   1.226 -      (extend h F Join G \<in> Stable (extend_set h A))"
   1.227 +     "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A)  =   
   1.228 +      (extend h F\<squnion>G \<in> Stable (extend_set h A))"
   1.229  apply (unfold Stable_def)
   1.230  apply (rule project_Constrains)
   1.231  done
   1.232  
   1.233  lemma (in Extend) project_Increasing: 
   1.234 -   "(F Join project h (reachable (extend h F Join G)) G \<in> Increasing func)  =  
   1.235 -    (extend h F Join G \<in> Increasing (func o f))"
   1.236 +   "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func)  =  
   1.237 +    (extend h F\<squnion>G \<in> Increasing (func o f))"
   1.238  apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
   1.239  done
   1.240  
   1.241 @@ -335,7 +335,7 @@
   1.242      about guarantees.*}
   1.243  
   1.244  lemma (in Extend) projecting_Constrains: 
   1.245 -     "projecting (%G. reachable (extend h F Join G)) h F  
   1.246 +     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
   1.247                   (extend_set h A Co extend_set h B) (A Co B)"
   1.248  
   1.249  apply (unfold projecting_def)
   1.250 @@ -343,49 +343,49 @@
   1.251  done
   1.252  
   1.253  lemma (in Extend) projecting_Stable: 
   1.254 -     "projecting (%G. reachable (extend h F Join G)) h F  
   1.255 +     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
   1.256                   (Stable (extend_set h A)) (Stable A)"
   1.257  apply (unfold Stable_def)
   1.258  apply (rule projecting_Constrains)
   1.259  done
   1.260  
   1.261  lemma (in Extend) projecting_Always: 
   1.262 -     "projecting (%G. reachable (extend h F Join G)) h F  
   1.263 +     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
   1.264                   (Always (extend_set h A)) (Always A)"
   1.265  apply (unfold projecting_def)
   1.266  apply (blast intro: project_Always_I)
   1.267  done
   1.268  
   1.269  lemma (in Extend) projecting_Increasing: 
   1.270 -     "projecting (%G. reachable (extend h F Join G)) h F  
   1.271 +     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
   1.272                   (Increasing (func o f)) (Increasing func)"
   1.273  apply (unfold projecting_def)
   1.274  apply (blast intro: project_Increasing_I)
   1.275  done
   1.276  
   1.277  lemma (in Extend) extending_Constrains: 
   1.278 -     "extending (%G. reachable (extend h F Join G)) h F  
   1.279 +     "extending (%G. reachable (extend h F\<squnion>G)) h F  
   1.280                    (extend_set h A Co extend_set h B) (A Co B)"
   1.281  apply (unfold extending_def)
   1.282  apply (blast intro: project_Constrains_D)
   1.283  done
   1.284  
   1.285  lemma (in Extend) extending_Stable: 
   1.286 -     "extending (%G. reachable (extend h F Join G)) h F  
   1.287 +     "extending (%G. reachable (extend h F\<squnion>G)) h F  
   1.288                    (Stable (extend_set h A)) (Stable A)"
   1.289  apply (unfold extending_def)
   1.290  apply (blast intro: project_Stable_D)
   1.291  done
   1.292  
   1.293  lemma (in Extend) extending_Always: 
   1.294 -     "extending (%G. reachable (extend h F Join G)) h F  
   1.295 +     "extending (%G. reachable (extend h F\<squnion>G)) h F  
   1.296                    (Always (extend_set h A)) (Always A)"
   1.297  apply (unfold extending_def)
   1.298  apply (blast intro: project_Always_D)
   1.299  done
   1.300  
   1.301  lemma (in Extend) extending_Increasing: 
   1.302 -     "extending (%G. reachable (extend h F Join G)) h F  
   1.303 +     "extending (%G. reachable (extend h F\<squnion>G)) h F  
   1.304                    (Increasing (func o f)) (Increasing func)"
   1.305  apply (unfold extending_def)
   1.306  apply (blast intro: project_Increasing_D)
   1.307 @@ -423,8 +423,8 @@
   1.308  (*Used to prove project_leadsETo_I*)
   1.309  lemma (in Extend) ensures_extend_set_imp_project_ensures:
   1.310       "[| extend h F \<in> stable C;  G \<in> stable C;   
   1.311 -         extend h F Join G \<in> A ensures B;  A-B = C \<inter> extend_set h D |]   
   1.312 -      ==> F Join project h C G   
   1.313 +         extend h F\<squnion>G \<in> A ensures B;  A-B = C \<inter> extend_set h D |]   
   1.314 +      ==> F\<squnion>project h C G   
   1.315              \<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)"
   1.316  apply (simp add: ensures_def project_constrains Join_transient extend_transient,
   1.317         clarify)
   1.318 @@ -482,9 +482,9 @@
   1.319  
   1.320  (*Used to prove project_leadsETo_D*)
   1.321  lemma (in Extend) Join_project_ensures [rule_format]:
   1.322 -     "[| extend h F Join G \<in> stable C;   
   1.323 -         F Join project h C G \<in> A ensures B |]  
   1.324 -      ==> extend h F Join G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
   1.325 +     "[| extend h F\<squnion>G \<in> stable C;   
   1.326 +         F\<squnion>project h C G \<in> A ensures B |]  
   1.327 +      ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
   1.328  apply (auto simp add: ensures_eq extend_unless project_unless)
   1.329  apply (blast intro:  extend_transient [THEN iffD2] transient_strengthen)  
   1.330  apply (blast intro: project_transient_extend_set transient_strengthen)  
   1.331 @@ -496,9 +496,9 @@
   1.332  (*The strange induction formula allows induction over the leadsTo
   1.333    assumption's non-atomic precondition*)
   1.334  lemma (in Extend) PLD_lemma:
   1.335 -     "[| extend h F Join G \<in> stable C;   
   1.336 -         F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
   1.337 -      ==> extend h F Join G \<in>  
   1.338 +     "[| extend h F\<squnion>G \<in> stable C;   
   1.339 +         F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
   1.340 +      ==> extend h F\<squnion>G \<in>  
   1.341            C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)"
   1.342  apply (erule leadsTo_induct)
   1.343    apply (blast intro: leadsTo_Basis Join_project_ensures)
   1.344 @@ -507,17 +507,17 @@
   1.345  done
   1.346  
   1.347  lemma (in Extend) project_leadsTo_D_lemma:
   1.348 -     "[| extend h F Join G \<in> stable C;   
   1.349 -         F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
   1.350 -      ==> extend h F Join G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
   1.351 +     "[| extend h F\<squnion>G \<in> stable C;   
   1.352 +         F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
   1.353 +      ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
   1.354  apply (rule PLD_lemma [THEN leadsTo_weaken])
   1.355  apply (auto simp add: split_extended_all)
   1.356  done
   1.357  
   1.358  lemma (in Extend) Join_project_LeadsTo:
   1.359 -     "[| C = (reachable (extend h F Join G));  
   1.360 -         F Join project h C G \<in> A LeadsTo B |]  
   1.361 -      ==> extend h F Join G \<in> (extend_set h A) LeadsTo (extend_set h B)"
   1.362 +     "[| C = (reachable (extend h F\<squnion>G));  
   1.363 +         F\<squnion>project h C G \<in> A LeadsTo B |]  
   1.364 +      ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
   1.365  by (simp del: Join_stable    add: LeadsTo_def project_leadsTo_D_lemma
   1.366                                    project_set_reachable_extend_eq)
   1.367  
   1.368 @@ -526,9 +526,9 @@
   1.369  
   1.370  lemma (in Extend) project_ensures_D_lemma:
   1.371       "[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B));   
   1.372 -         F Join project h C G \<in> (project_set h C \<inter> A) ensures B;   
   1.373 -         extend h F Join G \<in> stable C |]  
   1.374 -      ==> extend h F Join G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
   1.375 +         F\<squnion>project h C G \<in> (project_set h C \<inter> A) ensures B;   
   1.376 +         extend h F\<squnion>G \<in> stable C |]  
   1.377 +      ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
   1.378  (*unless*)
   1.379  apply (auto intro!: project_unless2 [unfolded unless_def] 
   1.380              intro: project_extend_constrains_I 
   1.381 @@ -543,17 +543,17 @@
   1.382  done
   1.383  
   1.384  lemma (in Extend) project_ensures_D:
   1.385 -     "[| F Join project h UNIV G \<in> A ensures B;   
   1.386 +     "[| F\<squnion>project h UNIV G \<in> A ensures B;   
   1.387           G \<in> stable (extend_set h A - extend_set h B) |]  
   1.388 -      ==> extend h F Join G \<in> (extend_set h A) ensures (extend_set h B)"
   1.389 +      ==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)"
   1.390  apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
   1.391  done
   1.392  
   1.393  lemma (in Extend) project_Ensures_D: 
   1.394 -     "[| F Join project h (reachable (extend h F Join G)) G \<in> A Ensures B;   
   1.395 -         G \<in> stable (reachable (extend h F Join G) \<inter> extend_set h A -  
   1.396 +     "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Ensures B;   
   1.397 +         G \<in> stable (reachable (extend h F\<squnion>G) \<inter> extend_set h A -  
   1.398                       extend_set h B) |]  
   1.399 -      ==> extend h F Join G \<in> (extend_set h A) Ensures (extend_set h B)"
   1.400 +      ==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)"
   1.401  apply (unfold Ensures_def)
   1.402  apply (rule project_ensures_D_lemma [THEN revcut_rl])
   1.403  apply (auto simp add: project_set_reachable_extend_eq [symmetric])
   1.404 @@ -585,14 +585,14 @@
   1.405    Not clear that it has a converse [or that we want one!]*)
   1.406  
   1.407  (*The raw version; 3rd premise could be weakened by adding the
   1.408 -  precondition extend h F Join G \<in> X' *)
   1.409 +  precondition extend h F\<squnion>G \<in> X' *)
   1.410  lemma (in Extend) project_guarantees_raw:
   1.411   assumes xguary:  "F \<in> X guarantees Y"
   1.412       and closed:  "subset_closed (AllowedActs F)"
   1.413 -     and project: "!!G. extend h F Join G \<in> X' 
   1.414 -                        ==> F Join project h (C G) G \<in> X"
   1.415 -     and extend:  "!!G. [| F Join project h (C G) G \<in> Y |]  
   1.416 -                        ==> extend h F Join G \<in> Y'"
   1.417 +     and project: "!!G. extend h F\<squnion>G \<in> X' 
   1.418 +                        ==> F\<squnion>project h (C G) G \<in> X"
   1.419 +     and extend:  "!!G. [| F\<squnion>project h (C G) G \<in> Y |]  
   1.420 +                        ==> extend h F\<squnion>G \<in> Y'"
   1.421   shows "extend h F \<in> X' guarantees Y'"
   1.422  apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI])
   1.423  apply (blast intro: closed subset_closed_ok_extend_imp_ok_project)
   1.424 @@ -648,14 +648,14 @@
   1.425  subsubsection{*Guarantees with a leadsTo postcondition*}
   1.426  
   1.427  lemma (in Extend) project_leadsTo_D:
   1.428 -     "F Join project h UNIV G \<in> A leadsTo B
   1.429 -      ==> extend h F Join G \<in> (extend_set h A) leadsTo (extend_set h B)"
   1.430 +     "F\<squnion>project h UNIV G \<in> A leadsTo B
   1.431 +      ==> extend h F\<squnion>G \<in> (extend_set h A) leadsTo (extend_set h B)"
   1.432  apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto)
   1.433  done
   1.434  
   1.435  lemma (in Extend) project_LeadsTo_D:
   1.436 -     "F Join project h (reachable (extend h F Join G)) G \<in> A LeadsTo B   
   1.437 -       ==> extend h F Join G \<in> (extend_set h A) LeadsTo (extend_set h B)"
   1.438 +     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A LeadsTo B   
   1.439 +       ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
   1.440  apply (rule refl [THEN Join_project_LeadsTo], auto)
   1.441  done
   1.442  
   1.443 @@ -667,7 +667,7 @@
   1.444  done
   1.445  
   1.446  lemma (in Extend) extending_LeadsTo: 
   1.447 -     "extending (%G. reachable (extend h F Join G)) h F  
   1.448 +     "extending (%G. reachable (extend h F\<squnion>G)) h F  
   1.449                  (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
   1.450  apply (unfold extending_def)
   1.451  apply (blast intro: project_LeadsTo_D)