--- 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
--- a/src/HOL/UNITY/Constrains.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Constrains.thy Tue Feb 04 18:12:40 2003 +0100
@@ -18,65 +18,65 @@
inductive "traces init acts"
intros
(*Initial trace is empty*)
- Init: "s: init ==> (s,[]) : traces init acts"
+ Init: "s \<in> init ==> (s,[]) \<in> traces init acts"
- Acts: "[| act: acts; (s,evs) : traces init acts; (s,s'): act |]
- ==> (s', s#evs) : traces init acts"
+ Acts: "[| act: acts; (s,evs) \<in> traces init acts; (s,s'): act |]
+ ==> (s', s#evs) \<in> traces init acts"
consts reachable :: "'a program => 'a set"
inductive "reachable F"
intros
- Init: "s: Init F ==> s : reachable F"
+ Init: "s \<in> Init F ==> s \<in> reachable F"
- Acts: "[| act: Acts F; s : reachable F; (s,s'): act |]
- ==> s' : reachable F"
+ Acts: "[| act: Acts F; s \<in> reachable F; (s,s'): act |]
+ ==> s' \<in> reachable F"
constdefs
Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60)
- "A Co B == {F. F : (reachable F Int A) co B}"
+ "A Co B == {F. F \<in> (reachable F \<inter> A) co B}"
Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60)
- "A Unless B == (A-B) Co (A Un B)"
+ "A Unless B == (A-B) Co (A \<union> B)"
Stable :: "'a set => 'a program set"
"Stable A == A Co A"
(*Always is the weak form of "invariant"*)
Always :: "'a set => 'a program set"
- "Always A == {F. Init F <= A} Int Stable A"
+ "Always A == {F. Init F \<subseteq> A} \<inter> Stable A"
- (*Polymorphic in both states and the meaning of <= *)
+ (*Polymorphic in both states and the meaning of \<le> *)
Increasing :: "['a => 'b::{order}] => 'a program set"
- "Increasing f == INT z. Stable {s. z <= f s}"
+ "Increasing f == \<Inter>z. Stable {s. z \<le> f s}"
subsection{*traces and reachable*}
lemma reachable_equiv_traces:
- "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"
+ "reachable F = {s. \<exists>evs. (s,evs): traces (Init F) (Acts F)}"
apply safe
apply (erule_tac [2] traces.induct)
apply (erule reachable.induct)
apply (blast intro: reachable.intros traces.intros)+
done
-lemma Init_subset_reachable: "Init F <= reachable F"
+lemma Init_subset_reachable: "Init F \<subseteq> reachable F"
by (blast intro: reachable.intros)
lemma stable_reachable [intro!,simp]:
- "Acts G <= Acts F ==> G : stable (reachable F)"
+ "Acts G \<subseteq> Acts F ==> G \<in> stable (reachable F)"
by (blast intro: stableI constrainsI reachable.intros)
(*The set of all reachable states is an invariant...*)
-lemma invariant_reachable: "F : invariant (reachable F)"
+lemma invariant_reachable: "F \<in> invariant (reachable F)"
apply (simp add: invariant_def)
apply (blast intro: reachable.intros)
done
(*...in fact the strongest invariant!*)
-lemma invariant_includes_reachable: "F : invariant A ==> reachable F <= A"
+lemma invariant_includes_reachable: "F \<in> invariant A ==> reachable F \<subseteq> A"
apply (simp add: stable_def constrains_def invariant_def)
apply (rule subsetI)
apply (erule reachable.induct)
@@ -86,55 +86,55 @@
subsection{*Co*}
-(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
+(*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
lemmas constrains_reachable_Int =
subset_refl [THEN stable_reachable [unfolded stable_def],
THEN constrains_Int, standard]
(*Resembles the previous definition of Constrains*)
lemma Constrains_eq_constrains:
- "A Co B = {F. F : (reachable F Int A) co (reachable F Int B)}"
+ "A Co B = {F. F \<in> (reachable F \<inter> A) co (reachable F \<inter> B)}"
apply (unfold Constrains_def)
apply (blast dest: constrains_reachable_Int intro: constrains_weaken)
done
-lemma constrains_imp_Constrains: "F : A co A' ==> F : A Co A'"
+lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'"
apply (unfold Constrains_def)
apply (blast intro: constrains_weaken_L)
done
-lemma stable_imp_Stable: "F : stable A ==> F : Stable A"
+lemma stable_imp_Stable: "F \<in> stable A ==> F \<in> Stable A"
apply (unfold stable_def Stable_def)
apply (erule constrains_imp_Constrains)
done
lemma ConstrainsI:
- "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A')
- ==> F : A Co A'"
+ "(!!act s s'. [| act: Acts F; (s,s') \<in> act; s \<in> A |] ==> s': A')
+ ==> F \<in> A Co A'"
apply (rule constrains_imp_Constrains)
apply (blast intro: constrainsI)
done
-lemma Constrains_empty [iff]: "F : {} Co B"
+lemma Constrains_empty [iff]: "F \<in> {} Co B"
by (unfold Constrains_def constrains_def, blast)
-lemma Constrains_UNIV [iff]: "F : A Co UNIV"
+lemma Constrains_UNIV [iff]: "F \<in> A Co UNIV"
by (blast intro: ConstrainsI)
lemma Constrains_weaken_R:
- "[| F : A Co A'; A'<=B' |] ==> F : A Co B'"
+ "[| F \<in> A Co A'; A'<=B' |] ==> F \<in> A Co B'"
apply (unfold Constrains_def)
apply (blast intro: constrains_weaken_R)
done
lemma Constrains_weaken_L:
- "[| F : A Co A'; B<=A |] ==> F : B Co A'"
+ "[| F \<in> A Co A'; B \<subseteq> A |] ==> F \<in> B Co A'"
apply (unfold Constrains_def)
apply (blast intro: constrains_weaken_L)
done
lemma Constrains_weaken:
- "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'"
+ "[| F \<in> A Co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B Co B'"
apply (unfold Constrains_def)
apply (blast intro: constrains_weaken)
done
@@ -142,14 +142,14 @@
(** Union **)
lemma Constrains_Un:
- "[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')"
+ "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<union> B) Co (A' \<union> B')"
apply (unfold Constrains_def)
apply (blast intro: constrains_Un [THEN constrains_weaken])
done
lemma Constrains_UN:
- assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
- shows "F : (UN i:I. A i) Co (UN i:I. A' i)"
+ assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)"
+ shows "F \<in> (\<Union>i \<in> I. A i) Co (\<Union>i \<in> I. A' i)"
apply (unfold Constrains_def)
apply (rule CollectI)
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN,
@@ -159,83 +159,83 @@
(** Intersection **)
lemma Constrains_Int:
- "[| F : A Co A'; F : B Co B' |] ==> F : (A Int B) Co (A' Int B')"
+ "[| F \<in> A Co A'; F \<in> B Co B' |] ==> F \<in> (A \<inter> B) Co (A' \<inter> B')"
apply (unfold Constrains_def)
apply (blast intro: constrains_Int [THEN constrains_weaken])
done
lemma Constrains_INT:
- assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
- shows "F : (INT i:I. A i) Co (INT i:I. A' i)"
+ assumes Co: "!!i. i \<in> I ==> F \<in> (A i) Co (A' i)"
+ shows "F \<in> (\<Inter>i \<in> I. A i) Co (\<Inter>i \<in> I. A' i)"
apply (unfold Constrains_def)
apply (rule CollectI)
apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT,
THEN constrains_weaken], auto)
done
-lemma Constrains_imp_subset: "F : A Co A' ==> reachable F Int A <= A'"
+lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable F \<inter> A \<subseteq> A'"
by (simp add: constrains_imp_subset Constrains_def)
-lemma Constrains_trans: "[| F : A Co B; F : B Co C |] ==> F : A Co C"
+lemma Constrains_trans: "[| F \<in> A Co B; F \<in> B Co C |] ==> F \<in> A Co C"
apply (simp add: Constrains_eq_constrains)
apply (blast intro: constrains_trans constrains_weaken)
done
lemma Constrains_cancel:
- "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')"
+ "[| F \<in> A Co (A' \<union> B); F \<in> B Co B' |] ==> F \<in> A Co (A' \<union> B')"
by (simp add: Constrains_eq_constrains constrains_def, blast)
subsection{*Stable*}
(*Useful because there's no Stable_weaken. [Tanja Vos]*)
-lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B"
+lemma Stable_eq: "[| F \<in> Stable A; A = B |] ==> F \<in> Stable B"
by blast
-lemma Stable_eq_stable: "(F : Stable A) = (F : stable (reachable F Int A))"
+lemma Stable_eq_stable: "(F \<in> Stable A) = (F \<in> stable (reachable F \<inter> A))"
by (simp add: Stable_def Constrains_eq_constrains stable_def)
-lemma StableI: "F : A Co A ==> F : Stable A"
+lemma StableI: "F \<in> A Co A ==> F \<in> Stable A"
by (unfold Stable_def, assumption)
-lemma StableD: "F : Stable A ==> F : A Co A"
+lemma StableD: "F \<in> Stable A ==> F \<in> A Co A"
by (unfold Stable_def, assumption)
lemma Stable_Un:
- "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')"
+ "[| F \<in> Stable A; F \<in> Stable A' |] ==> F \<in> Stable (A \<union> A')"
apply (unfold Stable_def)
apply (blast intro: Constrains_Un)
done
lemma Stable_Int:
- "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')"
+ "[| F \<in> Stable A; F \<in> Stable A' |] ==> F \<in> Stable (A \<inter> A')"
apply (unfold Stable_def)
apply (blast intro: Constrains_Int)
done
lemma Stable_Constrains_Un:
- "[| F : Stable C; F : A Co (C Un A') |]
- ==> F : (C Un A) Co (C Un A')"
+ "[| F \<in> Stable C; F \<in> A Co (C \<union> A') |]
+ ==> F \<in> (C \<union> A) Co (C \<union> A')"
apply (unfold Stable_def)
apply (blast intro: Constrains_Un [THEN Constrains_weaken])
done
lemma Stable_Constrains_Int:
- "[| F : Stable C; F : (C Int A) Co A' |]
- ==> F : (C Int A) Co (C Int A')"
+ "[| F \<in> Stable C; F \<in> (C \<inter> A) Co A' |]
+ ==> F \<in> (C \<inter> A) Co (C \<inter> A')"
apply (unfold Stable_def)
apply (blast intro: Constrains_Int [THEN Constrains_weaken])
done
lemma Stable_UN:
- "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)"
+ "(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Union>i \<in> I. A i)"
by (simp add: Stable_def Constrains_UN)
lemma Stable_INT:
- "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)"
+ "(!!i. i \<in> I ==> F \<in> Stable (A i)) ==> F \<in> Stable (\<Inter>i \<in> I. A i)"
by (simp add: Stable_def Constrains_INT)
-lemma Stable_reachable: "F : Stable (reachable F)"
+lemma Stable_reachable: "F \<in> Stable (reachable F)"
by (simp add: Stable_eq_stable)
@@ -243,22 +243,22 @@
subsection{*Increasing*}
lemma IncreasingD:
- "F : Increasing f ==> F : Stable {s. x <= f s}"
+ "F \<in> Increasing f ==> F \<in> Stable {s. x \<le> f s}"
by (unfold Increasing_def, blast)
lemma mono_Increasing_o:
- "mono g ==> Increasing f <= Increasing (g o f)"
+ "mono g ==> Increasing f \<subseteq> Increasing (g o f)"
apply (simp add: Increasing_def Stable_def Constrains_def stable_def
constrains_def)
apply (blast intro: monoD order_trans)
done
lemma strict_IncreasingD:
- "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}"
+ "!!z::nat. F \<in> Increasing f ==> F \<in> Stable {s. z < f s}"
by (simp add: Increasing_def Suc_le_eq [symmetric])
lemma increasing_imp_Increasing:
- "F : increasing f ==> F : Increasing f"
+ "F \<in> increasing f ==> F \<in> Increasing f"
apply (unfold increasing_def Increasing_def)
apply (blast intro: stable_imp_Stable)
done
@@ -270,17 +270,17 @@
subsection{*The Elimination Theorem*}
(*The "free" m has become universally quantified! Should the premise be !!m
-instead of ALL m ? Would make it harder to use in forward proof.*)
+instead of \<forall>m ? Would make it harder to use in forward proof.*)
lemma Elimination:
- "[| ALL m. F : {s. s x = m} Co (B m) |]
- ==> F : {s. s x : M} Co (UN m:M. B m)"
+ "[| \<forall>m. F \<in> {s. s x = m} Co (B m) |]
+ ==> F \<in> {s. s x \<in> M} Co (\<Union>m \<in> M. B m)"
by (unfold Constrains_def constrains_def, blast)
(*As above, but for the trivial case of a one-variable state, in which the
state is identified with its one variable.*)
lemma Elimination_sing:
- "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)"
+ "(\<forall>m. F \<in> {m} Co (B m)) ==> F \<in> M Co (\<Union>m \<in> M. B m)"
by (unfold Constrains_def constrains_def, blast)
@@ -288,10 +288,10 @@
(** Natural deduction rules for "Always A" **)
-lemma AlwaysI: "[| Init F<=A; F : Stable A |] ==> F : Always A"
+lemma AlwaysI: "[| Init F \<subseteq> A; F \<in> Stable A |] ==> F \<in> Always A"
by (simp add: Always_def)
-lemma AlwaysD: "F : Always A ==> Init F<=A & F : Stable A"
+lemma AlwaysD: "F \<in> Always A ==> Init F \<subseteq> A & F \<in> Stable A"
by (simp add: Always_def)
lemmas AlwaysE = AlwaysD [THEN conjE, standard]
@@ -299,7 +299,7 @@
(*The set of all reachable states is Always*)
-lemma Always_includes_reachable: "F : Always A ==> reachable F <= A"
+lemma Always_includes_reachable: "F \<in> Always A ==> reachable F \<subseteq> A"
apply (simp add: Stable_def Constrains_def constrains_def Always_def)
apply (rule subsetI)
apply (erule reachable.induct)
@@ -307,7 +307,7 @@
done
lemma invariant_imp_Always:
- "F : invariant A ==> F : Always A"
+ "F \<in> invariant A ==> F \<in> Always A"
apply (unfold Always_def invariant_def Stable_def stable_def)
apply (blast intro: constrains_imp_Constrains)
done
@@ -316,55 +316,55 @@
invariant_reachable [THEN invariant_imp_Always, standard]
lemma Always_eq_invariant_reachable:
- "Always A = {F. F : invariant (reachable F Int A)}"
+ "Always A = {F. F \<in> invariant (reachable F \<inter> A)}"
apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains
stable_def)
apply (blast intro: reachable.intros)
done
(*the RHS is the traditional definition of the "always" operator*)
-lemma Always_eq_includes_reachable: "Always A = {F. reachable F <= A}"
+lemma Always_eq_includes_reachable: "Always A = {F. reachable F \<subseteq> A}"
by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable)
lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV"
by (auto simp add: Always_eq_includes_reachable)
-lemma UNIV_AlwaysI: "UNIV <= A ==> F : Always A"
+lemma UNIV_AlwaysI: "UNIV \<subseteq> A ==> F \<in> Always A"
by (auto simp add: Always_eq_includes_reachable)
-lemma Always_eq_UN_invariant: "Always A = (UN I: Pow A. invariant I)"
+lemma Always_eq_UN_invariant: "Always A = (\<Union>I \<in> Pow A. invariant I)"
apply (simp add: Always_eq_includes_reachable)
apply (blast intro: invariantI Init_subset_reachable [THEN subsetD]
invariant_includes_reachable [THEN subsetD])
done
-lemma Always_weaken: "[| F : Always A; A <= B |] ==> F : Always B"
+lemma Always_weaken: "[| F \<in> Always A; A \<subseteq> B |] ==> F \<in> Always B"
by (auto simp add: Always_eq_includes_reachable)
subsection{*"Co" rules involving Always*}
lemma Always_Constrains_pre:
- "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')"
+ "F \<in> Always INV ==> (F \<in> (INV \<inter> A) Co A') = (F \<in> A Co A')"
by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def
Int_assoc [symmetric])
lemma Always_Constrains_post:
- "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')"
+ "F \<in> Always INV ==> (F \<in> A Co (INV \<inter> A')) = (F \<in> A Co A')"
by (simp add: Always_includes_reachable [THEN Int_absorb2]
Constrains_eq_constrains Int_assoc [symmetric])
-(* [| F : Always INV; F : (INV Int A) Co A' |] ==> F : A Co A' *)
+(* [| F \<in> Always INV; F \<in> (INV \<inter> A) Co A' |] ==> F \<in> A Co A' *)
lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard]
-(* [| F : Always INV; F : A Co A' |] ==> F : A Co (INV Int A') *)
+(* [| F \<in> Always INV; F \<in> A Co A' |] ==> F \<in> A Co (INV \<inter> A') *)
lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
lemma Always_Constrains_weaken:
- "[| F : Always C; F : A Co A';
- C Int B <= A; C Int A' <= B' |]
- ==> F : B Co B'"
+ "[| F \<in> Always C; F \<in> A Co A';
+ C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |]
+ ==> F \<in> B Co B'"
apply (rule Always_ConstrainsI, assumption)
apply (drule Always_ConstrainsD, assumption)
apply (blast intro: Constrains_weaken)
@@ -373,23 +373,23 @@
(** Conjoining Always properties **)
-lemma Always_Int_distrib: "Always (A Int B) = Always A Int Always B"
+lemma Always_Int_distrib: "Always (A \<inter> B) = Always A \<inter> Always B"
by (auto simp add: Always_eq_includes_reachable)
-lemma Always_INT_distrib: "Always (INTER I A) = (INT i:I. Always (A i))"
+lemma Always_INT_distrib: "Always (INTER I A) = (\<Inter>i \<in> I. Always (A i))"
by (auto simp add: Always_eq_includes_reachable)
lemma Always_Int_I:
- "[| F : Always A; F : Always B |] ==> F : Always (A Int B)"
+ "[| F \<in> Always A; F \<in> Always B |] ==> F \<in> Always (A \<inter> B)"
by (simp add: Always_Int_distrib)
(*Allows a kind of "implication introduction"*)
lemma Always_Compl_Un_eq:
- "F : Always A ==> (F : Always (-A Un B)) = (F : Always B)"
+ "F \<in> Always A ==> (F \<in> Always (-A \<union> B)) = (F \<in> Always B)"
by (auto simp add: Always_eq_includes_reachable)
(*Delete the nearest invariance assumption (which will be the second one
used by Always_Int_I) *)
-lemmas Always_thin = thin_rl [of "F : Always A", standard]
+lemmas Always_thin = thin_rl [of "F \<in> Always A", standard]
end
--- a/src/HOL/UNITY/Detects.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Detects.thy Tue Feb 04 18:12:40 2003 +0100
@@ -15,47 +15,47 @@
op_Equality :: "['a set, 'a set] => 'a set" (infixl "<==>" 60)
defs
- Detects_def: "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)"
- Equality_def: "A <==> B == (-A Un B) Int (A Un -B)"
+ Detects_def: "A Detects B == (Always (-A \<union> B)) \<inter> (B LeadsTo A)"
+ Equality_def: "A <==> B == (-A \<union> B) \<inter> (A \<union> -B)"
(* Corollary from Sectiom 3.6.4 *)
-lemma Always_at_FP: "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))"
+lemma Always_at_FP: "F \<in> A LeadsTo B ==> F \<in> Always (-((FP F) \<inter> A \<inter> -B))"
apply (rule LeadsTo_empty)
-apply (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))")
-apply (subgoal_tac [2] " (FP F Int A Int - B) = (A Int (FP F Int -B))")
-apply (subgoal_tac "(B Int (FP F Int -B)) = {}")
+apply (subgoal_tac "F \<in> (FP F \<inter> A \<inter> - B) LeadsTo (B \<inter> (FP F \<inter> -B))")
+apply (subgoal_tac [2] " (FP F \<inter> A \<inter> - B) = (A \<inter> (FP F \<inter> -B))")
+apply (subgoal_tac "(B \<inter> (FP F \<inter> -B)) = {}")
apply auto
apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int)
done
lemma Detects_Trans:
- "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C"
+ "[| F \<in> A Detects B; F \<in> B Detects C |] ==> F \<in> A Detects C"
apply (unfold Detects_def Int_def)
apply (simp (no_asm))
apply safe
apply (rule_tac [2] LeadsTo_Trans)
apply auto
-apply (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))")
+apply (subgoal_tac "F \<in> Always ((-A \<union> B) \<inter> (-B \<union> C))")
apply (blast intro: Always_weaken)
apply (simp add: Always_Int_distrib)
done
-lemma Detects_refl: "F : A Detects A"
+lemma Detects_refl: "F \<in> A Detects A"
apply (unfold Detects_def)
apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo)
done
-lemma Detects_eq_Un: "(A<==>B) = (A Int B) Un (-A Int -B)"
+lemma Detects_eq_Un: "(A<==>B) = (A \<inter> B) \<union> (-A \<inter> -B)"
apply (unfold Equality_def)
apply blast
done
(*Not quite antisymmetry: sets A and B agree in all reachable states *)
lemma Detects_antisym:
- "[| F : A Detects B; F : B Detects A|] ==> F : Always (A <==> B)"
+ "[| F \<in> A Detects B; F \<in> B Detects A|] ==> F \<in> Always (A <==> B)"
apply (unfold Detects_def Equality_def)
apply (simp add: Always_Int_I Un_commute)
done
@@ -64,7 +64,7 @@
(* Theorem from Section 3.8 *)
lemma Detects_Always:
- "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))"
+ "F \<in> A Detects B ==> F \<in> Always ((-(FP F)) \<union> (A <==> B))"
apply (unfold Detects_def Equality_def)
apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib)
apply (blast dest: Always_at_FP intro: Always_weaken)
@@ -73,11 +73,11 @@
(* Theorem from exercise 11.1 Section 11.3.1 *)
lemma Detects_Imp_LeadstoEQ:
- "F : A Detects B ==> F : UNIV LeadsTo (A <==> B)"
+ "F \<in> A Detects B ==> F \<in> UNIV LeadsTo (A <==> B)"
apply (unfold Detects_def Equality_def)
apply (rule_tac B = "B" in LeadsTo_Diff)
-prefer 2 apply (blast intro: Always_LeadsTo_weaken)
-apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
+ apply (blast intro: Always_LeadsToI subset_imp_LeadsTo)
+apply (blast intro: Always_LeadsTo_weaken)
done
--- a/src/HOL/UNITY/Extend.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Extend.thy Tue Feb 04 18:12:40 2003 +0100
@@ -16,23 +16,23 @@
(*MOVE to Relation.thy?*)
Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
- "Restrict A r == r Int (A <*> UNIV)"
+ "Restrict A r == r \<inter> (A <*> UNIV)"
good_map :: "['a*'b => 'c] => bool"
- "good_map h == surj h & (ALL x y. fst (inv h (h (x,y))) = x)"
+ "good_map h == surj h & (\<forall>x y. fst (inv h (h (x,y))) = x)"
(*Using the locale constant "f", this is f (h (x,y))) = x*)
extend_set :: "['a*'b => 'c, 'a set] => 'c set"
"extend_set h A == h ` (A <*> UNIV)"
project_set :: "['a*'b => 'c, 'c set] => 'a set"
- "project_set h C == {x. EX y. h(x,y) : C}"
+ "project_set h C == {x. \<exists>y. h(x,y) \<in> C}"
extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
- "extend_act h == %act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
+ "extend_act h == %act. \<Union>(s,s') \<in> act. \<Union>y. {(h(s,y), h(s',y))}"
project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
- "project_act h act == {(x,x'). EX y y'. (h(x,y), h(x',y')) : act}"
+ "project_act h act == {(x,x'). \<exists>y y'. (h(x,y), h(x',y')) \<in> act}"
extend :: "['a*'b => 'c, 'a program] => 'c program"
"extend h F == mk_program (extend_set h (Init F),
@@ -56,7 +56,7 @@
good_h: "good_map h"
defines f_def: "f z == fst (inv h z)"
and g_def: "g z == snd (inv h z)"
- and slice_def: "slice Z y == {x. h(x,y) : Z}"
+ and slice_def: "slice Z y == {x. h(x,y) \<in> Z}"
(** These we prove OUTSIDE the locale. **)
@@ -65,7 +65,7 @@
subsection{*Restrict*}
(*MOVE to Relation.thy?*)
-lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x: A)"
+lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x \<in> A)"
by (unfold Restrict_def, blast)
lemma Restrict_UNIV [simp]: "Restrict UNIV = id"
@@ -76,29 +76,29 @@
lemma Restrict_empty [simp]: "Restrict {} r = {}"
by (auto simp add: Restrict_def)
-lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A Int B) r"
+lemma Restrict_Int [simp]: "Restrict A (Restrict B r) = Restrict (A \<inter> B) r"
by (unfold Restrict_def, blast)
-lemma Restrict_triv: "Domain r <= A ==> Restrict A r = r"
+lemma Restrict_triv: "Domain r \<subseteq> A ==> Restrict A r = r"
by (unfold Restrict_def, auto)
-lemma Restrict_subset: "Restrict A r <= r"
+lemma Restrict_subset: "Restrict A r \<subseteq> r"
by (unfold Restrict_def, auto)
lemma Restrict_eq_mono:
- "[| A <= B; Restrict B r = Restrict B s |]
+ "[| A \<subseteq> B; Restrict B r = Restrict B s |]
==> Restrict A r = Restrict A s"
by (unfold Restrict_def, blast)
lemma Restrict_imageI:
- "[| s : RR; Restrict A r = Restrict A s |]
- ==> Restrict A r : Restrict A ` RR"
+ "[| s \<in> RR; Restrict A r = Restrict A s |]
+ ==> Restrict A r \<in> Restrict A ` RR"
by (unfold Restrict_def image_def, auto)
-lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A Int Domain r"
+lemma Domain_Restrict [simp]: "Domain (Restrict A r) = A \<inter> Domain r"
by blast
-lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A Int B)"
+lemma Image_Restrict [simp]: "(Restrict A r) `` B = r `` (A \<inter> B)"
by blast
lemma insert_Id_image_Acts: "f Id = Id ==> insert Id (f`Acts F) = f ` Acts F"
@@ -169,19 +169,19 @@
subsection{*@{term extend_set}: basic properties*}
lemma project_set_iff [iff]:
- "(x : project_set h C) = (EX y. h(x,y) : C)"
+ "(x \<in> project_set h C) = (\<exists>y. h(x,y) \<in> C)"
by (simp add: project_set_def)
-lemma extend_set_mono: "A<=B ==> extend_set h A <= extend_set h B"
+lemma extend_set_mono: "A \<subseteq> B ==> extend_set h A \<subseteq> extend_set h B"
by (unfold extend_set_def, blast)
-lemma (in Extend) mem_extend_set_iff [iff]: "z : extend_set h A = (f z : A)"
+lemma (in Extend) mem_extend_set_iff [iff]: "z \<in> extend_set h A = (f z \<in> A)"
apply (unfold extend_set_def)
apply (force intro: h_f_g_eq [symmetric])
done
lemma (in Extend) extend_set_strict_mono [iff]:
- "(extend_set h A <= extend_set h B) = (A <= B)"
+ "(extend_set h A \<subseteq> extend_set h B) = (A \<subseteq> B)"
by (unfold extend_set_def, force)
lemma extend_set_empty [simp]: "extend_set h {} = {}"
@@ -198,7 +198,7 @@
by (unfold extend_set_def, auto)
lemma (in Extend) extend_set_project_set:
- "C <= extend_set h (project_set h C)"
+ "C \<subseteq> extend_set h (project_set h C)"
apply (unfold extend_set_def)
apply (auto simp add: split_extended_all, blast)
done
@@ -220,7 +220,7 @@
by (auto intro: f_h_eq [symmetric] simp add: split_extended_all)
(*Converse appears to fail*)
-lemma (in Extend) project_set_I: "!!z. z : C ==> f z : project_set h C"
+lemma (in Extend) project_set_I: "!!z. z \<in> C ==> f z \<in> project_set h C"
by (auto simp add: split_extended_all)
@@ -228,31 +228,31 @@
(*Because A and B could differ on the "other" part of the state,
cannot generalize to
- project_set h (A Int B) = project_set h A Int project_set h B
+ project_set h (A \<inter> B) = project_set h A \<inter> project_set h B
*)
lemma (in Extend) project_set_extend_set_Int:
- "project_set h ((extend_set h A) Int B) = A Int (project_set h B)"
+ "project_set h ((extend_set h A) \<inter> B) = A \<inter> (project_set h B)"
by auto
(*Unused, but interesting?*)
lemma (in Extend) project_set_extend_set_Un:
- "project_set h ((extend_set h A) Un B) = A Un (project_set h B)"
+ "project_set h ((extend_set h A) \<union> B) = A \<union> (project_set h B)"
by auto
lemma project_set_Int_subset:
- "project_set h (A Int B) <= (project_set h A) Int (project_set h B)"
+ "project_set h (A \<inter> B) \<subseteq> (project_set h A) \<inter> (project_set h B)"
by auto
lemma (in Extend) extend_set_Un_distrib:
- "extend_set h (A Un B) = extend_set h A Un extend_set h B"
+ "extend_set h (A \<union> B) = extend_set h A \<union> extend_set h B"
by auto
lemma (in Extend) extend_set_Int_distrib:
- "extend_set h (A Int B) = extend_set h A Int extend_set h B"
+ "extend_set h (A \<inter> B) = extend_set h A \<inter> extend_set h B"
by auto
lemma (in Extend) extend_set_INT_distrib:
- "extend_set h (INTER A B) = (INT x:A. extend_set h (B x))"
+ "extend_set h (INTER A B) = (\<Inter>x \<in> A. extend_set h (B x))"
by auto
lemma (in Extend) extend_set_Diff_distrib:
@@ -260,26 +260,26 @@
by auto
lemma (in Extend) extend_set_Union:
- "extend_set h (Union A) = (UN X:A. extend_set h X)"
+ "extend_set h (Union A) = (\<Union>X \<in> A. extend_set h X)"
by blast
lemma (in Extend) extend_set_subset_Compl_eq:
- "(extend_set h A <= - extend_set h B) = (A <= - B)"
+ "(extend_set h A \<subseteq> - extend_set h B) = (A \<subseteq> - B)"
by (unfold extend_set_def, auto)
subsection{*@{term extend_act}*}
(*Can't strengthen it to
- ((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y')
+ ((h(s,y), h(s',y')) \<in> extend_act h act) = ((s, s') \<in> act & y=y')
because h doesn't have to be injective in the 2nd argument*)
lemma (in Extend) mem_extend_act_iff [iff]:
- "((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)"
+ "((h(s,y), h(s',y)) \<in> extend_act h act) = ((s, s') \<in> act)"
by (unfold extend_act_def, auto)
(*Converse fails: (z,z') would include actions that changed the g-part*)
lemma (in Extend) extend_act_D:
- "(z, z') : extend_act h act ==> (f z, f z') : act"
+ "(z, z') \<in> extend_act h act ==> (f z, f z') \<in> act"
by (unfold extend_act_def, auto)
lemma (in Extend) extend_act_inverse [simp]:
@@ -292,7 +292,7 @@
by (unfold extend_act_def project_act_def, blast)
lemma (in Extend) subset_extend_act_D:
- "act' <= extend_act h act ==> project_act h act' <= act"
+ "act' \<subseteq> extend_act h act ==> project_act h act' \<subseteq> act"
by (unfold extend_act_def project_act_def, force)
lemma (in Extend) inj_extend_act: "inj (extend_act h)"
@@ -305,7 +305,7 @@
by (unfold extend_set_def extend_act_def, force)
lemma (in Extend) extend_act_strict_mono [iff]:
- "(extend_act h act' <= extend_act h act) = (act'<=act)"
+ "(extend_act h act' \<subseteq> extend_act h act) = (act'<=act)"
by (unfold extend_act_def, auto)
declare (in Extend) inj_extend_act [THEN inj_eq, iff]
@@ -322,7 +322,7 @@
done
lemma (in Extend) project_act_I:
- "!!z z'. (z, z') : act ==> (f z, f z') : project_act h act"
+ "!!z z'. (z, z') \<in> act ==> (f z, f z') \<in> project_act h act"
apply (unfold project_act_def)
apply (force simp add: split_extended_all)
done
@@ -365,7 +365,7 @@
lemma (in Extend) AllowedActs_project [simp]:
"AllowedActs(project h C F) =
{act. Restrict (project_set h C) act
- : project_act h ` Restrict C ` AllowedActs F}"
+ \<in> project_act h ` Restrict C ` AllowedActs F}"
apply (simp (no_asm) add: project_def image_iff)
apply (subst insert_absorb)
apply (auto intro!: bexI [of _ Id] simp add: project_act_def)
@@ -386,14 +386,14 @@
by auto
lemma project_set_Union:
- "project_set h (Union A) = (UN X:A. project_set h X)"
+ "project_set h (Union A) = (\<Union>X \<in> A. project_set h X)"
by blast
(*Converse FAILS: the extended state contributing to project_set h C
may not coincide with the one contributing to project_act h act*)
lemma (in Extend) project_act_Restrict_subset:
- "project_act h (Restrict C act) <=
+ "project_act h (Restrict C act) \<subseteq>
Restrict (project_set h C) (project_act h act)"
by (auto simp add: project_act_def)
@@ -405,7 +405,7 @@
"project h C (extend h F) =
mk_program (Init F, Restrict (project_set h C) ` Acts F,
{act. Restrict (project_set h C) act
- : project_act h ` Restrict C `
+ \<in> project_act h ` Restrict C `
(project_act h -` AllowedActs F)})"
apply (rule program_equalityI)
apply simp
@@ -439,7 +439,7 @@
done
lemma (in Extend) extend_JN [simp]:
- "extend h (JOIN I F) = (JN i:I. extend h (F i))"
+ "extend h (JOIN I F) = (\<Squnion>i \<in> I. extend h (F i))"
apply (rule program_equalityI)
apply (simp (no_asm) add: extend_set_INT_distrib)
apply (simp add: image_UN, auto)
@@ -447,49 +447,49 @@
(** These monotonicity results look natural but are UNUSED **)
-lemma (in Extend) extend_mono: "F <= G ==> extend h F <= extend h G"
+lemma (in Extend) extend_mono: "F \<le> G ==> extend h F \<le> extend h G"
by (force simp add: component_eq_subset)
-lemma (in Extend) project_mono: "F <= G ==> project h C F <= project h C G"
+lemma (in Extend) project_mono: "F \<le> G ==> project h C F \<le> project h C G"
by (simp add: component_eq_subset, blast)
subsection{*Safety: co, stable*}
lemma (in Extend) extend_constrains:
- "(extend h F : (extend_set h A) co (extend_set h B)) =
- (F : A co B)"
+ "(extend h F \<in> (extend_set h A) co (extend_set h B)) =
+ (F \<in> A co B)"
by (simp add: constrains_def)
lemma (in Extend) extend_stable:
- "(extend h F : stable (extend_set h A)) = (F : stable A)"
+ "(extend h F \<in> stable (extend_set h A)) = (F \<in> stable A)"
by (simp add: stable_def extend_constrains)
lemma (in Extend) extend_invariant:
- "(extend h F : invariant (extend_set h A)) = (F : invariant A)"
+ "(extend h F \<in> invariant (extend_set h A)) = (F \<in> invariant A)"
by (simp add: invariant_def extend_stable)
(*Projects the state predicates in the property satisfied by extend h F.
Converse fails: A and B may differ in their extra variables*)
lemma (in Extend) extend_constrains_project_set:
- "extend h F : A co B ==> F : (project_set h A) co (project_set h B)"
+ "extend h F \<in> A co B ==> F \<in> (project_set h A) co (project_set h B)"
by (auto simp add: constrains_def, force)
lemma (in Extend) extend_stable_project_set:
- "extend h F : stable A ==> F : stable (project_set h A)"
+ "extend h F \<in> stable A ==> F \<in> stable (project_set h A)"
by (simp add: stable_def extend_constrains_project_set)
subsection{*Weak safety primitives: Co, Stable*}
lemma (in Extend) reachable_extend_f:
- "p : reachable (extend h F) ==> f p : reachable F"
+ "p \<in> reachable (extend h F) ==> f p \<in> reachable F"
apply (erule reachable.induct)
apply (auto intro: reachable.intros simp add: extend_act_def image_iff)
done
lemma (in Extend) h_reachable_extend:
- "h(s,y) : reachable (extend h F) ==> s : reachable F"
+ "h(s,y) \<in> reachable (extend h F) ==> s \<in> reachable F"
by (force dest!: reachable_extend_f)
lemma (in Extend) reachable_extend_eq:
@@ -502,17 +502,17 @@
done
lemma (in Extend) extend_Constrains:
- "(extend h F : (extend_set h A) Co (extend_set h B)) =
- (F : A Co B)"
+ "(extend h F \<in> (extend_set h A) Co (extend_set h B)) =
+ (F \<in> A Co B)"
by (simp add: Constrains_def reachable_extend_eq extend_constrains
extend_set_Int_distrib [symmetric])
lemma (in Extend) extend_Stable:
- "(extend h F : Stable (extend_set h A)) = (F : Stable A)"
+ "(extend h F \<in> Stable (extend_set h A)) = (F \<in> Stable A)"
by (simp add: Stable_def extend_Constrains)
lemma (in Extend) extend_Always:
- "(extend h F : Always (extend_set h A)) = (F : Always A)"
+ "(extend h F \<in> Always (extend_set h A)) = (F \<in> Always A)"
by (simp (no_asm_simp) add: Always_def extend_Stable)
@@ -521,24 +521,24 @@
(** projection: monotonicity for safety **)
lemma project_act_mono:
- "D <= C ==>
- project_act h (Restrict D act) <= project_act h (Restrict C act)"
+ "D \<subseteq> C ==>
+ project_act h (Restrict D act) \<subseteq> project_act h (Restrict C act)"
by (auto simp add: project_act_def)
lemma (in Extend) project_constrains_mono:
- "[| D <= C; project h C F : A co B |] ==> project h D F : A co B"
+ "[| D \<subseteq> C; project h C F \<in> A co B |] ==> project h D F \<in> A co B"
apply (auto simp add: constrains_def)
apply (drule project_act_mono, blast)
done
lemma (in Extend) project_stable_mono:
- "[| D <= C; project h C F : stable A |] ==> project h D F : stable A"
+ "[| D \<subseteq> C; project h C F \<in> stable A |] ==> project h D F \<in> stable A"
by (simp add: stable_def project_constrains_mono)
(*Key lemma used in several proofs about project and co*)
lemma (in Extend) project_constrains:
- "(project h C F : A co B) =
- (F : (C Int extend_set h A) co (extend_set h B) & A <= B)"
+ "(project h C F \<in> A co B) =
+ (F \<in> (C \<inter> extend_set h A) co (extend_set h B) & A \<subseteq> B)"
apply (unfold constrains_def)
apply (auto intro!: project_act_I simp add: ball_Un)
apply (force intro!: project_act_I dest!: subsetD)
@@ -548,46 +548,46 @@
done
lemma (in Extend) project_stable:
- "(project h UNIV F : stable A) = (F : stable (extend_set h A))"
+ "(project h UNIV F \<in> stable A) = (F \<in> stable (extend_set h A))"
apply (unfold stable_def)
apply (simp (no_asm) add: project_constrains)
done
lemma (in Extend) project_stable_I:
- "F : stable (extend_set h A) ==> project h C F : stable A"
+ "F \<in> stable (extend_set h A) ==> project h C F \<in> stable A"
apply (drule project_stable [THEN iffD2])
apply (blast intro: project_stable_mono)
done
lemma (in Extend) Int_extend_set_lemma:
- "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B"
+ "A \<inter> extend_set h ((project_set h A) \<inter> B) = A \<inter> extend_set h B"
by (auto simp add: split_extended_all)
(*Strange (look at occurrences of C) but used in leadsETo proofs*)
lemma project_constrains_project_set:
- "G : C co B ==> project h C G : project_set h C co project_set h B"
+ "G \<in> C co B ==> project h C G \<in> project_set h C co project_set h B"
by (simp add: constrains_def project_def project_act_def, blast)
lemma project_stable_project_set:
- "G : stable C ==> project h C G : stable (project_set h C)"
+ "G \<in> stable C ==> project h C G \<in> stable (project_set h C)"
by (simp add: stable_def project_constrains_project_set)
subsection{*Progress: transient, ensures*}
lemma (in Extend) extend_transient:
- "(extend h F : transient (extend_set h A)) = (F : transient A)"
+ "(extend h F \<in> transient (extend_set h A)) = (F \<in> transient A)"
by (auto simp add: transient_def extend_set_subset_Compl_eq Domain_extend_act)
lemma (in Extend) extend_ensures:
- "(extend h F : (extend_set h A) ensures (extend_set h B)) =
- (F : A ensures B)"
+ "(extend h F \<in> (extend_set h A) ensures (extend_set h B)) =
+ (F \<in> A ensures B)"
by (simp add: ensures_def extend_constrains extend_transient
extend_set_Un_distrib [symmetric] extend_set_Diff_distrib [symmetric])
lemma (in Extend) leadsTo_imp_extend_leadsTo:
- "F : A leadsTo B
- ==> extend h F : (extend_set h A) leadsTo (extend_set h B)"
+ "F \<in> A leadsTo B
+ ==> extend h F \<in> (extend_set h A) leadsTo (extend_set h B)"
apply (erule leadsTo_induct)
apply (simp add: leadsTo_Basis extend_ensures)
apply (blast intro: leadsTo_Trans)
@@ -596,21 +596,21 @@
subsection{*Proving the converse takes some doing!*}
-lemma (in Extend) slice_iff [iff]: "(x : slice C y) = (h(x,y) : C)"
+lemma (in Extend) slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
by (simp (no_asm) add: slice_def)
-lemma (in Extend) slice_Union: "slice (Union S) y = (UN x:S. slice x y)"
+lemma (in Extend) slice_Union: "slice (Union S) y = (\<Union>x \<in> S. slice x y)"
by auto
lemma (in Extend) slice_extend_set: "slice (extend_set h A) y = A"
by auto
lemma (in Extend) project_set_is_UN_slice:
- "project_set h A = (UN y. slice A y)"
+ "project_set h A = (\<Union>y. slice A y)"
by auto
lemma (in Extend) extend_transient_slice:
- "extend h F : transient A ==> F : transient (slice A y)"
+ "extend h F \<in> transient A ==> F \<in> transient (slice A y)"
apply (unfold transient_def, auto)
apply (rule bexI, auto)
apply (force simp add: extend_act_def)
@@ -618,25 +618,25 @@
(*Converse?*)
lemma (in Extend) extend_constrains_slice:
- "extend h F : A co B ==> F : (slice A y) co (slice B y)"
+ "extend h F \<in> A co B ==> F \<in> (slice A y) co (slice B y)"
by (auto simp add: constrains_def)
lemma (in Extend) extend_ensures_slice:
- "extend h F : A ensures B ==> F : (slice A y) ensures (project_set h B)"
+ "extend h F \<in> A ensures B ==> F \<in> (slice A y) ensures (project_set h B)"
apply (auto simp add: ensures_def extend_constrains extend_transient)
apply (erule_tac [2] extend_transient_slice [THEN transient_strengthen])
apply (erule extend_constrains_slice [THEN constrains_weaken], auto)
done
lemma (in Extend) leadsTo_slice_project_set:
- "ALL y. F : (slice B y) leadsTo CU ==> F : (project_set h B) leadsTo CU"
+ "\<forall>y. F \<in> (slice B y) leadsTo CU ==> F \<in> (project_set h B) leadsTo CU"
apply (simp (no_asm) add: project_set_is_UN_slice)
apply (blast intro: leadsTo_UN)
done
lemma (in Extend) extend_leadsTo_slice [rule_format]:
- "extend h F : AU leadsTo BU
- ==> ALL y. F : (slice AU y) leadsTo (project_set h BU)"
+ "extend h F \<in> AU leadsTo BU
+ ==> \<forall>y. F \<in> (slice AU y) leadsTo (project_set h BU)"
apply (erule leadsTo_induct)
apply (blast intro: extend_ensures_slice leadsTo_Basis)
apply (blast intro: leadsTo_slice_project_set leadsTo_Trans)
@@ -644,8 +644,8 @@
done
lemma (in Extend) extend_leadsTo:
- "(extend h F : (extend_set h A) leadsTo (extend_set h B)) =
- (F : A leadsTo B)"
+ "(extend h F \<in> (extend_set h A) leadsTo (extend_set h B)) =
+ (F \<in> A leadsTo B)"
apply safe
apply (erule_tac [2] leadsTo_imp_extend_leadsTo)
apply (drule extend_leadsTo_slice)
@@ -653,8 +653,8 @@
done
lemma (in Extend) extend_LeadsTo:
- "(extend h F : (extend_set h A) LeadsTo (extend_set h B)) =
- (F : A LeadsTo B)"
+ "(extend h F \<in> (extend_set h A) LeadsTo (extend_set h B)) =
+ (F \<in> A LeadsTo B)"
by (simp add: LeadsTo_def reachable_extend_eq extend_leadsTo
extend_set_Int_distrib [symmetric])
@@ -662,20 +662,20 @@
subsection{*preserves*}
lemma (in Extend) project_preserves_I:
- "G : preserves (v o f) ==> project h C G : preserves v"
+ "G \<in> preserves (v o f) ==> project h C G \<in> preserves v"
by (auto simp add: preserves_def project_stable_I extend_set_eq_Collect)
(*to preserve f is to preserve the whole original state*)
lemma (in Extend) project_preserves_id_I:
- "G : preserves f ==> project h C G : preserves id"
+ "G \<in> preserves f ==> project h C G \<in> preserves id"
by (simp add: project_preserves_I)
lemma (in Extend) extend_preserves:
- "(extend h G : preserves (v o f)) = (G : preserves v)"
+ "(extend h G \<in> preserves (v o f)) = (G \<in> preserves v)"
by (auto simp add: preserves_def extend_stable [symmetric]
extend_set_eq_Collect)
-lemma (in Extend) inj_extend_preserves: "inj h ==> (extend h G : preserves g)"
+lemma (in Extend) inj_extend_preserves: "inj h ==> (extend h G \<in> preserves g)"
by (auto simp add: preserves_def extend_def extend_act_def stable_def
constrains_def g_def)
@@ -719,16 +719,16 @@
done
lemma (in Extend) guarantees_imp_extend_guarantees:
- "F : X guarantees Y ==>
- extend h F : (extend h ` X) guarantees (extend h ` Y)"
+ "F \<in> X guarantees Y ==>
+ extend h F \<in> (extend h ` X) guarantees (extend h ` Y)"
apply (rule guaranteesI, clarify)
apply (blast dest: ok_extend_imp_ok_project extend_Join_eq_extend_D
guaranteesD)
done
lemma (in Extend) extend_guarantees_imp_guarantees:
- "extend h F : (extend h ` X) guarantees (extend h ` Y)
- ==> F : X guarantees Y"
+ "extend h F \<in> (extend h ` X) guarantees (extend h ` Y)
+ ==> F \<in> X guarantees Y"
apply (auto simp add: guar_def)
apply (drule_tac x = "extend h G" in spec)
apply (simp del: extend_Join
@@ -737,8 +737,8 @@
done
lemma (in Extend) extend_guarantees_eq:
- "(extend h F : (extend h ` X) guarantees (extend h ` Y)) =
- (F : X guarantees Y)"
+ "(extend h F \<in> (extend h ` X) guarantees (extend h ` Y)) =
+ (F \<in> X guarantees Y)"
by (blast intro: guarantees_imp_extend_guarantees
extend_guarantees_imp_guarantees)
--- a/src/HOL/UNITY/Follows.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Follows.thy Tue Feb 04 18:12:40 2003 +0100
@@ -12,22 +12,22 @@
Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set"
(infixl "Fols" 65)
- "f Fols g == Increasing g Int Increasing f Int
- Always {s. f s <= g s} Int
- (INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
+ "f Fols g == Increasing g \<inter> Increasing f Int
+ Always {s. f s \<le> g s} Int
+ (\<Inter>k. {s. k \<le> g s} LeadsTo {s. k \<le> f s})"
(*Does this hold for "invariant"?*)
lemma mono_Always_o:
- "mono h ==> Always {s. f s <= g s} <= Always {s. h (f s) <= h (g s)}"
+ "mono h ==> Always {s. f s \<le> g s} \<subseteq> Always {s. h (f s) \<le> h (g s)}"
apply (simp add: Always_eq_includes_reachable)
apply (blast intro: monoD)
done
lemma mono_LeadsTo_o:
"mono (h::'a::order => 'b::order)
- ==> (INT j. {s. j <= g s} LeadsTo {s. j <= f s}) <=
- (INT k. {s. k <= h (g s)} LeadsTo {s. k <= h (f s)})"
+ ==> (\<Inter>j. {s. j \<le> g s} LeadsTo {s. j \<le> f s}) \<subseteq>
+ (\<Inter>k. {s. k \<le> h (g s)} LeadsTo {s. k \<le> h (f s)})"
apply auto
apply (rule single_LeadsTo_I)
apply (drule_tac x = "g s" in spec)
@@ -35,10 +35,10 @@
apply (blast intro: monoD order_trans)+
done
-lemma Follows_constant [iff]: "F : (%s. c) Fols (%s. c)"
+lemma Follows_constant [iff]: "F \<in> (%s. c) Fols (%s. c)"
by (unfold Follows_def, auto)
-lemma mono_Follows_o: "mono h ==> f Fols g <= (h o f) Fols (h o g)"
+lemma mono_Follows_o: "mono h ==> f Fols g \<subseteq> (h o f) Fols (h o g)"
apply (unfold Follows_def, clarify)
apply (simp add: mono_Increasing_o [THEN [2] rev_subsetD]
mono_Always_o [THEN [2] rev_subsetD]
@@ -46,13 +46,13 @@
done
lemma mono_Follows_apply:
- "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))"
+ "mono h ==> f Fols g \<subseteq> (%x. h (f x)) Fols (%x. h (g x))"
apply (drule mono_Follows_o)
apply (force simp add: o_def)
done
lemma Follows_trans:
- "[| F : f Fols g; F: g Fols h |] ==> F : f Fols h"
+ "[| F \<in> f Fols g; F \<in> g Fols h |] ==> F \<in> f Fols h"
apply (unfold Follows_def)
apply (simp add: Always_eq_includes_reachable)
apply (blast intro: order_trans LeadsTo_Trans)
@@ -61,24 +61,24 @@
subsection{*Destruction rules*}
-lemma Follows_Increasing1: "F : f Fols g ==> F : Increasing f"
+lemma Follows_Increasing1: "F \<in> f Fols g ==> F \<in> Increasing f"
apply (unfold Follows_def, blast)
done
-lemma Follows_Increasing2: "F : f Fols g ==> F : Increasing g"
+lemma Follows_Increasing2: "F \<in> f Fols g ==> F \<in> Increasing g"
apply (unfold Follows_def, blast)
done
-lemma Follows_Bounded: "F : f Fols g ==> F : Always {s. f s <= g s}"
+lemma Follows_Bounded: "F \<in> f Fols g ==> F \<in> Always {s. f s \<subseteq> g s}"
apply (unfold Follows_def, blast)
done
lemma Follows_LeadsTo:
- "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}"
+ "F \<in> f Fols g ==> F \<in> {s. k \<le> g s} LeadsTo {s. k \<le> f s}"
by (unfold Follows_def, blast)
lemma Follows_LeadsTo_pfixLe:
- "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}"
+ "F \<in> f Fols g ==> F \<in> {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}"
apply (rule single_LeadsTo_I, clarify)
apply (drule_tac k="g s" in Follows_LeadsTo)
apply (erule LeadsTo_weaken)
@@ -87,7 +87,7 @@
done
lemma Follows_LeadsTo_pfixGe:
- "F : f Fols g ==> F : {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}"
+ "F \<in> f Fols g ==> F \<in> {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}"
apply (rule single_LeadsTo_I, clarify)
apply (drule_tac k="g s" in Follows_LeadsTo)
apply (erule LeadsTo_weaken)
@@ -97,21 +97,21 @@
lemma Always_Follows1:
- "[| F : Always {s. f s = f' s}; F : f Fols g |] ==> F : f' Fols g"
+ "[| F \<in> Always {s. f s = f' s}; F \<in> f Fols g |] ==> F \<in> f' Fols g"
apply (unfold Follows_def Increasing_def Stable_def, auto)
apply (erule_tac [3] Always_LeadsTo_weaken)
-apply (erule_tac A = "{s. z <= f s}" and A' = "{s. z <= f s}"
+apply (erule_tac A = "{s. z \<le> f s}" and A' = "{s. z \<le> f s}"
in Always_Constrains_weaken, auto)
apply (drule Always_Int_I, assumption)
apply (force intro: Always_weaken)
done
lemma Always_Follows2:
- "[| F : Always {s. g s = g' s}; F : f Fols g |] ==> F : f Fols g'"
+ "[| F \<in> Always {s. g s = g' s}; F \<in> f Fols g |] ==> F \<in> f Fols g'"
apply (unfold Follows_def Increasing_def Stable_def, auto)
apply (erule_tac [3] Always_LeadsTo_weaken)
-apply (erule_tac A = "{s. z <= g s}" and A' = "{s. z <= g s}"
+apply (erule_tac A = "{s. z \<le> g s}" and A' = "{s. z \<le> g s}"
in Always_Constrains_weaken, auto)
apply (drule Always_Int_I, assumption)
apply (force intro: Always_weaken)
@@ -122,8 +122,8 @@
(*Can replace "Un" by any sup. But existing max only works for linorders.*)
lemma increasing_Un:
- "[| F : increasing f; F: increasing g |]
- ==> F : increasing (%s. (f s) Un (g s))"
+ "[| F \<in> increasing f; F \<in> increasing g |]
+ ==> F \<in> increasing (%s. (f s) \<union> (g s))"
apply (unfold increasing_def stable_def constrains_def, auto)
apply (drule_tac x = "f xa" in spec)
apply (drule_tac x = "g xa" in spec)
@@ -131,8 +131,8 @@
done
lemma Increasing_Un:
- "[| F : Increasing f; F: Increasing g |]
- ==> F : Increasing (%s. (f s) Un (g s))"
+ "[| F \<in> Increasing f; F \<in> Increasing g |]
+ ==> F \<in> Increasing (%s. (f s) \<union> (g s))"
apply (auto simp add: Increasing_def Stable_def Constrains_def
stable_def constrains_def)
apply (drule_tac x = "f xa" in spec)
@@ -142,17 +142,17 @@
lemma Always_Un:
- "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |]
- ==> F : Always {s. f' s Un g' s <= f s Un g s}"
+ "[| F \<in> Always {s. f' s \<le> f s}; F \<in> Always {s. g' s \<le> g s} |]
+ ==> F \<in> Always {s. f' s \<union> g' s \<le> f s \<union> g s}"
by (simp add: Always_eq_includes_reachable, blast)
(*Lemma to re-use the argument that one variable increases (progress)
while the other variable doesn't decrease (safety)*)
lemma Follows_Un_lemma:
- "[| F : Increasing f; F : Increasing g;
- F : Increasing g'; F : Always {s. f' s <= f s};
- ALL k. F : {s. k <= f s} LeadsTo {s. k <= f' s} |]
- ==> F : {s. k <= f s Un g s} LeadsTo {s. k <= f' s Un g s}"
+ "[| F \<in> Increasing f; F \<in> Increasing g;
+ F \<in> Increasing g'; F \<in> Always {s. f' s \<le> f s};
+ \<forall>k. F \<in> {s. k \<le> f s} LeadsTo {s. k \<le> f' s} |]
+ ==> F \<in> {s. k \<le> f s \<union> g s} LeadsTo {s. k \<le> f' s \<union> g s}"
apply (rule single_LeadsTo_I)
apply (drule_tac x = "f s" in IncreasingD)
apply (drule_tac x = "g s" in IncreasingD)
@@ -164,8 +164,8 @@
done
lemma Follows_Un:
- "[| F : f' Fols f; F: g' Fols g |]
- ==> F : (%s. (f' s) Un (g' s)) Fols (%s. (f s) Un (g s))"
+ "[| F \<in> f' Fols f; F \<in> g' Fols g |]
+ ==> F \<in> (%s. (f' s) \<union> (g' s)) Fols (%s. (f s) \<union> (g s))"
apply (unfold Follows_def)
apply (simp add: Increasing_Un Always_Un, auto)
apply (rule LeadsTo_Trans)
@@ -178,8 +178,8 @@
subsection{*Multiset union properties (with the multiset ordering)*}
lemma increasing_union:
- "[| F : increasing f; F: increasing g |]
- ==> F : increasing (%s. (f s) + (g s :: ('a::order) multiset))"
+ "[| F \<in> increasing f; F \<in> increasing g |]
+ ==> F \<in> increasing (%s. (f s) + (g s :: ('a::order) multiset))"
apply (unfold increasing_def stable_def constrains_def, auto)
apply (drule_tac x = "f xa" in spec)
apply (drule_tac x = "g xa" in spec)
@@ -188,8 +188,8 @@
done
lemma Increasing_union:
- "[| F : Increasing f; F: Increasing g |]
- ==> F : Increasing (%s. (f s) + (g s :: ('a::order) multiset))"
+ "[| F \<in> Increasing f; F \<in> Increasing g |]
+ ==> F \<in> Increasing (%s. (f s) + (g s :: ('a::order) multiset))"
apply (auto simp add: Increasing_def Stable_def Constrains_def
stable_def constrains_def)
apply (drule_tac x = "f xa" in spec)
@@ -199,19 +199,19 @@
done
lemma Always_union:
- "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |]
- ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}"
+ "[| F \<in> Always {s. f' s \<le> f s}; F \<in> Always {s. g' s \<le> g s} |]
+ ==> F \<in> Always {s. f' s + g' s \<le> f s + (g s :: ('a::order) multiset)}"
apply (simp add: Always_eq_includes_reachable)
apply (blast intro: union_le_mono)
done
(*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
lemma Follows_union_lemma:
- "[| F : Increasing f; F : Increasing g;
- F : Increasing g'; F : Always {s. f' s <= f s};
- ALL k::('a::order) multiset.
- F : {s. k <= f s} LeadsTo {s. k <= f' s} |]
- ==> F : {s. k <= f s + g s} LeadsTo {s. k <= f' s + g s}"
+ "[| F \<in> Increasing f; F \<in> Increasing g;
+ F \<in> Increasing g'; F \<in> Always {s. f' s \<le> f s};
+ \<forall>k::('a::order) multiset.
+ F \<in> {s. k \<le> f s} LeadsTo {s. k \<le> f' s} |]
+ ==> F \<in> {s. k \<le> f s + g s} LeadsTo {s. k \<le> f' s + g s}"
apply (rule single_LeadsTo_I)
apply (drule_tac x = "f s" in IncreasingD)
apply (drule_tac x = "g s" in IncreasingD)
@@ -226,8 +226,8 @@
(*The !! is there to influence to effect of permutative rewriting at the end*)
lemma Follows_union:
"!!g g' ::'b => ('a::order) multiset.
- [| F : f' Fols f; F: g' Fols g |]
- ==> F : (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))"
+ [| F \<in> f' Fols f; F \<in> g' Fols g |]
+ ==> F \<in> (%s. (f' s) + (g' s)) Fols (%s. (f s) + (g s))"
apply (unfold Follows_def)
apply (simp add: Increasing_union Always_union, auto)
apply (rule LeadsTo_Trans)
@@ -239,8 +239,8 @@
lemma Follows_setsum:
"!!f ::['c,'b] => ('a::order) multiset.
- [| ALL i: I. F : f' i Fols f i; finite I |]
- ==> F : (%s. \<Sum>i:I. f' i s) Fols (%s. \<Sum>i:I. f i s)"
+ [| \<forall>i \<in> I. F \<in> f' i Fols f i; finite I |]
+ ==> F \<in> (%s. \<Sum>i \<in> I. f' i s) Fols (%s. \<Sum>i \<in> I. f i s)"
apply (erule rev_mp)
apply (erule finite_induct, simp)
apply (simp add: Follows_union)
@@ -249,7 +249,7 @@
(*Currently UNUSED, but possibly of interest*)
lemma Increasing_imp_Stable_pfixGe:
- "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}"
+ "F \<in> Increasing func ==> F \<in> Stable {s. h pfixGe (func s)}"
apply (simp add: Increasing_def Stable_def Constrains_def constrains_def)
apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD]
prefix_imp_pfixGe)
@@ -257,8 +257,8 @@
(*Currently UNUSED, but possibly of interest*)
lemma LeadsTo_le_imp_pfixGe:
- "ALL z. F : {s. z <= f s} LeadsTo {s. z <= g s}
- ==> F : {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}"
+ "\<forall>z. F \<in> {s. z \<le> f s} LeadsTo {s. z \<le> g s}
+ ==> F \<in> {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}"
apply (rule single_LeadsTo_I)
apply (drule_tac x = "f s" in spec)
apply (erule LeadsTo_weaken)
--- a/src/HOL/UNITY/Guar.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Guar.thy Tue Feb 04 18:12:40 2003 +0100
@@ -32,57 +32,57 @@
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:X | G: X --> (F Join G) : X"
+ "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F Join G) \<in> X"
strict_ex_prop :: "'a program set => bool"
- "strict_ex_prop X == \<forall>F G. F ok G --> (F:X | G: X) = (F Join G : X)"
+ "strict_ex_prop X == \<forall>F G. F ok G --> (F \<in> X | G \<in> X) = (F Join G \<in> X)"
uv_prop :: "'a program set => bool"
- "uv_prop X == SKIP : X & (\<forall>F G. F ok G --> F:X & G: X --> (F Join G) : X)"
+ "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F Join G) \<in> X)"
strict_uv_prop :: "'a program set => bool"
"strict_uv_prop X ==
- SKIP : X & (\<forall>F G. F ok G --> (F:X & G: X) = (F Join G : X))"
+ SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F Join 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 : X --> F Join G : Y}"
+ "X guarantees Y == {F. \<forall>G. F ok G --> F Join G \<in> X --> F Join G \<in> Y}"
(* Weakest guarantees *)
wg :: "['a program, 'a program set] => 'a program set"
- "wg F Y == Union({X. F:X guarantees Y})"
+ "wg F Y == Union({X. F \<in> X guarantees Y})"
(* Weakest existential property stronger than X *)
wx :: "('a program) set => ('a program)set"
- "wx X == Union({Y. Y<=X & ex_prop Y})"
+ "wx X == Union({Y. Y \<subseteq> X & ex_prop Y})"
(*Ill-defined programs can arise through "Join"*)
welldef :: "'a program set"
- "welldef == {F. Init F ~= {}}"
+ "welldef == {F. Init F \<noteq> {}}"
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 : welldef Int X) -->
- (G Join H : welldef Int X)"
+ \<forall>H. (F ok H & G ok H & F Join H \<in> welldef \<inter> X) -->
+ (G Join H \<in> welldef \<inter> X)"
iso_refines :: "['a program, 'a program, 'a program set] => bool"
("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
"G iso_refines F wrt X ==
- F : welldef Int X --> G : welldef Int X"
+ F \<in> welldef \<inter> X --> G \<in> welldef \<inter> X"
lemma OK_insert_iff:
"(OK (insert i I) F) =
- (if i:I then OK I F else OK I F & (F i ok JOIN I F))"
+ (if i \<in> I then OK I F else OK I F & (F i ok JOIN I F))"
by (auto intro: ok_sym simp add: OK_iff_ok)
(*** existential properties ***)
lemma ex1 [rule_format]:
"[| ex_prop X; finite GG |] ==>
- GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X"
+ GG \<inter> X \<noteq> {}--> OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
apply (unfold ex_prop_def)
apply (erule finite_induct)
apply (auto simp add: OK_insert_iff Int_insert_left)
@@ -90,7 +90,7 @@
lemma ex2:
- "\<forall>GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X
+ "\<forall>GG. finite GG & GG \<inter> X \<noteq> {} --> OK GG (%G. G) -->(\<Squnion>G \<in> GG. G):X
==> ex_prop X"
apply (unfold ex_prop_def, clarify)
apply (drule_tac x = "{F,G}" in spec)
@@ -101,13 +101,13 @@
(*Chandy & Sanders take this as a definition*)
lemma ex_prop_finite:
"ex_prop X =
- (\<forall>GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)"
+ (\<forall>GG. finite GG & GG \<inter> X \<noteq> {} & OK GG (%G. G)--> (\<Squnion>G \<in> GG. G) \<in> X)"
by (blast intro: ex1 ex2)
(*Their "equivalent definition" given at the end of section 3*)
lemma ex_prop_equiv:
- "ex_prop X = (\<forall>G. G:X = (\<forall>H. (G component_of H) --> H: X))"
+ "ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))"
apply auto
apply (unfold ex_prop_def component_of_def, safe)
apply blast
@@ -120,14 +120,14 @@
(*** universal properties ***)
lemma uv1 [rule_format]:
"[| uv_prop X; finite GG |]
- ==> GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X"
+ ==> GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
apply (unfold uv_prop_def)
apply (erule finite_induct)
apply (auto simp add: Int_insert_left OK_insert_iff)
done
lemma uv2:
- "\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X
+ "\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X
==> uv_prop X"
apply (unfold uv_prop_def)
apply (rule conjI)
@@ -141,37 +141,37 @@
(*Chandy & Sanders take this as a definition*)
lemma uv_prop_finite:
"uv_prop X =
- (\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G): X)"
+ (\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G): X)"
by (blast intro: uv1 uv2)
(*** guarantees ***)
lemma guaranteesI:
- "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y)
- ==> F : X guarantees Y"
+ "(!!G. [| F ok G; F Join G \<in> X |] ==> F Join G \<in> Y)
+ ==> F \<in> X guarantees Y"
by (simp add: guar_def component_def)
lemma guaranteesD:
- "[| F : X guarantees Y; F ok G; F Join G : X |]
- ==> F Join G : Y"
+ "[| F \<in> X guarantees Y; F ok G; F Join G \<in> X |]
+ ==> F Join 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<=H since we need to reason about G*)
+ The major premise can no longer be F \<subseteq> H since we need to reason about G*)
lemma component_guaranteesD:
- "[| F : X guarantees Y; F Join G = H; H : X; F ok G |]
- ==> H : Y"
+ "[| F \<in> X guarantees Y; F Join G = H; H \<in> X; F ok G |]
+ ==> H \<in> Y"
by (unfold guar_def, blast)
lemma guarantees_weaken:
- "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"
+ "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'"
by (unfold guar_def, blast)
-lemma subset_imp_guarantees_UNIV: "X <= Y ==> X guarantees Y = UNIV"
+lemma subset_imp_guarantees_UNIV: "X \<subseteq> Y ==> X guarantees Y = UNIV"
by (unfold guar_def, blast)
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
-lemma subset_imp_guarantees: "X <= Y ==> F : X guarantees Y"
+lemma subset_imp_guarantees: "X \<subseteq> Y ==> F \<in> X guarantees Y"
by (unfold guar_def, blast)
(*Remark at end of section 4.1 *)
@@ -201,31 +201,31 @@
(** Distributive laws. Re-orient to perform miniscoping **)
lemma guarantees_UN_left:
- "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)"
+ "(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)"
by (unfold guar_def, blast)
lemma guarantees_Un_left:
- "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"
+ "(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)"
by (unfold guar_def, blast)
lemma guarantees_INT_right:
- "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)"
+ "X guarantees (\<Inter>i \<in> I. Y i) = (\<Inter>i \<in> I. X guarantees Y i)"
by (unfold guar_def, blast)
lemma guarantees_Int_right:
- "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"
+ "Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)"
by (unfold guar_def, blast)
lemma guarantees_Int_right_I:
- "[| F : Z guarantees X; F : Z guarantees Y |]
- ==> F : Z guarantees (X Int Y)"
+ "[| F \<in> Z guarantees X; F \<in> Z guarantees Y |]
+ ==> F \<in> Z guarantees (X \<inter> Y)"
by (simp add: guarantees_Int_right)
lemma guarantees_INT_right_iff:
- "(F : X guarantees (INTER I Y)) = (\<forall>i\<in>I. F : X guarantees (Y i))"
+ "(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
by (simp add: guarantees_INT_right)
-lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X Un Y))"
+lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))"
by (unfold guar_def, blast)
lemma contrapositive: "(X guarantees Y) = -Y guarantees -X"
@@ -236,35 +236,35 @@
**)
lemma combining1:
- "[| F : V guarantees X; F : (X Int Y) guarantees Z |]
- ==> F : (V Int Y) guarantees Z"
+ "[| F \<in> V guarantees X; F \<in> (X \<inter> Y) guarantees Z |]
+ ==> F \<in> (V \<inter> Y) guarantees Z"
by (unfold guar_def, blast)
lemma combining2:
- "[| F : V guarantees (X Un Y); F : Y guarantees Z |]
- ==> F : V guarantees (X Un Z)"
+ "[| F \<in> V guarantees (X \<union> Y); F \<in> Y guarantees Z |]
+ ==> F \<in> V guarantees (X \<union> Z)"
by (unfold guar_def, blast)
(** The following two follow Chandy-Sanders, but the use of object-quantifiers
does not suit Isabelle... **)
-(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
+(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
lemma all_guarantees:
- "\<forall>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"
+ "\<forall>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Inter>i \<in> I. Y i)"
by (unfold guar_def, blast)
-(*Premises should be [| F: X guarantees Y i; i: I |] *)
+(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
lemma ex_guarantees:
- "\<exists>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"
+ "\<exists>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y i)"
by (unfold guar_def, blast)
(*** Additional guarantees laws, by lcp ***)
lemma guarantees_Join_Int:
- "[| F: U guarantees V; G: X guarantees Y; F ok G |]
- ==> F Join G: (U Int X) guarantees (V Int Y)"
+ "[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |]
+ ==> F Join G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
@@ -275,8 +275,8 @@
done
lemma guarantees_Join_Un:
- "[| F: U guarantees V; G: X guarantees Y; F ok G |]
- ==> F Join G: (U Un X) guarantees (V Un Y)"
+ "[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |]
+ ==> F Join G \<in> (U \<union> X) guarantees (V \<union> Y)"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
@@ -287,8 +287,8 @@
done
lemma guarantees_JN_INT:
- "[| \<forall>i\<in>I. F i : X i guarantees Y i; OK I F |]
- ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)"
+ "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F |]
+ ==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)"
apply (unfold guar_def, auto)
apply (drule bspec, assumption)
apply (rename_tac "i")
@@ -298,8 +298,8 @@
done
lemma guarantees_JN_UN:
- "[| \<forall>i\<in>I. F i : X i guarantees Y i; OK I F |]
- ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)"
+ "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F |]
+ ==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)"
apply (unfold guar_def, auto)
apply (drule bspec, assumption)
apply (rename_tac "i")
@@ -312,7 +312,7 @@
(*** guarantees laws for breaking down the program, by lcp ***)
lemma guarantees_Join_I1:
- "[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"
+ "[| F \<in> X guarantees Y; F ok G |] ==> F Join G \<in> X guarantees Y"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
@@ -320,14 +320,14 @@
done
lemma guarantees_Join_I2:
- "[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"
+ "[| G \<in> X guarantees Y; F ok G |] ==> F Join G \<in> X guarantees Y"
apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
apply (blast intro: guarantees_Join_I1)
done
lemma guarantees_JN_I:
- "[| i : I; F i: X guarantees Y; OK I F |]
- ==> (JN i:I. (F i)) : X guarantees Y"
+ "[| 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 (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
@@ -336,10 +336,10 @@
(*** well-definedness ***)
-lemma Join_welldef_D1: "F Join G: welldef ==> F: welldef"
+lemma Join_welldef_D1: "F Join G \<in> welldef ==> F \<in> welldef"
by (unfold welldef_def, auto)
-lemma Join_welldef_D2: "F Join G: welldef ==> G: welldef"
+lemma Join_welldef_D2: "F Join G \<in> welldef ==> G \<in> welldef"
by (unfold welldef_def, auto)
(*** refinement ***)
@@ -357,14 +357,14 @@
lemma strict_ex_refine_lemma:
"strict_ex_prop X
- ==> (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X)
- = (F:X --> G: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)"
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 : welldef & F Join H : X --> G Join H : X) =
- (F: welldef Int X --> G:X)"
+ ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join 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)
apply (auto dest: Join_welldef_D1 Join_welldef_D2)
@@ -372,7 +372,7 @@
lemma ex_refinement_thm:
"[| strict_ex_prop X;
- \<forall>H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |]
+ \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X --> G Join 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)
@@ -381,13 +381,13 @@
lemma strict_uv_refine_lemma:
"strict_uv_prop X ==>
- (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G: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)"
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 : welldef & F Join H : X --> G Join H : X) =
- (F: welldef Int X --> G:X)"
+ ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join 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)
apply (auto dest: Join_welldef_D1 Join_welldef_D2)
@@ -395,8 +395,8 @@
lemma uv_refinement_thm:
"[| strict_uv_prop X;
- \<forall>H. F ok H & G ok H & F Join H : welldef Int X -->
- G Join H : welldef |]
+ \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X -->
+ G Join 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)
@@ -404,17 +404,17 @@
(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
lemma guarantees_equiv:
- "(F:X guarantees Y) = (\<forall>H. H:X \<longrightarrow> (F component_of H \<longrightarrow> H:Y))"
+ "(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))"
by (unfold guar_def component_of_def, auto)
-lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X <= (wg F Y)"
+lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X \<subseteq> (wg F Y)"
by (unfold wg_def, auto)
lemma wg_guarantees: "F:((wg F Y) guarantees Y)"
by (unfold wg_def guar_def, blast)
lemma wg_equiv:
- "(H: wg F X) = (F component_of H --> H:X)"
+ "(H \<in> wg F X) = (F component_of H --> H \<in> X)"
apply (unfold wg_def)
apply (simp (no_asm) add: guarantees_equiv)
apply (rule iffI)
@@ -423,21 +423,21 @@
done
-lemma component_of_wg: "F component_of H ==> (H:wg F X) = (H:X)"
+lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)"
by (simp add: wg_equiv)
lemma wg_finite:
- "\<forall>FF. finite FF & FF Int X ~= {} --> OK FF (%F. F)
- --> (\<forall>F\<in>FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))"
+ "\<forall>FF. finite FF & FF \<inter> X \<noteq> {} --> OK FF (%F. F)
+ --> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F): wg F X) = ((\<Squnion>F \<in> FF. F):X))"
apply clarify
-apply (subgoal_tac "F component_of (JN F:FF. F) ")
+apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
apply (drule_tac X = X in component_of_wg, simp)
apply (simp add: component_of_def)
-apply (rule_tac x = "JN F: (FF-{F}) . F" in exI)
+apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
done
-lemma wg_ex_prop: "ex_prop X ==> (F:X) = (\<forall>H. H : wg F X)"
+lemma wg_ex_prop: "ex_prop X ==> (F \<in> X) = (\<forall>H. H \<in> wg F X)"
apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
apply blast
done
@@ -455,11 +455,11 @@
apply auto
done
-lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z <= wx X"
+lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X"
by (unfold wx_def, auto)
(* Proposition 6 *)
-lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G:X})"
+lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G \<in> X})"
apply (unfold ex_prop_def, safe)
apply (drule_tac x = "G Join Ga" in spec)
apply (force simp add: ok_Join_iff1 Join_assoc)
@@ -483,7 +483,7 @@
apply (drule_tac x = G in spec)
apply (frule_tac c = "x Join G" in subsetD, safe)
apply (simp (no_asm))
-apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G:X}" in exI, safe)
+apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join 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)
@@ -496,7 +496,7 @@
(* Proposition 12 *)
(* Main result of the paper *)
lemma guarantees_wx_eq:
- "(X guarantees Y) = wx(-X Un Y)"
+ "(X guarantees Y) = wx(-X \<union> Y)"
apply (unfold guar_def)
apply (simp (no_asm) add: wx_equiv)
done
@@ -511,7 +511,7 @@
Reasoning About Program composition paper *)
lemma stable_guarantees_Always:
- "Init F <= A ==> F:(stable A) guarantees (Always A)"
+ "Init F \<subseteq> A ==> F:(stable A) guarantees (Always A)"
apply (rule guaranteesI)
apply (simp (no_asm) add: Join_commute)
apply (rule stable_Join_Always1)
@@ -519,7 +519,7 @@
done
(* To be moved to WFair.ML *)
-lemma leadsTo_Basis': "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B"
+lemma leadsTo_Basis': "[| F \<in> A co A \<union> B; F \<in> transient A |] ==> F \<in> A leadsTo B"
apply (drule_tac B = "A-B" in constrains_weaken_L)
apply (drule_tac [2] B = "A-B" in transient_strengthen)
apply (rule_tac [3] ensuresI [THEN leadsTo_Basis])
@@ -529,7 +529,7 @@
lemma constrains_guarantees_leadsTo:
- "F : transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"
+ "F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (B-A))"
apply (rule guaranteesI)
apply (rule leadsTo_Basis')
apply (drule constrains_weaken_R)
--- a/src/HOL/UNITY/Lift_prog.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Tue Feb 04 18:12:40 2003 +0100
@@ -116,23 +116,23 @@
lemma lift_set_empty [simp]: "lift_set i {} = {}"
by (unfold lift_set_def, auto)
-lemma lift_set_iff: "(lift_map i x : lift_set i A) = (x : A)"
+lemma lift_set_iff: "(lift_map i x \<in> lift_set i A) = (x \<in> A)"
apply (unfold lift_set_def)
apply (rule inj_lift_map [THEN inj_image_mem_iff])
done
(*Do we really need both this one and its predecessor?*)
lemma lift_set_iff2 [iff]:
- "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)"
+ "((f,uu) \<in> lift_set i A) = ((f i, (delete_map i f, uu)) \<in> A)"
by (simp add: lift_set_def mem_rename_set_iff drop_map_def)
-lemma lift_set_mono: "A<=B ==> lift_set i A <= lift_set i B"
+lemma lift_set_mono: "A \<subseteq> B ==> lift_set i A \<subseteq> lift_set i B"
apply (unfold lift_set_def)
apply (erule image_mono)
done
-lemma lift_set_Un_distrib: "lift_set i (A Un B) = lift_set i A Un lift_set i B"
+lemma lift_set_Un_distrib: "lift_set i (A \<union> B) = lift_set i A \<union> lift_set i B"
apply (unfold lift_set_def)
apply (simp add: image_Un)
done
@@ -154,39 +154,39 @@
lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
by (simp add: lift_def)
-lemma lift_JN [simp]: "lift j (JOIN I F) = (JN i:I. lift j (F i))"
+lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
by (simp add: lift_def)
(*** Safety: co, stable, invariant ***)
lemma lift_constrains:
- "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)"
+ "(lift i F \<in> (lift_set i A) co (lift_set i B)) = (F \<in> A co B)"
by (simp add: lift_def lift_set_def rename_constrains)
lemma lift_stable:
- "(lift i F : stable (lift_set i A)) = (F : stable A)"
+ "(lift i F \<in> stable (lift_set i A)) = (F \<in> stable A)"
by (simp add: lift_def lift_set_def rename_stable)
lemma lift_invariant:
- "(lift i F : invariant (lift_set i A)) = (F : invariant A)"
+ "(lift i F \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
apply (unfold lift_def lift_set_def)
apply (simp add: rename_invariant)
done
lemma lift_Constrains:
- "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)"
+ "(lift i F \<in> (lift_set i A) Co (lift_set i B)) = (F \<in> A Co B)"
apply (unfold lift_def lift_set_def)
apply (simp add: rename_Constrains)
done
lemma lift_Stable:
- "(lift i F : Stable (lift_set i A)) = (F : Stable A)"
+ "(lift i F \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
apply (unfold lift_def lift_set_def)
apply (simp add: rename_Stable)
done
lemma lift_Always:
- "(lift i F : Always (lift_set i A)) = (F : Always A)"
+ "(lift i F \<in> Always (lift_set i A)) = (F \<in> Always A)"
apply (unfold lift_def lift_set_def)
apply (simp add: rename_Always)
done
@@ -194,37 +194,37 @@
(*** Progress: transient, ensures ***)
lemma lift_transient:
- "(lift i F : transient (lift_set i A)) = (F : transient A)"
+ "(lift i F \<in> transient (lift_set i A)) = (F \<in> transient A)"
by (simp add: lift_def lift_set_def rename_transient)
lemma lift_ensures:
- "(lift i F : (lift_set i A) ensures (lift_set i B)) =
- (F : A ensures B)"
+ "(lift i F \<in> (lift_set i A) ensures (lift_set i B)) =
+ (F \<in> A ensures B)"
by (simp add: lift_def lift_set_def rename_ensures)
lemma lift_leadsTo:
- "(lift i F : (lift_set i A) leadsTo (lift_set i B)) =
- (F : A leadsTo B)"
+ "(lift i F \<in> (lift_set i A) leadsTo (lift_set i B)) =
+ (F \<in> A leadsTo B)"
by (simp add: lift_def lift_set_def rename_leadsTo)
lemma lift_LeadsTo:
- "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) =
- (F : A LeadsTo B)"
+ "(lift i F \<in> (lift_set i A) LeadsTo (lift_set i B)) =
+ (F \<in> A LeadsTo B)"
by (simp add: lift_def lift_set_def rename_LeadsTo)
(** guarantees **)
lemma lift_lift_guarantees_eq:
- "(lift i F : (lift i ` X) guarantees (lift i ` Y)) =
- (F : X guarantees Y)"
+ "(lift i F \<in> (lift i ` X) guarantees (lift i ` Y)) =
+ (F \<in> X guarantees Y)"
apply (unfold lift_def)
apply (subst bij_lift_map [THEN rename_rename_guarantees_eq, symmetric])
apply (simp add: o_def)
done
-lemma lift_guarantees_eq_lift_inv: "(lift i F : X guarantees Y) =
- (F : (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
+lemma lift_guarantees_eq_lift_inv: "(lift i F \<in> X guarantees Y) =
+ (F \<in> (rename (drop_map i) ` X) guarantees (rename (drop_map i) ` Y))"
by (simp add: bij_lift_map [THEN rename_guarantees_eq_rename_inv] lift_def)
@@ -236,14 +236,14 @@
(*To preserve snd means that the second component is there just to allow
guarantees properties to be stated. Converse fails, for lift i F can
change function components other than i*)
-lemma lift_preserves_snd_I: "F : preserves snd ==> lift i F : preserves snd"
+lemma lift_preserves_snd_I: "F \<in> preserves snd ==> lift i F \<in> preserves snd"
apply (drule_tac w1=snd in subset_preserves_o [THEN subsetD])
apply (simp add: lift_def rename_preserves)
apply (simp add: lift_map_def o_def split_def)
done
lemma delete_map_eqE':
- "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)"
+ "(delete_map i g) = (delete_map i g') ==> \<exists>x. g = g'(i:=x)"
apply (drule_tac f = "insert_map i (g i) " in arg_cong)
apply (simp add: insert_map_delete_map_eq)
apply (erule exI)
@@ -252,7 +252,7 @@
lemmas delete_map_eqE = delete_map_eqE' [THEN exE, elim!]
lemma delete_map_neq_apply:
- "[| delete_map j g = delete_map j g'; i~=j |] ==> g i = g' i"
+ "[| delete_map j g = delete_map j g'; i\<noteq>j |] ==> g i = g' i"
by force
(*A set of the form (A <*> UNIV) ignores the second (dummy) state component*)
@@ -265,27 +265,27 @@
by auto
lemma mem_lift_act_iff [iff]:
- "((s,s') : extend_act (%(x,u::unit). lift_map i x) act) =
- ((drop_map i s, drop_map i s') : act)"
+ "((s,s') \<in> extend_act (%(x,u::unit). lift_map i x) act) =
+ ((drop_map i s, drop_map i s') \<in> act)"
apply (unfold extend_act_def, auto)
apply (rule bexI, auto)
done
lemma preserves_snd_lift_stable:
- "[| F : preserves snd; i~=j |]
- ==> lift j F : stable (lift_set i (A <*> UNIV))"
+ "[| F \<in> preserves snd; i\<noteq>j |]
+ ==> lift j F \<in> stable (lift_set i (A <*> UNIV))"
apply (auto simp add: lift_def lift_set_def stable_def constrains_def
rename_def extend_def mem_rename_set_iff)
apply (auto dest!: preserves_imp_eq simp add: lift_map_def drop_map_def)
apply (drule_tac x = i in fun_cong, auto)
done
-(*If i~=j then lift j F does nothing to lift_set i, and the
- premise ensures A<=B.*)
+(*If i\<noteq>j then lift j F does nothing to lift_set i, and the
+ premise ensures A \<subseteq> B.*)
lemma constrains_imp_lift_constrains:
- "[| F i : (A <*> UNIV) co (B <*> UNIV);
- F j : preserves snd |]
- ==> lift j (F j) : (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
+ "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);
+ F j \<in> preserves snd |]
+ ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
apply (case_tac "i=j")
apply (simp add: lift_def lift_set_def rename_constrains)
apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
@@ -309,24 +309,24 @@
done
lemma insert_map_eq_diff:
- "[| insert_map i s f = insert_map j t g; i~=j |]
- ==> EX g'. insert_map i s' f = insert_map j t g'"
+ "[| insert_map i s f = insert_map j t g; i\<noteq>j |]
+ ==> \<exists>g'. insert_map i s' f = insert_map j t g'"
apply (subst insert_map_upd_same [symmetric])
apply (erule ssubst)
apply (simp only: insert_map_upd if_False split: split_if, blast)
done
lemma lift_map_eq_diff:
- "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i~=j |]
- ==> EX g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
+ "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i\<noteq>j |]
+ ==> \<exists>g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"
apply (unfold lift_map_def, auto)
apply (blast dest: insert_map_eq_diff)
done
lemma lift_transient_eq_disj:
- "F : preserves snd
- ==> (lift i F : transient (lift_set j (A <*> UNIV))) =
- (i=j & F : transient (A <*> UNIV) | A={})"
+ "F \<in> preserves snd
+ ==> (lift i F \<in> transient (lift_set j (A <*> UNIV))) =
+ (i=j & F \<in> transient (A <*> UNIV) | A={})"
apply (case_tac "i=j")
apply (auto simp add: lift_transient)
apply (auto simp add: lift_set_def lift_def transient_def rename_def
@@ -346,21 +346,21 @@
(*USELESS??*)
lemma lift_map_image_Times: "lift_map i ` (A <*> UNIV) =
- (UN s:A. UN f. {insert_map i s f}) <*> UNIV"
+ (\<Union>s \<in> A. \<Union>f. {insert_map i s f}) <*> UNIV"
apply (auto intro!: bexI image_eqI simp add: lift_map_def)
apply (rule split_conv [symmetric])
done
lemma lift_preserves_eq:
- "(lift i F : preserves v) = (F : preserves (v o lift_map i))"
+ "(lift i F \<in> preserves v) = (F \<in> preserves (v o lift_map i))"
by (simp add: lift_def rename_preserves)
(*A useful rewrite. If o, sub have been rewritten out already then can also
use it as rewrite_rule [sub_def, o_def] lift_preserves_sub*)
lemma lift_preserves_sub:
- "F : preserves snd
- ==> lift i F : preserves (v o sub j o fst) =
- (if i=j then F : preserves (v o fst) else True)"
+ "F \<in> preserves snd
+ ==> lift i F \<in> preserves (v o sub j o fst) =
+ (if i=j then F \<in> preserves (v o fst) else True)"
apply (drule subset_preserves_o [THEN subsetD])
apply (simp add: lift_preserves_eq o_def drop_map_lift_map_eq)
apply (auto cong del: if_weak_cong
@@ -374,7 +374,7 @@
lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
by (simp add: expand_fun_eq o_def)
-lemma o_equiv_apply: "f o g = h ==> ALL x. f(g x) = h x"
+lemma o_equiv_apply: "f o g = h ==> \<forall>x. f(g x) = h x"
by (simp add: expand_fun_eq o_def)
lemma fst_o_lift_map: "sub i o fst o lift_map i = fst"
@@ -402,7 +402,7 @@
lemma project_act_extend_act:
"project_act h (extend_act h' act) =
- {(x,x'). EX s s' y y' z. (s,s') : act &
+ {(x,x'). \<exists>s s' y y' z. (s,s') \<in> act &
h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}"
by (simp add: extend_act_def project_act_def, blast)
@@ -410,24 +410,24 @@
(*** OK and "lift" ***)
lemma act_in_UNION_preserves_fst:
- "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts"
+ "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"
apply (rule_tac a = "mk_program (UNIV,{act},UNIV) " in UN_I)
apply (auto simp add: preserves_def stable_def constrains_def)
done
lemma UNION_OK_lift_I:
- "[| ALL i:I. F i : preserves snd;
- ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |]
+ "[| \<forall>i \<in> I. F i \<in> preserves snd;
+ \<forall>i \<in> I. UNION (preserves fst) Acts \<subseteq> AllowedActs (F i) |]
==> OK I (%i. lift i (F i))"
apply (auto simp add: OK_def lift_def rename_def Extend.Acts_extend)
apply (simp add: Extend.AllowedActs_extend project_act_extend_act)
apply (rename_tac "act")
apply (subgoal_tac
"{(x, x'). \<exists>s f u s' f' u'.
- ((s, f, u), s', f', u') : act &
+ ((s, f, u), s', f', u') \<in> act &
lift_map j x = lift_map i (s, f, u) &
lift_map j x' = lift_map i (s', f', u') }
- <= { (x,x') . fst x = fst x'}")
+ \<subseteq> { (x,x') . fst x = fst x'}")
apply (blast intro: act_in_UNION_preserves_fst, clarify)
apply (drule_tac x = j in fun_cong)+
apply (drule_tac x = i in bspec, assumption)
@@ -435,8 +435,8 @@
done
lemma OK_lift_I:
- "[| ALL i:I. F i : preserves snd;
- ALL i:I. preserves fst <= Allowed (F i) |]
+ "[| \<forall>i \<in> I. F i \<in> preserves snd;
+ \<forall>i \<in> I. preserves fst \<subseteq> Allowed (F i) |]
==> OK I (%i. lift i (F i))"
by (simp add: safety_prop_AllowedActs_iff_Allowed UNION_OK_lift_I)
--- a/src/HOL/UNITY/PPROD.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/PPROD.thy Tue Feb 04 18:12:40 2003 +0100
@@ -15,19 +15,19 @@
PLam :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
=> ((nat=>'b) * 'c) program"
- "PLam I F == JN i:I. lift i (F i)"
+ "PLam I F == \<Squnion>i \<in> I. lift i (F i)"
syntax
"@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"
("(3plam _:_./ _)" 10)
translations
- "plam x:A. B" == "PLam A (%x. B)"
+ "plam x : A. B" == "PLam A (%x. B)"
(*** Basic properties ***)
-lemma Init_PLam: "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))"
+lemma Init_PLam: "Init (PLam I F) = (\<Inter>i \<in> I. lift_set i (Init (F i)))"
apply (simp (no_asm) add: PLam_def lift_def lift_set_def)
done
@@ -37,7 +37,7 @@
apply (simp (no_asm) add: PLam_def)
done
-lemma PLam_SKIP: "(plam i: I. SKIP) = SKIP"
+lemma PLam_SKIP: "(plam i : I. SKIP) = SKIP"
apply (simp (no_asm) add: PLam_def lift_SKIP JN_constant)
done
@@ -46,11 +46,11 @@
lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
by (unfold PLam_def, auto)
-lemma PLam_component_iff: "((PLam I F) <= H) = (ALL i: I. lift i (F i) <= H)"
+lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
apply (simp (no_asm) add: PLam_def JN_component_iff)
done
-lemma component_PLam: "i : I ==> lift i (F i) <= (PLam I F)"
+lemma component_PLam: "i \<in> I ==> lift i (F i) \<le> (PLam I F)"
apply (unfold PLam_def)
(*blast_tac doesn't use HO unification*)
apply (fast intro: component_JN)
@@ -60,10 +60,10 @@
(** Safety & Progress: but are they used anywhere? **)
lemma PLam_constrains:
- "[| i : I; ALL j. F j : preserves snd |] ==>
- (PLam I F : (lift_set i (A <*> UNIV)) co
+ "[| i \<in> I; \<forall>j. F j \<in> preserves snd |] ==>
+ (PLam I F \<in> (lift_set i (A <*> UNIV)) co
(lift_set i (B <*> UNIV))) =
- (F i : (A <*> UNIV) co (B <*> UNIV))"
+ (F i \<in> (A <*> UNIV) co (B <*> UNIV))"
apply (simp (no_asm_simp) add: PLam_def JN_constrains)
apply (subst insert_Diff [symmetric], assumption)
apply (simp (no_asm_simp) add: lift_constrains)
@@ -71,33 +71,33 @@
done
lemma PLam_stable:
- "[| i : I; ALL j. F j : preserves snd |]
- ==> (PLam I F : stable (lift_set i (A <*> UNIV))) =
- (F i : stable (A <*> UNIV))"
+ "[| i \<in> I; \<forall>j. F j \<in> preserves snd |]
+ ==> (PLam I F \<in> stable (lift_set i (A <*> UNIV))) =
+ (F i \<in> stable (A <*> UNIV))"
apply (simp (no_asm_simp) add: stable_def PLam_constrains)
done
lemma PLam_transient:
- "i : I ==>
- PLam I F : transient A = (EX i:I. lift i (F i) : transient A)"
+ "i \<in> I ==>
+ PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
apply (simp (no_asm_simp) add: JN_transient PLam_def)
done
(*This holds because the F j cannot change (lift_set i)*)
lemma PLam_ensures:
- "[| i : I; F i : (A <*> UNIV) ensures (B <*> UNIV);
- ALL j. F j : preserves snd |] ==>
- PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
+ "[| i \<in> I; F i \<in> (A <*> UNIV) ensures (B <*> UNIV);
+ \<forall>j. F j \<in> preserves snd |] ==>
+ PLam I F \<in> lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)"
apply (auto simp add: ensures_def PLam_constrains PLam_transient lift_transient_eq_disj lift_set_Un_distrib [symmetric] lift_set_Diff_distrib [symmetric] Times_Un_distrib1 [symmetric] Times_Diff_distrib1 [symmetric])
done
lemma PLam_leadsTo_Basis:
- "[| i : I;
- F i : ((A <*> UNIV) - (B <*> UNIV)) co
- ((A <*> UNIV) Un (B <*> UNIV));
- F i : transient ((A <*> UNIV) - (B <*> UNIV));
- ALL j. F j : preserves snd |] ==>
- PLam I F : lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
+ "[| i \<in> I;
+ F i \<in> ((A <*> UNIV) - (B <*> UNIV)) co
+ ((A <*> UNIV) \<union> (B <*> UNIV));
+ F i \<in> transient ((A <*> UNIV) - (B <*> UNIV));
+ \<forall>j. F j \<in> preserves snd |] ==>
+ PLam I F \<in> lift_set i (A <*> UNIV) leadsTo lift_set i (B <*> UNIV)"
by (rule PLam_ensures [THEN leadsTo_Basis], rule_tac [2] ensuresI)
@@ -105,20 +105,20 @@
(** invariant **)
lemma invariant_imp_PLam_invariant:
- "[| F i : invariant (A <*> UNIV); i : I;
- ALL j. F j : preserves snd |]
- ==> PLam I F : invariant (lift_set i (A <*> UNIV))"
+ "[| F i \<in> invariant (A <*> UNIV); i \<in> I;
+ \<forall>j. F j \<in> preserves snd |]
+ ==> PLam I F \<in> invariant (lift_set i (A <*> UNIV))"
by (auto simp add: PLam_stable invariant_def)
lemma PLam_preserves_fst [simp]:
- "ALL j. F j : preserves snd
- ==> (PLam I F : preserves (v o sub j o fst)) =
- (if j: I then F j : preserves (v o fst) else True)"
+ "\<forall>j. F j \<in> preserves snd
+ ==> (PLam I F \<in> preserves (v o sub j o fst)) =
+ (if j \<in> I then F j \<in> preserves (v o fst) else True)"
by (simp (no_asm_simp) add: PLam_def lift_preserves_sub)
lemma PLam_preserves_snd [simp,intro]:
- "ALL j. F j : preserves snd ==> PLam I F : preserves snd"
+ "\<forall>j. F j \<in> preserves snd ==> PLam I F \<in> preserves snd"
by (simp (no_asm_simp) add: PLam_def lift_preserves_snd_I)
@@ -130,44 +130,44 @@
something like lift_preserves_sub to rewrite the third. However there's
no obvious way to alternative for the third premise.*)
lemma guarantees_PLam_I:
- "[| lift i (F i): X guarantees Y; i : I;
+ "[| lift i (F i): X guarantees Y; i \<in> I;
OK I (%i. lift i (F i)) |]
- ==> (PLam I F) : X guarantees Y"
+ ==> (PLam I F) \<in> X guarantees Y"
apply (unfold PLam_def)
apply (simp (no_asm_simp) add: guarantees_JN_I)
done
lemma Allowed_PLam [simp]:
- "Allowed (PLam I F) = (INT i:I. lift i ` Allowed(F i))"
+ "Allowed (PLam I F) = (\<Inter>i \<in> I. lift i ` Allowed(F i))"
by (simp (no_asm) add: PLam_def)
lemma PLam_preserves [simp]:
- "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))"
-by (simp (no_asm) add: PLam_def lift_def rename_preserves)
+ "(PLam I F) \<in> preserves v = (\<forall>i \<in> I. F i \<in> preserves (v o lift_map i))"
+by (simp add: PLam_def lift_def rename_preserves)
(**UNUSED
(*The f0 premise ensures that the product is well-defined.*)
lemma PLam_invariant_imp_invariant:
- "[| PLam I F : invariant (lift_set i A); i : I;
- f0: Init (PLam I F) |] ==> F i : invariant A"
+ "[| PLam I F \<in> invariant (lift_set i A); i \<in> I;
+ f0: Init (PLam I F) |] ==> F i \<in> invariant A"
apply (auto simp add: invariant_def)
apply (drule_tac c = "f0 (i:=x) " in subsetD)
apply auto
done
lemma PLam_invariant:
- "[| i : I; f0: Init (PLam I F) |]
- ==> (PLam I F : invariant (lift_set i A)) = (F i : invariant A)"
+ "[| i \<in> I; f0: Init (PLam I F) |]
+ ==> (PLam I F \<in> invariant (lift_set i A)) = (F i \<in> invariant A)"
apply (blast intro: invariant_imp_PLam_invariant PLam_invariant_imp_invariant)
done
(*The f0 premise isn't needed if F is a constant program because then
we get an initial state by replicating that of F*)
lemma reachable_PLam:
- "i : I
- ==> ((plam x:I. F) : invariant (lift_set i A)) = (F : invariant A)"
+ "i \<in> I
+ ==> ((plam x \<in> I. F) \<in> invariant (lift_set i A)) = (F \<in> invariant A)"
apply (auto simp add: invariant_def)
done
**)
@@ -176,25 +176,25 @@
(**UNUSED
(** Reachability **)
- Goal "[| f : reachable (PLam I F); i : I |] ==> f i : reachable (F i)"
+ Goal "[| f \<in> reachable (PLam I F); i \<in> I |] ==> f i \<in> reachable (F i)"
apply (erule reachable.induct)
apply (auto intro: reachable.intrs)
done
(*Result to justify a re-organization of this file*)
- lemma "{f. ALL i:I. f i : R i} = (INT i:I. lift_set i (R i))"
+ lemma "{f. \<forall>i \<in> I. f i \<in> R i} = (\<Inter>i \<in> I. lift_set i (R i))"
by auto
lemma reachable_PLam_subset1:
- "reachable (PLam I F) <= (INT i:I. lift_set i (reachable (F i)))"
+ "reachable (PLam I F) \<subseteq> (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
apply (force dest!: reachable_PLam)
done
(*simplify using reachable_lift??*)
lemma reachable_lift_Join_PLam [rule_format]:
- "[| i ~: I; A : reachable (F i) |]
- ==> ALL f. f : reachable (PLam I F)
- --> f(i:=A) : reachable (lift i (F i) Join PLam I F)"
+ "[| i \<notin> I; A \<in> reachable (F i) |]
+ ==> \<forall>f. f \<in> reachable (PLam I F)
+ --> f(i:=A) \<in> reachable (lift i (F i) Join PLam I F)"
apply (erule reachable.induct)
apply (ALLGOALS Clarify_tac)
apply (erule reachable.induct)
@@ -224,7 +224,7 @@
perform actions, and PLam can never catch up in finite time.*)
lemma reachable_PLam_subset2:
"finite I
- ==> (INT i:I. lift_set i (reachable (F i))) <= reachable (PLam I F)"
+ ==> (\<Inter>i \<in> I. lift_set i (reachable (F i))) \<subseteq> reachable (PLam I F)"
apply (erule finite_induct)
apply (simp (no_asm))
apply (force dest: reachable_lift_Join_PLam simp add: PLam_insert)
@@ -232,7 +232,7 @@
lemma reachable_PLam_eq:
"finite I ==>
- reachable (PLam I F) = (INT i:I. lift_set i (reachable (F i)))"
+ reachable (PLam I F) = (\<Inter>i \<in> I. lift_set i (reachable (F i)))"
apply (REPEAT_FIRST (ares_tac [equalityI, reachable_PLam_subset1, reachable_PLam_subset2]))
done
@@ -240,8 +240,8 @@
(** Co **)
lemma Constrains_imp_PLam_Constrains:
- "[| F i : A Co B; i: I; finite I |]
- ==> PLam I F : (lift_set i A) Co (lift_set i B)"
+ "[| F i \<in> A Co B; i \<in> I; finite I |]
+ ==> PLam I F \<in> (lift_set i A) Co (lift_set i B)"
apply (auto simp add: Constrains_def Collect_conj_eq [symmetric] reachable_PLam_eq)
apply (auto simp add: constrains_def PLam_def)
apply (REPEAT (blast intro: reachable.intrs))
@@ -250,15 +250,15 @@
lemma PLam_Constrains:
- "[| i: I; finite I; f0: Init (PLam I F) |]
- ==> (PLam I F : (lift_set i A) Co (lift_set i B)) =
- (F i : A Co B)"
+ "[| i \<in> I; finite I; f0: Init (PLam I F) |]
+ ==> (PLam I F \<in> (lift_set i A) Co (lift_set i B)) =
+ (F i \<in> A Co B)"
apply (blast intro: Constrains_imp_PLam_Constrains PLam_Constrains_imp_Constrains)
done
lemma PLam_Stable:
- "[| i: I; finite I; f0: Init (PLam I F) |]
- ==> (PLam I F : Stable (lift_set i A)) = (F i : Stable A)"
+ "[| i \<in> I; finite I; f0: Init (PLam I F) |]
+ ==> (PLam I F \<in> Stable (lift_set i A)) = (F i \<in> Stable A)"
apply (simp (no_asm_simp) del: Init_PLam add: Stable_def PLam_Constrains)
done
@@ -266,23 +266,23 @@
(** const_PLam (no dependence on i) doesn't require the f0 premise **)
lemma const_PLam_Constrains:
- "[| i: I; finite I |]
- ==> ((plam x:I. F) : (lift_set i A) Co (lift_set i B)) =
- (F : A Co B)"
+ "[| i \<in> I; finite I |]
+ ==> ((plam x \<in> I. F) \<in> (lift_set i A) Co (lift_set i B)) =
+ (F \<in> A Co B)"
apply (blast intro: Constrains_imp_PLam_Constrains const_PLam_Constrains_imp_Constrains)
done
lemma const_PLam_Stable:
- "[| i: I; finite I |]
- ==> ((plam x:I. F) : Stable (lift_set i A)) = (F : Stable A)"
+ "[| i \<in> I; finite I |]
+ ==> ((plam x \<in> I. F) \<in> Stable (lift_set i A)) = (F \<in> Stable A)"
apply (simp (no_asm_simp) add: Stable_def const_PLam_Constrains)
done
lemma const_PLam_Increasing:
- "[| i: I; finite I |]
- ==> ((plam x:I. F) : Increasing (f o sub i)) = (F : Increasing f)"
+ "[| i \<in> I; finite I |]
+ ==> ((plam x \<in> I. F) \<in> Increasing (f o sub i)) = (F \<in> Increasing f)"
apply (unfold Increasing_def)
- apply (subgoal_tac "ALL z. {s. z <= (f o sub i) s} = lift_set i {s. z <= f s}")
+ apply (subgoal_tac "\<forall>z. {s. z \<subseteq> (f o sub i) s} = lift_set i {s. z \<subseteq> f s}")
apply (asm_simp_tac (simpset () add: lift_set_sub) 2)
apply (simp add: finite_lessThan const_PLam_Stable)
done
--- a/src/HOL/UNITY/Rename.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Rename.thy Tue Feb 04 18:12:40 2003 +0100
@@ -31,7 +31,7 @@
apply (erule surj_f_inv_f)
done
-lemma mem_rename_set_iff: "bij h ==> z : h`A = (inv h z : A)"
+lemma mem_rename_set_iff: "bij h ==> z \<in> h`A = (inv h z \<in> A)"
by (force simp add: bij_is_inj bij_is_surj [THEN surj_f_inv_f])
@@ -176,31 +176,31 @@
by (simp add: rename_def Extend.extend_Join)
lemma rename_JN [simp]:
- "bij h ==> rename h (JOIN I F) = (JN i:I. rename h (F i))"
+ "bij h ==> rename h (JOIN I F) = (\<Squnion>i \<in> I. rename h (F i))"
by (simp add: rename_def Extend.extend_JN)
subsection{*Strong Safety: co, stable*}
lemma rename_constrains:
- "bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)"
+ "bij h ==> (rename h F \<in> (h`A) co (h`B)) = (F \<in> A co B)"
apply (unfold rename_def)
apply (subst extend_set_eq_image [symmetric])+
apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_constrains])
done
lemma rename_stable:
- "bij h ==> (rename h F : stable (h`A)) = (F : stable A)"
+ "bij h ==> (rename h F \<in> stable (h`A)) = (F \<in> stable A)"
apply (simp add: stable_def rename_constrains)
done
lemma rename_invariant:
- "bij h ==> (rename h F : invariant (h`A)) = (F : invariant A)"
+ "bij h ==> (rename h F \<in> invariant (h`A)) = (F \<in> invariant A)"
apply (simp add: invariant_def rename_stable bij_is_inj [THEN inj_image_subset_iff])
done
lemma rename_increasing:
- "bij h ==> (rename h F : increasing func) = (F : increasing (func o h))"
+ "bij h ==> (rename h F \<in> increasing func) = (F \<in> increasing (func o h))"
apply (simp add: increasing_def rename_stable [symmetric] bij_image_Collect_eq bij_is_surj [THEN surj_f_inv_f])
done
@@ -213,19 +213,19 @@
done
lemma rename_Constrains:
- "bij h ==> (rename h F : (h`A) Co (h`B)) = (F : A Co B)"
+ "bij h ==> (rename h F \<in> (h`A) Co (h`B)) = (F \<in> A Co B)"
by (simp add: Constrains_def reachable_rename_eq rename_constrains
bij_is_inj image_Int [symmetric])
lemma rename_Stable:
- "bij h ==> (rename h F : Stable (h`A)) = (F : Stable A)"
+ "bij h ==> (rename h F \<in> Stable (h`A)) = (F \<in> Stable A)"
by (simp add: Stable_def rename_Constrains)
-lemma rename_Always: "bij h ==> (rename h F : Always (h`A)) = (F : Always A)"
+lemma rename_Always: "bij h ==> (rename h F \<in> Always (h`A)) = (F \<in> Always A)"
by (simp add: Always_def rename_Stable bij_is_inj [THEN inj_image_subset_iff])
lemma rename_Increasing:
- "bij h ==> (rename h F : Increasing func) = (F : Increasing (func o h))"
+ "bij h ==> (rename h F \<in> Increasing func) = (F \<in> Increasing (func o h))"
by (simp add: Increasing_def rename_Stable [symmetric] bij_image_Collect_eq
bij_is_surj [THEN surj_f_inv_f])
@@ -233,52 +233,52 @@
subsection{*Progress: transient, ensures*}
lemma rename_transient:
- "bij h ==> (rename h F : transient (h`A)) = (F : transient A)"
+ "bij h ==> (rename h F \<in> transient (h`A)) = (F \<in> transient A)"
apply (unfold rename_def)
apply (subst extend_set_eq_image [symmetric])
apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_transient])
done
lemma rename_ensures:
- "bij h ==> (rename h F : (h`A) ensures (h`B)) = (F : A ensures B)"
+ "bij h ==> (rename h F \<in> (h`A) ensures (h`B)) = (F \<in> A ensures B)"
apply (unfold rename_def)
apply (subst extend_set_eq_image [symmetric])+
apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_ensures])
done
lemma rename_leadsTo:
- "bij h ==> (rename h F : (h`A) leadsTo (h`B)) = (F : A leadsTo B)"
+ "bij h ==> (rename h F \<in> (h`A) leadsTo (h`B)) = (F \<in> A leadsTo B)"
apply (unfold rename_def)
apply (subst extend_set_eq_image [symmetric])+
apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_leadsTo])
done
lemma rename_LeadsTo:
- "bij h ==> (rename h F : (h`A) LeadsTo (h`B)) = (F : A LeadsTo B)"
+ "bij h ==> (rename h F \<in> (h`A) LeadsTo (h`B)) = (F \<in> A LeadsTo B)"
apply (unfold rename_def)
apply (subst extend_set_eq_image [symmetric])+
apply (erule good_map_bij [THEN Extend.intro, THEN Extend.extend_LeadsTo])
done
lemma rename_rename_guarantees_eq:
- "bij h ==> (rename h F : (rename h ` X) guarantees
+ "bij h ==> (rename h F \<in> (rename h ` X) guarantees
(rename h ` Y)) =
- (F : X guarantees Y)"
+ (F \<in> X guarantees Y)"
apply (unfold rename_def)
apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_guarantees_eq [symmetric]], assumption)
apply (simp (no_asm_simp) add: fst_o_inv_eq_inv o_def)
done
lemma rename_guarantees_eq_rename_inv:
- "bij h ==> (rename h F : X guarantees Y) =
- (F : (rename (inv h) ` X) guarantees
+ "bij h ==> (rename h F \<in> X guarantees Y) =
+ (F \<in> (rename (inv h) ` X) guarantees
(rename (inv h) ` Y))"
apply (subst rename_rename_guarantees_eq [symmetric], assumption)
apply (simp add: image_eq_UN o_def bij_is_surj [THEN surj_f_inv_f])
done
lemma rename_preserves:
- "bij h ==> (rename h G : preserves v) = (G : preserves (v o h))"
+ "bij h ==> (rename h G \<in> preserves v) = (G \<in> preserves (v o h))"
apply (subst good_map_bij [THEN Extend.intro, THEN Extend.extend_preserves [symmetric]], assumption)
apply (simp add: o_def fst_o_inv_eq_inv rename_def bij_is_surj [THEN surj_f_inv_f])
done
--- a/src/HOL/UNITY/SubstAx.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Tue Feb 04 18:12:40 2003 +0100
@@ -12,10 +12,10 @@
constdefs
Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60)
- "A Ensures B == {F. F : (reachable F Int A) ensures B}"
+ "A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}"
LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60)
- "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
+ "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
syntax (xsymbols)
"op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60)
@@ -23,7 +23,7 @@
(*Resembles the previous definition of LeadsTo*)
lemma LeadsTo_eq_leadsTo:
- "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}"
+ "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}"
apply (unfold LeadsTo_def)
apply (blast dest: psp_stable2 intro: leadsTo_weaken)
done
@@ -34,35 +34,37 @@
(** Conjoining an Always property **)
lemma Always_LeadsTo_pre:
- "F : Always INV ==> (F : (INV Int A) LeadsTo A') = (F : A LeadsTo A')"
-by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric])
+ "F \<in> Always INV ==> (F \<in> (INV \<inter> A) LeadsTo A') = (F \<in> A LeadsTo A')"
+by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2
+ Int_assoc [symmetric])
lemma Always_LeadsTo_post:
- "F : Always INV ==> (F : A LeadsTo (INV Int A')) = (F : A LeadsTo A')"
-by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric])
+ "F \<in> Always INV ==> (F \<in> A LeadsTo (INV \<inter> A')) = (F \<in> A LeadsTo A')"
+by (simp add: LeadsTo_eq_leadsTo Always_eq_includes_reachable Int_absorb2
+ Int_assoc [symmetric])
-(* [| F : Always C; F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
+(* [| F \<in> Always C; F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A' *)
lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard]
-(* [| F : Always INV; F : A LeadsTo A' |] ==> F : A LeadsTo (INV Int A') *)
+(* [| F \<in> Always INV; F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (INV \<inter> A') *)
lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
subsection{*Introduction rules: Basis, Trans, Union*}
-lemma leadsTo_imp_LeadsTo: "F : A leadsTo B ==> F : A LeadsTo B"
+lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"
apply (simp add: LeadsTo_def)
apply (blast intro: leadsTo_weaken_L)
done
lemma LeadsTo_Trans:
- "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C"
+ "[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C"
apply (simp add: LeadsTo_eq_leadsTo)
apply (blast intro: leadsTo_Trans)
done
lemma LeadsTo_Union:
- "(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B"
+ "(!!A. A \<in> S ==> F \<in> A LeadsTo B) ==> F \<in> (Union S) LeadsTo B"
apply (simp add: LeadsTo_def)
apply (subst Int_Union)
apply (blast intro: leadsTo_UN)
@@ -71,37 +73,37 @@
subsection{*Derived rules*}
-lemma LeadsTo_UNIV [simp]: "F : A LeadsTo UNIV"
+lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV"
by (simp add: LeadsTo_def)
(*Useful with cancellation, disjunction*)
lemma LeadsTo_Un_duplicate:
- "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'"
+ "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'"
by (simp add: Un_ac)
lemma LeadsTo_Un_duplicate2:
- "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)"
+ "F \<in> A LeadsTo (A' \<union> C \<union> C) ==> F \<in> A LeadsTo (A' \<union> C)"
by (simp add: Un_ac)
lemma LeadsTo_UN:
- "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B"
+ "(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B"
apply (simp only: Union_image_eq [symmetric])
apply (blast intro: LeadsTo_Union)
done
(*Binary union introduction rule*)
lemma LeadsTo_Un:
- "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C"
+ "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
apply (subst Un_eq_Union)
apply (blast intro: LeadsTo_Union)
done
(*Lets us look at the starting state*)
lemma single_LeadsTo_I:
- "(!!s. s : A ==> F : {s} LeadsTo B) ==> F : A LeadsTo B"
+ "(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B"
by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
-lemma subset_imp_LeadsTo: "A <= B ==> F : A LeadsTo B"
+lemma subset_imp_LeadsTo: "A \<subseteq> B ==> F \<in> A LeadsTo B"
apply (simp add: LeadsTo_def)
apply (blast intro: subset_imp_leadsTo)
done
@@ -109,73 +111,73 @@
lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
lemma LeadsTo_weaken_R [rule_format]:
- "[| F : A LeadsTo A'; A' <= B' |] ==> F : A LeadsTo B'"
-apply (simp (no_asm_use) add: LeadsTo_def)
+ "[| F \<in> A LeadsTo A'; A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'"
+apply (simp add: LeadsTo_def)
apply (blast intro: leadsTo_weaken_R)
done
lemma LeadsTo_weaken_L [rule_format]:
- "[| F : A LeadsTo A'; B <= A |]
- ==> F : B LeadsTo A'"
-apply (simp (no_asm_use) add: LeadsTo_def)
+ "[| F \<in> A LeadsTo A'; B \<subseteq> A |]
+ ==> F \<in> B LeadsTo A'"
+apply (simp add: LeadsTo_def)
apply (blast intro: leadsTo_weaken_L)
done
lemma LeadsTo_weaken:
- "[| F : A LeadsTo A';
- B <= A; A' <= B' |]
- ==> F : B LeadsTo B'"
+ "[| F \<in> A LeadsTo A';
+ B \<subseteq> A; A' \<subseteq> B' |]
+ ==> F \<in> B LeadsTo B'"
by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
lemma Always_LeadsTo_weaken:
- "[| F : Always C; F : A LeadsTo A';
- C Int B <= A; C Int A' <= B' |]
- ==> F : B LeadsTo B'"
+ "[| F \<in> Always C; F \<in> A LeadsTo A';
+ C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |]
+ ==> F \<in> B LeadsTo B'"
by (blast dest: Always_LeadsToI intro: LeadsTo_weaken intro: Always_LeadsToD)
(** Two theorems for "proof lattices" **)
-lemma LeadsTo_Un_post: "F : A LeadsTo B ==> F : (A Un B) LeadsTo B"
+lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F \<in> (A \<union> B) LeadsTo B"
by (blast intro: LeadsTo_Un subset_imp_LeadsTo)
lemma LeadsTo_Trans_Un:
- "[| F : A LeadsTo B; F : B LeadsTo C |]
- ==> F : (A Un B) LeadsTo C"
+ "[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |]
+ ==> F \<in> (A \<union> B) LeadsTo C"
by (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans)
(** Distributive laws **)
lemma LeadsTo_Un_distrib:
- "(F : (A Un B) LeadsTo C) = (F : A LeadsTo C & F : B LeadsTo C)"
+ "(F \<in> (A \<union> B) LeadsTo C) = (F \<in> A LeadsTo C & F \<in> B LeadsTo C)"
by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
lemma LeadsTo_UN_distrib:
- "(F : (UN i:I. A i) LeadsTo B) = (ALL i : I. F : (A i) LeadsTo B)"
+ "(F \<in> (\<Union>i \<in> I. A i) LeadsTo B) = (\<forall>i \<in> I. F \<in> (A i) LeadsTo B)"
by (blast intro: LeadsTo_UN LeadsTo_weaken_L)
lemma LeadsTo_Union_distrib:
- "(F : (Union S) LeadsTo B) = (ALL A : S. F : A LeadsTo B)"
+ "(F \<in> (Union S) LeadsTo B) = (\<forall>A \<in> S. F \<in> A LeadsTo B)"
by (blast intro: LeadsTo_Union LeadsTo_weaken_L)
(** More rules using the premise "Always INV" **)
-lemma LeadsTo_Basis: "F : A Ensures B ==> F : A LeadsTo B"
+lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B"
by (simp add: Ensures_def LeadsTo_def leadsTo_Basis)
lemma EnsuresI:
- "[| F : (A-B) Co (A Un B); F : transient (A-B) |]
- ==> F : A Ensures B"
+ "[| F \<in> (A-B) Co (A \<union> B); F \<in> transient (A-B) |]
+ ==> F \<in> A Ensures B"
apply (simp add: Ensures_def Constrains_eq_constrains)
apply (blast intro: ensuresI constrains_weaken transient_strengthen)
done
lemma Always_LeadsTo_Basis:
- "[| F : Always INV;
- F : (INV Int (A-A')) Co (A Un A');
- F : transient (INV Int (A-A')) |]
- ==> F : A LeadsTo A'"
+ "[| F \<in> Always INV;
+ F \<in> (INV \<inter> (A-A')) Co (A \<union> A');
+ F \<in> transient (INV \<inter> (A-A')) |]
+ ==> F \<in> A LeadsTo A'"
apply (rule Always_LeadsToI, assumption)
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
done
@@ -183,14 +185,14 @@
(*Set difference: maybe combine with leadsTo_weaken_L??
This is the most useful form of the "disjunction" rule*)
lemma LeadsTo_Diff:
- "[| F : (A-B) LeadsTo C; F : (A Int B) LeadsTo C |]
- ==> F : A LeadsTo C"
+ "[| F \<in> (A-B) LeadsTo C; F \<in> (A \<inter> B) LeadsTo C |]
+ ==> F \<in> A LeadsTo C"
by (blast intro: LeadsTo_Un LeadsTo_weaken)
lemma LeadsTo_UN_UN:
- "(!! i. i:I ==> F : (A i) LeadsTo (A' i))
- ==> F : (UN i:I. A i) LeadsTo (UN i:I. A' i)"
+ "(!! i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i))
+ ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo (\<Union>i \<in> I. A' i)"
apply (simp only: Union_image_eq [symmetric])
apply (blast intro: LeadsTo_Union LeadsTo_weaken_R)
done
@@ -198,48 +200,47 @@
(*Version with no index set*)
lemma LeadsTo_UN_UN_noindex:
- "(!! i. F : (A i) LeadsTo (A' i))
- ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
+ "(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
by (blast intro: LeadsTo_UN_UN)
(*Version with no index set*)
lemma all_LeadsTo_UN_UN:
- "ALL i. F : (A i) LeadsTo (A' i)
- ==> F : (UN i. A i) LeadsTo (UN i. A' i)"
+ "\<forall>i. F \<in> (A i) LeadsTo (A' i)
+ ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
by (blast intro: LeadsTo_UN_UN)
(*Binary union version*)
lemma LeadsTo_Un_Un:
- "[| F : A LeadsTo A'; F : B LeadsTo B' |]
- ==> F : (A Un B) LeadsTo (A' Un B')"
+ "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |]
+ ==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')"
by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
(** The cancellation law **)
lemma LeadsTo_cancel2:
- "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |]
- ==> F : A LeadsTo (A' Un B')"
+ "[| F \<in> A LeadsTo (A' \<union> B); F \<in> B LeadsTo B' |]
+ ==> F \<in> A LeadsTo (A' \<union> B')"
by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans)
lemma LeadsTo_cancel_Diff2:
- "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |]
- ==> F : A LeadsTo (A' Un B')"
+ "[| F \<in> A LeadsTo (A' \<union> B); F \<in> (B-A') LeadsTo B' |]
+ ==> F \<in> A LeadsTo (A' \<union> B')"
apply (rule LeadsTo_cancel2)
prefer 2 apply assumption
apply (simp_all (no_asm_simp))
done
lemma LeadsTo_cancel1:
- "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |]
- ==> F : A LeadsTo (B' Un A')"
+ "[| F \<in> A LeadsTo (B \<union> A'); F \<in> B LeadsTo B' |]
+ ==> F \<in> A LeadsTo (B' \<union> A')"
apply (simp add: Un_commute)
apply (blast intro!: LeadsTo_cancel2)
done
lemma LeadsTo_cancel_Diff1:
- "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |]
- ==> F : A LeadsTo (B' Un A')"
+ "[| F \<in> A LeadsTo (B \<union> A'); F \<in> (B-A') LeadsTo B' |]
+ ==> F \<in> A LeadsTo (B' \<union> A')"
apply (rule LeadsTo_cancel1)
prefer 2 apply assumption
apply (simp_all (no_asm_simp))
@@ -249,8 +250,8 @@
(** The impossibility law **)
(*The set "A" may be non-empty, but it contains no reachable states*)
-lemma LeadsTo_empty: "F : A LeadsTo {} ==> F : Always (-A)"
-apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
+lemma LeadsTo_empty: "F \<in> A LeadsTo {} ==> F \<in> Always (-A)"
+apply (simp add: LeadsTo_def Always_eq_includes_reachable)
apply (drule leadsTo_empty, auto)
done
@@ -259,33 +260,33 @@
(*Special case of PSP: Misra's "stable conjunction"*)
lemma PSP_Stable:
- "[| F : A LeadsTo A'; F : Stable B |]
- ==> F : (A Int B) LeadsTo (A' Int B)"
-apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo Stable_eq_stable)
+ "[| F \<in> A LeadsTo A'; F \<in> Stable B |]
+ ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)"
+apply (simp add: LeadsTo_eq_leadsTo Stable_eq_stable)
apply (drule psp_stable, assumption)
apply (simp add: Int_ac)
done
lemma PSP_Stable2:
- "[| F : A LeadsTo A'; F : Stable B |]
- ==> F : (B Int A) LeadsTo (B Int A')"
+ "[| F \<in> A LeadsTo A'; F \<in> Stable B |]
+ ==> F \<in> (B \<inter> A) LeadsTo (B \<inter> A')"
by (simp add: PSP_Stable Int_ac)
lemma PSP:
- "[| F : A LeadsTo A'; F : B Co B' |]
- ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))"
-apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
+ "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]
+ ==> F \<in> (A \<inter> B') LeadsTo ((A' \<inter> B) \<union> (B' - B))"
+apply (simp add: LeadsTo_def Constrains_eq_constrains)
apply (blast dest: psp intro: leadsTo_weaken)
done
lemma PSP2:
- "[| F : A LeadsTo A'; F : B Co B' |]
- ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))"
+ "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]
+ ==> F \<in> (B' \<inter> A) LeadsTo ((B \<inter> A') \<union> (B' - B))"
by (simp add: PSP Int_ac)
lemma PSP_Unless:
- "[| F : A LeadsTo A'; F : B Unless B' |]
- ==> F : (A Int B) LeadsTo ((A' Int B) Un B')"
+ "[| F \<in> A LeadsTo A'; F \<in> B Unless B' |]
+ ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B) \<union> B')"
apply (unfold Unless_def)
apply (drule PSP, assumption)
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
@@ -293,8 +294,8 @@
lemma Stable_transient_Always_LeadsTo:
- "[| F : Stable A; F : transient C;
- F : Always (-A Un B Un C) |] ==> F : A LeadsTo B"
+ "[| F \<in> Stable A; F \<in> transient C;
+ F \<in> Always (-A \<union> B \<union> C) |] ==> F \<in> A LeadsTo B"
apply (erule Always_LeadsTo_weaken)
apply (rule LeadsTo_Diff)
prefer 2
@@ -309,10 +310,10 @@
(** Meta or object quantifier ????? **)
lemma LeadsTo_wf_induct:
"[| wf r;
- ALL m. F : (A Int f-`{m}) LeadsTo
- ((A Int f-`(r^-1 `` {m})) Un B) |]
- ==> F : A LeadsTo B"
-apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo)
+ \<forall>m. F \<in> (A \<inter> f-`{m}) LeadsTo
+ ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]
+ ==> F \<in> A LeadsTo B"
+apply (simp add: LeadsTo_eq_leadsTo)
apply (erule leadsTo_wf_induct)
apply (blast intro: leadsTo_weaken)
done
@@ -320,28 +321,27 @@
lemma Bounded_induct:
"[| wf r;
- ALL m:I. F : (A Int f-`{m}) LeadsTo
- ((A Int f-`(r^-1 `` {m})) Un B) |]
- ==> F : A LeadsTo ((A - (f-`I)) Un B)"
+ \<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) LeadsTo
+ ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]
+ ==> F \<in> A LeadsTo ((A - (f-`I)) \<union> B)"
apply (erule LeadsTo_wf_induct, safe)
-apply (case_tac "m:I")
+apply (case_tac "m \<in> I")
apply (blast intro: LeadsTo_weaken)
apply (blast intro: subset_imp_LeadsTo)
done
lemma LessThan_induct:
- "(!!m::nat. F : (A Int f-`{m}) LeadsTo ((A Int f-`(lessThan m)) Un B))
- ==> F : A LeadsTo B"
-apply (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
-done
+ "(!!m::nat. F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B))
+ ==> F \<in> A LeadsTo B"
+by (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
(*Integer version. Could generalize from 0 to any lower bound*)
lemma integ_0_le_induct:
- "[| F : Always {s. (0::int) <= f s};
- !! z. F : (A Int {s. f s = z}) LeadsTo
- ((A Int {s. f s < z}) Un B) |]
- ==> F : A LeadsTo B"
+ "[| F \<in> Always {s. (0::int) \<le> f s};
+ !! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo
+ ((A \<inter> {s. f s < z}) \<union> B) |]
+ ==> F \<in> A LeadsTo B"
apply (rule_tac f = "nat o f" in LessThan_induct)
apply (simp add: vimage_def)
apply (rule Always_LeadsTo_weaken, assumption+)
@@ -349,42 +349,42 @@
done
lemma LessThan_bounded_induct:
- "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-`{m}) LeadsTo
- ((A Int f-`(lessThan m)) Un B) |]
- ==> F : A LeadsTo ((A Int (f-`(atMost l))) Un B)"
-apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
-apply (rule wf_less_than [THEN Bounded_induct])
-apply (simp (no_asm_simp))
+ "!!l::nat. \<forall>m \<in> greaterThan l.
+ F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B)
+ ==> F \<in> A LeadsTo ((A \<inter> (f-`(atMost l))) \<union> B)"
+apply (simp only: Diff_eq [symmetric] vimage_Compl
+ Compl_greaterThan [symmetric])
+apply (rule wf_less_than [THEN Bounded_induct], simp)
done
lemma GreaterThan_bounded_induct:
- "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-`{m}) LeadsTo
- ((A Int f-`(greaterThan m)) Un B) |]
- ==> F : A LeadsTo ((A Int (f-`(atLeast l))) Un B)"
+ "!!l::nat. \<forall>m \<in> lessThan l.
+ F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(greaterThan m)) \<union> B)
+ ==> F \<in> A LeadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
apply (rule_tac f = f and f1 = "%k. l - k"
in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
apply (simp add: inv_image_def Image_singleton, clarify)
apply (case_tac "m<l")
- prefer 2 apply (blast intro: not_leE subset_imp_LeadsTo)
-apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
+ apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
+apply (blast intro: not_leE subset_imp_LeadsTo)
done
subsection{*Completion: Binary and General Finite versions*}
lemma Completion:
- "[| F : A LeadsTo (A' Un C); F : A' Co (A' Un C);
- F : B LeadsTo (B' Un C); F : B' Co (B' Un C) |]
- ==> F : (A Int B) LeadsTo ((A' Int B') Un C)"
-apply (simp (no_asm_use) add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib)
+ "[| F \<in> A LeadsTo (A' \<union> C); F \<in> A' Co (A' \<union> C);
+ F \<in> B LeadsTo (B' \<union> C); F \<in> B' Co (B' \<union> C) |]
+ ==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B') \<union> C)"
+apply (simp add: LeadsTo_eq_leadsTo Constrains_eq_constrains Int_Un_distrib)
apply (blast intro: completion leadsTo_weaken)
done
lemma Finite_completion_lemma:
"finite I
- ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) -->
- (ALL i:I. F : (A' i) Co (A' i Un C)) -->
- F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)"
+ ==> (\<forall>i \<in> I. F \<in> (A i) LeadsTo (A' i \<union> C)) -->
+ (\<forall>i \<in> I. F \<in> (A' i) Co (A' i \<union> C)) -->
+ F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
apply (erule finite_induct, auto)
apply (rule Completion)
prefer 4
@@ -394,15 +394,15 @@
lemma Finite_completion:
"[| finite I;
- !!i. i:I ==> F : (A i) LeadsTo (A' i Un C);
- !!i. i:I ==> F : (A' i) Co (A' i Un C) |]
- ==> F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)"
+ !!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i \<union> C);
+ !!i. i \<in> I ==> F \<in> (A' i) Co (A' i \<union> C) |]
+ ==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
by (blast intro: Finite_completion_lemma [THEN mp, THEN mp])
lemma Stable_completion:
- "[| F : A LeadsTo A'; F : Stable A';
- F : B LeadsTo B'; F : Stable B' |]
- ==> F : (A Int B) LeadsTo (A' Int B')"
+ "[| F \<in> A LeadsTo A'; F \<in> Stable A';
+ F \<in> B LeadsTo B'; F \<in> Stable B' |]
+ ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B')"
apply (unfold Stable_def)
apply (rule_tac C1 = "{}" in Completion [THEN LeadsTo_weaken_R])
apply (force+)
@@ -410,14 +410,12 @@
lemma Finite_stable_completion:
"[| finite I;
- !!i. i:I ==> F : (A i) LeadsTo (A' i);
- !!i. i:I ==> F : Stable (A' i) |]
- ==> F : (INT i:I. A i) LeadsTo (INT i:I. A' i)"
+ !!i. i \<in> I ==> F \<in> (A i) LeadsTo (A' i);
+ !!i. i \<in> I ==> F \<in> Stable (A' i) |]
+ ==> F \<in> (\<Inter>i \<in> I. A i) LeadsTo (\<Inter>i \<in> I. A' i)"
apply (unfold Stable_def)
apply (rule_tac C1 = "{}" in Finite_completion [THEN LeadsTo_weaken_R])
-apply (simp_all (no_asm_simp))
-apply blast+
+apply (simp_all, blast+)
done
-
end
--- a/src/HOL/UNITY/UNITY.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/UNITY.thy Tue Feb 04 18:12:40 2003 +0100
@@ -14,15 +14,15 @@
typedef (Program)
'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
- allowed :: ('a * 'a)set set). Id:acts & Id: allowed}"
+ allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}"
by blast
constdefs
constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60)
- "A co B == {F. ALL act: Acts F. act``A <= B}"
+ "A co B == {F. \<forall>act \<in> Acts F. act``A \<subseteq> B}"
unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60)
- "A unless B == (A-B) co (A Un B)"
+ "A unless B == (A-B) co (A \<union> B)"
mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
=> 'a program"
@@ -39,20 +39,20 @@
"AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
Allowed :: "'a program => 'a program set"
- "Allowed F == {G. Acts G <= AllowedActs F}"
+ "Allowed F == {G. Acts G \<subseteq> AllowedActs F}"
stable :: "'a set => 'a program set"
"stable A == A co A"
strongest_rhs :: "['a program, 'a set] => 'a set"
- "strongest_rhs F A == Inter {B. F : A co B}"
+ "strongest_rhs F A == Inter {B. F \<in> A co B}"
invariant :: "'a set => 'a program set"
- "invariant A == {F. Init F <= A} Int stable A"
+ "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
- (*Polymorphic in both states and the meaning of <= *)
+ (*Polymorphic in both states and the meaning of \<le> *)
increasing :: "['a => 'b::{order}] => 'a program set"
- "increasing f == INT z. stable {s. z <= f s}"
+ "increasing f == \<Inter>z. stable {s. z \<le> f s}"
(*Perhaps equalities.ML shouldn't add this in the first place!*)
@@ -64,7 +64,7 @@
Rep_Program Rep_Program_inverse Abs_Program_inverse
Program_def Init_def Acts_def AllowedActs_def mk_program_def
-lemma Id_in_Acts [iff]: "Id : Acts F"
+lemma Id_in_Acts [iff]: "Id \<in> Acts F"
apply (cut_tac x = F in Rep_Program)
apply (auto simp add: program_typedef)
done
@@ -72,7 +72,7 @@
lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
by (simp add: insert_absorb Id_in_Acts)
-lemma Id_in_AllowedActs [iff]: "Id : AllowedActs F"
+lemma Id_in_AllowedActs [iff]: "Id \<in> AllowedActs F"
apply (cut_tac x = F in Rep_Program)
apply (auto simp add: program_typedef)
done
@@ -145,114 +145,114 @@
(*An action is expanded only if a pair of states is being tested against it*)
lemma def_act_simp:
- "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"
+ "[| act == {(s,s'). P s s'} |] ==> ((s,s') \<in> act) = P s s'"
by auto
(*A set is expanded only if an element is being tested against it*)
-lemma def_set_simp: "A == B ==> (x : A) = (x : B)"
+lemma def_set_simp: "A == B ==> (x \<in> A) = (x \<in> B)"
by auto
(*** co ***)
lemma constrainsI:
- "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A')
- ==> F : A co A'"
+ "(!!act s s'. [| act: Acts F; (s,s') \<in> act; s \<in> A |] ==> s': A')
+ ==> F \<in> A co A'"
by (simp add: constrains_def, blast)
lemma constrainsD:
- "[| F : A co A'; act: Acts F; (s,s'): act; s: A |] ==> s': A'"
+ "[| F \<in> A co A'; act: Acts F; (s,s'): act; s \<in> A |] ==> s': A'"
by (unfold constrains_def, blast)
-lemma constrains_empty [iff]: "F : {} co B"
+lemma constrains_empty [iff]: "F \<in> {} co B"
by (unfold constrains_def, blast)
-lemma constrains_empty2 [iff]: "(F : A co {}) = (A={})"
+lemma constrains_empty2 [iff]: "(F \<in> A co {}) = (A={})"
by (unfold constrains_def, blast)
-lemma constrains_UNIV [iff]: "(F : UNIV co B) = (B = UNIV)"
+lemma constrains_UNIV [iff]: "(F \<in> UNIV co B) = (B = UNIV)"
by (unfold constrains_def, blast)
-lemma constrains_UNIV2 [iff]: "F : A co UNIV"
+lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
by (unfold constrains_def, blast)
(*monotonic in 2nd argument*)
lemma constrains_weaken_R:
- "[| F : A co A'; A'<=B' |] ==> F : A co B'"
+ "[| F \<in> A co A'; A'<=B' |] ==> F \<in> A co B'"
by (unfold constrains_def, blast)
(*anti-monotonic in 1st argument*)
lemma constrains_weaken_L:
- "[| F : A co A'; B<=A |] ==> F : B co A'"
+ "[| F \<in> A co A'; B \<subseteq> A |] ==> F \<in> B co A'"
by (unfold constrains_def, blast)
lemma constrains_weaken:
- "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'"
+ "[| F \<in> A co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B co B'"
by (unfold constrains_def, blast)
(** Union **)
lemma constrains_Un:
- "[| F : A co A'; F : B co B' |] ==> F : (A Un B) co (A' Un B')"
+ "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')"
by (unfold constrains_def, blast)
lemma constrains_UN:
- "(!!i. i:I ==> F : (A i) co (A' i))
- ==> F : (UN i:I. A i) co (UN i:I. A' i)"
+ "(!!i. i \<in> I ==> F \<in> (A i) co (A' i))
+ ==> F \<in> (\<Union>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
by (unfold constrains_def, blast)
-lemma constrains_Un_distrib: "(A Un B) co C = (A co C) Int (B co C)"
+lemma constrains_Un_distrib: "(A \<union> B) co C = (A co C) \<inter> (B co C)"
by (unfold constrains_def, blast)
-lemma constrains_UN_distrib: "(UN i:I. A i) co B = (INT i:I. A i co B)"
+lemma constrains_UN_distrib: "(\<Union>i \<in> I. A i) co B = (\<Inter>i \<in> I. A i co B)"
by (unfold constrains_def, blast)
-lemma constrains_Int_distrib: "C co (A Int B) = (C co A) Int (C co B)"
+lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)"
by (unfold constrains_def, blast)
-lemma constrains_INT_distrib: "A co (INT i:I. B i) = (INT i:I. A co B i)"
+lemma constrains_INT_distrib: "A co (\<Inter>i \<in> I. B i) = (\<Inter>i \<in> I. A co B i)"
by (unfold constrains_def, blast)
(** Intersection **)
lemma constrains_Int:
- "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')"
+ "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
by (unfold constrains_def, blast)
lemma constrains_INT:
- "(!!i. i:I ==> F : (A i) co (A' i))
- ==> F : (INT i:I. A i) co (INT i:I. A' i)"
+ "(!!i. i \<in> I ==> F \<in> (A i) co (A' i))
+ ==> F \<in> (\<Inter>i \<in> I. A i) co (\<Inter>i \<in> I. A' i)"
by (unfold constrains_def, blast)
-lemma constrains_imp_subset: "F : A co A' ==> A <= A'"
+lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
by (unfold constrains_def, auto)
(*The reasoning is by subsets since "co" refers to single actions
only. So this rule isn't that useful.*)
lemma constrains_trans:
- "[| F : A co B; F : B co C |] ==> F : A co C"
+ "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
by (unfold constrains_def, blast)
lemma constrains_cancel:
- "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')"
+ "[| F \<in> A co (A' \<union> B); F \<in> B co B' |] ==> F \<in> A co (A' \<union> B')"
by (unfold constrains_def, clarify, blast)
(*** unless ***)
-lemma unlessI: "F : (A-B) co (A Un B) ==> F : A unless B"
+lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
by (unfold unless_def, assumption)
-lemma unlessD: "F : A unless B ==> F : (A-B) co (A Un B)"
+lemma unlessD: "F \<in> A unless B ==> F \<in> (A-B) co (A \<union> B)"
by (unfold unless_def, assumption)
(*** stable ***)
-lemma stableI: "F : A co A ==> F : stable A"
+lemma stableI: "F \<in> A co A ==> F \<in> stable A"
by (unfold stable_def, assumption)
-lemma stableD: "F : stable A ==> F : A co A"
+lemma stableD: "F \<in> stable A ==> F \<in> A co A"
by (unfold stable_def, assumption)
lemma stable_UNIV [simp]: "stable UNIV = UNIV"
@@ -261,14 +261,14 @@
(** Union **)
lemma stable_Un:
- "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')"
+ "[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
apply (unfold stable_def)
apply (blast intro: constrains_Un)
done
lemma stable_UN:
- "(!!i. i:I ==> F : stable (A i)) ==> F : stable (UN i:I. A i)"
+ "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Union>i \<in> I. A i)"
apply (unfold stable_def)
apply (blast intro: constrains_UN)
done
@@ -276,75 +276,75 @@
(** Intersection **)
lemma stable_Int:
- "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')"
+ "[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<inter> A')"
apply (unfold stable_def)
apply (blast intro: constrains_Int)
done
lemma stable_INT:
- "(!!i. i:I ==> F : stable (A i)) ==> F : stable (INT i:I. A i)"
+ "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Inter>i \<in> I. A i)"
apply (unfold stable_def)
apply (blast intro: constrains_INT)
done
lemma stable_constrains_Un:
- "[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"
+ "[| F \<in> stable C; F \<in> A co (C \<union> A') |] ==> F \<in> (C \<union> A) co (C \<union> A')"
by (unfold stable_def constrains_def, blast)
lemma stable_constrains_Int:
- "[| F : stable C; F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')"
+ "[| F \<in> stable C; F \<in> (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')"
by (unfold stable_def constrains_def, blast)
-(*[| F : stable C; F : (C Int A) co A |] ==> F : stable (C Int A) *)
+(*[| F \<in> stable C; F \<in> (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
(*** invariant ***)
-lemma invariantI: "[| Init F<=A; F: stable A |] ==> F : invariant A"
+lemma invariantI: "[| Init F \<subseteq> A; F \<in> stable A |] ==> F \<in> invariant A"
by (simp add: invariant_def)
-(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
+(*Could also say "invariant A \<inter> invariant B \<subseteq> invariant (A \<inter> B)"*)
lemma invariant_Int:
- "[| F : invariant A; F : invariant B |] ==> F : invariant (A Int B)"
+ "[| F \<in> invariant A; F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
by (auto simp add: invariant_def stable_Int)
(*** increasing ***)
lemma increasingD:
- "F : increasing f ==> F : stable {s. z <= f s}"
+ "F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
by (unfold increasing_def, blast)
-lemma increasing_constant [iff]: "F : increasing (%s. c)"
+lemma increasing_constant [iff]: "F \<in> increasing (%s. c)"
by (unfold increasing_def stable_def, auto)
lemma mono_increasing_o:
- "mono g ==> increasing f <= increasing (g o f)"
+ "mono g ==> increasing f \<subseteq> increasing (g o f)"
apply (unfold increasing_def stable_def constrains_def, auto)
apply (blast intro: monoD order_trans)
done
-(*Holds by the theorem (Suc m <= n) = (m < n) *)
+(*Holds by the theorem (Suc m \<subseteq> n) = (m < n) *)
lemma strict_increasingD:
- "!!z::nat. F : increasing f ==> F: stable {s. z < f s}"
+ "!!z::nat. F \<in> increasing f ==> F \<in> stable {s. z < f s}"
by (simp add: increasing_def Suc_le_eq [symmetric])
(** The Elimination Theorem. The "free" m has become universally quantified!
- Should the premise be !!m instead of ALL m ? Would make it harder to use
+ Should the premise be !!m instead of \<forall>m ? Would make it harder to use
in forward proof. **)
lemma elimination:
- "[| ALL m:M. F : {s. s x = m} co (B m) |]
- ==> F : {s. s x : M} co (UN m:M. B m)"
+ "[| \<forall>m \<in> M. F \<in> {s. s x = m} co (B m) |]
+ ==> F \<in> {s. s x \<in> M} co (\<Union>m \<in> M. B m)"
by (unfold constrains_def, blast)
(*As above, but for the trivial case of a one-variable state, in which the
state is identified with its one variable.*)
lemma elimination_sing:
- "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)"
+ "(\<forall>m \<in> M. F \<in> {m} co (B m)) ==> F \<in> M co (\<Union>m \<in> M. B m)"
by (unfold constrains_def, blast)
@@ -352,20 +352,20 @@
(*** Theoretical Results from Section 6 ***)
lemma constrains_strongest_rhs:
- "F : A co (strongest_rhs F A )"
+ "F \<in> A co (strongest_rhs F A )"
by (unfold constrains_def strongest_rhs_def, blast)
lemma strongest_rhs_is_strongest:
- "F : A co B ==> strongest_rhs F A <= B"
+ "F \<in> A co B ==> strongest_rhs F A \<subseteq> B"
by (unfold constrains_def strongest_rhs_def, blast)
(** Ad-hoc set-theory rules **)
-lemma Un_Diff_Diff [simp]: "A Un B - (A - B) = B"
+lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
by blast
-lemma Int_Union_Union: "Union(B) Int A = Union((%C. C Int A)`B)"
+lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
by blast
(** Needed for WF reasoning in WFair.ML **)
--- a/src/HOL/UNITY/Union.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Union.thy Tue Feb 04 18:12:40 2003 +0100
@@ -12,36 +12,36 @@
constdefs
- (*FIXME: conjoin Init F Int Init G ~= {} *)
+ (*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *)
ok :: "['a program, 'a program] => bool" (infixl "ok" 65)
- "F ok G == Acts F <= AllowedActs G &
- Acts G <= AllowedActs F"
+ "F ok G == Acts F \<subseteq> AllowedActs G &
+ Acts G \<subseteq> AllowedActs F"
- (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *)
+ (*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *)
OK :: "['a set, 'a => 'b program] => bool"
- "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
+ "OK I F == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))"
JOIN :: "['a set, 'a => 'b program] => 'b program"
- "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
- INT i:I. AllowedActs (F i))"
+ "JOIN I F == mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i),
+ \<Inter>i \<in> I. AllowedActs (F i))"
Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65)
- "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
- AllowedActs F Int AllowedActs G)"
+ "F Join G == mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
+ AllowedActs F \<inter> AllowedActs G)"
SKIP :: "'a program"
"SKIP == mk_program (UNIV, {}, UNIV)"
(*Characterizes safety properties. Used with specifying AllowedActs*)
safety_prop :: "'a program set => bool"
- "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
+ "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
syntax
"@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10)
"@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10)
translations
- "JN x:A. B" == "JOIN A (%x. B)"
+ "JN x : A. B" == "JOIN A (%x. B)"
"JN x y. B" == "JN x. JN y. B"
"JN x. B" == "JOIN UNIV (%x. B)"
@@ -49,7 +49,7 @@
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> _:_./ _)" 10)
+ "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10)
subsection{*SKIP*}
@@ -68,13 +68,13 @@
subsection{*SKIP and safety properties*}
-lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)"
+lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) = (A \<subseteq> B)"
by (unfold constrains_def, auto)
-lemma SKIP_in_Constrains_iff [iff]: "(SKIP : A Co B) = (A<=B)"
+lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B) = (A \<subseteq> B)"
by (unfold Constrains_def, auto)
-lemma SKIP_in_stable [iff]: "SKIP : stable A"
+lemma SKIP_in_stable [iff]: "SKIP \<in> stable A"
by (unfold stable_def, auto)
declare SKIP_in_stable [THEN stable_imp_Stable, iff]
@@ -82,40 +82,40 @@
subsection{*Join*}
-lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G"
+lemma Init_Join [simp]: "Init (F Join G) = Init F \<inter> Init G"
by (simp add: Join_def)
-lemma Acts_Join [simp]: "Acts (F Join G) = Acts F Un Acts G"
+lemma Acts_Join [simp]: "Acts (F Join G) = Acts F \<union> Acts G"
by (auto simp add: Join_def)
lemma AllowedActs_Join [simp]:
- "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G"
+ "AllowedActs (F Join G) = AllowedActs F \<inter> AllowedActs G"
by (auto simp add: Join_def)
subsection{*JN*}
-lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP"
+lemma JN_empty [simp]: "(\<Squnion>i\<in>{}. F i) = SKIP"
by (unfold JOIN_def SKIP_def, auto)
-lemma JN_insert [simp]: "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)"
+lemma JN_insert [simp]: "(\<Squnion>i \<in> insert a I. F i) = (F a) Join (\<Squnion>i \<in> I. F i)"
apply (rule program_equalityI)
apply (auto simp add: JOIN_def Join_def)
done
-lemma Init_JN [simp]: "Init (JN i:I. F i) = (INT i:I. Init (F i))"
+lemma Init_JN [simp]: "Init (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. Init (F i))"
by (simp add: JOIN_def)
-lemma Acts_JN [simp]: "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))"
+lemma Acts_JN [simp]: "Acts (\<Squnion>i \<in> I. F i) = insert Id (\<Union>i \<in> I. Acts (F i))"
by (auto simp add: JOIN_def)
lemma AllowedActs_JN [simp]:
- "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))"
+ "AllowedActs (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. AllowedActs (F i))"
by (auto simp add: JOIN_def)
lemma JN_cong [cong]:
- "[| I=J; !!i. i:J ==> F i = G i |] ==> (JN i:I. F i) = (JN i:J. G i)"
+ "[| I=J; !!i. i \<in> J ==> F i = G i |] ==> (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> J. G i)"
by (simp add: JOIN_def)
@@ -156,28 +156,28 @@
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
-subsection{*JN laws*}
+subsection{*\<Squnion>laws*}
(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
-lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)"
+lemma JN_absorb: "k \<in> I ==> F k Join (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
by (auto intro!: program_equalityI)
-lemma JN_Un: "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))"
+lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F i) = ((\<Squnion>i \<in> I. F i) Join (\<Squnion>i \<in> J. F i))"
by (auto intro!: program_equalityI)
-lemma JN_constant: "(JN i:I. c) = (if I={} then SKIP else c)"
+lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I={} then SKIP else c)"
by (rule program_equalityI, auto)
lemma JN_Join_distrib:
- "(JN i:I. F i Join G i) = (JN i:I. F i) Join (JN i:I. G i)"
+ "(\<Squnion>i \<in> I. F i Join G i) = (\<Squnion>i \<in> I. F i) Join (\<Squnion>i \<in> I. G i)"
by (auto intro!: program_equalityI)
lemma JN_Join_miniscope:
- "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)"
+ "i \<in> I ==> (\<Squnion>i \<in> I. F i Join G) = ((\<Squnion>i \<in> I. F i) Join G)"
by (auto simp add: JN_Join_distrib JN_constant)
(*Used to prove guarantees_JN_I*)
-lemma JN_Join_diff: "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F"
+lemma JN_Join_diff: "i \<in> I ==> F i Join JOIN (I - {i}) F = JOIN I F"
apply (unfold JOIN_def Join_def)
apply (rule program_equalityI, auto)
done
@@ -185,19 +185,19 @@
subsection{*Safety: co, stable, FP*}
-(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B. So an
- alternative precondition is A<=B, but most proofs using this rule require
+(*Fails if I={} because it collapses to SKIP \<in> A co B, i.e. to A \<subseteq> B. So an
+ alternative precondition is A \<subseteq> B, but most proofs using this rule require
I to be nonempty for other reasons anyway.*)
lemma JN_constrains:
- "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)"
+ "i \<in> I ==> (\<Squnion>i \<in> I. F i) \<in> A co B = (\<forall>i \<in> I. F i \<in> A co B)"
by (simp add: constrains_def JOIN_def, blast)
lemma Join_constrains [simp]:
- "(F Join G : A co B) = (F : A co B & G : A co B)"
+ "(F Join 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 : A unless B) = (F : A unless B & G : A unless B)"
+ "(F Join 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.
@@ -206,100 +206,100 @@
lemma Join_constrains_weaken:
- "[| F : A co A'; G : B co B' |]
- ==> F Join G : (A Int B) co (A' Un B')"
+ "[| F \<in> A co A'; G \<in> B co B' |]
+ ==> F Join G \<in> (A \<inter> B) co (A' \<union> B')"
by (simp, blast intro: constrains_weaken)
-(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*)
+(*If I={}, it degenerates to SKIP \<in> UNIV co {}, which is false.*)
lemma JN_constrains_weaken:
- "[| ALL i:I. F i : A i co A' i; i: I |]
- ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)"
+ "[| \<forall>i \<in> I. F i \<in> A i co A' i; i \<in> I |]
+ ==> (\<Squnion>i \<in> I. F i) \<in> (\<Inter>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
apply (simp (no_asm_simp) add: JN_constrains)
apply (blast intro: constrains_weaken)
done
-lemma JN_stable: "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)"
+lemma JN_stable: "(\<Squnion>i \<in> I. F i) \<in> stable A = (\<forall>i \<in> I. F i \<in> stable A)"
by (simp add: stable_def constrains_def JOIN_def)
lemma invariant_JN_I:
- "[| !!i. i:I ==> F i : invariant A; i : I |]
- ==> (JN i:I. F i) : invariant A"
+ "[| !!i. i \<in> I ==> F i \<in> invariant A; i \<in> I |]
+ ==> (\<Squnion>i \<in> I. F i) \<in> invariant A"
by (simp add: invariant_def JN_stable, blast)
lemma Join_stable [simp]:
- "(F Join G : stable A) =
- (F : stable A & G : stable A)"
+ "(F Join G \<in> stable A) =
+ (F \<in> stable A & G \<in> stable A)"
by (simp add: stable_def)
lemma Join_increasing [simp]:
- "(F Join G : increasing f) =
- (F : increasing f & G : increasing f)"
+ "(F Join G \<in> increasing f) =
+ (F \<in> increasing f & G \<in> increasing f)"
by (simp add: increasing_def Join_stable, blast)
lemma invariant_JoinI:
- "[| F : invariant A; G : invariant A |]
- ==> F Join G : invariant A"
+ "[| F \<in> invariant A; G \<in> invariant A |]
+ ==> F Join G \<in> invariant A"
by (simp add: invariant_def, blast)
-lemma FP_JN: "FP (JN i:I. F i) = (INT i:I. FP (F i))"
+lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
by (simp add: FP_def JN_stable INTER_def)
subsection{*Progress: transient, ensures*}
lemma JN_transient:
- "i : I ==>
- (JN i:I. F i) : transient A = (EX i:I. F i : transient A)"
+ "i \<in> I ==>
+ (\<Squnion>i \<in> I. F i) \<in> transient A = (\<exists>i \<in> I. F i \<in> transient A)"
by (auto simp add: transient_def JOIN_def)
lemma Join_transient [simp]:
- "F Join G : transient A =
- (F : transient A | G : transient A)"
+ "F Join 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 : transient A ==> F Join G : transient A"
+lemma Join_transient_I1: "F \<in> transient A ==> F Join G \<in> transient A"
by (simp add: Join_transient)
-lemma Join_transient_I2: "G : transient A ==> F Join G : transient A"
+lemma Join_transient_I2: "G \<in> transient A ==> F Join G \<in> transient A"
by (simp add: Join_transient)
-(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
+(*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
lemma JN_ensures:
- "i : I ==>
- (JN i:I. F i) : A ensures B =
- ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))"
+ "i \<in> I ==>
+ (\<Squnion>i \<in> I. F i) \<in> A ensures B =
+ ((\<forall>i \<in> I. F i \<in> (A-B) co (A \<union> B)) & (\<exists>i \<in> I. F i \<in> A ensures B))"
by (auto simp add: ensures_def JN_constrains JN_transient)
lemma Join_ensures:
- "F Join G : A ensures B =
- (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) &
- (F : transient (A-B) | G : transient (A-B)))"
+ "F Join 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 : stable A; G : A co A' |]
- ==> F Join G : A co A'"
+ "[| F \<in> stable A; G \<in> A co A' |]
+ ==> F Join G \<in> A co A'"
apply (unfold stable_def constrains_def Join_def)
apply (simp add: ball_Un, blast)
done
-(*Premise for G cannot use Always because F: Stable A is weaker than
- G : stable A *)
+(*Premise for G cannot use Always because F \<in> Stable A is weaker than
+ G \<in> stable A *)
lemma stable_Join_Always1:
- "[| F : stable A; G : invariant A |] ==> F Join G : Always A"
+ "[| F \<in> stable A; G \<in> invariant A |] ==> F Join 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 : invariant A; G : stable A |] ==> F Join G : Always A"
+ "[| F \<in> invariant A; G \<in> stable A |] ==> F Join G \<in> Always A"
apply (subst Join_commute)
apply (blast intro: stable_Join_Always1)
done
lemma stable_Join_ensures1:
- "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B"
+ "[| F \<in> stable A; G \<in> A ensures B |] ==> F Join 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 : A ensures B; G : stable A |] ==> F Join G : A ensures B"
+ "[| F \<in> A ensures B; G \<in> stable A |] ==> F Join G \<in> A ensures B"
apply (subst Join_commute)
apply (blast intro: stable_Join_ensures1)
done
@@ -344,16 +344,16 @@
lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"
by (auto simp add: ok_def)
-lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (ALL i:I. F ok G i)"
+lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (\<forall>i \<in> I. F ok G i)"
by (auto simp add: ok_def)
-lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F = (ALL i:I. G i ok F)"
+lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F = (\<forall>i \<in> I. G i ok F)"
by (auto simp add: ok_def)
-lemma OK_iff_ok: "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))"
+lemma OK_iff_ok: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. (F i) ok (F j))"
by (auto simp add: ok_def OK_def)
-lemma OK_imp_ok: "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)"
+lemma OK_imp_ok: "[| OK I F; i \<in> I; j \<in> I; i \<noteq> j|] ==> (F i) ok (F j)"
by (auto simp add: OK_iff_ok)
@@ -362,27 +362,27 @@
lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
by (auto simp add: Allowed_def)
-lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F Int Allowed G"
+lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F \<inter> Allowed G"
by (auto simp add: Allowed_def)
-lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (INT i:I. Allowed (F i))"
+lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\<Inter>i \<in> I. Allowed (F i))"
by (auto simp add: Allowed_def)
-lemma ok_iff_Allowed: "F ok G = (F : Allowed G & G : Allowed F)"
+lemma ok_iff_Allowed: "F ok G = (F \<in> Allowed G & G \<in> Allowed F)"
by (simp add: ok_def Allowed_def)
-lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"
+lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F i \<in> Allowed(F j))"
by (auto simp add: OK_iff_ok ok_iff_Allowed)
subsection{*@{text safety_prop}, for reasoning about
given instances of "ok"*}
lemma safety_prop_Acts_iff:
- "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)"
+ "safety_prop X ==> (Acts G \<subseteq> insert Id (UNION X Acts)) = (G \<in> X)"
by (auto simp add: safety_prop_def)
lemma safety_prop_AllowedActs_iff_Allowed:
- "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)"
+ "safety_prop X ==> (UNION X Acts \<subseteq> AllowedActs F) = (X \<subseteq> Allowed F)"
by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric])
lemma Allowed_eq:
@@ -395,27 +395,27 @@
by (simp add: Allowed_eq)
(*For safety_prop to hold, the property must be satisfiable!*)
-lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A <= B)"
+lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \<subseteq> B)"
by (simp add: safety_prop_def constrains_def, blast)
lemma safety_prop_stable [iff]: "safety_prop (stable A)"
by (simp add: stable_def)
lemma safety_prop_Int [simp]:
- "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)"
+ "[| safety_prop X; safety_prop Y |] ==> safety_prop (X \<inter> Y)"
by (simp add: safety_prop_def, blast)
lemma safety_prop_INTER1 [simp]:
- "(!!i. safety_prop (X i)) ==> safety_prop (INT i. X i)"
+ "(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)"
by (auto simp add: safety_prop_def, blast)
lemma safety_prop_INTER [simp]:
- "(!!i. i:I ==> safety_prop (X i)) ==> safety_prop (INT i:I. X i)"
+ "(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)"
by (auto simp add: safety_prop_def, blast)
lemma def_UNION_ok_iff:
"[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]
- ==> F ok G = (G : X & acts <= AllowedActs G)"
+ ==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
by (auto simp add: ok_def safety_prop_Acts_iff)
end
--- a/src/HOL/UNITY/WFair.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/WFair.thy Tue Feb 04 18:12:40 2003 +0100
@@ -17,10 +17,10 @@
(*This definition specifies weak fairness. The rest of the theory
is generic to all forms of fairness.*)
transient :: "'a set => 'a program set"
- "transient A == {F. EX act: Acts F. A <= Domain act & act``A <= -A}"
+ "transient A == {F. \<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A}"
ensures :: "['a set, 'a set] => 'a program set" (infixl "ensures" 60)
- "A ensures B == (A-B co A Un B) Int transient (A-B)"
+ "A ensures B == (A-B co A \<union> B) \<inter> transient (A-B)"
consts
@@ -32,22 +32,22 @@
inductive "leads F"
intros
- Basis: "F : A ensures B ==> (A,B) : leads F"
+ Basis: "F \<in> A ensures B ==> (A,B) \<in> leads F"
- Trans: "[| (A,B) : leads F; (B,C) : leads F |] ==> (A,C) : leads F"
+ Trans: "[| (A,B) \<in> leads F; (B,C) \<in> leads F |] ==> (A,C) \<in> leads F"
- Union: "ALL A: S. (A,B) : leads F ==> (Union S, B) : leads F"
+ Union: "\<forall>A \<in> S. (A,B) \<in> leads F ==> (Union S, B) \<in> leads F"
constdefs
(*visible version of the LEADS-TO relation*)
leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60)
- "A leadsTo B == {F. (A,B) : leads F}"
+ "A leadsTo B == {F. (A,B) \<in> leads F}"
(*wlt F B is the largest set that leads to B*)
wlt :: "['a program, 'a set] => 'a set"
- "wlt F B == Union {A. F: A leadsTo B}"
+ "wlt F B == Union {A. F \<in> A leadsTo B}"
syntax (xsymbols)
"op leadsTo" :: "['a set, 'a set] => 'a program set" (infixl "\<longmapsto>" 60)
@@ -56,22 +56,22 @@
subsection{*transient*}
lemma stable_transient_empty:
- "[| F : stable A; F : transient A |] ==> A = {}"
+ "[| F \<in> stable A; F \<in> transient A |] ==> A = {}"
by (unfold stable_def constrains_def transient_def, blast)
lemma transient_strengthen:
- "[| F : transient A; B<=A |] ==> F : transient B"
+ "[| F \<in> transient A; B \<subseteq> A |] ==> F \<in> transient B"
apply (unfold transient_def, clarify)
apply (blast intro!: rev_bexI)
done
lemma transientI:
- "[| act: Acts F; A <= Domain act; act``A <= -A |] ==> F : transient A"
+ "[| act: Acts F; A \<subseteq> Domain act; act``A \<subseteq> -A |] ==> F \<in> transient A"
by (unfold transient_def, blast)
lemma transientE:
- "[| F : transient A;
- !!act. [| act: Acts F; A <= Domain act; act``A <= -A |] ==> P |]
+ "[| F \<in> transient A;
+ !!act. [| act: Acts F; A \<subseteq> Domain act; act``A \<subseteq> -A |] ==> P |]
==> P"
by (unfold transient_def, blast)
@@ -85,23 +85,23 @@
subsection{*ensures*}
lemma ensuresI:
- "[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B"
+ "[| F \<in> (A-B) co (A \<union> B); F \<in> transient (A-B) |] ==> F \<in> A ensures B"
by (unfold ensures_def, blast)
lemma ensuresD:
- "F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)"
+ "F \<in> A ensures B ==> F \<in> (A-B) co (A \<union> B) & F \<in> transient (A-B)"
by (unfold ensures_def, blast)
lemma ensures_weaken_R:
- "[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'"
+ "[| F \<in> A ensures A'; A'<=B' |] ==> F \<in> A ensures B'"
apply (unfold ensures_def)
apply (blast intro: constrains_weaken transient_strengthen)
done
(*The L-version (precondition strengthening) fails, but we have this*)
lemma stable_ensures_Int:
- "[| F : stable C; F : A ensures B |]
- ==> F : (C Int A) ensures (C Int B)"
+ "[| F \<in> stable C; F \<in> A ensures B |]
+ ==> F \<in> (C \<inter> A) ensures (C \<inter> B)"
apply (unfold ensures_def)
apply (auto simp add: ensures_def Int_Un_distrib [symmetric] Diff_Int_distrib [symmetric])
prefer 2 apply (blast intro: transient_strengthen)
@@ -109,78 +109,78 @@
done
lemma stable_transient_ensures:
- "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B"
+ "[| F \<in> stable A; F \<in> transient C; A \<subseteq> B \<union> C |] ==> F \<in> A ensures B"
apply (simp add: ensures_def stable_def)
apply (blast intro: constrains_weaken transient_strengthen)
done
-lemma ensures_eq: "(A ensures B) = (A unless B) Int transient (A-B)"
+lemma ensures_eq: "(A ensures B) = (A unless B) \<inter> transient (A-B)"
by (simp (no_asm) add: ensures_def unless_def)
subsection{*leadsTo*}
-lemma leadsTo_Basis [intro]: "F : A ensures B ==> F : A leadsTo B"
+lemma leadsTo_Basis [intro]: "F \<in> A ensures B ==> F \<in> A leadsTo B"
apply (unfold leadsTo_def)
apply (blast intro: leads.Basis)
done
lemma leadsTo_Trans:
- "[| F : A leadsTo B; F : B leadsTo C |] ==> F : A leadsTo C"
+ "[| F \<in> A leadsTo B; F \<in> B leadsTo C |] ==> F \<in> A leadsTo C"
apply (unfold leadsTo_def)
apply (blast intro: leads.Trans)
done
-lemma transient_imp_leadsTo: "F : transient A ==> F : A leadsTo (-A)"
+lemma transient_imp_leadsTo: "F \<in> transient A ==> F \<in> A leadsTo (-A)"
by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)
(*Useful with cancellation, disjunction*)
-lemma leadsTo_Un_duplicate: "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"
+lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'"
by (simp add: Un_ac)
lemma leadsTo_Un_duplicate2:
- "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)"
+ "F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)"
by (simp add: Un_ac)
(*The Union introduction rule as we should have liked to state it*)
lemma leadsTo_Union:
- "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B"
+ "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (Union S) leadsTo B"
apply (unfold leadsTo_def)
apply (blast intro: leads.Union)
done
lemma leadsTo_Union_Int:
- "(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B"
+ "(!!A. A \<in> S ==> F \<in> (A \<inter> C) leadsTo B) ==> F \<in> (Union S \<inter> C) leadsTo B"
apply (unfold leadsTo_def)
apply (simp only: Int_Union_Union)
apply (blast intro: leads.Union)
done
lemma leadsTo_UN:
- "(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B"
+ "(!!i. i \<in> I ==> F \<in> (A i) leadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) leadsTo B"
apply (subst Union_image_eq [symmetric])
apply (blast intro: leadsTo_Union)
done
(*Binary union introduction rule*)
lemma leadsTo_Un:
- "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C"
+ "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
apply (subst Un_eq_Union)
apply (blast intro: leadsTo_Union)
done
lemma single_leadsTo_I:
- "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B"
+ "(!!x. x \<in> A ==> F \<in> {x} leadsTo B) ==> F \<in> A leadsTo B"
by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
(*The INDUCTION rule as we should have liked to state it*)
lemma leadsTo_induct:
- "[| F : za leadsTo zb;
- !!A B. F : A ensures B ==> P A B;
- !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |]
+ "[| F \<in> za leadsTo zb;
+ !!A B. F \<in> A ensures B ==> P A B;
+ !!A B C. [| F \<in> A leadsTo B; P A B; F \<in> B leadsTo C; P B C |]
==> P A C;
- !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B
+ !!B S. \<forall>A \<in> S. F \<in> A leadsTo B & P A B ==> P (Union S) B
|] ==> P za zb"
apply (unfold leadsTo_def)
apply (drule CollectD, erule leads.induct)
@@ -188,7 +188,7 @@
done
-lemma subset_imp_ensures: "A<=B ==> F : A ensures B"
+lemma subset_imp_ensures: "A \<subseteq> B ==> F \<in> A ensures B"
by (unfold ensures_def constrains_def transient_def, blast)
lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
@@ -205,10 +205,10 @@
(*Lemma is the weak version: can't see how to do it in one step*)
lemma leadsTo_induct_pre_lemma:
- "[| F : za leadsTo zb;
+ "[| F \<in> za leadsTo zb;
P zb;
- !!A B. [| F : A ensures B; P B |] ==> P A;
- !!S. ALL A:S. P A ==> P (Union S)
+ !!A B. [| F \<in> A ensures B; P B |] ==> P A;
+ !!S. \<forall>A \<in> S. P A ==> P (Union S)
|] ==> P za"
(*by induction on this formula*)
apply (subgoal_tac "P zb --> P za")
@@ -219,12 +219,12 @@
done
lemma leadsTo_induct_pre:
- "[| F : za leadsTo zb;
+ "[| F \<in> za leadsTo zb;
P zb;
- !!A B. [| F : A ensures B; F : B leadsTo zb; P B |] ==> P A;
- !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S)
+ !!A B. [| F \<in> A ensures B; F \<in> B leadsTo zb; P B |] ==> P A;
+ !!S. \<forall>A \<in> S. F \<in> A leadsTo zb & P A ==> P (Union S)
|] ==> P za"
-apply (subgoal_tac "F : za leadsTo zb & P za")
+apply (subgoal_tac "F \<in> za leadsTo zb & P za")
apply (erule conjunct2)
apply (erule leadsTo_induct_pre_lemma)
prefer 3 apply (blast intro: leadsTo_Union)
@@ -233,76 +233,76 @@
done
-lemma leadsTo_weaken_R: "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'"
+lemma leadsTo_weaken_R: "[| F \<in> A leadsTo A'; A'<=B' |] ==> F \<in> A leadsTo B'"
by (blast intro: subset_imp_leadsTo leadsTo_Trans)
lemma leadsTo_weaken_L [rule_format]:
- "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'"
+ "[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'"
by (blast intro: leadsTo_Trans subset_imp_leadsTo)
(*Distributes over binary unions*)
lemma leadsTo_Un_distrib:
- "F : (A Un B) leadsTo C = (F : A leadsTo C & F : B leadsTo C)"
+ "F \<in> (A \<union> B) leadsTo C = (F \<in> A leadsTo C & F \<in> B leadsTo C)"
by (blast intro: leadsTo_Un leadsTo_weaken_L)
lemma leadsTo_UN_distrib:
- "F : (UN i:I. A i) leadsTo B = (ALL i : I. F : (A i) leadsTo B)"
+ "F \<in> (\<Union>i \<in> I. A i) leadsTo B = (\<forall>i \<in> I. F \<in> (A i) leadsTo B)"
by (blast intro: leadsTo_UN leadsTo_weaken_L)
lemma leadsTo_Union_distrib:
- "F : (Union S) leadsTo B = (ALL A : S. F : A leadsTo B)"
+ "F \<in> (Union S) leadsTo B = (\<forall>A \<in> S. F \<in> A leadsTo B)"
by (blast intro: leadsTo_Union leadsTo_weaken_L)
lemma leadsTo_weaken:
- "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'"
+ "[| F \<in> A leadsTo A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B leadsTo B'"
by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans)
(*Set difference: maybe combine with leadsTo_weaken_L?*)
lemma leadsTo_Diff:
- "[| F : (A-B) leadsTo C; F : B leadsTo C |] ==> F : A leadsTo C"
+ "[| F \<in> (A-B) leadsTo C; F \<in> B leadsTo C |] ==> F \<in> A leadsTo C"
by (blast intro: leadsTo_Un leadsTo_weaken)
lemma leadsTo_UN_UN:
- "(!! i. i:I ==> F : (A i) leadsTo (A' i))
- ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"
+ "(!! i. i \<in> I ==> F \<in> (A i) leadsTo (A' i))
+ ==> F \<in> (\<Union>i \<in> I. A i) leadsTo (\<Union>i \<in> I. A' i)"
apply (simp only: Union_image_eq [symmetric])
apply (blast intro: leadsTo_Union leadsTo_weaken_R)
done
(*Binary union version*)
lemma leadsTo_Un_Un:
- "[| F : A leadsTo A'; F : B leadsTo B' |]
- ==> F : (A Un B) leadsTo (A' Un B')"
+ "[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |]
+ ==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"
by (blast intro: leadsTo_Un leadsTo_weaken_R)
(** The cancellation law **)
lemma leadsTo_cancel2:
- "[| F : A leadsTo (A' Un B); F : B leadsTo B' |]
- ==> F : A leadsTo (A' Un B')"
+ "[| F \<in> A leadsTo (A' \<union> B); F \<in> B leadsTo B' |]
+ ==> F \<in> A leadsTo (A' \<union> B')"
by (blast intro: leadsTo_Un_Un subset_imp_leadsTo leadsTo_Trans)
lemma leadsTo_cancel_Diff2:
- "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |]
- ==> F : A leadsTo (A' Un B')"
+ "[| F \<in> A leadsTo (A' \<union> B); F \<in> (B-A') leadsTo B' |]
+ ==> F \<in> A leadsTo (A' \<union> B')"
apply (rule leadsTo_cancel2)
prefer 2 apply assumption
apply (simp_all (no_asm_simp))
done
lemma leadsTo_cancel1:
- "[| F : A leadsTo (B Un A'); F : B leadsTo B' |]
- ==> F : A leadsTo (B' Un A')"
+ "[| F \<in> A leadsTo (B \<union> A'); F \<in> B leadsTo B' |]
+ ==> F \<in> A leadsTo (B' \<union> A')"
apply (simp add: Un_commute)
apply (blast intro!: leadsTo_cancel2)
done
lemma leadsTo_cancel_Diff1:
- "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |]
- ==> F : A leadsTo (B' Un A')"
+ "[| F \<in> A leadsTo (B \<union> A'); F \<in> (B-A') leadsTo B' |]
+ ==> F \<in> A leadsTo (B' \<union> A')"
apply (rule leadsTo_cancel1)
prefer 2 apply assumption
apply (simp_all (no_asm_simp))
@@ -312,7 +312,7 @@
(** The impossibility law **)
-lemma leadsTo_empty: "F : A leadsTo {} ==> A={}"
+lemma leadsTo_empty: "F \<in> A leadsTo {} ==> A={}"
apply (erule leadsTo_induct_pre)
apply (simp_all add: ensures_def constrains_def transient_def, blast)
done
@@ -322,8 +322,8 @@
(*Special case of PSP: Misra's "stable conjunction"*)
lemma psp_stable:
- "[| F : A leadsTo A'; F : stable B |]
- ==> F : (A Int B) leadsTo (A' Int B)"
+ "[| F \<in> A leadsTo A'; F \<in> stable B |]
+ ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)"
apply (unfold stable_def)
apply (erule leadsTo_induct)
prefer 3 apply (blast intro: leadsTo_Union_Int)
@@ -334,19 +334,19 @@
done
lemma psp_stable2:
- "[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')"
+ "[| F \<in> A leadsTo A'; F \<in> stable B |] ==> F \<in> (B \<inter> A) leadsTo (B \<inter> A')"
by (simp add: psp_stable Int_ac)
lemma psp_ensures:
- "[| F : A ensures A'; F : B co B' |]
- ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))"
+ "[| F \<in> A ensures A'; F \<in> B co B' |]
+ ==> F \<in> (A \<inter> B') ensures ((A' \<inter> B) \<union> (B' - B))"
apply (unfold ensures_def constrains_def, clarify) (*speeds up the proof*)
apply (blast intro: transient_strengthen)
done
lemma psp:
- "[| F : A leadsTo A'; F : B co B' |]
- ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))"
+ "[| F \<in> A leadsTo A'; F \<in> B co B' |]
+ ==> F \<in> (A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B' - B))"
apply (erule leadsTo_induct)
prefer 3 apply (blast intro: leadsTo_Union_Int)
txt{*Basis case*}
@@ -359,13 +359,13 @@
done
lemma psp2:
- "[| F : A leadsTo A'; F : B co B' |]
- ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))"
+ "[| F \<in> A leadsTo A'; F \<in> B co B' |]
+ ==> F \<in> (B' \<inter> A) leadsTo ((B \<inter> A') \<union> (B' - B))"
by (simp (no_asm_simp) add: psp Int_ac)
lemma psp_unless:
- "[| F : A leadsTo A'; F : B unless B' |]
- ==> F : (A Int B) leadsTo ((A' Int B) Un B')"
+ "[| F \<in> A leadsTo A'; F \<in> B unless B' |]
+ ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B) \<union> B')"
apply (unfold unless_def)
apply (drule psp, assumption)
@@ -379,11 +379,11 @@
lemma leadsTo_wf_induct_lemma:
"[| wf r;
- ALL m. F : (A Int f-`{m}) leadsTo
- ((A Int f-`(r^-1 `` {m})) Un B) |]
- ==> F : (A Int f-`{m}) leadsTo B"
+ \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo
+ ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]
+ ==> F \<in> (A \<inter> f-`{m}) leadsTo B"
apply (erule_tac a = m in wf_induct)
-apply (subgoal_tac "F : (A Int (f -` (r^-1 `` {x}))) leadsTo B")
+apply (subgoal_tac "F \<in> (A \<inter> (f -` (r^-1 `` {x}))) leadsTo B")
apply (blast intro: leadsTo_cancel1 leadsTo_Un_duplicate)
apply (subst vimage_eq_UN)
apply (simp only: UN_simps [symmetric])
@@ -394,9 +394,9 @@
(** Meta or object quantifier ? **)
lemma leadsTo_wf_induct:
"[| wf r;
- ALL m. F : (A Int f-`{m}) leadsTo
- ((A Int f-`(r^-1 `` {m})) Un B) |]
- ==> F : A leadsTo B"
+ \<forall>m. F \<in> (A \<inter> f-`{m}) leadsTo
+ ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]
+ ==> F \<in> A leadsTo B"
apply (rule_tac t = A in subst)
defer 1
apply (rule leadsTo_UN)
@@ -408,102 +408,102 @@
lemma bounded_induct:
"[| wf r;
- ALL m:I. F : (A Int f-`{m}) leadsTo
- ((A Int f-`(r^-1 `` {m})) Un B) |]
- ==> F : A leadsTo ((A - (f-`I)) Un B)"
+ \<forall>m \<in> I. F \<in> (A \<inter> f-`{m}) leadsTo
+ ((A \<inter> f-`(r^-1 `` {m})) \<union> B) |]
+ ==> F \<in> A leadsTo ((A - (f-`I)) \<union> B)"
apply (erule leadsTo_wf_induct, safe)
-apply (case_tac "m:I")
+apply (case_tac "m \<in> I")
apply (blast intro: leadsTo_weaken)
apply (blast intro: subset_imp_leadsTo)
done
-(*Alternative proof is via the lemma F : (A Int f-`(lessThan m)) leadsTo B*)
+(*Alternative proof is via the lemma F \<in> (A \<inter> f-`(lessThan m)) leadsTo B*)
lemma lessThan_induct:
- "[| !!m::nat. F : (A Int f-`{m}) leadsTo ((A Int f-`{..m(}) Un B) |]
- ==> F : A leadsTo B"
+ "[| !!m::nat. F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`{..m(}) \<union> B) |]
+ ==> F \<in> A leadsTo B"
apply (rule wf_less_than [THEN leadsTo_wf_induct])
apply (simp (no_asm_simp))
apply blast
done
lemma lessThan_bounded_induct:
- "!!l::nat. [| ALL m:(greaterThan l).
- F : (A Int f-`{m}) leadsTo ((A Int f-`(lessThan m)) Un B) |]
- ==> F : A leadsTo ((A Int (f-`(atMost l))) Un B)"
+ "!!l::nat. [| \<forall>m \<in> greaterThan l.
+ F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(lessThan m)) \<union> B) |]
+ ==> F \<in> A leadsTo ((A \<inter> (f-`(atMost l))) \<union> B)"
apply (simp only: Diff_eq [symmetric] vimage_Compl Compl_greaterThan [symmetric])
apply (rule wf_less_than [THEN bounded_induct])
apply (simp (no_asm_simp))
done
lemma greaterThan_bounded_induct:
- "!!l::nat. [| ALL m:(lessThan l).
- F : (A Int f-`{m}) leadsTo ((A Int f-`(greaterThan m)) Un B) |]
- ==> F : A leadsTo ((A Int (f-`(atLeast l))) Un B)"
+ "(!!l::nat. \<forall>m \<in> lessThan l.
+ F \<in> (A \<inter> f-`{m}) leadsTo ((A \<inter> f-`(greaterThan m)) \<union> B))
+ ==> F \<in> A leadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
apply (rule_tac f = f and f1 = "%k. l - k"
in wf_less_than [THEN wf_inv_image, THEN leadsTo_wf_induct])
apply (simp (no_asm) add: inv_image_def Image_singleton)
apply clarify
apply (case_tac "m<l")
-prefer 2 apply (blast intro: not_leE subset_imp_leadsTo)
-apply (blast intro: leadsTo_weaken_R diff_less_mono2)
+ apply (blast intro: leadsTo_weaken_R diff_less_mono2)
+apply (blast intro: not_leE subset_imp_leadsTo)
done
subsection{*wlt*}
(*Misra's property W3*)
-lemma wlt_leadsTo: "F : (wlt F B) leadsTo B"
+lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B"
apply (unfold wlt_def)
apply (blast intro!: leadsTo_Union)
done
-lemma leadsTo_subset: "F : A leadsTo B ==> A <= wlt F B"
+lemma leadsTo_subset: "F \<in> A leadsTo B ==> A \<subseteq> wlt F B"
apply (unfold wlt_def)
apply (blast intro!: leadsTo_Union)
done
(*Misra's property W2*)
-lemma leadsTo_eq_subset_wlt: "F : A leadsTo B = (A <= wlt F B)"
+lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)"
by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])
(*Misra's property W4*)
-lemma wlt_increasing: "B <= wlt F B"
+lemma wlt_increasing: "B \<subseteq> wlt F B"
apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
done
(*Used in the Trans case below*)
lemma lemma1:
- "[| B <= A2;
- F : (A1 - B) co (A1 Un B);
- F : (A2 - C) co (A2 Un C) |]
- ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"
+ "[| B \<subseteq> A2;
+ F \<in> (A1 - B) co (A1 \<union> B);
+ F \<in> (A2 - C) co (A2 \<union> C) |]
+ ==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)"
by (unfold constrains_def, clarify, blast)
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*)
lemma leadsTo_123:
- "F : A leadsTo A'
- ==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')"
+ "F \<in> A leadsTo A'
+ ==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')"
apply (erule leadsTo_induct)
(*Basis*)
apply (blast dest: ensuresD)
(*Trans*)
apply clarify
-apply (rule_tac x = "Ba Un Bb" in exI)
+apply (rule_tac x = "Ba \<union> Bb" in exI)
apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
(*Union*)
apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
-apply (rule_tac x = "UN A:S. f A" in exI)
+apply (rule_tac x = "\<Union>A \<in> S. f A" in exI)
apply (auto intro: leadsTo_UN)
(*Blast_tac says PROOF FAILED*)
-apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i Un B"
+apply (rule_tac I1=S and A1="%i. f i - B" and A'1="%i. f i \<union> B"
in constrains_UN [THEN constrains_weaken], auto)
done
(*Misra's property W5*)
-lemma wlt_constrains_wlt: "F : (wlt F B - B) co (wlt F B)"
+lemma wlt_constrains_wlt: "F \<in> (wlt F B - B) co (wlt F B)"
proof -
from wlt_leadsTo [of F B, THEN leadsTo_123]
show ?thesis
@@ -527,28 +527,28 @@
subsection{*Completion: Binary and General Finite versions*}
lemma completion_lemma :
- "[| W = wlt F (B' Un C);
- F : A leadsTo (A' Un C); F : A' co (A' Un C);
- F : B leadsTo (B' Un C); F : B' co (B' Un C) |]
- ==> F : (A Int B) leadsTo ((A' Int B') Un C)"
-apply (subgoal_tac "F : (W-C) co (W Un B' Un C) ")
+ "[| W = wlt F (B' \<union> C);
+ F \<in> A leadsTo (A' \<union> C); F \<in> A' co (A' \<union> C);
+ F \<in> B leadsTo (B' \<union> C); F \<in> B' co (B' \<union> C) |]
+ ==> F \<in> (A \<inter> B) leadsTo ((A' \<inter> B') \<union> C)"
+apply (subgoal_tac "F \<in> (W-C) co (W \<union> B' \<union> C) ")
prefer 2
apply (blast intro: wlt_constrains_wlt [THEN [2] constrains_Un,
THEN constrains_weaken])
-apply (subgoal_tac "F : (W-C) co W")
+apply (subgoal_tac "F \<in> (W-C) co W")
prefer 2
apply (simp add: wlt_increasing Un_assoc Un_absorb2)
-apply (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C) ")
+apply (subgoal_tac "F \<in> (A \<inter> W - C) leadsTo (A' \<inter> W \<union> C) ")
prefer 2 apply (blast intro: wlt_leadsTo psp [THEN leadsTo_weaken])
(** LEVEL 6 **)
-apply (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C) ")
+apply (subgoal_tac "F \<in> (A' \<inter> W \<union> C) leadsTo (A' \<inter> B' \<union> C) ")
prefer 2
apply (rule leadsTo_Un_duplicate2)
apply (blast intro: leadsTo_Un_Un wlt_leadsTo
[THEN psp2, THEN leadsTo_weaken] leadsTo_refl)
apply (drule leadsTo_Diff)
apply (blast intro: subset_imp_leadsTo)
-apply (subgoal_tac "A Int B <= A Int W")
+apply (subgoal_tac "A \<inter> B \<subseteq> A \<inter> W")
prefer 2
apply (blast dest!: leadsTo_subset intro!: subset_refl [THEN Int_mono])
apply (blast intro: leadsTo_Trans subset_imp_leadsTo)
@@ -557,9 +557,9 @@
lemmas completion = completion_lemma [OF refl]
lemma finite_completion_lemma:
- "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) -->
- (ALL i:I. F : (A' i) co (A' i Un C)) -->
- F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
+ "finite I ==> (\<forall>i \<in> I. F \<in> (A i) leadsTo (A' i \<union> C)) -->
+ (\<forall>i \<in> I. F \<in> (A' i) co (A' i \<union> C)) -->
+ F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
apply (erule finite_induct, auto)
apply (rule completion)
prefer 4
@@ -569,15 +569,15 @@
lemma finite_completion:
"[| finite I;
- !!i. i:I ==> F : (A i) leadsTo (A' i Un C);
- !!i. i:I ==> F : (A' i) co (A' i Un C) |]
- ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"
+ !!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i \<union> C);
+ !!i. i \<in> I ==> F \<in> (A' i) co (A' i \<union> C) |]
+ ==> F \<in> (\<Inter>i \<in> I. A i) leadsTo ((\<Inter>i \<in> I. A' i) \<union> C)"
by (blast intro: finite_completion_lemma [THEN mp, THEN mp])
lemma stable_completion:
- "[| F : A leadsTo A'; F : stable A';
- F : B leadsTo B'; F : stable B' |]
- ==> F : (A Int B) leadsTo (A' Int B')"
+ "[| F \<in> A leadsTo A'; F \<in> stable A';
+ F \<in> B leadsTo B'; F \<in> stable B' |]
+ ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B')"
apply (unfold stable_def)
apply (rule_tac C1 = "{}" in completion [THEN leadsTo_weaken_R])
apply (force+)
@@ -585,9 +585,9 @@
lemma finite_stable_completion:
"[| finite I;
- !!i. i:I ==> F : (A i) leadsTo (A' i);
- !!i. i:I ==> F : stable (A' i) |]
- ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)"
+ !!i. i \<in> I ==> F \<in> (A i) leadsTo (A' i);
+ !!i. i \<in> I ==> F \<in> stable (A' i) |]
+ ==> F \<in> (\<Inter>i \<in> I. A i) leadsTo (\<Inter>i \<in> I. A' i)"
apply (unfold stable_def)
apply (rule_tac C1 = "{}" in finite_completion [THEN leadsTo_weaken_R])
apply (simp_all (no_asm_simp))