# HG changeset patch
# User paulson
# Date 1045394260 -3600
# Node ID 78f5885b76a99af7806f48781ff05fe399f7c62d
# Parent  274fda8cca4b5c008c5da495e6c1770b169abb93
minor revisions

diff -r 274fda8cca4b -r 78f5885b76a9 src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/Comp.thy	Sun Feb 16 12:17:40 2003 +0100
@@ -7,9 +7,9 @@
 From Chandy and Sanders, "Reasoning About Program Composition",
 Technical Report 2000-003, University of Florida, 2000.
 
-Revised by Sidi Ehmety on January  2001 
+Revised by Sidi Ehmety on January  2001
 
-Added: a strong form of the \<subseteq> relation (component_of) and localize 
+Added: a strong form of the \<subseteq> relation (component_of) and localize
 
 *)
 
@@ -20,19 +20,19 @@
 instance program :: (type) ord ..
 
 defs
-  component_def:          "F \<le> H == \<exists>G. F Join G = H"
+  component_def:          "F \<le> H == \<exists>G. F\<squnion>G = H"
   strict_component_def:   "(F < (H::'a program)) == (F \<le> H & F \<noteq> H)"
 
 
 constdefs
   component_of :: "'a program =>'a program=> bool"
                                     (infixl "component'_of" 50)
-  "F component_of H == \<exists>G. F ok G & F Join G = H"
+  "F component_of H == \<exists>G. F ok G & F\<squnion>G = H"
 
   strict_component_of :: "'a program\<Rightarrow>'a program=> bool"
                                     (infixl "strict'_component'_of" 50)
   "F strict_component_of H == F component_of H & F\<noteq>H"
-  
+
   preserves :: "('a=>'b) => 'a program set"
     "preserves v == \<Inter>z. stable {s. v s = z}"
 
@@ -45,15 +45,15 @@
 
 
 subsection{*The component relation*}
-lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F Join G)"
+lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F\<squnion>G)"
 apply (unfold component_def, auto)
-apply (rule_tac x = "G Join Ga" in exI)
-apply (rule_tac [2] x = "G Join F" in exI)
+apply (rule_tac x = "G\<squnion>Ga" in exI)
+apply (rule_tac [2] x = "G\<squnion>F" in exI)
 apply (auto simp add: Join_ac)
 done
 
-lemma component_eq_subset: 
-     "(F \<le> G) =  
+lemma component_eq_subset:
+     "(F \<le> G) =
       (Init G \<subseteq> Init F & Acts F \<subseteq> Acts G & AllowedActs G \<subseteq> AllowedActs F)"
 apply (unfold component_def)
 apply (force intro!: exI program_equalityI)
@@ -72,18 +72,18 @@
 lemma SKIP_minimal: "F \<le> SKIP ==> F = SKIP"
 by (auto intro!: program_equalityI simp add: component_eq_subset)
 
-lemma component_Join1: "F \<le> (F Join G)"
+lemma component_Join1: "F \<le> (F\<squnion>G)"
 by (unfold component_def, blast)
 
-lemma component_Join2: "G \<le> (F Join G)"
+lemma component_Join2: "G \<le> (F\<squnion>G)"
 apply (unfold component_def)
 apply (simp add: Join_commute, blast)
 done
 
-lemma Join_absorb1: "F \<le> G ==> F Join G = G"
+lemma Join_absorb1: "F \<le> G ==> F\<squnion>G = G"
 by (auto simp add: component_def Join_left_absorb)
 
-lemma Join_absorb2: "G \<le> F ==> F Join G = F"
+lemma Join_absorb2: "G \<le> F ==> F\<squnion>G = F"
 by (auto simp add: Join_ac component_def)
 
 lemma JN_component_iff: "((JOIN I F) \<le> H) = (\<forall>i \<in> I. F i \<le> H)"
@@ -104,7 +104,7 @@
 apply (blast intro!: program_equalityI)
 done
 
-lemma Join_component_iff: "((F Join G) \<le> H) = (F \<le> H & G \<le> H)"
+lemma Join_component_iff: "((F\<squnion>G) \<le> H) = (F \<le> H & G \<le> H)"
 by (simp add: component_eq_subset, blast)
 
 lemma component_constrains: "[| F \<le> G; G \<in> A co B |] ==> F \<in> A co B"
@@ -119,20 +119,17 @@
 lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v"
 by (unfold preserves_def, blast)
 
-lemma preserves_imp_eq: 
+lemma preserves_imp_eq:
      "[| F \<in> preserves v;  act \<in> Acts F;  (s,s') \<in> act |] ==> v s = v s'"
-apply (unfold preserves_def stable_def constrains_def, force)
-done
+by (unfold preserves_def stable_def constrains_def, force)
 
-lemma Join_preserves [iff]: 
-     "(F Join G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)"
-apply (unfold preserves_def, auto)
-done
+lemma Join_preserves [iff]:
+     "(F\<squnion>G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)"
+by (unfold preserves_def, auto)
 
 lemma JN_preserves [iff]:
      "(JOIN I F \<in> preserves v) = (\<forall>i \<in> I. F i \<in> preserves v)"
-apply (simp add: JN_stable preserves_def, blast)
-done
+by (simp add: JN_stable preserves_def, blast)
 
 lemma SKIP_preserves [iff]: "SKIP \<in> preserves v"
 by (auto simp add: preserves_def)
@@ -182,19 +179,19 @@
 (** Some lemmas used only in Client.ML **)
 
 lemma stable_localTo_stable2:
-     "[| F \<in> stable {s. P (v s) (w s)};    
-         G \<in> preserves v;  G \<in> preserves w |]                
-      ==> F Join G \<in> stable {s. P (v s) (w s)}"
+     "[| F \<in> stable {s. P (v s) (w s)};
+         G \<in> preserves v;  G \<in> preserves w |]
+      ==> F\<squnion>G \<in> stable {s. P (v s) (w s)}"
 apply simp
 apply (subgoal_tac "G \<in> preserves (funPair v w) ")
- prefer 2 apply simp 
-apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)
+ prefer 2 apply simp
+apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], 
+       auto)
 done
 
 lemma Increasing_preserves_Stable:
-     "[| F \<in> stable {s. v s \<le> w s};  G \<in> preserves v;        
-         F Join G \<in> Increasing w |]                
-      ==> F Join G \<in> Stable {s. v s \<le> w s}"
+     "[| F \<in> stable {s. v s \<le> w s};  G \<in> preserves v; F\<squnion>G \<in> Increasing w |]
+      ==> F\<squnion>G \<in> Stable {s. v s \<le> w s}"
 apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
 apply (blast intro: constrains_weaken)
 (*The G case remains*)
@@ -204,8 +201,7 @@
 apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl)
 apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl)
 apply (subgoal_tac "v x = v xa")
-prefer 2 apply blast
-apply auto
+ apply auto
 apply (erule order_trans, blast)
 done
 
@@ -225,7 +221,7 @@
 lemma component_of_SKIP [simp]: "SKIP component_of F"
 by (unfold component_of_def, auto)
 
-lemma component_of_trans: 
+lemma component_of_trans:
      "[| F component_of G; G component_of H |] ==> F component_of H"
 apply (unfold component_of_def)
 apply (blast intro: Join_assoc [symmetric])
@@ -241,8 +237,8 @@
 lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F"
 by (simp add: localize_def)
 
-lemma localize_AllowedActs_eq [simp]: 
- "AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)"
+lemma localize_AllowedActs_eq [simp]:
+   "AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)"
 by (unfold localize_def, auto)
 
 end
diff -r 274fda8cca4b -r 78f5885b76a9 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/ELT.thy	Sun Feb 16 12:17:40 2003 +0100
@@ -127,8 +127,7 @@
 (*Useful with cancellation, disjunction*)
 lemma leadsETo_Un_duplicate:
      "F : A leadsTo[CC] (A' Un A') ==> F : A leadsTo[CC] A'"
-apply (simp add: Un_ac)
-done
+by (simp add: Un_ac)
 
 lemma leadsETo_Un_duplicate2:
      "F : A leadsTo[CC] (A' Un C Un C) ==> F : A leadsTo[CC] (A' Un C)"
@@ -195,12 +194,12 @@
 
 lemma single_leadsETo_I:
      "(!!x. x : A ==> F : {x} leadsTo[CC] B) ==> F : A leadsTo[CC] B"
-apply (subst UN_singleton [symmetric], rule leadsETo_UN, blast)
-done
+by (subst UN_singleton [symmetric], rule leadsETo_UN, blast)
 
 
 lemma subset_imp_leadsETo: "A<=B ==> F : A leadsTo[CC] B"
-by (simp add: subset_imp_ensures [THEN leadsETo_Basis] Diff_eq_empty_iff [THEN iffD2])
+by (simp add: subset_imp_ensures [THEN leadsETo_Basis] 
+              Diff_eq_empty_iff [THEN iffD2])
 
 lemmas empty_leadsETo = empty_subsetI [THEN subset_imp_leadsETo, simp]
 
@@ -210,37 +209,33 @@
 
 lemma leadsETo_weaken_R:
      "[| F : A leadsTo[CC] A';  A'<=B' |] ==> F : A leadsTo[CC] B'"
-apply (blast intro: subset_imp_leadsETo leadsETo_Trans)
-done
+by (blast intro: subset_imp_leadsETo leadsETo_Trans)
 
 lemma leadsETo_weaken_L [rule_format]:
      "[| F : A leadsTo[CC] A'; B<=A |] ==> F : B leadsTo[CC] A'"
-apply (blast intro: leadsETo_Trans subset_imp_leadsETo)
-done
+by (blast intro: leadsETo_Trans subset_imp_leadsETo)
 
 (*Distributes over binary unions*)
 lemma leadsETo_Un_distrib:
      "F : (A Un B) leadsTo[CC] C  =   
       (F : A leadsTo[CC] C & F : B leadsTo[CC] C)"
-apply (blast intro: leadsETo_Un leadsETo_weaken_L)
-done
+by (blast intro: leadsETo_Un leadsETo_weaken_L)
 
 lemma leadsETo_UN_distrib:
      "F : (UN i:I. A i) leadsTo[CC] B  =   
       (ALL i : I. F : (A i) leadsTo[CC] B)"
-apply (blast intro: leadsETo_UN leadsETo_weaken_L)
-done
+by (blast intro: leadsETo_UN leadsETo_weaken_L)
 
 lemma leadsETo_Union_distrib:
      "F : (Union S) leadsTo[CC] B  =  (ALL A : S. F : A leadsTo[CC] B)"
-apply (blast intro: leadsETo_Union leadsETo_weaken_L)
-done
+by (blast intro: leadsETo_Union leadsETo_weaken_L)
 
 lemma leadsETo_weaken:
      "[| F : A leadsTo[CC'] A'; B<=A; A'<=B';  CC' <= CC |]  
       ==> F : B leadsTo[CC] B'"
 apply (drule leadsETo_mono [THEN subsetD], assumption)
-apply (blast del: subsetCE intro: leadsETo_weaken_R leadsETo_weaken_L leadsETo_Trans)
+apply (blast del: subsetCE 
+             intro: leadsETo_weaken_R leadsETo_weaken_L leadsETo_Trans)
 done
 
 lemma leadsETo_givenBy:
@@ -286,7 +281,6 @@
 done
 
 
-
 (** PSP: Progress-Safety-Progress **)
 
 (*Special case of PSP: Misra's "stable conjunction"*)
@@ -299,7 +293,8 @@
 prefer 2 apply (blast intro: leadsETo_Trans)
 apply (rule leadsETo_Basis)
 prefer 2 apply (force simp add: Diff_Int_distrib2 [symmetric])
-apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] Int_Un_distrib2 [symmetric])
+apply (simp add: ensures_def Diff_Int_distrib2 [symmetric] 
+                 Int_Un_distrib2 [symmetric])
 apply (blast intro: transient_strengthen constrains_Int)
 done
 
@@ -339,8 +334,8 @@
 (*??IS THIS NEEDED?? or is it just an example of what's provable??*)
 lemma gen_leadsETo_imp_Join_leadsETo:
      "[| F: (A leadsTo[givenBy v] B);  G : preserves v;   
-         F Join G : stable C |]  
-      ==> F Join G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)"
+         F\<squnion>G : stable C |]  
+      ==> F\<squnion>G : ((C Int A) leadsTo[(%D. C Int D) ` givenBy v] B)"
 apply (erule leadsETo_induct)
   prefer 3
   apply (subst Int_Union) 
@@ -348,7 +343,8 @@
 prefer 2
  apply (blast intro: e_psp_stable2 [THEN leadsETo_weaken_L] leadsETo_Trans)
 apply (rule leadsETo_Basis)
-apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] Int_Diff ensures_def givenBy_eq_Collect Join_transient)
+apply (auto simp add: Diff_eq_empty_iff [THEN iffD2] 
+                      Int_Diff ensures_def givenBy_eq_Collect Join_transient)
 prefer 3 apply (blast intro: transient_strengthen)
 apply (drule_tac [2] P1 = P in preserves_subset_stable [THEN subsetD])
 apply (drule_tac P1 = P in preserves_subset_stable [THEN subsetD])
@@ -363,8 +359,8 @@
 lemma leadsETo_subset_leadsTo: "(A leadsTo[CC] B) <= (A leadsTo B)"
 apply safe
 apply (erule leadsETo_induct)
-prefer 3 apply (blast intro: leadsTo_Union)
-prefer 2 apply (blast intro: leadsTo_Trans, blast)
+  prefer 3 apply (blast intro: leadsTo_Union)
+ prefer 2 apply (blast intro: leadsTo_Trans, blast)
 done
 
 lemma leadsETo_UNIV_eq_leadsTo: "(A leadsTo[UNIV] B) = (A leadsTo B)"
@@ -372,8 +368,8 @@
 apply (erule leadsETo_subset_leadsTo [THEN subsetD])
 (*right-to-left case*)
 apply (erule leadsTo_induct)
-prefer 3 apply (blast intro: leadsETo_Union)
-prefer 2 apply (blast intro: leadsETo_Trans, blast)
+  prefer 3 apply (blast intro: leadsETo_Union)
+ prefer 2 apply (blast intro: leadsETo_Trans, blast)
 done
 
 (**** weak ****)
@@ -420,8 +416,7 @@
 (*Lets us look at the starting state*)
 lemma single_LeadsETo_I:
      "(!!s. s : A ==> F : {s} LeadsTo[CC] B) ==> F : A LeadsTo[CC] B"
-apply (subst UN_singleton [symmetric], rule LeadsETo_UN, blast)
-done
+by (subst UN_singleton [symmetric], rule LeadsETo_UN, blast)
 
 lemma subset_imp_LeadsETo:
      "A <= B ==> F : A LeadsTo[CC] B"
@@ -482,10 +477,9 @@
 
 (**** EXTEND/PROJECT PROPERTIES ****)
 
-lemma (in Extend) givenBy_o_eq_extend_set: "givenBy (v o f) = extend_set h ` (givenBy v)"
-apply (simp (no_asm) add: givenBy_eq_Collect)
-apply best 
-done
+lemma (in Extend) givenBy_o_eq_extend_set:
+     "givenBy (v o f) = extend_set h ` (givenBy v)"
+by (simp add: givenBy_eq_Collect, best)
 
 lemma (in Extend) givenBy_eq_extend_set: "givenBy f = range (extend_set h)"
 apply (simp (no_asm) add: givenBy_eq_Collect)
@@ -515,9 +509,9 @@
 lemma (in Extend) Join_project_ensures_strong:
      "[| project h C G ~: transient (project_set h C Int (A-B)) |  
            project_set h C Int (A - B) = {};   
-         extend h F Join G : stable C;   
-         F Join project h C G : (project_set h C Int A) ensures B |]  
-      ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
+         extend h F\<squnion>G : stable C;   
+         F\<squnion>project h C G : (project_set h C Int A) ensures B |]  
+      ==> extend h F\<squnion>G : (C Int extend_set h A) ensures (extend_set h B)"
 apply (subst Int_extend_set_lemma [symmetric])
 apply (rule Join_project_ensures)
 apply (auto simp add: Int_Diff)
@@ -525,10 +519,10 @@
 
 (*NOT WORKING.  MODIFY AS IN Project.thy
 lemma (in Extend) pld_lemma:
-     "[| extend h F Join G : stable C;   
-         F Join project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;   
+     "[| extend h F\<squnion>G : stable C;   
+         F\<squnion>project h C G : (project_set h C Int A) leadsTo[(%D. project_set h C Int D)`givenBy v] B;   
          G : preserves (v o f) |]  
-      ==> extend h F Join G :  
+      ==> extend h F\<squnion>G :  
             (C Int extend_set h (project_set h C Int A))  
             leadsTo[(%D. C Int extend_set h D)`givenBy v]  (extend_set h B)"
 apply (erule leadsETo_induct)
@@ -548,21 +542,21 @@
 done
 
 lemma (in Extend) project_leadsETo_D_lemma:
-     "[| extend h F Join G : stable C;   
-         F Join project h C G :  
+     "[| extend h F\<squnion>G : stable C;   
+         F\<squnion>project h C G :  
              (project_set h C Int A)  
              leadsTo[(%D. project_set h C Int D)`givenBy v] B;   
          G : preserves (v o f) |]  
-      ==> extend h F Join G : (C Int extend_set h A)  
+      ==> extend h F\<squnion>G : (C Int extend_set h A)  
             leadsTo[(%D. C Int extend_set h D)`givenBy v] (extend_set h B)"
 apply (rule pld_lemma [THEN leadsETo_weaken])
 apply (auto simp add: split_extended_all)
 done
 
 lemma (in Extend) project_leadsETo_D:
-     "[| F Join project h UNIV G : A leadsTo[givenBy v] B;   
+     "[| F\<squnion>project h UNIV G : A leadsTo[givenBy v] B;   
          G : preserves (v o f) |]   
-      ==> extend h F Join G : (extend_set h A)  
+      ==> extend h F\<squnion>G : (extend_set h A)  
             leadsTo[givenBy (v o f)] (extend_set h B)"
 apply (cut_tac project_leadsETo_D_lemma [of _ _ UNIV], auto) 
 apply (erule leadsETo_givenBy)
@@ -570,10 +564,10 @@
 done
 
 lemma (in Extend) project_LeadsETo_D:
-     "[| F Join project h (reachable (extend h F Join G)) G  
+     "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G  
              : A LeadsTo[givenBy v] B;   
          G : preserves (v o f) |]  
-      ==> extend h F Join G :  
+      ==> extend h F\<squnion>G :  
             (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)"
 apply (cut_tac subset_refl [THEN stable_reachable, THEN project_leadsETo_D_lemma])
 apply (auto simp add: LeadsETo_def)
@@ -593,7 +587,7 @@
 
 lemma (in Extend) extending_LeadsETo: 
      "(ALL G. extend h F ok G --> G : preserves (v o f))  
-      ==> extending (%G. reachable (extend h F Join G)) h F  
+      ==> extending (%G. reachable (extend h F\<squnion>G)) h F  
                 (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B)  
                 (A LeadsTo[givenBy v]  B)"
 apply (unfold extending_def)
@@ -606,10 +600,10 @@
 
 (*Lemma for the Trans case*)
 lemma (in Extend) pli_lemma:
-     "[| extend h F Join G : stable C;     
-         F Join project h C G     
+     "[| extend h F\<squnion>G : stable C;     
+         F\<squnion>project h C G     
            : project_set h C Int project_set h A leadsTo project_set h B |]  
-      ==> F Join project h C G     
+      ==> F\<squnion>project h C G     
             : project_set h C Int project_set h A leadsTo     
               project_set h C Int project_set h B"
 apply (rule psp_stable2 [THEN leadsTo_weaken_L])
@@ -617,10 +611,10 @@
 done
 
 lemma (in Extend) project_leadsETo_I_lemma:
-     "[| extend h F Join G : stable C;   
-         extend h F Join G :  
+     "[| extend h F\<squnion>G : stable C;   
+         extend h F\<squnion>G :  
            (C Int A) leadsTo[(%D. C Int D)`givenBy f]  B |]   
-  ==> F Join project h C G   
+  ==> F\<squnion>project h C G   
     : (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)"
 apply (erule leadsETo_induct)
   prefer 3
@@ -633,14 +627,14 @@
 done
 
 lemma (in Extend) project_leadsETo_I:
-     "extend h F Join G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)
-      ==> F Join project h UNIV G : A leadsTo B"
+     "extend h F\<squnion>G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)
+      ==> F\<squnion>project h UNIV G : A leadsTo B"
 apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken], auto)
 done
 
 lemma (in Extend) project_LeadsETo_I:
-     "extend h F Join G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B) 
-      ==> F Join project h (reachable (extend h F Join G)) G   
+     "extend h F\<squnion>G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B) 
+      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G   
            : A LeadsTo B"
 apply (simp (no_asm_use) add: LeadsTo_def LeadsETo_def)
 apply (rule project_leadsETo_I_lemma [THEN leadsTo_weaken])
@@ -656,7 +650,7 @@
 done
 
 lemma (in Extend) projecting_LeadsTo: 
-     "projecting (%G. reachable (extend h F Join G)) h F  
+     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
                  (extend_set h A LeadsTo[givenBy f] extend_set h B)  
                  (A LeadsTo B)"
 apply (unfold projecting_def)
diff -r 274fda8cca4b -r 78f5885b76a9 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/Extend.thy	Sun Feb 16 12:17:40 2003 +0100
@@ -429,7 +429,7 @@
 done
 
 lemma (in Extend) extend_Join [simp]:
-     "extend h (F Join G) = extend h F Join extend h G"
+     "extend h (F\<squnion>G) = extend h F\<squnion>extend h G"
 apply (rule program_equalityI)
 apply (simp (no_asm) add: extend_set_Int_distrib)
 apply (simp add: image_Un, auto)
@@ -679,14 +679,14 @@
 subsection{*Guarantees*}
 
 lemma (in Extend) project_extend_Join:
-     "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)"
+     "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
 apply (rule program_equalityI)
   apply (simp add: project_set_extend_set_Int)
  apply (simp add: image_eq_UN UN_Un, auto)
 done
 
 lemma (in Extend) extend_Join_eq_extend_D:
-     "(extend h F) Join G = extend h H ==> H = F Join (project h UNIV G)"
+     "(extend h F)\<squnion>G = extend h H ==> H = F\<squnion>(project h UNIV G)"
 apply (drule_tac f = "project h UNIV" in arg_cong)
 apply (simp add: project_extend_Join)
 done
diff -r 274fda8cca4b -r 78f5885b76a9 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/Guar.thy	Sun Feb 16 12:17:40 2003 +0100
@@ -32,21 +32,21 @@
     case, proving equivalence with Chandy and Sanders's n-ary definitions*)
 
   ex_prop  :: "'a program set => bool"
-   "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F Join G) \<in> X"
+   "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F\<squnion>G) \<in> X"
 
   strict_ex_prop  :: "'a program set => bool"
-   "strict_ex_prop X == \<forall>F G.  F ok G --> (F \<in> X | G \<in> X) = (F Join G \<in> X)"
+   "strict_ex_prop X == \<forall>F G.  F ok G --> (F \<in> X | G \<in> X) = (F\<squnion>G \<in> X)"
 
   uv_prop  :: "'a program set => bool"
-   "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F Join G) \<in> X)"
+   "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F\<squnion>G) \<in> X)"
 
   strict_uv_prop  :: "'a program set => bool"
    "strict_uv_prop X == 
-      SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F Join G \<in> X))"
+      SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F\<squnion>G \<in> X))"
 
   guar :: "['a program set, 'a program set] => 'a program set"
           (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
-   "X guarantees Y == {F. \<forall>G. F ok G --> F Join G \<in> X --> F Join G \<in> Y}"
+   "X guarantees Y == {F. \<forall>G. F ok G --> F\<squnion>G \<in> X --> F\<squnion>G \<in> Y}"
   
 
   (* Weakest guarantees *)
@@ -64,8 +64,8 @@
   refines :: "['a program, 'a program, 'a program set] => bool"
 			("(3_ refines _ wrt _)" [10,10,10] 10)
   "G refines F wrt X ==
-     \<forall>H. (F ok H  & G ok H & F Join H \<in> welldef \<inter> X) --> 
-         (G Join H \<in> welldef \<inter> X)"
+     \<forall>H. (F ok H  & G ok H & F\<squnion>H \<in> welldef \<inter> X) --> 
+         (G\<squnion>H \<in> welldef \<inter> X)"
 
   iso_refines :: "['a program, 'a program, 'a program set] => bool"
                               ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
@@ -146,19 +146,19 @@
 (*** guarantees ***)
 
 lemma guaranteesI:
-     "(!!G. [| F ok G; F Join G \<in> X |] ==> F Join G \<in> Y)  
+     "(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y)  
       ==> F \<in> X guarantees Y"
 by (simp add: guar_def component_def)
 
 lemma guaranteesD: 
-     "[| F \<in> X guarantees Y;  F ok G;  F Join G \<in> X |]  
-      ==> F Join G \<in> Y"
+     "[| F \<in> X guarantees Y;  F ok G;  F\<squnion>G \<in> X |]  
+      ==> F\<squnion>G \<in> Y"
 by (unfold guar_def component_def, blast)
 
 (*This version of guaranteesD matches more easily in the conclusion
   The major premise can no longer be  F \<subseteq> H since we need to reason about G*)
 lemma component_guaranteesD: 
-     "[| F \<in> X guarantees Y;  F Join G = H;  H \<in> X;  F ok G |]  
+     "[| F \<in> X guarantees Y;  F\<squnion>G = H;  H \<in> X;  F ok G |]  
       ==> H \<in> Y"
 by (unfold guar_def, blast)
 
@@ -263,24 +263,24 @@
 
 lemma guarantees_Join_Int: 
     "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]  
-     ==> F Join G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
+     ==> F\<squnion>G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
 apply (unfold guar_def)
 apply (simp (no_asm))
 apply safe
 apply (simp add: Join_assoc)
-apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
+apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
 apply (simp add: ok_commute)
 apply (simp (no_asm_simp) add: Join_ac)
 done
 
 lemma guarantees_Join_Un: 
     "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]   
-     ==> F Join G \<in> (U \<union> X) guarantees (V \<union> Y)"
+     ==> F\<squnion>G \<in> (U \<union> X) guarantees (V \<union> Y)"
 apply (unfold guar_def)
 apply (simp (no_asm))
 apply safe
 apply (simp add: Join_assoc)
-apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ")
+apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
 apply (simp add: ok_commute)
 apply (simp (no_asm_simp) add: Join_ac)
 done
@@ -291,7 +291,7 @@
 apply (unfold guar_def, auto)
 apply (drule bspec, assumption)
 apply (rename_tac "i")
-apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
+apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
 apply (auto intro: OK_imp_ok
             simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
 done
@@ -302,7 +302,7 @@
 apply (unfold guar_def, auto)
 apply (drule bspec, assumption)
 apply (rename_tac "i")
-apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
+apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
 apply (auto intro: OK_imp_ok
             simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
 done
@@ -311,7 +311,7 @@
 (*** guarantees laws for breaking down the program, by lcp ***)
 
 lemma guarantees_Join_I1: 
-     "[| F \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
+     "[| F \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
 apply (unfold guar_def)
 apply (simp (no_asm))
 apply safe
@@ -319,7 +319,7 @@
 done
 
 lemma guarantees_Join_I2:
-     "[| G \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
+     "[| G \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
 apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
 apply (blast intro: guarantees_Join_I1)
 done
@@ -328,17 +328,17 @@
      "[| i \<in> I;  F i \<in> X guarantees Y;  OK I F |]  
       ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
 apply (unfold guar_def, clarify)
-apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
+apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
 apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
 done
 
 
 (*** well-definedness ***)
 
-lemma Join_welldef_D1: "F Join G \<in> welldef ==> F \<in> welldef"
+lemma Join_welldef_D1: "F\<squnion>G \<in> welldef ==> F \<in> welldef"
 by (unfold welldef_def, auto)
 
-lemma Join_welldef_D2: "F Join G \<in> welldef ==> G \<in> welldef"
+lemma Join_welldef_D2: "F\<squnion>G \<in> welldef ==> G \<in> welldef"
 by (unfold welldef_def, auto)
 
 (*** refinement ***)
@@ -356,13 +356,13 @@
 
 lemma strict_ex_refine_lemma: 
      "strict_ex_prop X  
-      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X)  
+      ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X)  
               = (F \<in> X --> G \<in> X)"
 by (unfold strict_ex_prop_def, auto)
 
 lemma strict_ex_refine_lemma_v: 
      "strict_ex_prop X  
-      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =  
+      ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =  
           (F \<in> welldef \<inter> X --> G \<in> X)"
 apply (unfold strict_ex_prop_def, safe)
 apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
@@ -371,7 +371,7 @@
 
 lemma ex_refinement_thm:
      "[| strict_ex_prop X;   
-         \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X --> G Join H \<in> welldef |]  
+         \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> G\<squnion>H \<in> welldef |]  
       ==> (G refines F wrt X) = (G iso_refines F wrt X)"
 apply (rule_tac x = SKIP in allE, assumption)
 apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
@@ -380,12 +380,12 @@
 
 lemma strict_uv_refine_lemma: 
      "strict_uv_prop X ==> 
-      (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X) = (F \<in> X --> G \<in> X)"
+      (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = (F \<in> X --> G \<in> X)"
 by (unfold strict_uv_prop_def, blast)
 
 lemma strict_uv_refine_lemma_v: 
      "strict_uv_prop X  
-      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =  
+      ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =  
           (F \<in> welldef \<inter> X --> G \<in> X)"
 apply (unfold strict_uv_prop_def, safe)
 apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
@@ -394,8 +394,8 @@
 
 lemma uv_refinement_thm:
      "[| strict_uv_prop X;   
-         \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X --> 
-             G Join H \<in> welldef |]  
+         \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> 
+             G\<squnion>H \<in> welldef |]  
       ==> (G refines F wrt X) = (G iso_refines F wrt X)"
 apply (rule_tac x = SKIP in allE, assumption)
 apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
@@ -458,15 +458,15 @@
 by (unfold wx_def, auto)
 
 (* Proposition 6 *)
-lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G \<in> X})"
+lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F\<squnion>G \<in> X})"
 apply (unfold ex_prop_def, safe)
-apply (drule_tac x = "G Join Ga" in spec)
+apply (drule_tac x = "G\<squnion>Ga" in spec)
 apply (force simp add: ok_Join_iff1 Join_assoc)
-apply (drule_tac x = "F Join Ga" in spec)
+apply (drule_tac x = "F\<squnion>Ga" in spec)
 apply (simp (no_asm_use) add: ok_Join_iff1)
 apply safe
 apply (simp (no_asm_simp) add: ok_commute)
-apply (subgoal_tac "F Join G = G Join F")
+apply (subgoal_tac "F\<squnion>G = G\<squnion>F")
 apply (simp (no_asm_simp) add: Join_assoc)
 apply (simp (no_asm) add: Join_commute)
 done
@@ -474,15 +474,15 @@
 (* Equivalence with the other definition of wx *)
 
 lemma wx_equiv: 
- "wx X = {F. \<forall>G. F ok G --> (F Join G):X}"
+ "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G):X}"
 
 apply (unfold wx_def, safe)
 apply (simp (no_asm_use) add: ex_prop_def)
 apply (drule_tac x = x in spec)
 apply (drule_tac x = G in spec)
-apply (frule_tac c = "x Join G" in subsetD, safe)
+apply (frule_tac c = "x\<squnion>G" in subsetD, safe)
 apply (simp (no_asm))
-apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G \<in> X}" in exI, safe)
+apply (rule_tac x = "{F. \<forall>G. F ok G --> F\<squnion>G \<in> X}" in exI, safe)
 apply (rule_tac [2] wx'_ex_prop)
 apply (rotate_tac 1)
 apply (drule_tac x = SKIP in spec, auto)
diff -r 274fda8cca4b -r 78f5885b76a9 src/HOL/UNITY/Project.thy
--- a/src/HOL/UNITY/Project.thy	Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/Project.thy	Sun Feb 16 12:17:40 2003 +0100
@@ -16,13 +16,13 @@
   projecting :: "['c program => 'c set, 'a*'b => 'c, 
 		  'a program, 'c program set, 'a program set] => bool"
     "projecting C h F X' X ==
-       \<forall>G. extend h F Join G \<in> X' --> F Join project h (C G) G \<in> X"
+       \<forall>G. extend h F\<squnion>G \<in> X' --> F\<squnion>project h (C G) G \<in> X"
 
   extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
 		 'c program set, 'a program set] => bool"
     "extending C h F Y' Y ==
-       \<forall>G. extend h F  ok G --> F Join project h (C G) G \<in> Y
-	      --> extend h F Join G \<in> Y'"
+       \<forall>G. extend h F  ok G --> F\<squnion>project h (C G) G \<in> Y
+	      --> extend h F\<squnion>G \<in> Y'"
 
   subset_closed :: "'a set set => bool"
     "subset_closed U == \<forall>A \<in> U. Pow A \<subseteq> U"  
@@ -44,11 +44,11 @@
 apply (blast dest: stable_constrains_Int intro: constrains_weaken)
 done
 
-(*Generalizes project_constrains to the program F Join project h C G
+(*Generalizes project_constrains to the program F\<squnion>project h C G
   useful with guarantees reasoning*)
 lemma (in Extend) Join_project_constrains:
-     "(F Join project h C G \<in> A co B)  =   
-        (extend h F Join G \<in> (C \<inter> extend_set h A) co (extend_set h B) &   
+     "(F\<squnion>project h C G \<in> A co B)  =   
+        (extend h F\<squnion>G \<in> (C \<inter> extend_set h A) co (extend_set h B) &   
          F \<in> A co B)"
 apply (simp (no_asm) add: project_constrains)
 apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken] 
@@ -58,9 +58,9 @@
 (*The condition is required to prove the left-to-right direction
   could weaken it to G \<in> (C \<inter> extend_set h A) co C*)
 lemma (in Extend) Join_project_stable: 
-     "extend h F Join G \<in> stable C  
-      ==> (F Join project h C G \<in> stable A)  =   
-          (extend h F Join G \<in> stable (C \<inter> extend_set h A) &   
+     "extend h F\<squnion>G \<in> stable C  
+      ==> (F\<squnion>project h C G \<in> stable A)  =   
+          (extend h F\<squnion>G \<in> stable (C \<inter> extend_set h A) &   
            F \<in> stable A)"
 apply (unfold stable_def)
 apply (simp only: Join_project_constrains)
@@ -69,23 +69,23 @@
 
 (*For using project_guarantees in particular cases*)
 lemma (in Extend) project_constrains_I:
-     "extend h F Join G \<in> extend_set h A co extend_set h B  
-      ==> F Join project h C G \<in> A co B"
+     "extend h F\<squnion>G \<in> extend_set h A co extend_set h B  
+      ==> F\<squnion>project h C G \<in> A co B"
 apply (simp add: project_constrains extend_constrains)
 apply (blast intro: constrains_weaken dest: constrains_imp_subset)
 done
 
 lemma (in Extend) project_increasing_I: 
-     "extend h F Join G \<in> increasing (func o f)  
-      ==> F Join project h C G \<in> increasing func"
+     "extend h F\<squnion>G \<in> increasing (func o f)  
+      ==> F\<squnion>project h C G \<in> increasing func"
 apply (unfold increasing_def stable_def)
 apply (simp del: Join_constrains
             add: project_constrains_I extend_set_eq_Collect)
 done
 
 lemma (in Extend) Join_project_increasing:
-     "(F Join project h UNIV G \<in> increasing func)  =   
-      (extend h F Join G \<in> increasing (func o f))"
+     "(F\<squnion>project h UNIV G \<in> increasing func)  =   
+      (extend h F\<squnion>G \<in> increasing (func o f))"
 apply (rule iffI)
 apply (erule_tac [2] project_increasing_I)
 apply (simp del: Join_stable
@@ -95,8 +95,8 @@
 
 (*The UNIV argument is essential*)
 lemma (in Extend) project_constrains_D:
-     "F Join project h UNIV G \<in> A co B  
-      ==> extend h F Join G \<in> extend_set h A co extend_set h B"
+     "F\<squnion>project h UNIV G \<in> A co B  
+      ==> extend h F\<squnion>G \<in> extend_set h A co extend_set h B"
 by (simp add: project_constrains extend_constrains)
 
 
@@ -204,9 +204,9 @@
 
 (*In practice, C = reachable(...): the inclusion is equality*)
 lemma (in Extend) reachable_imp_reachable_project:
-     "[| reachable (extend h F Join G) \<subseteq> C;   
-         z \<in> reachable (extend h F Join G) |]  
-      ==> f z \<in> reachable (F Join project h C G)"
+     "[| reachable (extend h F\<squnion>G) \<subseteq> C;   
+         z \<in> reachable (extend h F\<squnion>G) |]  
+      ==> f z \<in> reachable (F\<squnion>project h C G)"
 apply (erule reachable.induct)
 apply (force intro!: reachable.Init simp add: split_extended_all, auto)
  apply (rule_tac act = x in reachable.Acts)
@@ -217,8 +217,8 @@
 done
 
 lemma (in Extend) project_Constrains_D: 
-     "F Join project h (reachable (extend h F Join G)) G \<in> A Co B   
-      ==> extend h F Join G \<in> (extend_set h A) Co (extend_set h B)"
+     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B   
+      ==> extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)"
 apply (unfold Constrains_def)
 apply (simp del: Join_constrains
             add: Join_project_constrains, clarify)
@@ -227,22 +227,22 @@
 done
 
 lemma (in Extend) project_Stable_D: 
-     "F Join project h (reachable (extend h F Join G)) G \<in> Stable A   
-      ==> extend h F Join G \<in> Stable (extend_set h A)"
+     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A   
+      ==> extend h F\<squnion>G \<in> Stable (extend_set h A)"
 apply (unfold Stable_def)
 apply (simp (no_asm_simp) add: project_Constrains_D)
 done
 
 lemma (in Extend) project_Always_D: 
-     "F Join project h (reachable (extend h F Join G)) G \<in> Always A   
-      ==> extend h F Join G \<in> Always (extend_set h A)"
+     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A   
+      ==> extend h F\<squnion>G \<in> Always (extend_set h A)"
 apply (unfold Always_def)
 apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
 done
 
 lemma (in Extend) project_Increasing_D: 
-     "F Join project h (reachable (extend h F Join G)) G \<in> Increasing func   
-      ==> extend h F Join G \<in> Increasing (func o f)"
+     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func   
+      ==> extend h F\<squnion>G \<in> Increasing (func o f)"
 apply (unfold Increasing_def, auto)
 apply (subst extend_set_eq_Collect [symmetric])
 apply (simp (no_asm_simp) add: project_Stable_D)
@@ -253,9 +253,9 @@
 
 (*In practice, C = reachable(...): the inclusion is equality*)
 lemma (in Extend) reachable_project_imp_reachable:
-     "[| C \<subseteq> reachable(extend h F Join G);    
-         x \<in> reachable (F Join project h C G) |]  
-      ==> \<exists>y. h(x,y) \<in> reachable (extend h F Join G)"
+     "[| C \<subseteq> reachable(extend h F\<squnion>G);    
+         x \<in> reachable (F\<squnion>project h C G) |]  
+      ==> \<exists>y. h(x,y) \<in> reachable (extend h F\<squnion>G)"
 apply (erule reachable.induct)
 apply  (force intro: reachable.Init)
 apply (auto simp add: project_act_def)
@@ -263,22 +263,22 @@
 done
 
 lemma (in Extend) project_set_reachable_extend_eq:
-     "project_set h (reachable (extend h F Join G)) =  
-      reachable (F Join project h (reachable (extend h F Join G)) G)"
+     "project_set h (reachable (extend h F\<squnion>G)) =  
+      reachable (F\<squnion>project h (reachable (extend h F\<squnion>G)) G)"
 by (auto dest: subset_refl [THEN reachable_imp_reachable_project] 
                subset_refl [THEN reachable_project_imp_reachable])
 
 (*UNUSED*)
 lemma (in Extend) reachable_extend_Join_subset:
-     "reachable (extend h F Join G) \<subseteq> C   
-      ==> reachable (extend h F Join G) \<subseteq>  
-          extend_set h (reachable (F Join project h C G))"
+     "reachable (extend h F\<squnion>G) \<subseteq> C   
+      ==> reachable (extend h F\<squnion>G) \<subseteq>  
+          extend_set h (reachable (F\<squnion>project h C G))"
 apply (auto dest: reachable_imp_reachable_project)
 done
 
 lemma (in Extend) project_Constrains_I: 
-     "extend h F Join G \<in> (extend_set h A) Co (extend_set h B)   
-      ==> F Join project h (reachable (extend h F Join G)) G \<in> A Co B"
+     "extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)   
+      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B"
 apply (unfold Constrains_def)
 apply (simp del: Join_constrains
             add: Join_project_constrains extend_set_Int_distrib)
@@ -291,43 +291,43 @@
 done
 
 lemma (in Extend) project_Stable_I: 
-     "extend h F Join G \<in> Stable (extend_set h A)   
-      ==> F Join project h (reachable (extend h F Join G)) G \<in> Stable A"
+     "extend h F\<squnion>G \<in> Stable (extend_set h A)   
+      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A"
 apply (unfold Stable_def)
 apply (simp (no_asm_simp) add: project_Constrains_I)
 done
 
 lemma (in Extend) project_Always_I: 
-     "extend h F Join G \<in> Always (extend_set h A)   
-      ==> F Join project h (reachable (extend h F Join G)) G \<in> Always A"
+     "extend h F\<squnion>G \<in> Always (extend_set h A)   
+      ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A"
 apply (unfold Always_def)
 apply (auto simp add: project_Stable_I)
 apply (unfold extend_set_def, blast)
 done
 
 lemma (in Extend) project_Increasing_I: 
-    "extend h F Join G \<in> Increasing (func o f)   
-     ==> F Join project h (reachable (extend h F Join G)) G \<in> Increasing func"
+    "extend h F\<squnion>G \<in> Increasing (func o f)   
+     ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func"
 apply (unfold Increasing_def, auto)
 apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
 done
 
 lemma (in Extend) project_Constrains:
-     "(F Join project h (reachable (extend h F Join G)) G \<in> A Co B)  =   
-      (extend h F Join G \<in> (extend_set h A) Co (extend_set h B))"
+     "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B)  =   
+      (extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B))"
 apply (blast intro: project_Constrains_I project_Constrains_D)
 done
 
 lemma (in Extend) project_Stable: 
-     "(F Join project h (reachable (extend h F Join G)) G \<in> Stable A)  =   
-      (extend h F Join G \<in> Stable (extend_set h A))"
+     "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A)  =   
+      (extend h F\<squnion>G \<in> Stable (extend_set h A))"
 apply (unfold Stable_def)
 apply (rule project_Constrains)
 done
 
 lemma (in Extend) project_Increasing: 
-   "(F Join project h (reachable (extend h F Join G)) G \<in> Increasing func)  =  
-    (extend h F Join G \<in> Increasing (func o f))"
+   "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func)  =  
+    (extend h F\<squnion>G \<in> Increasing (func o f))"
 apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
 done
 
@@ -335,7 +335,7 @@
     about guarantees.*}
 
 lemma (in Extend) projecting_Constrains: 
-     "projecting (%G. reachable (extend h F Join G)) h F  
+     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
                  (extend_set h A Co extend_set h B) (A Co B)"
 
 apply (unfold projecting_def)
@@ -343,49 +343,49 @@
 done
 
 lemma (in Extend) projecting_Stable: 
-     "projecting (%G. reachable (extend h F Join G)) h F  
+     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
                  (Stable (extend_set h A)) (Stable A)"
 apply (unfold Stable_def)
 apply (rule projecting_Constrains)
 done
 
 lemma (in Extend) projecting_Always: 
-     "projecting (%G. reachable (extend h F Join G)) h F  
+     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
                  (Always (extend_set h A)) (Always A)"
 apply (unfold projecting_def)
 apply (blast intro: project_Always_I)
 done
 
 lemma (in Extend) projecting_Increasing: 
-     "projecting (%G. reachable (extend h F Join G)) h F  
+     "projecting (%G. reachable (extend h F\<squnion>G)) h F  
                  (Increasing (func o f)) (Increasing func)"
 apply (unfold projecting_def)
 apply (blast intro: project_Increasing_I)
 done
 
 lemma (in Extend) extending_Constrains: 
-     "extending (%G. reachable (extend h F Join G)) h F  
+     "extending (%G. reachable (extend h F\<squnion>G)) h F  
                   (extend_set h A Co extend_set h B) (A Co B)"
 apply (unfold extending_def)
 apply (blast intro: project_Constrains_D)
 done
 
 lemma (in Extend) extending_Stable: 
-     "extending (%G. reachable (extend h F Join G)) h F  
+     "extending (%G. reachable (extend h F\<squnion>G)) h F  
                   (Stable (extend_set h A)) (Stable A)"
 apply (unfold extending_def)
 apply (blast intro: project_Stable_D)
 done
 
 lemma (in Extend) extending_Always: 
-     "extending (%G. reachable (extend h F Join G)) h F  
+     "extending (%G. reachable (extend h F\<squnion>G)) h F  
                   (Always (extend_set h A)) (Always A)"
 apply (unfold extending_def)
 apply (blast intro: project_Always_D)
 done
 
 lemma (in Extend) extending_Increasing: 
-     "extending (%G. reachable (extend h F Join G)) h F  
+     "extending (%G. reachable (extend h F\<squnion>G)) h F  
                   (Increasing (func o f)) (Increasing func)"
 apply (unfold extending_def)
 apply (blast intro: project_Increasing_D)
@@ -423,8 +423,8 @@
 (*Used to prove project_leadsETo_I*)
 lemma (in Extend) ensures_extend_set_imp_project_ensures:
      "[| extend h F \<in> stable C;  G \<in> stable C;   
-         extend h F Join G \<in> A ensures B;  A-B = C \<inter> extend_set h D |]   
-      ==> F Join project h C G   
+         extend h F\<squnion>G \<in> A ensures B;  A-B = C \<inter> extend_set h D |]   
+      ==> F\<squnion>project h C G   
             \<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)"
 apply (simp add: ensures_def project_constrains Join_transient extend_transient,
        clarify)
@@ -482,9 +482,9 @@
 
 (*Used to prove project_leadsETo_D*)
 lemma (in Extend) Join_project_ensures [rule_format]:
-     "[| extend h F Join G \<in> stable C;   
-         F Join project h C G \<in> A ensures B |]  
-      ==> extend h F Join G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
+     "[| extend h F\<squnion>G \<in> stable C;   
+         F\<squnion>project h C G \<in> A ensures B |]  
+      ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
 apply (auto simp add: ensures_eq extend_unless project_unless)
 apply (blast intro:  extend_transient [THEN iffD2] transient_strengthen)  
 apply (blast intro: project_transient_extend_set transient_strengthen)  
@@ -496,9 +496,9 @@
 (*The strange induction formula allows induction over the leadsTo
   assumption's non-atomic precondition*)
 lemma (in Extend) PLD_lemma:
-     "[| extend h F Join G \<in> stable C;   
-         F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
-      ==> extend h F Join G \<in>  
+     "[| extend h F\<squnion>G \<in> stable C;   
+         F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
+      ==> extend h F\<squnion>G \<in>  
           C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)"
 apply (erule leadsTo_induct)
   apply (blast intro: leadsTo_Basis Join_project_ensures)
@@ -507,17 +507,17 @@
 done
 
 lemma (in Extend) project_leadsTo_D_lemma:
-     "[| extend h F Join G \<in> stable C;   
-         F Join project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
-      ==> extend h F Join G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
+     "[| extend h F\<squnion>G \<in> stable C;   
+         F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |]  
+      ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)"
 apply (rule PLD_lemma [THEN leadsTo_weaken])
 apply (auto simp add: split_extended_all)
 done
 
 lemma (in Extend) Join_project_LeadsTo:
-     "[| C = (reachable (extend h F Join G));  
-         F Join project h C G \<in> A LeadsTo B |]  
-      ==> extend h F Join G \<in> (extend_set h A) LeadsTo (extend_set h B)"
+     "[| C = (reachable (extend h F\<squnion>G));  
+         F\<squnion>project h C G \<in> A LeadsTo B |]  
+      ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
 by (simp del: Join_stable    add: LeadsTo_def project_leadsTo_D_lemma
                                   project_set_reachable_extend_eq)
 
@@ -526,9 +526,9 @@
 
 lemma (in Extend) project_ensures_D_lemma:
      "[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B));   
-         F Join project h C G \<in> (project_set h C \<inter> A) ensures B;   
-         extend h F Join G \<in> stable C |]  
-      ==> extend h F Join G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
+         F\<squnion>project h C G \<in> (project_set h C \<inter> A) ensures B;   
+         extend h F\<squnion>G \<in> stable C |]  
+      ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)"
 (*unless*)
 apply (auto intro!: project_unless2 [unfolded unless_def] 
             intro: project_extend_constrains_I 
@@ -543,17 +543,17 @@
 done
 
 lemma (in Extend) project_ensures_D:
-     "[| F Join project h UNIV G \<in> A ensures B;   
+     "[| F\<squnion>project h UNIV G \<in> A ensures B;   
          G \<in> stable (extend_set h A - extend_set h B) |]  
-      ==> extend h F Join G \<in> (extend_set h A) ensures (extend_set h B)"
+      ==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)"
 apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
 done
 
 lemma (in Extend) project_Ensures_D: 
-     "[| F Join project h (reachable (extend h F Join G)) G \<in> A Ensures B;   
-         G \<in> stable (reachable (extend h F Join G) \<inter> extend_set h A -  
+     "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Ensures B;   
+         G \<in> stable (reachable (extend h F\<squnion>G) \<inter> extend_set h A -  
                      extend_set h B) |]  
-      ==> extend h F Join G \<in> (extend_set h A) Ensures (extend_set h B)"
+      ==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)"
 apply (unfold Ensures_def)
 apply (rule project_ensures_D_lemma [THEN revcut_rl])
 apply (auto simp add: project_set_reachable_extend_eq [symmetric])
@@ -585,14 +585,14 @@
   Not clear that it has a converse [or that we want one!]*)
 
 (*The raw version; 3rd premise could be weakened by adding the
-  precondition extend h F Join G \<in> X' *)
+  precondition extend h F\<squnion>G \<in> X' *)
 lemma (in Extend) project_guarantees_raw:
  assumes xguary:  "F \<in> X guarantees Y"
      and closed:  "subset_closed (AllowedActs F)"
-     and project: "!!G. extend h F Join G \<in> X' 
-                        ==> F Join project h (C G) G \<in> X"
-     and extend:  "!!G. [| F Join project h (C G) G \<in> Y |]  
-                        ==> extend h F Join G \<in> Y'"
+     and project: "!!G. extend h F\<squnion>G \<in> X' 
+                        ==> F\<squnion>project h (C G) G \<in> X"
+     and extend:  "!!G. [| F\<squnion>project h (C G) G \<in> Y |]  
+                        ==> extend h F\<squnion>G \<in> Y'"
  shows "extend h F \<in> X' guarantees Y'"
 apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI])
 apply (blast intro: closed subset_closed_ok_extend_imp_ok_project)
@@ -648,14 +648,14 @@
 subsubsection{*Guarantees with a leadsTo postcondition*}
 
 lemma (in Extend) project_leadsTo_D:
-     "F Join project h UNIV G \<in> A leadsTo B
-      ==> extend h F Join G \<in> (extend_set h A) leadsTo (extend_set h B)"
+     "F\<squnion>project h UNIV G \<in> A leadsTo B
+      ==> extend h F\<squnion>G \<in> (extend_set h A) leadsTo (extend_set h B)"
 apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto)
 done
 
 lemma (in Extend) project_LeadsTo_D:
-     "F Join project h (reachable (extend h F Join G)) G \<in> A LeadsTo B   
-       ==> extend h F Join G \<in> (extend_set h A) LeadsTo (extend_set h B)"
+     "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A LeadsTo B   
+       ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)"
 apply (rule refl [THEN Join_project_LeadsTo], auto)
 done
 
@@ -667,7 +667,7 @@
 done
 
 lemma (in Extend) extending_LeadsTo: 
-     "extending (%G. reachable (extend h F Join G)) h F  
+     "extending (%G. reachable (extend h F\<squnion>G)) h F  
                 (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
 apply (unfold extending_def)
 apply (blast intro: project_LeadsTo_D)
diff -r 274fda8cca4b -r 78f5885b76a9 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Sun Feb 16 12:16:07 2003 +0100
+++ b/src/HOL/UNITY/Union.thy	Sun Feb 16 12:17:40 2003 +0100
@@ -46,10 +46,10 @@
   "JN x. B"     == "JOIN UNIV (%x. B)"
 
 syntax (xsymbols)
-  SKIP      :: "'a program"                              ("\<bottom>")
-  "op Join" :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
-  "@JOIN1"  :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
-  "@JOIN"   :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
+  SKIP     :: "'a program"                              ("\<bottom>")
+  Join     :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
+  "@JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
+  "@JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
 
 
 subsection{*SKIP*}
@@ -82,14 +82,14 @@
 
 subsection{*Join*}
 
-lemma Init_Join [simp]: "Init (F Join G) = Init F \<inter> Init G"
+lemma Init_Join [simp]: "Init (F\<squnion>G) = Init F \<inter> Init G"
 by (simp add: Join_def)
 
-lemma Acts_Join [simp]: "Acts (F Join G) = Acts F \<union> Acts G"
+lemma Acts_Join [simp]: "Acts (F\<squnion>G) = Acts F \<union> Acts G"
 by (auto simp add: Join_def)
 
 lemma AllowedActs_Join [simp]:
-     "AllowedActs (F Join G) = AllowedActs F \<inter> AllowedActs G"
+     "AllowedActs (F\<squnion>G) = AllowedActs F \<inter> AllowedActs G"
 by (auto simp add: Join_def)
 
 
@@ -98,7 +98,7 @@
 lemma JN_empty [simp]: "(\<Squnion>i\<in>{}. F i) = SKIP"
 by (unfold JOIN_def SKIP_def, auto)
 
-lemma JN_insert [simp]: "(\<Squnion>i \<in> insert a I. F i) = (F a) Join (\<Squnion>i \<in> I. F i)"
+lemma JN_insert [simp]: "(\<Squnion>i \<in> insert a I. F i) = (F a)\<squnion>(\<Squnion>i \<in> I. F i)"
 apply (rule program_equalityI)
 apply (auto simp add: JOIN_def Join_def)
 done
@@ -121,33 +121,33 @@
 
 subsection{*Algebraic laws*}
 
-lemma Join_commute: "F Join G = G Join F"
+lemma Join_commute: "F\<squnion>G = G\<squnion>F"
 by (simp add: Join_def Un_commute Int_commute)
 
-lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)"
+lemma Join_assoc: "(F\<squnion>G)\<squnion>H = F\<squnion>(G\<squnion>H)"
 by (simp add: Un_ac Join_def Int_assoc insert_absorb)
  
-lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)"
+lemma Join_left_commute: "A\<squnion>(B\<squnion>C) = B\<squnion>(A\<squnion>C)"
 by (simp add: Un_ac Int_ac Join_def insert_absorb)
 
-lemma Join_SKIP_left [simp]: "SKIP Join F = F"
+lemma Join_SKIP_left [simp]: "SKIP\<squnion>F = F"
 apply (unfold Join_def SKIP_def)
 apply (rule program_equalityI)
 apply (simp_all (no_asm) add: insert_absorb)
 done
 
-lemma Join_SKIP_right [simp]: "F Join SKIP = F"
+lemma Join_SKIP_right [simp]: "F\<squnion>SKIP = F"
 apply (unfold Join_def SKIP_def)
 apply (rule program_equalityI)
 apply (simp_all (no_asm) add: insert_absorb)
 done
 
-lemma Join_absorb [simp]: "F Join F = F"
+lemma Join_absorb [simp]: "F\<squnion>F = F"
 apply (unfold Join_def)
 apply (rule program_equalityI, auto)
 done
 
-lemma Join_left_absorb: "F Join (F Join G) = F Join G"
+lemma Join_left_absorb: "F\<squnion>(F\<squnion>G) = F\<squnion>G"
 apply (unfold Join_def)
 apply (rule program_equalityI, auto)
 done
@@ -159,25 +159,25 @@
 subsection{*\<Squnion>laws*}
 
 (*Also follows by JN_insert and insert_absorb, but the proof is longer*)
-lemma JN_absorb: "k \<in> I ==> F k Join (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
+lemma JN_absorb: "k \<in> I ==> F k\<squnion>(\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
 by (auto intro!: program_equalityI)
 
-lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F i) = ((\<Squnion>i \<in> I. F i) Join (\<Squnion>i \<in> J. F i))"
+lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F i) = ((\<Squnion>i \<in> I. F i)\<squnion>(\<Squnion>i \<in> J. F i))"
 by (auto intro!: program_equalityI)
 
 lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I={} then SKIP else c)"
 by (rule program_equalityI, auto)
 
 lemma JN_Join_distrib:
-     "(\<Squnion>i \<in> I. F i Join G i) = (\<Squnion>i \<in> I. F i)  Join  (\<Squnion>i \<in> I. G i)"
+     "(\<Squnion>i \<in> I. F i\<squnion>G i) = (\<Squnion>i \<in> I. F i) \<squnion> (\<Squnion>i \<in> I. G i)"
 by (auto intro!: program_equalityI)
 
 lemma JN_Join_miniscope:
-     "i \<in> I ==> (\<Squnion>i \<in> I. F i Join G) = ((\<Squnion>i \<in> I. F i) Join G)"
+     "i \<in> I ==> (\<Squnion>i \<in> I. F i\<squnion>G) = ((\<Squnion>i \<in> I. F i)\<squnion>G)"
 by (auto simp add: JN_Join_distrib JN_constant)
 
 (*Used to prove guarantees_JN_I*)
-lemma JN_Join_diff: "i \<in> I ==> F i Join JOIN (I - {i}) F = JOIN I F"
+lemma JN_Join_diff: "i \<in> I ==> F i\<squnion>JOIN (I - {i}) F = JOIN I F"
 apply (unfold JOIN_def Join_def)
 apply (rule program_equalityI, auto)
 done
@@ -193,21 +193,21 @@
 by (simp add: constrains_def JOIN_def, blast)
 
 lemma Join_constrains [simp]:
-     "(F Join G \<in> A co B) = (F \<in> A co B & G \<in> A co B)"
+     "(F\<squnion>G \<in> A co B) = (F \<in> A co B & G \<in> A co B)"
 by (auto simp add: constrains_def Join_def)
 
 lemma Join_unless [simp]:
-     "(F Join G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"
+     "(F\<squnion>G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"
 by (simp add: Join_constrains unless_def)
 
 (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
-  reachable (F Join G) could be much bigger than reachable F, reachable G
+  reachable (F\<squnion>G) could be much bigger than reachable F, reachable G
 *)
 
 
 lemma Join_constrains_weaken:
      "[| F \<in> A co A';  G \<in> B co B' |]  
-      ==> F Join G \<in> (A \<inter> B) co (A' \<union> B')"
+      ==> F\<squnion>G \<in> (A \<inter> B) co (A' \<union> B')"
 by (simp, blast intro: constrains_weaken)
 
 (*If I={}, it degenerates to SKIP \<in> UNIV co {}, which is false.*)
@@ -227,18 +227,18 @@
 by (simp add: invariant_def JN_stable, blast)
 
 lemma Join_stable [simp]:
-     "(F Join G \<in> stable A) =  
+     "(F\<squnion>G \<in> stable A) =  
       (F \<in> stable A & G \<in> stable A)"
 by (simp add: stable_def)
 
 lemma Join_increasing [simp]:
-     "(F Join G \<in> increasing f) =  
+     "(F\<squnion>G \<in> increasing f) =  
       (F \<in> increasing f & G \<in> increasing f)"
 by (simp add: increasing_def Join_stable, blast)
 
 lemma invariant_JoinI:
      "[| F \<in> invariant A; G \<in> invariant A |]   
-      ==> F Join G \<in> invariant A"
+      ==> F\<squnion>G \<in> invariant A"
 by (simp add: invariant_def, blast)
 
 lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
@@ -253,14 +253,14 @@
 by (auto simp add: transient_def JOIN_def)
 
 lemma Join_transient [simp]:
-     "F Join G \<in> transient A =  
+     "F\<squnion>G \<in> transient A =  
       (F \<in> transient A | G \<in> transient A)"
 by (auto simp add: bex_Un transient_def Join_def)
 
-lemma Join_transient_I1: "F \<in> transient A ==> F Join G \<in> transient A"
+lemma Join_transient_I1: "F \<in> transient A ==> F\<squnion>G \<in> transient A"
 by (simp add: Join_transient)
 
-lemma Join_transient_I2: "G \<in> transient A ==> F Join G \<in> transient A"
+lemma Join_transient_I2: "G \<in> transient A ==> F\<squnion>G \<in> transient A"
 by (simp add: Join_transient)
 
 (*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
@@ -271,14 +271,14 @@
 by (auto simp add: ensures_def JN_constrains JN_transient)
 
 lemma Join_ensures: 
-     "F Join G \<in> A ensures B =      
+     "F\<squnion>G \<in> A ensures B =      
       (F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &  
        (F \<in> transient (A-B) | G \<in> transient (A-B)))"
 by (auto simp add: ensures_def Join_transient)
 
 lemma stable_Join_constrains: 
     "[| F \<in> stable A;  G \<in> A co A' |]  
-     ==> F Join G \<in> A co A'"
+     ==> F\<squnion>G \<in> A co A'"
 apply (unfold stable_def constrains_def Join_def)
 apply (simp add: ball_Un, blast)
 done
@@ -286,20 +286,20 @@
 (*Premise for G cannot use Always because  F \<in> Stable A  is weaker than
   G \<in> stable A *)
 lemma stable_Join_Always1:
-     "[| F \<in> stable A;  G \<in> invariant A |] ==> F Join G \<in> Always A"
+     "[| F \<in> stable A;  G \<in> invariant A |] ==> F\<squnion>G \<in> Always A"
 apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable)
 apply (force intro: stable_Int)
 done
 
 (*As above, but exchanging the roles of F and G*)
 lemma stable_Join_Always2:
-     "[| F \<in> invariant A;  G \<in> stable A |] ==> F Join G \<in> Always A"
+     "[| F \<in> invariant A;  G \<in> stable A |] ==> F\<squnion>G \<in> Always A"
 apply (subst Join_commute)
 apply (blast intro: stable_Join_Always1)
 done
 
 lemma stable_Join_ensures1:
-     "[| F \<in> stable A;  G \<in> A ensures B |] ==> F Join G \<in> A ensures B"
+     "[| F \<in> stable A;  G \<in> A ensures B |] ==> F\<squnion>G \<in> A ensures B"
 apply (simp (no_asm_simp) add: Join_ensures)
 apply (simp add: stable_def ensures_def)
 apply (erule constrains_weaken, auto)
@@ -307,7 +307,7 @@
 
 (*As above, but exchanging the roles of F and G*)
 lemma stable_Join_ensures2:
-     "[| F \<in> A ensures B;  G \<in> stable A |] ==> F Join G \<in> A ensures B"
+     "[| F \<in> A ensures B;  G \<in> stable A |] ==> F\<squnion>G \<in> A ensures B"
 apply (subst Join_commute)
 apply (blast intro: stable_Join_ensures1)
 done
@@ -322,7 +322,7 @@
 by (simp add: ok_def)
 
 lemma ok_Join_commute:
-     "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))"
+     "(F ok G & (F\<squnion>G) ok H) = (G ok H & F ok (G\<squnion>H))"
 by (auto simp add: ok_def)
 
 lemma ok_commute: "(F ok G) = (G ok F)"
@@ -331,18 +331,18 @@
 lemmas ok_sym = ok_commute [THEN iffD1, standard]
 
 lemma ok_iff_OK:
-     "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"
+     "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)"
 by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb
               all_conj_distrib eq_commute,   blast)
 
-lemma ok_Join_iff1 [iff]: "F ok (G Join H) = (F ok G & F ok H)"
+lemma ok_Join_iff1 [iff]: "F ok (G\<squnion>H) = (F ok G & F ok H)"
 by (auto simp add: ok_def)
 
-lemma ok_Join_iff2 [iff]: "(G Join H) ok F = (G ok F & H ok F)"
+lemma ok_Join_iff2 [iff]: "(G\<squnion>H) ok F = (G ok F & H ok F)"
 by (auto simp add: ok_def)
 
 (*useful?  Not with the previous two around*)
-lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"
+lemma ok_Join_commute_I: "[| F ok G; (F\<squnion>G) ok H |] ==> F ok (G\<squnion>H)"
 by (auto simp add: ok_def)
 
 lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (\<forall>i \<in> I. F ok G i)"
@@ -363,7 +363,7 @@
 lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
 by (auto simp add: Allowed_def)
 
-lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F \<inter> Allowed G"
+lemma Allowed_Join [simp]: "Allowed (F\<squnion>G) = Allowed F \<inter> Allowed G"
 by (auto simp add: Allowed_def)
 
 lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\<Inter>i \<in> I. Allowed (F i))"
@@ -428,10 +428,10 @@
 by (auto simp add: ok_def safety_prop_Acts_iff)
 
 text{*The union of two total programs is total.*}
-lemma totalize_Join: "totalize F Join totalize G = totalize (F Join G)"
+lemma totalize_Join: "totalize F\<squnion>totalize G = totalize (F\<squnion>G)"
 by (simp add: program_equalityI totalize_def Join_def image_Un)
 
-lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F Join G)"
+lemma all_total_Join: "[|all_total F; all_total G|] ==> all_total (F\<squnion>G)"
 by (simp add: all_total_def, blast)
 
 lemma totalize_JN: "(\<Squnion>i \<in> I. totalize (F i)) = totalize(\<Squnion>i \<in> I. F i)"