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)"