author | paulson |
Tue, 08 Jul 2003 11:44:30 +0200 | |
changeset 14092 | 68da54626309 |
parent 14084 | ccb48f3239f7 |
permissions | -rw-r--r-- |
11479 | 1 |
(* Title: HOL/UNITY/WFair.ML |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
2 |
ID: $Id \\<in> WFair.ML,v 1.13 2003/06/30 16:15:52 paulson Exp $ |
11479 | 3 |
Author: Sidi O Ehmety, Computer Laboratory |
4 |
Copyright 2001 University of Cambridge |
|
5 |
||
6 |
Weak Fairness versions of transient, ensures, leadsTo. |
|
7 |
||
8 |
From Misra, "A Logic for Concurrent Programming", 1994 |
|
9 |
*) |
|
10 |
||
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14060
diff
changeset
|
11 |
(** Ad-hoc set-theory rules **) |
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14060
diff
changeset
|
12 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
13 |
Goal "Union(B) Int A = (\\<Union>b \\<in> B. b Int A)"; |
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14060
diff
changeset
|
14 |
by Auto_tac; |
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14060
diff
changeset
|
15 |
qed "Int_Union_Union"; |
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14060
diff
changeset
|
16 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
17 |
Goal "A Int Union(B) = (\\<Union>b \\<in> B. A Int b)"; |
14084
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14060
diff
changeset
|
18 |
by Auto_tac; |
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14060
diff
changeset
|
19 |
qed "Int_Union_Union2"; |
ccb48f3239f7
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
paulson
parents:
14060
diff
changeset
|
20 |
|
11479 | 21 |
(*** transient ***) |
22 |
||
12195 | 23 |
Goalw [transient_def] "transient(A)<=program"; |
11479 | 24 |
by Auto_tac; |
12195 | 25 |
qed "transient_type"; |
26 |
||
27 |
Goalw [transient_def] |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
28 |
"F \\<in> transient(A) ==> F \\<in> program & st_set(A)"; |
12195 | 29 |
by Auto_tac; |
30 |
qed "transientD2"; |
|
11479 | 31 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
32 |
Goal "[| F \\<in> stable(A); F \\<in> transient(A) |] ==> A = 0"; |
14060
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14054
diff
changeset
|
33 |
by (asm_full_simp_tac (simpset() addsimps [stable_def, constrains_def, transient_def]) 1); |
c0c4af41fa3b
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
paulson
parents:
14054
diff
changeset
|
34 |
by (Fast_tac 1); |
11479 | 35 |
qed "stable_transient_empty"; |
36 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
37 |
Goalw [transient_def, st_set_def] "[|F \\<in> transient(A); B<=A|] ==> F \\<in> transient(B)"; |
11479 | 38 |
by Safe_tac; |
39 |
by (res_inst_tac [("x", "act")] bexI 1); |
|
40 |
by (ALLGOALS(Asm_full_simp_tac)); |
|
41 |
by (Blast_tac 1); |
|
12195 | 42 |
by Auto_tac; |
11479 | 43 |
qed "transient_strengthen"; |
44 |
||
12195 | 45 |
Goalw [transient_def] |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
46 |
"[|act \\<in> Acts(F); A <= domain(act); act``A <= state-A; \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
47 |
\ F \\<in> program; st_set(A)|] ==> F \\<in> transient(A)"; |
11479 | 48 |
by (Blast_tac 1); |
49 |
qed "transientI"; |
|
50 |
||
51 |
val major::prems = |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
52 |
Goalw [transient_def] "[| F \\<in> transient(A); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
53 |
\ !!act. [| act \\<in> Acts(F); A <= domain(act); act``A <= state-A|]==>P|]==>P"; |
11479 | 54 |
by (rtac (major RS CollectE) 1); |
55 |
by (blast_tac (claset() addIs prems) 1); |
|
56 |
qed "transientE"; |
|
57 |
||
58 |
Goalw [transient_def] "transient(state) = 0"; |
|
59 |
by (rtac equalityI 1); |
|
60 |
by (ALLGOALS(Clarify_tac)); |
|
12195 | 61 |
by (cut_inst_tac [("F", "x")] Acts_type 1); |
11479 | 62 |
by (asm_full_simp_tac (simpset() addsimps [Diff_cancel]) 1); |
14046 | 63 |
by (auto_tac (claset() addIs [st0_in_state], simpset())); |
11479 | 64 |
qed "transient_state"; |
65 |
||
12195 | 66 |
Goalw [transient_def,st_set_def] "state<=B ==> transient(B) = 0"; |
67 |
by (rtac equalityI 1); |
|
68 |
by (ALLGOALS(Clarify_tac)); |
|
69 |
by (cut_inst_tac [("F", "x")] Acts_type 1); |
|
70 |
by (asm_full_simp_tac (simpset() addsimps [Diff_cancel]) 1); |
|
71 |
by (subgoal_tac "B=state" 1); |
|
14046 | 72 |
by (auto_tac (claset() addIs [st0_in_state], simpset())); |
12195 | 73 |
qed "transient_state2"; |
74 |
||
11479 | 75 |
Goalw [transient_def] "transient(0) = program"; |
76 |
by (rtac equalityI 1); |
|
12195 | 77 |
by Auto_tac; |
11479 | 78 |
qed "transient_empty"; |
79 |
||
12195 | 80 |
Addsimps [transient_empty, transient_state, transient_state2]; |
11479 | 81 |
|
82 |
(*** ensures ***) |
|
83 |
||
12195 | 84 |
Goalw [ensures_def, constrains_def] "A ensures B <=program"; |
85 |
by Auto_tac; |
|
86 |
qed "ensures_type"; |
|
87 |
||
11479 | 88 |
Goalw [ensures_def] |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
89 |
"[|F:(A-B) co (A Un B); F \\<in> transient(A-B)|]==>F \\<in> A ensures B"; |
12195 | 90 |
by (auto_tac (claset(), simpset() addsimps [transient_type RS subsetD])); |
11479 | 91 |
qed "ensuresI"; |
92 |
||
12195 | 93 |
(* Added by Sidi, from Misra's notes, Progress chapter, exercise 4 *) |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
94 |
Goal "[| F \\<in> A co A Un B; F \\<in> transient(A) |] ==> F \\<in> A ensures B"; |
11479 | 95 |
by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1); |
96 |
by (dres_inst_tac [("B", "A-B")] transient_strengthen 2); |
|
12195 | 97 |
by (auto_tac (claset(), simpset() addsimps [ensures_def, transient_type RS subsetD])); |
11479 | 98 |
qed "ensuresI2"; |
99 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
100 |
Goalw [ensures_def] "F \\<in> A ensures B ==> F:(A-B) co (A Un B) & F \\<in> transient (A-B)"; |
12195 | 101 |
by Auto_tac; |
11479 | 102 |
qed "ensuresD"; |
103 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
104 |
Goalw [ensures_def] "[|F \\<in> A ensures A'; A'<=B' |] ==> F \\<in> A ensures B'"; |
11479 | 105 |
by (blast_tac (claset() |
12195 | 106 |
addIs [transient_strengthen, constrains_weaken]) 1); |
11479 | 107 |
qed "ensures_weaken_R"; |
108 |
||
12215
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
109 |
(*The L-version (precondition strengthening) fails, but we have this*) |
12220 | 110 |
Goalw [ensures_def] |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
111 |
"[| F \\<in> stable(C); F \\<in> A ensures B |] ==> F:(C Int A) ensures (C Int B)"; |
12220 | 112 |
by (simp_tac (simpset() addsimps [Int_Un_distrib RS sym, |
113 |
Diff_Int_distrib RS sym]) 1); |
|
11479 | 114 |
by (blast_tac (claset() |
115 |
addIs [transient_strengthen, |
|
12195 | 116 |
stable_constrains_Int, constrains_weaken]) 1); |
11479 | 117 |
qed "stable_ensures_Int"; |
118 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
119 |
Goal "[|F \\<in> stable(A); F \\<in> transient(C); A<=B Un C|] ==> F \\<in> A ensures B"; |
12195 | 120 |
by (forward_tac [stable_type RS subsetD] 1); |
121 |
by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1); |
|
11479 | 122 |
by (Clarify_tac 1); |
123 |
by (blast_tac (claset() addIs [transient_strengthen, |
|
12195 | 124 |
constrains_weaken]) 1); |
11479 | 125 |
qed "stable_transient_ensures"; |
126 |
||
127 |
Goal "(A ensures B) = (A unless B) Int transient (A-B)"; |
|
12195 | 128 |
by (auto_tac (claset(), simpset() addsimps [ensures_def, unless_def])); |
11479 | 129 |
qed "ensures_eq"; |
130 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
131 |
Goal "[| F \\<in> program; A<=B |] ==> F \\<in> A ensures B"; |
12195 | 132 |
by (rewrite_goal_tac [ensures_def,constrains_def,transient_def, st_set_def] 1); |
133 |
by Auto_tac; |
|
134 |
qed "subset_imp_ensures"; |
|
135 |
||
11479 | 136 |
(*** leadsTo ***) |
12195 | 137 |
val leads_left = leads.dom_subset RS subsetD RS SigmaD1; |
138 |
val leads_right = leads.dom_subset RS subsetD RS SigmaD2; |
|
11479 | 139 |
|
12195 | 140 |
Goalw [leadsTo_def] "A leadsTo B <= program"; |
141 |
by Auto_tac; |
|
142 |
qed "leadsTo_type"; |
|
143 |
||
144 |
Goalw [leadsTo_def, st_set_def] |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
145 |
"F \\<in> A leadsTo B ==> F \\<in> program & st_set(A) & st_set(B)"; |
12195 | 146 |
by (blast_tac (claset() addDs [leads_left, leads_right]) 1); |
147 |
qed "leadsToD2"; |
|
11479 | 148 |
|
12195 | 149 |
Goalw [leadsTo_def, st_set_def] |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
150 |
"[|F \\<in> A ensures B; st_set(A); st_set(B)|] ==> F \\<in> A leadsTo B"; |
12195 | 151 |
by (cut_facts_tac [ensures_type] 1); |
152 |
by (auto_tac (claset() addIs [leads.Basis], simpset())); |
|
11479 | 153 |
qed "leadsTo_Basis"; |
12195 | 154 |
AddIs [leadsTo_Basis]; |
11479 | 155 |
|
12195 | 156 |
(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *) |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
157 |
(* [| F \\<in> program; A<=B; st_set(A); st_set(B) |] ==> A leadsTo B *) |
12195 | 158 |
bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); |
11479 | 159 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
160 |
Goalw [leadsTo_def] "[|F \\<in> A leadsTo B; F \\<in> B leadsTo C |]==>F \\<in> A leadsTo C"; |
12195 | 161 |
by (auto_tac (claset() addIs [leads.Trans], simpset())); |
11479 | 162 |
qed "leadsTo_Trans"; |
163 |
||
12195 | 164 |
(* Better when used in association with leadsTo_weaken_R *) |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
165 |
Goalw [transient_def] "F \\<in> transient(A) ==> F \\<in> A leadsTo (state-A )"; |
11479 | 166 |
by (rtac (ensuresI RS leadsTo_Basis) 1); |
167 |
by (ALLGOALS(Clarify_tac)); |
|
168 |
by (blast_tac (claset() addIs [transientI]) 2); |
|
169 |
by (rtac constrains_weaken 1); |
|
170 |
by Auto_tac; |
|
171 |
qed "transient_imp_leadsTo"; |
|
172 |
||
173 |
(*Useful with cancellation, disjunction*) |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
174 |
Goal "F \\<in> A leadsTo (A' Un A') ==> F \\<in> A leadsTo A'"; |
12220 | 175 |
by (Asm_full_simp_tac 1); |
11479 | 176 |
qed "leadsTo_Un_duplicate"; |
177 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
178 |
Goal "F \\<in> A leadsTo (A' Un C Un C) ==> F \\<in> A leadsTo (A' Un C)"; |
11479 | 179 |
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
180 |
qed "leadsTo_Un_duplicate2"; |
|
181 |
||
12220 | 182 |
(*The Union introduction rule as we should have liked to state it*) |
12195 | 183 |
val [major, program,B]= Goalw [leadsTo_def, st_set_def] |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
184 |
"[|(!!A. A \\<in> S ==> F \\<in> A leadsTo B); F \\<in> program; st_set(B)|]==>F \\<in> Union(S) leadsTo B"; |
12195 | 185 |
by (cut_facts_tac [program, B] 1); |
186 |
by Auto_tac; |
|
187 |
by (rtac leads.Union 1); |
|
188 |
by Auto_tac; |
|
189 |
by (ALLGOALS(dtac major)); |
|
190 |
by (auto_tac (claset() addDs [leads_left], simpset())); |
|
191 |
qed "leadsTo_Union"; |
|
11479 | 192 |
|
12215
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
193 |
val [major,program,B] = Goalw [leadsTo_def, st_set_def] |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
194 |
"[|(!!A. A \\<in> S ==>F:(A Int C) leadsTo B); F \\<in> program; st_set(B)|] \ |
12215
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
195 |
\ ==>F:(Union(S)Int C)leadsTo B"; |
12195 | 196 |
by (cut_facts_tac [program, B] 1); |
12215
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
197 |
by (asm_simp_tac (simpset() delsimps UN_simps addsimps [Int_Union_Union]) 1); |
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
198 |
by (resolve_tac [leads.Union] 1); |
12195 | 199 |
by Auto_tac; |
200 |
by (ALLGOALS(dtac major)); |
|
201 |
by (auto_tac (claset() addDs [leads_left], simpset())); |
|
202 |
qed "leadsTo_Union_Int"; |
|
11479 | 203 |
|
12195 | 204 |
val [major,program,B] = Goalw [leadsTo_def, st_set_def] |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
205 |
"[|(!!i. i \\<in> I ==> F \\<in> A(i) leadsTo B); F \\<in> program; st_set(B)|]==>F:(\\<Union>i \\<in> I. A(i)) leadsTo B"; |
12195 | 206 |
by (cut_facts_tac [program, B] 1); |
207 |
by (asm_simp_tac (simpset() addsimps [Int_Union_Union]) 1); |
|
208 |
by (rtac leads.Union 1); |
|
209 |
by Auto_tac; |
|
210 |
by (ALLGOALS(dtac major)); |
|
211 |
by (auto_tac (claset() addDs [leads_left], simpset())); |
|
212 |
qed "leadsTo_UN"; |
|
11479 | 213 |
|
12195 | 214 |
(* Binary union introduction rule *) |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
215 |
Goal "[| F \\<in> A leadsTo C; F \\<in> B leadsTo C |] ==> F \\<in> (A Un B) leadsTo C"; |
11479 | 216 |
by (stac Un_eq_Union 1); |
12195 | 217 |
by (blast_tac (claset() addIs [leadsTo_Union] addDs [leadsToD2]) 1); |
11479 | 218 |
qed "leadsTo_Un"; |
219 |
||
12195 | 220 |
val [major, program, B] = Goal |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
221 |
"[|(!!x. x \\<in> A==> F:{x} leadsTo B); F \\<in> program; st_set(B) |] ==> F \\<in> A leadsTo B"; |
12195 | 222 |
by (res_inst_tac [("b", "A")] (UN_singleton RS subst) 1); |
223 |
by (rtac leadsTo_UN 1); |
|
224 |
by (auto_tac (claset() addDs prems, simpset() addsimps [major, program, B])); |
|
225 |
qed "single_leadsTo_I"; |
|
226 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
227 |
Goal "[| F \\<in> program; st_set(A) |] ==> F \\<in> A leadsTo A"; |
12195 | 228 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
229 |
qed "leadsTo_refl"; |
|
230 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
231 |
Goal "F \\<in> A leadsTo A <-> F \\<in> program & st_set(A)"; |
12195 | 232 |
by (auto_tac (claset() addIs [leadsTo_refl] |
233 |
addDs [leadsToD2], simpset())); |
|
234 |
qed "leadsTo_refl_iff"; |
|
235 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
236 |
Goal "F \\<in> 0 leadsTo B <-> (F \\<in> program & st_set(B))"; |
12195 | 237 |
by (auto_tac (claset() addIs [subset_imp_leadsTo] |
238 |
addDs [leadsToD2], simpset())); |
|
239 |
qed "empty_leadsTo"; |
|
240 |
AddIffs [empty_leadsTo]; |
|
241 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
242 |
Goal "F \\<in> A leadsTo state <-> (F \\<in> program & st_set(A))"; |
12195 | 243 |
by (auto_tac (claset() addIs [subset_imp_leadsTo] |
244 |
addDs [leadsToD2, st_setD], simpset())); |
|
245 |
qed "leadsTo_state"; |
|
246 |
AddIffs [leadsTo_state]; |
|
247 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
248 |
Goal "[| F \\<in> A leadsTo A'; A'<=B'; st_set(B') |] ==> F \\<in> A leadsTo B'"; |
12195 | 249 |
by (blast_tac (claset() addDs [leadsToD2] |
250 |
addIs [subset_imp_leadsTo,leadsTo_Trans]) 1); |
|
251 |
qed "leadsTo_weaken_R"; |
|
252 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
253 |
Goal "[| F \\<in> A leadsTo A'; B<=A |] ==> F \\<in> B leadsTo A'"; |
12484 | 254 |
by (ftac leadsToD2 1); |
12195 | 255 |
by (blast_tac (claset() addIs [leadsTo_Trans,subset_imp_leadsTo, st_set_subset]) 1); |
256 |
qed_spec_mp "leadsTo_weaken_L"; |
|
257 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
258 |
Goal "[| F \\<in> A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F \\<in> B leadsTo B'"; |
12484 | 259 |
by (ftac leadsToD2 1); |
12195 | 260 |
by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L, |
261 |
leadsTo_Trans, leadsTo_refl]) 1); |
|
262 |
qed "leadsTo_weaken"; |
|
263 |
||
264 |
(* This rule has a nicer conclusion *) |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
265 |
Goal "[| F \\<in> transient(A); state-A<=B; st_set(B)|] ==> F \\<in> A leadsTo B"; |
12484 | 266 |
by (ftac transientD2 1); |
12195 | 267 |
by (rtac leadsTo_weaken_R 1); |
268 |
by (auto_tac (claset(), simpset() addsimps [transient_imp_leadsTo])); |
|
269 |
qed "transient_imp_leadsTo2"; |
|
270 |
||
271 |
(*Distributes over binary unions*) |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
272 |
Goal "F:(A Un B) leadsTo C <-> (F \\<in> A leadsTo C & F \\<in> B leadsTo C)"; |
12195 | 273 |
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); |
274 |
qed "leadsTo_Un_distrib"; |
|
275 |
||
276 |
Goal |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
277 |
"(F:(\\<Union>i \\<in> I. A(i)) leadsTo B)<-> ((\\<forall>i \\<in> I. F \\<in> A(i) leadsTo B) & F \\<in> program & st_set(B))"; |
12195 | 278 |
by (blast_tac (claset() addDs [leadsToD2] |
279 |
addIs [leadsTo_UN, leadsTo_weaken_L]) 1); |
|
280 |
qed "leadsTo_UN_distrib"; |
|
281 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
282 |
Goal "(F \\<in> Union(S) leadsTo B) <-> (\\<forall>A \\<in> S. F \\<in> A leadsTo B) & F \\<in> program & st_set(B)"; |
12195 | 283 |
by (blast_tac (claset() addDs [leadsToD2] |
284 |
addIs [leadsTo_Union, leadsTo_weaken_L]) 1); |
|
285 |
qed "leadsTo_Union_distrib"; |
|
286 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
287 |
(*Set difference \\<in> maybe combine with leadsTo_weaken_L?*) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
288 |
Goal "[| F: (A-B) leadsTo C; F \\<in> B leadsTo C; st_set(C) |] ==> F \\<in> A leadsTo C"; |
12195 | 289 |
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken] |
290 |
addDs [leadsToD2]) 1); |
|
291 |
qed "leadsTo_Diff"; |
|
292 |
||
293 |
val [major,minor] = Goal |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
294 |
"[|(!!i. i \\<in> I ==> F \\<in> A(i) leadsTo A'(i)); F \\<in> program |] \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
295 |
\ ==> F: (\\<Union>i \\<in> I. A(i)) leadsTo (\\<Union>i \\<in> I. A'(i))"; |
12195 | 296 |
by (rtac leadsTo_Union 1); |
297 |
by (ALLGOALS(Asm_simp_tac)); |
|
298 |
by Safe_tac; |
|
299 |
by (simp_tac (simpset() addsimps [minor]) 2); |
|
300 |
by (blast_tac (claset() addDs [leadsToD2, major])2); |
|
301 |
by (blast_tac (claset() addIs [leadsTo_weaken_R] addDs [major, leadsToD2]) 1); |
|
302 |
qed "leadsTo_UN_UN"; |
|
303 |
||
304 |
(*Binary union version*) |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
305 |
Goal "[| F \\<in> A leadsTo A'; F \\<in> B leadsTo B' |] ==> F \\<in> (A Un B) leadsTo (A' Un B')"; |
12195 | 306 |
by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B')" 1); |
307 |
by (blast_tac (claset() addDs [leadsToD2]) 2); |
|
308 |
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_R]) 1); |
|
309 |
qed "leadsTo_Un_Un"; |
|
310 |
||
311 |
(** The cancellation law **) |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
312 |
Goal "[|F \\<in> A leadsTo (A' Un B); F \\<in> B leadsTo B'|] ==> F \\<in> A leadsTo (A' Un B')"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
313 |
by (subgoal_tac "st_set(A) & st_set(A') & st_set(B) & st_set(B') &F \\<in> program" 1); |
12195 | 314 |
by (blast_tac (claset() addDs [leadsToD2]) 2); |
315 |
by (blast_tac (claset() addIs [leadsTo_Trans, leadsTo_Un_Un, leadsTo_refl]) 1); |
|
316 |
qed "leadsTo_cancel2"; |
|
317 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
318 |
Goal "[|F \\<in> A leadsTo (A' Un B); F \\<in> (B-A') leadsTo B'|]==> F \\<in> A leadsTo (A' Un B')"; |
12195 | 319 |
by (rtac leadsTo_cancel2 1); |
320 |
by (assume_tac 2); |
|
321 |
by (blast_tac (claset() addDs [leadsToD2] addIs [leadsTo_weaken_R]) 1); |
|
322 |
qed "leadsTo_cancel_Diff2"; |
|
323 |
||
11479 | 324 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
325 |
Goal "[| F \\<in> A leadsTo (B Un A'); F \\<in> B leadsTo B' |] ==> F \\<in> A leadsTo (B' Un A')"; |
12195 | 326 |
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); |
327 |
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1); |
|
328 |
qed "leadsTo_cancel1"; |
|
11479 | 329 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
330 |
Goal "[|F \\<in> A leadsTo (B Un A'); F: (B-A') leadsTo B'|]==> F \\<in> A leadsTo (B' Un A')"; |
12195 | 331 |
by (rtac leadsTo_cancel1 1); |
332 |
by (assume_tac 2); |
|
333 |
by (blast_tac (claset() addIs [leadsTo_weaken_R] addDs [leadsToD2]) 1); |
|
334 |
qed "leadsTo_cancel_Diff1"; |
|
11479 | 335 |
|
336 |
(*The INDUCTION rule as we should have liked to state it*) |
|
12195 | 337 |
val [major, basis_prem, trans_prem, union_prem] = Goalw [leadsTo_def, st_set_def] |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
338 |
"[| F \\<in> za leadsTo zb; \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
339 |
\ !!A B. [| F \\<in> A ensures B; st_set(A); st_set(B) |] ==> P(A, B); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
340 |
\ !!A B C. [| F \\<in> A leadsTo B; P(A, B); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
341 |
\ F \\<in> B leadsTo C; P(B, C) |] \ |
11479 | 342 |
\ ==> P(A, C); \ |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
343 |
\ !!B S. [| \\<forall>A \\<in> S. F \\<in> A leadsTo B; \\<forall>A \\<in> S. P(A, B); st_set(B); \\<forall>A \\<in> S. st_set(A)|] \ |
11479 | 344 |
\ ==> P(Union(S), B) \ |
345 |
\ |] ==> P(za, zb)"; |
|
346 |
by (cut_facts_tac [major] 1); |
|
347 |
by (rtac (major RS CollectD2 RS leads.induct) 1); |
|
12195 | 348 |
by (rtac union_prem 3); |
349 |
by (rtac trans_prem 2); |
|
350 |
by (rtac basis_prem 1); |
|
351 |
by Auto_tac; |
|
11479 | 352 |
qed "leadsTo_induct"; |
353 |
||
12195 | 354 |
(* Added by Sidi, an induction rule without ensures *) |
355 |
val [major,imp_prem,basis_prem,trans_prem,union_prem] = Goal |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
356 |
"[| F \\<in> za leadsTo zb; \ |
12195 | 357 |
\ !!A B. [| A<=B; st_set(B) |] ==> P(A, B); \ |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
358 |
\ !!A B. [| F \\<in> A co A Un B; F \\<in> transient(A); st_set(B) |] ==> P(A, B); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
359 |
\ !!A B C. [| F \\<in> A leadsTo B; P(A, B); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
360 |
\ F \\<in> B leadsTo C; P(B, C) |] \ |
11479 | 361 |
\ ==> P(A, C); \ |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
362 |
\ !!B S. [| \\<forall>A \\<in> S. F \\<in> A leadsTo B; \\<forall>A \\<in> S. P(A, B); st_set(B); \\<forall>A \\<in> S. st_set(A) |] \ |
11479 | 363 |
\ ==> P(Union(S), B) \ |
364 |
\ |] ==> P(za, zb)"; |
|
365 |
by (cut_facts_tac [major] 1); |
|
366 |
by (etac leadsTo_induct 1); |
|
12195 | 367 |
by (auto_tac (claset() addIs [trans_prem,union_prem], simpset())); |
11479 | 368 |
by (rewrite_goal_tac [ensures_def] 1); |
12195 | 369 |
by (Clarify_tac 1); |
12484 | 370 |
by (ftac constrainsD2 1); |
11479 | 371 |
by (dres_inst_tac [("B'", "(A-B) Un B")] constrains_weaken_R 1); |
12195 | 372 |
by (Blast_tac 1); |
11479 | 373 |
by (forward_tac [ensuresI2 RS leadsTo_Basis] 1); |
12195 | 374 |
by (dtac basis_prem 4); |
375 |
by (ALLGOALS(Asm_full_simp_tac)); |
|
376 |
by (forw_inst_tac [("A1", "A"), ("B", "B")] (Int_lower2 RS imp_prem) 1); |
|
377 |
by (subgoal_tac "A=Union({A - B, A Int B})" 1); |
|
378 |
by (Blast_tac 2); |
|
379 |
by (etac ssubst 1); |
|
380 |
by (rtac union_prem 1); |
|
11479 | 381 |
by (auto_tac (claset() addIs [subset_imp_leadsTo], simpset())); |
382 |
qed "leadsTo_induct2"; |
|
383 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
384 |
(** Variant induction rule \\<in> on the preconditions for B **) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
385 |
(*Lemma is the weak version \\<in> can't see how to do it in one step*) |
11479 | 386 |
val major::prems = Goal |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
387 |
"[| F \\<in> za leadsTo zb; \ |
11479 | 388 |
\ P(zb); \ |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
389 |
\ !!A B. [| F \\<in> A ensures B; P(B); st_set(A); st_set(B) |] ==> P(A); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
390 |
\ !!S. [| \\<forall>A \\<in> S. P(A); \\<forall>A \\<in> S. st_set(A) |] ==> P(Union(S)) \ |
11479 | 391 |
\ |] ==> P(za)"; |
392 |
(*by induction on this formula*) |
|
393 |
by (subgoal_tac "P(zb) --> P(za)" 1); |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
394 |
(*now solve first subgoal \\<in> this formula is sufficient*) |
11479 | 395 |
by (blast_tac (claset() addIs leadsTo_refl::prems) 1); |
396 |
by (rtac (major RS leadsTo_induct) 1); |
|
397 |
by (REPEAT (blast_tac (claset() addIs prems) 1)); |
|
13535 | 398 |
qed "leadsTo_induct_pre_aux"; |
11479 | 399 |
|
400 |
||
12195 | 401 |
val [major, zb_prem, basis_prem, union_prem] = Goal |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
402 |
"[| F \\<in> za leadsTo zb; \ |
11479 | 403 |
\ P(zb); \ |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
404 |
\ !!A B. [| F \\<in> A ensures B; F \\<in> B leadsTo zb; P(B); st_set(A) |] ==> P(A); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
405 |
\ !!S. \\<forall>A \\<in> S. F \\<in> A leadsTo zb & P(A) & st_set(A) ==> P(Union(S)) \ |
11479 | 406 |
\ |] ==> P(za)"; |
407 |
by (cut_facts_tac [major] 1); |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
408 |
by (subgoal_tac "(F \\<in> za leadsTo zb) & P(za)" 1); |
11479 | 409 |
by (etac conjunct2 1); |
13535 | 410 |
by (rtac (major RS leadsTo_induct_pre_aux) 1); |
12195 | 411 |
by (blast_tac (claset() addDs [leadsToD2] |
412 |
addIs [leadsTo_Union,union_prem]) 3); |
|
413 |
by (blast_tac (claset() addIs [leadsTo_Trans,basis_prem, leadsTo_Basis]) 2); |
|
414 |
by (blast_tac (claset() addIs [leadsTo_refl,zb_prem] |
|
415 |
addDs [leadsToD2]) 1); |
|
11479 | 416 |
qed "leadsTo_induct_pre"; |
417 |
||
418 |
(** The impossibility law **) |
|
419 |
Goal |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
420 |
"F \\<in> A leadsTo 0 ==> A=0"; |
11479 | 421 |
by (etac leadsTo_induct_pre 1); |
12195 | 422 |
by (auto_tac (claset(), simpset() addsimps |
423 |
[ensures_def, constrains_def, transient_def, st_set_def])); |
|
424 |
by (dtac bspec 1); |
|
425 |
by (REPEAT(Blast_tac 1)); |
|
11479 | 426 |
qed "leadsTo_empty"; |
12195 | 427 |
Addsimps [leadsTo_empty]; |
11479 | 428 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
429 |
(** PSP \\<in> Progress-Safety-Progress **) |
11479 | 430 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
431 |
(*Special case of PSP \\<in> Misra's "stable conjunction"*) |
11479 | 432 |
Goalw [stable_def] |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
433 |
"[| F \\<in> A leadsTo A'; F \\<in> stable(B) |] ==> F:(A Int B) leadsTo (A' Int B)"; |
11479 | 434 |
by (etac leadsTo_induct 1); |
435 |
by (rtac leadsTo_Union_Int 3); |
|
12195 | 436 |
by (ALLGOALS(Asm_simp_tac)); |
437 |
by (REPEAT(blast_tac (claset() addDs [constrainsD2]) 3)); |
|
11479 | 438 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
439 |
by (rtac leadsTo_Basis 1); |
|
440 |
by (asm_full_simp_tac (simpset() |
|
12220 | 441 |
addsimps [ensures_def, Diff_Int_distrib RS sym, |
442 |
Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1); |
|
11479 | 443 |
by (REPEAT(blast_tac (claset() |
444 |
addIs [transient_strengthen,constrains_Int] |
|
445 |
addDs [constrainsD2]) 1)); |
|
446 |
qed "psp_stable"; |
|
447 |
||
448 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
449 |
Goal "[|F \\<in> A leadsTo A'; F \\<in> stable(B) |]==>F: (B Int A) leadsTo (B Int A')"; |
11479 | 450 |
by (asm_simp_tac (simpset() |
451 |
addsimps psp_stable::Int_ac) 1); |
|
452 |
qed "psp_stable2"; |
|
453 |
||
12195 | 454 |
Goalw [ensures_def, constrains_def, st_set_def] |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
455 |
"[| F \\<in> A ensures A'; F \\<in> B co B' |]==> F: (A Int B') ensures ((A' Int B) Un (B' - B))"; |
11479 | 456 |
(*speeds up the proof*) |
457 |
by (Clarify_tac 1); |
|
458 |
by (blast_tac (claset() addIs [transient_strengthen]) 1); |
|
459 |
qed "psp_ensures"; |
|
460 |
||
12195 | 461 |
Goal |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
462 |
"[|F \\<in> A leadsTo A'; F \\<in> B co B'; st_set(B')|]==> F:(A Int B') leadsTo ((A' Int B) Un (B' - B))"; |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
463 |
by (subgoal_tac "F \\<in> program & st_set(A) & st_set(A')& st_set(B)" 1); |
12195 | 464 |
by (blast_tac (claset() addSDs [constrainsD2, leadsToD2]) 2); |
11479 | 465 |
by (etac leadsTo_induct 1); |
466 |
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); |
|
467 |
(*Transitivity case has a delicate argument involving "cancellation"*) |
|
468 |
by (rtac leadsTo_Un_duplicate2 2); |
|
469 |
by (etac leadsTo_cancel_Diff1 2); |
|
470 |
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2); |
|
471 |
by (blast_tac (claset() addIs [leadsTo_weaken_L] |
|
472 |
addDs [constrains_imp_subset]) 2); |
|
473 |
(*Basis case*) |
|
12195 | 474 |
by (blast_tac (claset() addIs [psp_ensures, leadsTo_Basis]) 1); |
11479 | 475 |
qed "psp"; |
476 |
||
477 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
478 |
Goal "[| F \\<in> A leadsTo A'; F \\<in> B co B'; st_set(B') |] \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
479 |
\ ==> F \\<in> (B' Int A) leadsTo ((B Int A') Un (B' - B))"; |
11479 | 480 |
by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1); |
481 |
qed "psp2"; |
|
482 |
||
483 |
Goalw [unless_def] |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
484 |
"[| F \\<in> A leadsTo A'; F \\<in> B unless B'; st_set(B); st_set(B') |] \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
485 |
\ ==> F \\<in> (A Int B) leadsTo ((A' Int B) Un B')"; |
12195 | 486 |
by (subgoal_tac "st_set(A)&st_set(A')" 1); |
487 |
by (blast_tac (claset() addDs [leadsToD2]) 2); |
|
11479 | 488 |
by (dtac psp 1); |
489 |
by (assume_tac 1); |
|
12195 | 490 |
by (Blast_tac 1); |
491 |
by (REPEAT(blast_tac (claset() addIs [leadsTo_weaken]) 1)); |
|
11479 | 492 |
qed "psp_unless"; |
493 |
||
12195 | 494 |
(*** Proving the wf induction rules ***) |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
495 |
(** The most general rule \\<in> r is any wf relation; f is any variant function **) |
11479 | 496 |
Goal "[| wf(r); \ |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
497 |
\ m \\<in> I; \ |
11479 | 498 |
\ field(r)<=I; \ |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
499 |
\ F \\<in> program; st_set(B);\ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
500 |
\ \\<forall>m \\<in> I. F \\<in> (A Int f-``{m}) leadsTo \ |
11479 | 501 |
\ ((A Int f-``(converse(r)``{m})) Un B) |] \ |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
502 |
\ ==> F \\<in> (A Int f-``{m}) leadsTo B"; |
11479 | 503 |
by (eres_inst_tac [("a","m")] wf_induct2 1); |
504 |
by (ALLGOALS(Asm_simp_tac)); |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
505 |
by (subgoal_tac "F \\<in> (A Int (f-``(converse(r)``{x}))) leadsTo B" 1); |
11479 | 506 |
by (stac vimage_eq_UN 2); |
12220 | 507 |
by (asm_simp_tac (simpset() delsimps UN_simps |
508 |
addsimps [Int_UN_distrib]) 2); |
|
11479 | 509 |
by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1); |
12215
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
510 |
by (auto_tac (claset() addIs [leadsTo_UN], |
55c084921240
Modified to make the files build with the new changes in ZF
ehmety
parents:
12195
diff
changeset
|
511 |
simpset() delsimps UN_simps addsimps [Int_UN_distrib])); |
13535 | 512 |
qed "leadsTo_wf_induct_aux"; |
11479 | 513 |
|
514 |
(** Meta or object quantifier ? **) |
|
515 |
Goal "[| wf(r); \ |
|
516 |
\ field(r)<=I; \ |
|
517 |
\ A<=f-``I;\ |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
518 |
\ F \\<in> program; st_set(A); st_set(B); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
519 |
\ \\<forall>m \\<in> I. F \\<in> (A Int f-``{m}) leadsTo \ |
11479 | 520 |
\ ((A Int f-``(converse(r)``{m})) Un B) |] \ |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
521 |
\ ==> F \\<in> A leadsTo B"; |
11479 | 522 |
by (res_inst_tac [("b", "A")] subst 1); |
523 |
by (res_inst_tac [("I", "I")] leadsTo_UN 2); |
|
524 |
by (REPEAT (assume_tac 2)); |
|
525 |
by (Clarify_tac 2); |
|
13535 | 526 |
by (eres_inst_tac [("I", "I")] leadsTo_wf_induct_aux 2); |
11479 | 527 |
by (REPEAT (assume_tac 2)); |
528 |
by (rtac equalityI 1); |
|
529 |
by Safe_tac; |
|
530 |
by (thin_tac "field(r)<=I" 1); |
|
531 |
by (dres_inst_tac [("c", "x")] subsetD 1); |
|
532 |
by Safe_tac; |
|
533 |
by (res_inst_tac [("b", "x")] UN_I 1); |
|
534 |
by Auto_tac; |
|
535 |
qed "leadsTo_wf_induct"; |
|
536 |
||
14046 | 537 |
Goalw [field_def] "field(measure(nat, %x. x)) = nat"; |
538 |
by (asm_full_simp_tac (simpset() addsimps [measure_def]) 1) ; |
|
11479 | 539 |
by (rtac equalityI 1); |
12195 | 540 |
by (force_tac (claset(), simpset()) 1); |
11479 | 541 |
by (Clarify_tac 1); |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
542 |
by (thin_tac "x\\<notin>range(?y)" 1); |
11479 | 543 |
by (etac nat_induct 1); |
14046 | 544 |
by (res_inst_tac [("b", "succ(succ(xa))")] domainI 2); |
545 |
by (res_inst_tac [("b","succ(0)")] domainI 1); |
|
546 |
by (ALLGOALS Asm_full_simp_tac); |
|
547 |
qed "nat_measure_field"; |
|
548 |
||
549 |
||
550 |
Goal "k<A ==> measure(A, %x. x) -`` {k} = k"; |
|
551 |
by (rtac equalityI 1); |
|
552 |
by (auto_tac (claset(), simpset() addsimps [measure_def])); |
|
553 |
by (blast_tac (claset() addIs [ltD]) 1); |
|
554 |
by (rtac vimageI 1); |
|
14053
4daa384f4fd7
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson
parents:
14046
diff
changeset
|
555 |
by (Blast_tac 2); |
14046 | 556 |
by (asm_full_simp_tac (simpset() addsimps [lt_Ord, lt_Ord2, Ord_mem_iff_lt]) 1); |
557 |
by (blast_tac (claset() addIs [lt_trans]) 1); |
|
558 |
qed "Image_inverse_lessThan"; |
|
11479 | 559 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
560 |
(*Alternative proof is via the lemma F \\<in> (A Int f-`(lessThan m)) leadsTo B*) |
11479 | 561 |
Goal |
562 |
"[| A<=f-``nat;\ |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
563 |
\ F \\<in> program; st_set(A); st_set(B); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
564 |
\ \\<forall>m \\<in> nat. F:(A Int f-``{m}) leadsTo ((A Int f -`` m) Un B) |] \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
565 |
\ ==> F \\<in> A leadsTo B"; |
14046 | 566 |
by (res_inst_tac [("A1", "nat"),("f1", "%x. x")] |
567 |
(wf_measure RS leadsTo_wf_induct) 1); |
|
11479 | 568 |
by (Clarify_tac 6); |
569 |
by (ALLGOALS(asm_full_simp_tac |
|
14046 | 570 |
(simpset() addsimps [nat_measure_field]))); |
571 |
by (asm_simp_tac (simpset() addsimps [ltI, Image_inverse_lessThan, symmetric vimage_def]) 1); |
|
11479 | 572 |
qed "lessThan_induct"; |
573 |
||
14046 | 574 |
|
11479 | 575 |
(*** wlt ****) |
576 |
||
577 |
(*Misra's property W3*) |
|
12195 | 578 |
Goalw [wlt_def] "wlt(F,B) <=state"; |
579 |
by Auto_tac; |
|
580 |
qed "wlt_type"; |
|
581 |
||
582 |
Goalw [st_set_def] "st_set(wlt(F, B))"; |
|
12484 | 583 |
by (rtac wlt_type 1); |
12195 | 584 |
qed "wlt_st_set"; |
585 |
AddIffs [wlt_st_set]; |
|
586 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
587 |
Goalw [wlt_def] "F \\<in> wlt(F, B) leadsTo B <-> (F \\<in> program & st_set(B))"; |
12195 | 588 |
by (blast_tac (claset() addDs [leadsToD2] addSIs [leadsTo_Union]) 1); |
589 |
qed "wlt_leadsTo_iff"; |
|
590 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
591 |
(* [| F \\<in> program; st_set(B) |] ==> F \\<in> wlt(F, B) leadsTo B *) |
12195 | 592 |
bind_thm("wlt_leadsTo", conjI RS (wlt_leadsTo_iff RS iffD2)); |
11479 | 593 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
594 |
Goalw [wlt_def] "F \\<in> A leadsTo B ==> A <= wlt(F, B)"; |
12484 | 595 |
by (ftac leadsToD2 1); |
12195 | 596 |
by (auto_tac (claset(), simpset() addsimps [st_set_def])); |
11479 | 597 |
qed "leadsTo_subset"; |
598 |
||
599 |
(*Misra's property W2*) |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
600 |
Goal "F \\<in> A leadsTo B <-> (A <= wlt(F,B) & F \\<in> program & st_set(B))"; |
12195 | 601 |
by Auto_tac; |
602 |
by (REPEAT(blast_tac (claset() addDs [leadsToD2,leadsTo_subset] |
|
603 |
addIs [leadsTo_weaken_L, wlt_leadsTo]) 1)); |
|
11479 | 604 |
qed "leadsTo_eq_subset_wlt"; |
605 |
||
606 |
(*Misra's property W4*) |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
607 |
Goal "[| F \\<in> program; st_set(B) |] ==> B <= wlt(F,B)"; |
12195 | 608 |
by (rtac leadsTo_subset 1); |
11479 | 609 |
by (asm_simp_tac (simpset() |
610 |
addsimps [leadsTo_eq_subset_wlt RS iff_sym, |
|
611 |
subset_imp_leadsTo]) 1); |
|
612 |
qed "wlt_increasing"; |
|
613 |
||
614 |
(*Used in the Trans case below*) |
|
12195 | 615 |
Goalw [constrains_def, st_set_def] |
11479 | 616 |
"[| B <= A2; \ |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
617 |
\ F \\<in> (A1 - B) co (A1 Un B); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
618 |
\ F \\<in> (A2 - C) co (A2 Un C) |] \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
619 |
\ ==> F \\<in> (A1 Un A2 - C) co (A1 Un A2 Un C)"; |
11479 | 620 |
by (Blast_tac 1); |
13535 | 621 |
qed "leadsTo_123_aux"; |
11479 | 622 |
|
623 |
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
624 |
(* slightly different from the HOL one \\<in> B here is bounded *) |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
625 |
Goal "F \\<in> A leadsTo A' \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
626 |
\ ==> \\<exists>B \\<in> Pow(state). A<=B & F \\<in> B leadsTo A' & F \\<in> (B-A') co (B Un A')"; |
12484 | 627 |
by (ftac leadsToD2 1); |
11479 | 628 |
by (etac leadsTo_induct 1); |
629 |
(*Basis*) |
|
12195 | 630 |
by (blast_tac (claset() addDs [ensuresD, constrainsD2, st_setD]) 1); |
11479 | 631 |
(*Trans*) |
632 |
by (Clarify_tac 1); |
|
633 |
by (res_inst_tac [("x", "Ba Un Bb")] bexI 1); |
|
13535 | 634 |
by (blast_tac (claset() addIs [leadsTo_123_aux,leadsTo_Un_Un, leadsTo_cancel1, |
11479 | 635 |
leadsTo_Un_duplicate]) 1); |
636 |
by (Blast_tac 1); |
|
637 |
(*Union*) |
|
638 |
by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1]) 1); |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
639 |
by (subgoal_tac "\\<exists>y. y \\<in> Pi(S, %A. {Ba \\<in> Pow(state). A<=Ba & \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
640 |
\ F \\<in> Ba leadsTo B & F \\<in> Ba - B co Ba Un B})" 1); |
11479 | 641 |
by (rtac AC_ball_Pi 2); |
12195 | 642 |
by (ALLGOALS(Clarify_tac)); |
643 |
by (rotate_tac 1 2); |
|
644 |
by (dres_inst_tac [("x", "x")] bspec 2); |
|
645 |
by (REPEAT(Blast_tac 2)); |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
646 |
by (res_inst_tac [("x", "\\<Union>A \\<in> S. y`A")] bexI 1); |
11479 | 647 |
by Safe_tac; |
648 |
by (res_inst_tac [("I1", "S")] (constrains_UN RS constrains_weaken) 3); |
|
649 |
by (rtac leadsTo_Union 2); |
|
12195 | 650 |
by (blast_tac (claset() addSDs [apply_type]) 5); |
651 |
by (ALLGOALS(Asm_full_simp_tac)); |
|
652 |
by (REPEAT(force_tac (claset() addSDs [apply_type], simpset()) 1)); |
|
11479 | 653 |
qed "leadsTo_123"; |
654 |
||
655 |
||
656 |
(*Misra's property W5*) |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
657 |
Goal "[| F \\<in> program; st_set(B) |] ==>F \\<in> (wlt(F, B) - B) co (wlt(F,B))"; |
11479 | 658 |
by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1); |
659 |
by (assume_tac 1); |
|
12195 | 660 |
by (Blast_tac 1); |
11479 | 661 |
by (Clarify_tac 1); |
662 |
by (subgoal_tac "Ba = wlt(F,B)" 1); |
|
663 |
by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2); |
|
664 |
by (Clarify_tac 1); |
|
665 |
by (asm_full_simp_tac (simpset() |
|
666 |
addsimps [wlt_increasing RS (subset_Un_iff2 RS iffD1)]) 1); |
|
667 |
qed "wlt_constrains_wlt"; |
|
668 |
||
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
669 |
(*** Completion \\<in> Binary and General Finite versions ***) |
11479 | 670 |
|
671 |
Goal "[| W = wlt(F, (B' Un C)); \ |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
672 |
\ F \\<in> A leadsTo (A' Un C); F \\<in> A' co (A' Un C); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
673 |
\ F \\<in> B leadsTo (B' Un C); F \\<in> B' co (B' Un C) |] \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
674 |
\ ==> F \\<in> (A Int B) leadsTo ((A' Int B') Un C)"; |
12195 | 675 |
by (subgoal_tac "st_set(C)&st_set(W)&st_set(W-C)&st_set(A')&st_set(A)\ |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
676 |
\ & st_set(B) & st_set(B') & F \\<in> program" 1); |
12195 | 677 |
by (Asm_simp_tac 2); |
678 |
by (blast_tac (claset() addSDs [leadsToD2]) 2); |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
679 |
by (subgoal_tac "F \\<in> (W-C) co (W Un B' Un C)" 1); |
14054 | 680 |
by (blast_tac (claset() addSIs [[asm_rl, wlt_constrains_wlt] |
12195 | 681 |
MRS constrains_Un RS constrains_weaken]) 2); |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
682 |
by (subgoal_tac "F \\<in> (W-C) co W" 1); |
12195 | 683 |
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing RS |
684 |
(subset_Un_iff2 RS iffD1), Un_assoc]) 2); |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
685 |
by (subgoal_tac "F \\<in> (A Int W - C) leadsTo (A' Int W Un C)" 1); |
12195 | 686 |
by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2); |
687 |
(** LEVEL 9 **) |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
688 |
by (subgoal_tac "F \\<in> (A' Int W Un C) leadsTo (A' Int B' Un C)" 1); |
11479 | 689 |
by (rtac leadsTo_Un_duplicate2 2); |
12195 | 690 |
by (rtac leadsTo_Un_Un 2); |
691 |
by (blast_tac (claset() addIs [leadsTo_refl]) 3); |
|
692 |
by (res_inst_tac [("A'1", "B' Un C")] (wlt_leadsTo RS psp2 RS leadsTo_weaken) 2); |
|
693 |
by (REPEAT(Blast_tac 2)); |
|
694 |
(** LEVEL 17 **) |
|
11479 | 695 |
by (dtac leadsTo_Diff 1); |
12195 | 696 |
by (blast_tac (claset() addIs [subset_imp_leadsTo] |
697 |
addDs [leadsToD2, constrainsD2]) 1); |
|
698 |
by (force_tac (claset(), simpset() addsimps [st_set_def]) 1); |
|
11479 | 699 |
by (subgoal_tac "A Int B <= A Int W" 1); |
700 |
by (blast_tac (claset() addSDs [leadsTo_subset] |
|
701 |
addSIs [subset_refl RS Int_mono]) 2); |
|
12195 | 702 |
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); |
703 |
qed "completion_aux"; |
|
704 |
bind_thm("completion", refl RS completion_aux); |
|
11479 | 705 |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
706 |
Goal "[| I \\<in> Fin(X); F \\<in> program; st_set(C) |] ==> \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
707 |
\(\\<forall>i \\<in> I. F \\<in> (A(i)) leadsTo (A'(i) Un C)) --> \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
708 |
\ (\\<forall>i \\<in> I. F \\<in> (A'(i)) co (A'(i) Un C)) --> \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
709 |
\ F \\<in> (\\<Inter>i \\<in> I. A(i)) leadsTo ((\\<Inter>i \\<in> I. A'(i)) Un C)"; |
12220 | 710 |
by (etac Fin_induct 1); |
12195 | 711 |
by (auto_tac (claset(), simpset() addsimps [Inter_0])); |
11479 | 712 |
by (rtac completion 1); |
12220 | 713 |
by (auto_tac (claset(), |
714 |
simpset() delsimps INT_simps addsimps INT_extend_simps)); |
|
715 |
by (rtac constrains_INT 1); |
|
11479 | 716 |
by (REPEAT(Blast_tac 1)); |
717 |
qed "lemma"; |
|
718 |
||
719 |
val prems = Goal |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
720 |
"[| I \\<in> Fin(X); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
721 |
\ !!i. i \\<in> I ==> F \\<in> A(i) leadsTo (A'(i) Un C); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
722 |
\ !!i. i \\<in> I ==> F \\<in> A'(i) co (A'(i) Un C); F \\<in> program; st_set(C)|] \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
723 |
\ ==> F \\<in> (\\<Inter>i \\<in> I. A(i)) leadsTo ((\\<Inter>i \\<in> I. A'(i)) Un C)"; |
12195 | 724 |
by (resolve_tac [lemma RS mp RS mp] 1); |
725 |
by (resolve_tac prems 3); |
|
726 |
by (REPEAT(blast_tac (claset() addIs prems) 1)); |
|
11479 | 727 |
qed "finite_completion"; |
728 |
||
729 |
Goalw [stable_def] |
|
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
730 |
"[| F \\<in> A leadsTo A'; F \\<in> stable(A'); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
731 |
\ F \\<in> B leadsTo B'; F \\<in> stable(B') |] \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
732 |
\ ==> F \\<in> (A Int B) leadsTo (A' Int B')"; |
11479 | 733 |
by (res_inst_tac [("C1", "0")] (completion RS leadsTo_weaken_R) 1); |
12195 | 734 |
by (REPEAT(blast_tac (claset() addDs [leadsToD2, constrainsD2]) 5)); |
11479 | 735 |
by (ALLGOALS(Asm_full_simp_tac)); |
736 |
qed "stable_completion"; |
|
737 |
||
738 |
||
12195 | 739 |
val major::prems = Goalw [stable_def] |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
740 |
"[| I \\<in> Fin(X); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
741 |
\ (!!i. i \\<in> I ==> F \\<in> A(i) leadsTo A'(i)); \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
742 |
\ (!!i. i \\<in> I ==> F \\<in> stable(A'(i))); F \\<in> program |] \ |
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
743 |
\ ==> F \\<in> (\\<Inter>i \\<in> I. A(i)) leadsTo (\\<Inter>i \\<in> I. A'(i))"; |
12195 | 744 |
by (cut_facts_tac [major] 1); |
14092
68da54626309
Conversion of ZF/UNITY/{FP,Union} to Isar script.
paulson
parents:
14084
diff
changeset
|
745 |
by (subgoal_tac "st_set(\\<Inter>i \\<in> I. A'(i))" 1); |
12195 | 746 |
by (blast_tac (claset() addDs [leadsToD2]@prems) 2); |
11479 | 747 |
by (res_inst_tac [("C1", "0")] (finite_completion RS leadsTo_weaken_R) 1); |
12195 | 748 |
by (Asm_simp_tac 1); |
749 |
by (assume_tac 6); |
|
750 |
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps prems))); |
|
751 |
by (resolve_tac prems 2); |
|
752 |
by (resolve_tac prems 1); |
|
753 |
by Auto_tac; |
|
11479 | 754 |
qed "finite_stable_completion"; |
755 |