--- a/src/HOL/UNITY/Comp.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Comp.thy Tue Feb 04 18:12:40 2003 +0100
@@ -9,7 +9,7 @@
Revised by Sidi Ehmety on January 2001
-Added: a strong form of the <= relation (component_of) and localize
+Added: a strong form of the \<subseteq> relation (component_of) and localize
*)
@@ -20,33 +20,32 @@
instance program :: (type) ord ..
defs
- component_def: "F <= H == EX G. F Join G = H"
- strict_component_def: "(F < (H::'a program)) == (F <= H & F ~= H)"
+ component_def: "F \<le> H == \<exists>G. F Join G = H"
+ strict_component_def: "(F < (H::'a program)) == (F \<le> H & F \<noteq> H)"
constdefs
- component_of :: "'a program=>'a program=> bool"
+ component_of :: "'a program =>'a program=> bool"
(infixl "component'_of" 50)
- "F component_of H == EX G. F ok G & F Join G = H"
+ "F component_of H == \<exists>G. F ok G & F Join 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~=H"
+ "F strict_component_of H == F component_of H & F\<noteq>H"
preserves :: "('a=>'b) => 'a program set"
- "preserves v == INT z. stable {s. v s = z}"
+ "preserves v == \<Inter>z. stable {s. v s = z}"
localize :: "('a=>'b) => 'a program => 'a program"
"localize v F == mk_program(Init F, Acts F,
- AllowedActs F Int (UN G:preserves v. Acts G))"
+ AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G))"
funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
"funPair f g == %x. (f x, g x)"
subsection{*The component relation*}
-lemma componentI:
- "H <= F | H <= G ==> H <= (F Join G)"
+lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F Join 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)
@@ -54,61 +53,61 @@
done
lemma component_eq_subset:
- "(F <= G) =
- (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)"
+ "(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)
done
-lemma component_SKIP [iff]: "SKIP <= F"
+lemma component_SKIP [iff]: "SKIP \<le> F"
apply (unfold component_def)
apply (force intro: Join_SKIP_left)
done
-lemma component_refl [iff]: "F <= (F :: 'a program)"
+lemma component_refl [iff]: "F \<le> (F :: 'a program)"
apply (unfold component_def)
apply (blast intro: Join_SKIP_right)
done
-lemma SKIP_minimal: "F <= SKIP ==> F = SKIP"
+lemma SKIP_minimal: "F \<le> SKIP ==> F = SKIP"
by (auto intro!: program_equalityI simp add: component_eq_subset)
-lemma component_Join1: "F <= (F Join G)"
+lemma component_Join1: "F \<le> (F Join G)"
by (unfold component_def, blast)
-lemma component_Join2: "G <= (F Join G)"
+lemma component_Join2: "G \<le> (F Join G)"
apply (unfold component_def)
apply (simp add: Join_commute, blast)
done
-lemma Join_absorb1: "F<=G ==> F Join G = G"
+lemma Join_absorb1: "F \<le> G ==> F Join G = G"
by (auto simp add: component_def Join_left_absorb)
-lemma Join_absorb2: "G<=F ==> F Join G = F"
+lemma Join_absorb2: "G \<le> F ==> F Join G = F"
by (auto simp add: Join_ac component_def)
-lemma JN_component_iff: "((JOIN I F) <= H) = (ALL i: I. F i <= H)"
+lemma JN_component_iff: "((JOIN I F) \<le> H) = (\<forall>i \<in> I. F i \<le> H)"
by (simp add: component_eq_subset, blast)
-lemma component_JN: "i : I ==> (F i) <= (JN i:I. (F i))"
+lemma component_JN: "i \<in> I ==> (F i) \<le> (\<Squnion>i \<in> I. (F i))"
apply (unfold component_def)
apply (blast intro: JN_absorb)
done
-lemma component_trans: "[| F <= G; G <= H |] ==> F <= (H :: 'a program)"
+lemma component_trans: "[| F \<le> G; G \<le> H |] ==> F \<le> (H :: 'a program)"
apply (unfold component_def)
apply (blast intro: Join_assoc [symmetric])
done
-lemma component_antisym: "[| F <= G; G <= F |] ==> F = (G :: 'a program)"
+lemma component_antisym: "[| F \<le> G; G \<le> F |] ==> F = (G :: 'a program)"
apply (simp (no_asm_use) add: component_eq_subset)
apply (blast intro!: program_equalityI)
done
-lemma Join_component_iff: "((F Join G) <= H) = (F <= H & G <= H)"
+lemma Join_component_iff: "((F Join G) \<le> H) = (F \<le> H & G \<le> H)"
by (simp add: component_eq_subset, blast)
-lemma component_constrains: "[| F <= G; G : A co B |] ==> F : A co B"
+lemma component_constrains: "[| F \<le> G; G \<in> A co B |] ==> F \<in> A co B"
by (auto simp add: constrains_def component_eq_subset)
(*Used in Guar.thy to show that programs are partially ordered*)
@@ -117,34 +116,34 @@
subsection{*The preserves property*}
-lemma preservesI: "(!!z. F : stable {s. v s = z}) ==> F : preserves v"
+lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v"
by (unfold preserves_def, blast)
lemma preserves_imp_eq:
- "[| F : preserves v; act : Acts F; (s,s') : act |] ==> v s = v s'"
+ "[| 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
lemma Join_preserves [iff]:
- "(F Join G : preserves v) = (F : preserves v & G : preserves v)"
+ "(F Join G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)"
apply (unfold preserves_def, auto)
done
lemma JN_preserves [iff]:
- "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)"
+ "(JOIN I F \<in> preserves v) = (\<forall>i \<in> I. F i \<in> preserves v)"
apply (simp add: JN_stable preserves_def, blast)
done
-lemma SKIP_preserves [iff]: "SKIP : preserves v"
+lemma SKIP_preserves [iff]: "SKIP \<in> preserves v"
by (auto simp add: preserves_def)
lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)"
by (simp add: funPair_def)
-lemma preserves_funPair: "preserves (funPair v w) = preserves v Int preserves w"
+lemma preserves_funPair: "preserves (funPair v w) = preserves v \<inter> preserves w"
by (auto simp add: preserves_def stable_def constrains_def, blast)
-(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *)
+(* (F \<in> preserves (funPair v w)) = (F \<in> preserves v \<inter> preserves w) *)
declare preserves_funPair [THEN eqset_imp_iff, iff]
@@ -157,20 +156,20 @@
lemma snd_o_funPair [simp]: "snd o (funPair f g) = g"
by (simp add: funPair_def o_def)
-lemma subset_preserves_o: "preserves v <= preserves (w o v)"
+lemma subset_preserves_o: "preserves v \<subseteq> preserves (w o v)"
by (force simp add: preserves_def stable_def constrains_def)
-lemma preserves_subset_stable: "preserves v <= stable {s. P (v s)}"
+lemma preserves_subset_stable: "preserves v \<subseteq> stable {s. P (v s)}"
apply (auto simp add: preserves_def stable_def constrains_def)
apply (rename_tac s' s)
apply (subgoal_tac "v s = v s'")
apply (force+)
done
-lemma preserves_subset_increasing: "preserves v <= increasing v"
+lemma preserves_subset_increasing: "preserves v \<subseteq> increasing v"
by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def)
-lemma preserves_id_subset_stable: "preserves id <= stable A"
+lemma preserves_id_subset_stable: "preserves id \<subseteq> stable A"
by (force simp add: preserves_def stable_def constrains_def)
@@ -183,27 +182,27 @@
(** Some lemmas used only in Client.ML **)
lemma stable_localTo_stable2:
- "[| F : stable {s. P (v s) (w s)};
- G : preserves v; G : preserves w |]
- ==> F Join G : stable {s. P (v s) (w s)}"
-apply (simp (no_asm_simp))
-apply (subgoal_tac "G: preserves (funPair v w) ")
+ "[| 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)}"
+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)
+apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)
done
lemma Increasing_preserves_Stable:
- "[| F : stable {s. v s <= w s}; G : preserves v;
- F Join G : Increasing w |]
- ==> F Join G : Stable {s. v s <= w s}"
+ "[| 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}"
apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
apply (blast intro: constrains_weaken)
(*The G case remains*)
apply (auto simp add: preserves_def stable_def constrains_def)
apply (case_tac "act: Acts F", blast)
(*We have a G-action, so delete assumptions about F-actions*)
-apply (erule_tac V = "ALL act:Acts F. ?P act" in thin_rl)
-apply (erule_tac V = "ALL z. ALL act:Acts F. ?P z act" in thin_rl)
+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
@@ -212,12 +211,12 @@
(** component_of **)
-(* component_of is stronger than <= *)
-lemma component_of_imp_component: "F component_of H ==> F <= H"
+(* component_of is stronger than \<le> *)
+lemma component_of_imp_component: "F component_of H ==> F \<le> H"
by (unfold component_def component_of_def, blast)
-(* component_of satisfies many of the <='s properties *)
+(* component_of satisfies many of the same properties as \<le> *)
lemma component_of_refl [simp]: "F component_of F"
apply (unfold component_of_def)
apply (rule_tac x = SKIP in exI, auto)
@@ -243,7 +242,7 @@
by (simp add: localize_def)
lemma localize_AllowedActs_eq [simp]:
- "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)"
+ "AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)"
by (unfold localize_def, auto)
end