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