
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




