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