--- a/src/ZF/UNITY/SubstAx.thy Sat Oct 10 21:43:07 2015 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Sat Oct 10 22:02:23 2015 +0200
@@ -17,58 +17,54 @@
"A Ensures B == {F \<in> program. F \<in> (reachable(F) \<inter> A) ensures (reachable(F) \<inter> B) }"
definition
- LeadsTo :: "[i, i] => i" (infixl "LeadsTo" 60) where
- "A LeadsTo B == {F \<in> program. F:(reachable(F) \<inter> A) leadsTo (reachable(F) \<inter> B)}"
-
-notation (xsymbols)
- LeadsTo (infixl " \<longmapsto>w " 60)
-
+ LeadsTo :: "[i, i] => i" (infixl "\<longmapsto>w" 60) where
+ "A \<longmapsto>w B == {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> (reachable(F) \<inter> B)}"
(*Resembles the previous definition of LeadsTo*)
(* Equivalence with the HOL-like definition *)
lemma LeadsTo_eq:
-"st_set(B)==> A LeadsTo B = {F \<in> program. F:(reachable(F) \<inter> A) leadsTo B}"
+"st_set(B)==> A \<longmapsto>w B = {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> B}"
apply (unfold LeadsTo_def)
apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken)
done
-lemma LeadsTo_type: "A LeadsTo B <=program"
+lemma LeadsTo_type: "A \<longmapsto>w B <=program"
by (unfold LeadsTo_def, auto)
(*** Specialized laws for handling invariants ***)
(** Conjoining an Always property **)
-lemma Always_LeadsTo_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) LeadsTo A') \<longleftrightarrow> (F \<in> A LeadsTo A')"
+lemma Always_LeadsTo_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) \<longmapsto>w A') \<longleftrightarrow> (F \<in> A \<longmapsto>w A')"
by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
-lemma Always_LeadsTo_post: "F \<in> Always(I) ==> (F \<in> A LeadsTo (I \<inter> A')) \<longleftrightarrow> (F \<in> A LeadsTo A')"
+lemma Always_LeadsTo_post: "F \<in> Always(I) ==> (F \<in> A \<longmapsto>w (I \<inter> A')) \<longleftrightarrow> (F \<in> A \<longmapsto>w A')"
apply (unfold LeadsTo_def)
apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2)
done
(* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *)
-lemma Always_LeadsToI: "[| F \<in> Always(C); F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A'"
+lemma Always_LeadsToI: "[| F \<in> Always(C); F \<in> (C \<inter> A) \<longmapsto>w A' |] ==> F \<in> A \<longmapsto>w A'"
by (blast intro: Always_LeadsTo_pre [THEN iffD1])
(* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *)
-lemma Always_LeadsToD: "[| F \<in> Always(C); F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (C \<inter> A')"
+lemma Always_LeadsToD: "[| F \<in> Always(C); F \<in> A \<longmapsto>w A' |] ==> F \<in> A \<longmapsto>w (C \<inter> A')"
by (blast intro: Always_LeadsTo_post [THEN iffD2])
(*** Introduction rules \<in> Basis, Trans, Union ***)
-lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A LeadsTo B"
+lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A \<longmapsto>w B"
by (auto simp add: Ensures_def LeadsTo_def)
lemma LeadsTo_Trans:
- "[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |] ==> F \<in> A LeadsTo C"
+ "[| F \<in> A \<longmapsto>w B; F \<in> B \<longmapsto>w C |] ==> F \<in> A \<longmapsto>w C"
apply (simp (no_asm_use) add: LeadsTo_def)
apply (blast intro: leadsTo_Trans)
done
lemma LeadsTo_Union:
-"[|(!!A. A \<in> S ==> F \<in> A LeadsTo B); F \<in> program|]==>F \<in> \<Union>(S) LeadsTo B"
+"[|(!!A. A \<in> S ==> F \<in> A \<longmapsto>w B); F \<in> program|]==>F \<in> \<Union>(S) \<longmapsto>w B"
apply (simp add: LeadsTo_def)
apply (subst Int_Union_Union2)
apply (rule leadsTo_UN, auto)
@@ -76,23 +72,23 @@
(*** Derived rules ***)
-lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"
+lemma leadsTo_imp_LeadsTo: "F \<in> A \<longmapsto> B ==> F \<in> A \<longmapsto>w B"
apply (frule leadsToD2, clarify)
apply (simp (no_asm_simp) add: LeadsTo_eq)
apply (blast intro: leadsTo_weaken_L)
done
(*Useful with cancellation, disjunction*)
-lemma LeadsTo_Un_duplicate: "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'"
+lemma LeadsTo_Un_duplicate: "F \<in> A \<longmapsto>w (A' \<union> A') ==> F \<in> A \<longmapsto>w A'"
by (simp add: Un_ac)
lemma LeadsTo_Un_duplicate2:
- "F \<in> A LeadsTo (A' \<union> C \<union> C) ==> F \<in> A LeadsTo (A' \<union> C)"
+ "F \<in> A \<longmapsto>w (A' \<union> C \<union> C) ==> F \<in> A \<longmapsto>w (A' \<union> C)"
by (simp add: Un_ac)
lemma LeadsTo_UN:
- "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo B); F \<in> program|]
- ==>F:(\<Union>i \<in> I. A(i)) LeadsTo B"
+ "[|(!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w B); F \<in> program|]
+ ==>F:(\<Union>i \<in> I. A(i)) \<longmapsto>w B"
apply (simp add: LeadsTo_def)
apply (simp (no_asm_simp) del: UN_simps add: Int_UN_distrib)
apply (rule leadsTo_UN, auto)
@@ -100,7 +96,7 @@
(*Binary union introduction rule*)
lemma LeadsTo_Un:
- "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
+ "[| F \<in> A \<longmapsto>w C; F \<in> B \<longmapsto>w C |] ==> F \<in> (A \<union> B) \<longmapsto>w C"
apply (subst Un_eq_Union)
apply (rule LeadsTo_Union)
apply (auto dest: LeadsTo_type [THEN subsetD])
@@ -108,63 +104,63 @@
(*Lets us look at the starting state*)
lemma single_LeadsTo_I:
- "[|(!!s. s \<in> A ==> F:{s} LeadsTo B); F \<in> program|]==>F \<in> A LeadsTo B"
+ "[|(!!s. s \<in> A ==> F:{s} \<longmapsto>w B); F \<in> program|]==>F \<in> A \<longmapsto>w B"
apply (subst UN_singleton [symmetric], rule LeadsTo_UN, auto)
done
-lemma subset_imp_LeadsTo: "[| A \<subseteq> B; F \<in> program |] ==> F \<in> A LeadsTo B"
+lemma subset_imp_LeadsTo: "[| A \<subseteq> B; F \<in> program |] ==> F \<in> A \<longmapsto>w B"
apply (simp (no_asm_simp) add: LeadsTo_def)
apply (blast intro: subset_imp_leadsTo)
done
-lemma empty_LeadsTo: "F \<in> 0 LeadsTo A \<longleftrightarrow> F \<in> program"
+lemma empty_LeadsTo: "F \<in> 0 \<longmapsto>w A \<longleftrightarrow> F \<in> program"
by (auto dest: LeadsTo_type [THEN subsetD]
intro: empty_subsetI [THEN subset_imp_LeadsTo])
declare empty_LeadsTo [iff]
-lemma LeadsTo_state: "F \<in> A LeadsTo state \<longleftrightarrow> F \<in> program"
+lemma LeadsTo_state: "F \<in> A \<longmapsto>w state \<longleftrightarrow> F \<in> program"
by (auto dest: LeadsTo_type [THEN subsetD] simp add: LeadsTo_eq)
declare LeadsTo_state [iff]
-lemma LeadsTo_weaken_R: "[| F \<in> A LeadsTo A'; A'<=B'|] ==> F \<in> A LeadsTo B'"
+lemma LeadsTo_weaken_R: "[| F \<in> A \<longmapsto>w A'; A'<=B'|] ==> F \<in> A \<longmapsto>w B'"
apply (unfold LeadsTo_def)
apply (auto intro: leadsTo_weaken_R)
done
-lemma LeadsTo_weaken_L: "[| F \<in> A LeadsTo A'; B \<subseteq> A |] ==> F \<in> B LeadsTo A'"
+lemma LeadsTo_weaken_L: "[| F \<in> A \<longmapsto>w A'; B \<subseteq> A |] ==> F \<in> B \<longmapsto>w A'"
apply (unfold LeadsTo_def)
apply (auto intro: leadsTo_weaken_L)
done
-lemma LeadsTo_weaken: "[| F \<in> A LeadsTo A'; B<=A; A'<=B' |] ==> F \<in> B LeadsTo B'"
+lemma LeadsTo_weaken: "[| F \<in> A \<longmapsto>w A'; B<=A; A'<=B' |] ==> F \<in> B \<longmapsto>w B'"
by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans)
lemma Always_LeadsTo_weaken:
-"[| F \<in> Always(C); F \<in> A LeadsTo A'; C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |]
- ==> F \<in> B LeadsTo B'"
+"[| F \<in> Always(C); F \<in> A \<longmapsto>w A'; C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |]
+ ==> F \<in> B \<longmapsto>w B'"
apply (blast dest: Always_LeadsToI intro: LeadsTo_weaken Always_LeadsToD)
done
(** Two theorems for "proof lattices" **)
-lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F:(A \<union> B) LeadsTo B"
+lemma LeadsTo_Un_post: "F \<in> A \<longmapsto>w B ==> F:(A \<union> B) \<longmapsto>w B"
by (blast dest: LeadsTo_type [THEN subsetD]
intro: LeadsTo_Un subset_imp_LeadsTo)
-lemma LeadsTo_Trans_Un: "[| F \<in> A LeadsTo B; F \<in> B LeadsTo C |]
- ==> F \<in> (A \<union> B) LeadsTo C"
+lemma LeadsTo_Trans_Un: "[| F \<in> A \<longmapsto>w B; F \<in> B \<longmapsto>w C |]
+ ==> F \<in> (A \<union> B) \<longmapsto>w C"
apply (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
done
(** Distributive laws **)
-lemma LeadsTo_Un_distrib: "(F \<in> (A \<union> B) LeadsTo C) \<longleftrightarrow> (F \<in> A LeadsTo C & F \<in> B LeadsTo C)"
+lemma LeadsTo_Un_distrib: "(F \<in> (A \<union> B) \<longmapsto>w C) \<longleftrightarrow> (F \<in> A \<longmapsto>w C & F \<in> B \<longmapsto>w C)"
by (blast intro: LeadsTo_Un LeadsTo_weaken_L)
-lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) LeadsTo B) \<longleftrightarrow> (\<forall>i \<in> I. F \<in> A(i) LeadsTo B) & F \<in> program"
+lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) \<longmapsto>w B) \<longleftrightarrow> (\<forall>i \<in> I. F \<in> A(i) \<longmapsto>w B) & F \<in> program"
by (blast dest: LeadsTo_type [THEN subsetD]
intro: LeadsTo_UN LeadsTo_weaken_L)
-lemma LeadsTo_Union_distrib: "(F \<in> \<Union>(S) LeadsTo B) \<longleftrightarrow> (\<forall>A \<in> S. F \<in> A LeadsTo B) & F \<in> program"
+lemma LeadsTo_Union_distrib: "(F \<in> \<Union>(S) \<longmapsto>w B) \<longleftrightarrow> (\<forall>A \<in> S. F \<in> A \<longmapsto>w B) & F \<in> program"
by (blast dest: LeadsTo_type [THEN subsetD]
intro: LeadsTo_Union LeadsTo_weaken_L)
@@ -177,7 +173,7 @@
lemma Always_LeadsTo_Basis: "[| F \<in> Always(I); F \<in> (I \<inter> (A-A')) Co (A \<union> A');
F \<in> transient (I \<inter> (A-A')) |]
- ==> F \<in> A LeadsTo A'"
+ ==> F \<in> A \<longmapsto>w A'"
apply (rule Always_LeadsToI, assumption)
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
done
@@ -185,36 +181,36 @@
(*Set difference: maybe combine with leadsTo_weaken_L??
This is the most useful form of the "disjunction" rule*)
lemma LeadsTo_Diff:
- "[| F \<in> (A-B) LeadsTo C; F \<in> (A \<inter> B) LeadsTo C |] ==> F \<in> A LeadsTo C"
+ "[| F \<in> (A-B) \<longmapsto>w C; F \<in> (A \<inter> B) \<longmapsto>w C |] ==> F \<in> A \<longmapsto>w C"
by (blast intro: LeadsTo_Un LeadsTo_weaken)
lemma LeadsTo_UN_UN:
- "[|(!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i)); F \<in> program |]
- ==> F \<in> (\<Union>i \<in> I. A(i)) LeadsTo (\<Union>i \<in> I. A'(i))"
+ "[|(!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w A'(i)); F \<in> program |]
+ ==> F \<in> (\<Union>i \<in> I. A(i)) \<longmapsto>w (\<Union>i \<in> I. A'(i))"
apply (rule LeadsTo_Union, auto)
apply (blast intro: LeadsTo_weaken_R)
done
(*Binary union version*)
lemma LeadsTo_Un_Un:
- "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |] ==> F:(A \<union> B) LeadsTo (A' \<union> B')"
+ "[| F \<in> A \<longmapsto>w A'; F \<in> B \<longmapsto>w B' |] ==> F:(A \<union> B) \<longmapsto>w (A' \<union> B')"
by (blast intro: LeadsTo_Un LeadsTo_weaken_R)
(** The cancellation law **)
-lemma LeadsTo_cancel2: "[| F \<in> A LeadsTo(A' \<union> B); F \<in> B LeadsTo B' |] ==> F \<in> A LeadsTo (A' \<union> B')"
+lemma LeadsTo_cancel2: "[| F \<in> A \<longmapsto>w(A' \<union> B); F \<in> B \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (A' \<union> B')"
by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans dest: LeadsTo_type [THEN subsetD])
lemma Un_Diff: "A \<union> (B - A) = A \<union> B"
by auto
-lemma LeadsTo_cancel_Diff2: "[| F \<in> A LeadsTo (A' \<union> B); F \<in> (B-A') LeadsTo B' |] ==> F \<in> A LeadsTo (A' \<union> B')"
+lemma LeadsTo_cancel_Diff2: "[| F \<in> A \<longmapsto>w (A' \<union> B); F \<in> (B-A') \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (A' \<union> B')"
apply (rule LeadsTo_cancel2)
prefer 2 apply assumption
apply (simp (no_asm_simp) add: Un_Diff)
done
-lemma LeadsTo_cancel1: "[| F \<in> A LeadsTo (B \<union> A'); F \<in> B LeadsTo B' |] ==> F \<in> A LeadsTo (B' \<union> A')"
+lemma LeadsTo_cancel1: "[| F \<in> A \<longmapsto>w (B \<union> A'); F \<in> B \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (B' \<union> A')"
apply (simp add: Un_commute)
apply (blast intro!: LeadsTo_cancel2)
done
@@ -222,7 +218,7 @@
lemma Diff_Un2: "(B - A) \<union> A = B \<union> A"
by auto
-lemma LeadsTo_cancel_Diff1: "[| F \<in> A LeadsTo (B \<union> A'); F \<in> (B-A') LeadsTo B' |] ==> F \<in> A LeadsTo (B' \<union> A')"
+lemma LeadsTo_cancel_Diff1: "[| F \<in> A \<longmapsto>w (B \<union> A'); F \<in> (B-A') \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (B' \<union> A')"
apply (rule LeadsTo_cancel1)
prefer 2 apply assumption
apply (simp (no_asm_simp) add: Diff_Un2)
@@ -231,7 +227,7 @@
(** The impossibility law **)
(*The set "A" may be non-empty, but it contains no reachable states*)
-lemma LeadsTo_empty: "F \<in> A LeadsTo 0 ==> F \<in> Always (state -A)"
+lemma LeadsTo_empty: "F \<in> A \<longmapsto>w 0 ==> F \<in> Always (state -A)"
apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable)
apply (cut_tac reachable_type)
apply (auto dest!: leadsTo_empty)
@@ -240,26 +236,26 @@
(** PSP \<in> Progress-Safety-Progress **)
(*Special case of PSP \<in> Misra's "stable conjunction"*)
-lemma PSP_Stable: "[| F \<in> A LeadsTo A'; F \<in> Stable(B) |]==> F:(A \<inter> B) LeadsTo (A' \<inter> B)"
+lemma PSP_Stable: "[| F \<in> A \<longmapsto>w A'; F \<in> Stable(B) |]==> F:(A \<inter> B) \<longmapsto>w (A' \<inter> B)"
apply (simp add: LeadsTo_def Stable_eq_stable, clarify)
apply (drule psp_stable, assumption)
apply (simp add: Int_ac)
done
-lemma PSP_Stable2: "[| F \<in> A LeadsTo A'; F \<in> Stable(B) |] ==> F \<in> (B \<inter> A) LeadsTo (B \<inter> A')"
+lemma PSP_Stable2: "[| F \<in> A \<longmapsto>w A'; F \<in> Stable(B) |] ==> F \<in> (B \<inter> A) \<longmapsto>w (B \<inter> A')"
apply (simp (no_asm_simp) add: PSP_Stable Int_ac)
done
-lemma PSP: "[| F \<in> A LeadsTo A'; F \<in> B Co B'|]==> F \<in> (A \<inter> B') LeadsTo ((A' \<inter> B) \<union> (B' - B))"
+lemma PSP: "[| F \<in> A \<longmapsto>w A'; F \<in> B Co B'|]==> F \<in> (A \<inter> B') \<longmapsto>w ((A' \<inter> B) \<union> (B' - B))"
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains)
apply (blast dest: psp intro: leadsTo_weaken)
done
-lemma PSP2: "[| F \<in> A LeadsTo A'; F \<in> B Co B' |]==> F:(B' \<inter> A) LeadsTo ((B \<inter> A') \<union> (B' - B))"
+lemma PSP2: "[| F \<in> A \<longmapsto>w A'; F \<in> B Co B' |]==> F:(B' \<inter> A) \<longmapsto>w ((B \<inter> A') \<union> (B' - B))"
by (simp (no_asm_simp) add: PSP Int_ac)
lemma PSP_Unless:
-"[| F \<in> A LeadsTo A'; F \<in> B Unless B'|]==> F:(A \<inter> B) LeadsTo ((A' \<inter> B) \<union> B')"
+"[| F \<in> A \<longmapsto>w A'; F \<in> B Unless B'|]==> F:(A \<inter> B) \<longmapsto>w ((A' \<inter> B) \<union> B')"
apply (unfold op_Unless_def)
apply (drule PSP, assumption)
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo)
@@ -269,10 +265,10 @@
(** Meta or object quantifier ????? **)
lemma LeadsTo_wf_induct: "[| wf(r);
- \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) LeadsTo
+ \<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) \<longmapsto>w
((A \<inter> f-``(converse(r) `` {m})) \<union> B);
field(r)<=I; A<=f-``I; F \<in> program |]
- ==> F \<in> A LeadsTo B"
+ ==> F \<in> A \<longmapsto>w B"
apply (simp (no_asm_use) add: LeadsTo_def)
apply auto
apply (erule_tac I = I and f = f in leadsTo_wf_induct, safe)
@@ -282,8 +278,8 @@
done
-lemma LessThan_induct: "[| \<forall>m \<in> nat. F:(A \<inter> f-``{m}) LeadsTo ((A \<inter> f-``m) \<union> B);
- A<=f-``nat; F \<in> program |] ==> F \<in> A LeadsTo B"
+lemma LessThan_induct: "[| \<forall>m \<in> nat. F:(A \<inter> f-``{m}) \<longmapsto>w ((A \<inter> f-``m) \<union> B);
+ A<=f-``nat; F \<in> program |] ==> F \<in> A \<longmapsto>w B"
apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN LeadsTo_wf_induct])
apply (simp_all add: nat_measure_field)
apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric])
@@ -301,18 +297,18 @@
(*** Completion \<in> Binary and General Finite versions ***)
-lemma Completion: "[| 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)"
+lemma Completion: "[| F \<in> A \<longmapsto>w (A' \<union> C); F \<in> A' Co (A' \<union> C);
+ F \<in> B \<longmapsto>w (B' \<union> C); F \<in> B' Co (B' \<union> C) |]
+ ==> F \<in> (A \<inter> B) \<longmapsto>w ((A' \<inter> B') \<union> C)"
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains Int_Un_distrib)
apply (blast intro: completion leadsTo_weaken)
done
lemma Finite_completion_aux:
"[| I \<in> Fin(X);F \<in> program |]
- ==> (\<forall>i \<in> I. F \<in> (A(i)) LeadsTo (A'(i) \<union> C)) \<longrightarrow>
+ ==> (\<forall>i \<in> I. F \<in> (A(i)) \<longmapsto>w (A'(i) \<union> C)) \<longrightarrow>
(\<forall>i \<in> I. F \<in> (A'(i)) Co (A'(i) \<union> C)) \<longrightarrow>
- F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)"
+ F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w ((\<Inter>i \<in> I. A'(i)) \<union> C)"
apply (erule Fin_induct)
apply (auto simp del: INT_simps simp add: Inter_0)
apply (rule Completion, auto)
@@ -321,16 +317,16 @@
done
lemma Finite_completion:
- "[| I \<in> Fin(X); !!i. i \<in> I ==> F \<in> A(i) LeadsTo (A'(i) \<union> C);
+ "[| I \<in> Fin(X); !!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w (A'(i) \<union> C);
!!i. i \<in> I ==> F \<in> A'(i) Co (A'(i) \<union> C);
F \<in> program |]
- ==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)"
+ ==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w ((\<Inter>i \<in> I. A'(i)) \<union> C)"
by (blast intro: Finite_completion_aux [THEN mp, THEN mp])
lemma Stable_completion:
- "[| 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')"
+ "[| F \<in> A \<longmapsto>w A'; F \<in> Stable(A');
+ F \<in> B \<longmapsto>w B'; F \<in> Stable(B') |]
+ ==> F \<in> (A \<inter> B) \<longmapsto>w (A' \<inter> B')"
apply (unfold Stable_def)
apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R])
prefer 5
@@ -340,9 +336,9 @@
lemma Finite_stable_completion:
"[| I \<in> Fin(X);
- (!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i));
+ (!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w A'(i));
(!!i. i \<in> I ==>F \<in> Stable(A'(i))); F \<in> program |]
- ==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo (\<Inter>i \<in> I. A'(i))"
+ ==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w (\<Inter>i \<in> I. A'(i))"
apply (unfold Stable_def)
apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all)
apply (rule_tac [3] subset_refl, auto)