author | paulson |
Fri, 03 Mar 2000 18:26:19 +0100 | |
changeset 8334 | 7896bcbd8641 |
parent 8251 | 9be357df93d4 |
child 8835 | 56187238220d |
permissions | -rw-r--r-- |
4776 | 1 |
(* Title: HOL/UNITY/WFair |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Weak Fairness versions of transient, ensures, leadsTo. |
|
7 |
||
8 |
From Misra, "A Logic for Concurrent Programming", 1994 |
|
9 |
*) |
|
10 |
||
11 |
||
5648 | 12 |
overload_1st_set "WFair.transient"; |
13 |
overload_1st_set "WFair.ensures"; |
|
6536 | 14 |
overload_1st_set "WFair.op leadsTo"; |
5340 | 15 |
|
4776 | 16 |
(*** transient ***) |
17 |
||
5069 | 18 |
Goalw [stable_def, constrains_def, transient_def] |
5648 | 19 |
"[| F : stable A; F : transient A |] ==> A = {}"; |
4776 | 20 |
by (Blast_tac 1); |
21 |
qed "stable_transient_empty"; |
|
22 |
||
5069 | 23 |
Goalw [transient_def] |
5648 | 24 |
"[| F : transient A; B<=A |] ==> F : transient B"; |
4776 | 25 |
by (Clarify_tac 1); |
6012
1894bfc4aee9
Addition of the States component; parts of Comp not working
paulson
parents:
5971
diff
changeset
|
26 |
by (blast_tac (claset() addSIs [rev_bexI]) 1); |
4776 | 27 |
qed "transient_strengthen"; |
28 |
||
5069 | 29 |
Goalw [transient_def] |
5648 | 30 |
"[| act: Acts F; A <= Domain act; act^^A <= -A |] ==> F : transient A"; |
4776 | 31 |
by (Blast_tac 1); |
8041 | 32 |
qed "transientI"; |
33 |
||
34 |
val major::prems = |
|
35 |
Goalw [transient_def] |
|
36 |
"[| F : transient A; \ |
|
37 |
\ !!act. [| act: Acts F; A <= Domain act; act^^A <= -A |] ==> P |] \ |
|
38 |
\ ==> P"; |
|
39 |
by (rtac (major RS CollectD RS bexE) 1); |
|
40 |
by (blast_tac (claset() addIs prems) 1); |
|
41 |
qed "transientE"; |
|
4776 | 42 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
43 |
Goalw [transient_def] "transient UNIV = {}"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
44 |
by Auto_tac; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
45 |
qed "transient_UNIV"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
46 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
47 |
Goalw [transient_def] "transient {} = UNIV"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
48 |
by Auto_tac; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
49 |
qed "transient_empty"; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
50 |
Addsimps [transient_UNIV, transient_empty]; |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7594
diff
changeset
|
51 |
|
4776 | 52 |
|
53 |
(*** ensures ***) |
|
54 |
||
5069 | 55 |
Goalw [ensures_def] |
7524 | 56 |
"[| F : (A-B) co (A Un B); F : transient (A-B) |] ==> F : A ensures B"; |
4776 | 57 |
by (Blast_tac 1); |
58 |
qed "ensuresI"; |
|
59 |
||
5069 | 60 |
Goalw [ensures_def] |
6536 | 61 |
"F : A ensures B ==> F : (A-B) co (A Un B) & F : transient (A-B)"; |
4776 | 62 |
by (Blast_tac 1); |
63 |
qed "ensuresD"; |
|
64 |
||
5069 | 65 |
Goalw [ensures_def] |
6536 | 66 |
"[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'"; |
4776 | 67 |
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); |
68 |
qed "ensures_weaken_R"; |
|
69 |
||
8041 | 70 |
(*The L-version (precondition strengthening) fails, but we have this*) |
5069 | 71 |
Goalw [ensures_def] |
8041 | 72 |
"[| F : stable C; F : A ensures B |] \ |
73 |
\ ==> F : (C Int A) ensures (C Int B)"; |
|
74 |
by (auto_tac (claset(), |
|
75 |
simpset() addsimps [ensures_def, |
|
76 |
Int_Un_distrib RS sym, |
|
77 |
Diff_Int_distrib RS sym])); |
|
78 |
by (blast_tac (claset() addIs [transient_strengthen]) 2); |
|
79 |
by (blast_tac (claset() addIs [stable_constrains_Int, constrains_weaken]) 1); |
|
4776 | 80 |
qed "stable_ensures_Int"; |
81 |
||
6536 | 82 |
Goal "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B"; |
5640 | 83 |
by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1); |
84 |
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1); |
|
85 |
qed "stable_transient_ensures"; |
|
86 |
||
8122
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8112
diff
changeset
|
87 |
Goal "(A ensures B) = (A unless B) Int transient (A-B)"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8112
diff
changeset
|
88 |
by (simp_tac (simpset() addsimps [ensures_def, unless_def]) 1); |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8112
diff
changeset
|
89 |
qed "ensures_eq"; |
b43ad07660b9
working version, with Alloc now working on the same state space as the whole
paulson
parents:
8112
diff
changeset
|
90 |
|
4776 | 91 |
|
92 |
(*** leadsTo ***) |
|
93 |
||
6536 | 94 |
Goalw [leadsTo_def] "F : A ensures B ==> F : A leadsTo B"; |
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6714
diff
changeset
|
95 |
by (blast_tac (claset() addIs [leads.Basis]) 1); |
5648 | 96 |
qed "leadsTo_Basis"; |
4776 | 97 |
|
5648 | 98 |
Goalw [leadsTo_def] |
6536 | 99 |
"[| F : A leadsTo B; F : B leadsTo C |] ==> F : A leadsTo C"; |
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6714
diff
changeset
|
100 |
by (blast_tac (claset() addIs [leads.Trans]) 1); |
5648 | 101 |
qed "leadsTo_Trans"; |
102 |
||
6536 | 103 |
Goal "F : transient A ==> F : A leadsTo (-A)"; |
5640 | 104 |
by (asm_simp_tac |
105 |
(simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1); |
|
106 |
qed "transient_imp_leadsTo"; |
|
107 |
||
4776 | 108 |
(*Useful with cancellation, disjunction*) |
6536 | 109 |
Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'"; |
4776 | 110 |
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
111 |
qed "leadsTo_Un_duplicate"; |
|
112 |
||
6536 | 113 |
Goal "F : A leadsTo (A' Un C Un C) ==> F : A leadsTo (A' Un C)"; |
4776 | 114 |
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1); |
115 |
qed "leadsTo_Un_duplicate2"; |
|
116 |
||
117 |
(*The Union introduction rule as we should have liked to state it*) |
|
5648 | 118 |
val prems = Goalw [leadsTo_def] |
6536 | 119 |
"(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B"; |
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6714
diff
changeset
|
120 |
by (blast_tac (claset() addIs [leads.Union] addDs prems) 1); |
4776 | 121 |
qed "leadsTo_Union"; |
122 |
||
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
123 |
val prems = Goalw [leadsTo_def] |
7524 | 124 |
"(!!A. A : S ==> F : (A Int C) leadsTo B) ==> F : (Union S Int C) leadsTo B"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
125 |
by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1); |
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6714
diff
changeset
|
126 |
by (blast_tac (claset() addIs [leads.Union] addDs prems) 1); |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
127 |
qed "leadsTo_Union_Int"; |
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
128 |
|
5648 | 129 |
val prems = Goal |
6536 | 130 |
"(!!i. i : I ==> F : (A i) leadsTo B) ==> F : (UN i:I. A i) leadsTo B"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
131 |
by (stac (Union_image_eq RS sym) 1); |
5648 | 132 |
by (blast_tac (claset() addIs leadsTo_Union::prems) 1); |
4776 | 133 |
qed "leadsTo_UN"; |
134 |
||
135 |
(*Binary union introduction rule*) |
|
6536 | 136 |
Goal "[| F : A leadsTo C; F : B leadsTo C |] ==> F : (A Un B) leadsTo C"; |
4776 | 137 |
by (stac Un_eq_Union 1); |
138 |
by (blast_tac (claset() addIs [leadsTo_Union]) 1); |
|
139 |
qed "leadsTo_Un"; |
|
140 |
||
6714 | 141 |
val prems = |
142 |
Goal "(!!x. x : A ==> F : {x} leadsTo B) ==> F : A leadsTo B"; |
|
143 |
by (stac (UN_singleton RS sym) 1 THEN rtac leadsTo_UN 1); |
|
144 |
by (blast_tac (claset() addIs prems) 1); |
|
145 |
qed "single_leadsTo_I"; |
|
146 |
||
4776 | 147 |
|
148 |
(*The INDUCTION rule as we should have liked to state it*) |
|
5648 | 149 |
val major::prems = Goalw [leadsTo_def] |
6536 | 150 |
"[| F : za leadsTo zb; \ |
151 |
\ !!A B. F : A ensures B ==> P A B; \ |
|
152 |
\ !!A B C. [| F : A leadsTo B; P A B; F : B leadsTo C; P B C |] \ |
|
4776 | 153 |
\ ==> P A C; \ |
6536 | 154 |
\ !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B \ |
4776 | 155 |
\ |] ==> P za zb"; |
6801
9e0037839d63
renamed the underlying relation of leadsTo from "leadsto"
paulson
parents:
6714
diff
changeset
|
156 |
by (rtac (major RS CollectD RS leads.induct) 1); |
4776 | 157 |
by (REPEAT (blast_tac (claset() addIs prems) 1)); |
158 |
qed "leadsTo_induct"; |
|
159 |
||
160 |
||
7594
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7524
diff
changeset
|
161 |
Goal "A<=B ==> F : A ensures B"; |
4776 | 162 |
by (rewrite_goals_tac [ensures_def, constrains_def, transient_def]); |
163 |
by (Blast_tac 1); |
|
7594
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7524
diff
changeset
|
164 |
qed "subset_imp_ensures"; |
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7524
diff
changeset
|
165 |
|
8a188ef6545e
working version with co-guarantees-leadsto results
paulson
parents:
7524
diff
changeset
|
166 |
bind_thm ("subset_imp_leadsTo", subset_imp_ensures RS leadsTo_Basis); |
4776 | 167 |
|
8112
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
168 |
bind_thm ("leadsTo_refl", subset_refl RS subset_imp_leadsTo); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
169 |
|
4776 | 170 |
bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo); |
171 |
Addsimps [empty_leadsTo]; |
|
172 |
||
8041 | 173 |
bind_thm ("leadsTo_UNIV", subset_UNIV RS subset_imp_leadsTo); |
174 |
Addsimps [leadsTo_UNIV]; |
|
175 |
||
4776 | 176 |
|
8112
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
177 |
|
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
178 |
(** Variant induction rule: on the preconditions for B **) |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
179 |
|
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
180 |
(*Lemma is the weak version: can't see how to do it in one step*) |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
181 |
val major::prems = Goal |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
182 |
"[| F : za leadsTo zb; \ |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
183 |
\ P zb; \ |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
184 |
\ !!A B. [| F : A ensures B; P B |] ==> P A; \ |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
185 |
\ !!S. ALL A:S. P A ==> P (Union S) \ |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
186 |
\ |] ==> P za"; |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
187 |
(*by induction on this formula*) |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
188 |
by (subgoal_tac "P zb --> P za" 1); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
189 |
(*now solve first subgoal: this formula is sufficient*) |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
190 |
by (blast_tac (claset() addIs leadsTo_refl::prems) 1); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
191 |
by (rtac (major RS leadsTo_induct) 1); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
192 |
by (REPEAT (blast_tac (claset() addIs prems) 1)); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
193 |
val lemma = result(); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
194 |
|
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
195 |
val major::prems = Goal |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
196 |
"[| F : za leadsTo zb; \ |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
197 |
\ P zb; \ |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
198 |
\ !!A B. [| F : A ensures B; F : B leadsTo zb; P B |] ==> P A; \ |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
199 |
\ !!S. ALL A:S. F : A leadsTo zb & P A ==> P (Union S) \ |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
200 |
\ |] ==> P za"; |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
201 |
by (subgoal_tac "F : za leadsTo zb & P za" 1); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
202 |
by (etac conjunct2 1); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
203 |
by (rtac (major RS lemma) 1); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
204 |
by (blast_tac (claset() addIs [leadsTo_Union]@prems) 3); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
205 |
by (blast_tac (claset() addIs [leadsTo_Basis,leadsTo_Trans]@prems) 2); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
206 |
by (blast_tac (claset() addIs [leadsTo_refl]@prems) 1); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
207 |
qed "leadsTo_induct_pre"; |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
208 |
|
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
209 |
|
6536 | 210 |
Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'"; |
5648 | 211 |
by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1); |
212 |
qed "leadsTo_weaken_R"; |
|
4776 | 213 |
|
6536 | 214 |
Goal "[| F : A leadsTo A'; B<=A |] ==> F : B leadsTo A'"; |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
215 |
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); |
4776 | 216 |
qed_spec_mp "leadsTo_weaken_L"; |
217 |
||
218 |
(*Distributes over binary unions*) |
|
6536 | 219 |
Goal "F : (A Un B) leadsTo C = (F : A leadsTo C & F : B leadsTo C)"; |
4776 | 220 |
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken_L]) 1); |
221 |
qed "leadsTo_Un_distrib"; |
|
222 |
||
6536 | 223 |
Goal "F : (UN i:I. A i) leadsTo B = (ALL i : I. F : (A i) leadsTo B)"; |
4776 | 224 |
by (blast_tac (claset() addIs [leadsTo_UN, leadsTo_weaken_L]) 1); |
225 |
qed "leadsTo_UN_distrib"; |
|
226 |
||
6536 | 227 |
Goal "F : (Union S) leadsTo B = (ALL A : S. F : A leadsTo B)"; |
4776 | 228 |
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_L]) 1); |
229 |
qed "leadsTo_Union_distrib"; |
|
230 |
||
231 |
||
6536 | 232 |
Goal "[| F : A leadsTo A'; B<=A; A'<=B' |] ==> F : B leadsTo B'"; |
5340 | 233 |
by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L, |
234 |
leadsTo_Trans]) 1); |
|
4776 | 235 |
qed "leadsTo_weaken"; |
236 |
||
237 |
||
238 |
(*Set difference: maybe combine with leadsTo_weaken_L??*) |
|
6536 | 239 |
Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |] ==> F : A leadsTo C"; |
4776 | 240 |
by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1); |
241 |
qed "leadsTo_Diff"; |
|
242 |
||
243 |
val prems = goal thy |
|
6536 | 244 |
"(!! i. i:I ==> F : (A i) leadsTo (A' i)) \ |
245 |
\ ==> F : (UN i:I. A i) leadsTo (UN i:I. A' i)"; |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
246 |
by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1); |
4776 | 247 |
by (blast_tac (claset() addIs [leadsTo_Union, leadsTo_weaken_R] |
248 |
addIs prems) 1); |
|
249 |
qed "leadsTo_UN_UN"; |
|
250 |
||
251 |
(*Binary union version*) |
|
6714 | 252 |
Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \ |
253 |
\ ==> F : (A Un B) leadsTo (A' Un B')"; |
|
4776 | 254 |
by (blast_tac (claset() addIs [leadsTo_Un, |
255 |
leadsTo_weaken_R]) 1); |
|
256 |
qed "leadsTo_Un_Un"; |
|
257 |
||
258 |
||
259 |
(** The cancellation law **) |
|
260 |
||
6536 | 261 |
Goal "[| F : A leadsTo (A' Un B); F : B leadsTo B' |] \ |
6714 | 262 |
\ ==> F : A leadsTo (A' Un B')"; |
4776 | 263 |
by (blast_tac (claset() addIs [leadsTo_Un_Un, |
264 |
subset_imp_leadsTo, leadsTo_Trans]) 1); |
|
265 |
qed "leadsTo_cancel2"; |
|
266 |
||
6536 | 267 |
Goal "[| F : A leadsTo (A' Un B); F : (B-A') leadsTo B' |] \ |
6714 | 268 |
\ ==> F : A leadsTo (A' Un B')"; |
4776 | 269 |
by (rtac leadsTo_cancel2 1); |
270 |
by (assume_tac 2); |
|
271 |
by (ALLGOALS Asm_simp_tac); |
|
272 |
qed "leadsTo_cancel_Diff2"; |
|
273 |
||
6536 | 274 |
Goal "[| F : A leadsTo (B Un A'); F : B leadsTo B' |] \ |
275 |
\ ==> F : A leadsTo (B' Un A')"; |
|
4776 | 276 |
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1); |
277 |
by (blast_tac (claset() addSIs [leadsTo_cancel2]) 1); |
|
278 |
qed "leadsTo_cancel1"; |
|
279 |
||
6536 | 280 |
Goal "[| F : A leadsTo (B Un A'); F : (B-A') leadsTo B' |] \ |
281 |
\ ==> F : A leadsTo (B' Un A')"; |
|
4776 | 282 |
by (rtac leadsTo_cancel1 1); |
283 |
by (assume_tac 2); |
|
284 |
by (ALLGOALS Asm_simp_tac); |
|
285 |
qed "leadsTo_cancel_Diff1"; |
|
286 |
||
287 |
||
288 |
||
289 |
(** The impossibility law **) |
|
290 |
||
8112
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
291 |
Goal "F : A leadsTo {} ==> A={}"; |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
292 |
by (etac leadsTo_induct_pre 1); |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
293 |
by (ALLGOALS |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
294 |
(asm_full_simp_tac |
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
295 |
(simpset() addsimps [ensures_def, constrains_def, transient_def]))); |
4776 | 296 |
by (Blast_tac 1); |
297 |
qed "leadsTo_empty"; |
|
298 |
||
299 |
||
300 |
(** PSP: Progress-Safety-Progress **) |
|
301 |
||
5640 | 302 |
(*Special case of PSP: Misra's "stable conjunction"*) |
5069 | 303 |
Goalw [stable_def] |
6536 | 304 |
"[| F : A leadsTo A'; F : stable B |] \ |
305 |
\ ==> F : (A Int B) leadsTo (A' Int B)"; |
|
4776 | 306 |
by (etac leadsTo_induct 1); |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
307 |
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); |
4776 | 308 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 2); |
309 |
by (rtac leadsTo_Basis 1); |
|
310 |
by (asm_full_simp_tac |
|
311 |
(simpset() addsimps [ensures_def, |
|
312 |
Diff_Int_distrib2 RS sym, Int_Un_distrib2 RS sym]) 1); |
|
313 |
by (blast_tac (claset() addIs [transient_strengthen, constrains_Int]) 1); |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
314 |
qed "psp_stable"; |
4776 | 315 |
|
7524 | 316 |
Goal |
317 |
"[| F : A leadsTo A'; F : stable B |] ==> F : (B Int A) leadsTo (B Int A')"; |
|
5536 | 318 |
by (asm_simp_tac (simpset() addsimps psp_stable::Int_ac) 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
319 |
qed "psp_stable2"; |
4776 | 320 |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
321 |
Goalw [ensures_def, constrains_def] |
6536 | 322 |
"[| F : A ensures A'; F : B co B' |] \ |
6714 | 323 |
\ ==> F : (A Int B') ensures ((A' Int B) Un (B' - B))"; |
324 |
by (Clarify_tac 1); (*speeds up the proof*) |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
325 |
by (blast_tac (claset() addIs [transient_strengthen]) 1); |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
326 |
qed "psp_ensures"; |
4776 | 327 |
|
6536 | 328 |
Goal "[| F : A leadsTo A'; F : B co B' |] \ |
6714 | 329 |
\ ==> F : (A Int B') leadsTo ((A' Int B) Un (B' - B))"; |
4776 | 330 |
by (etac leadsTo_induct 1); |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
331 |
by (blast_tac (claset() addIs [leadsTo_Union_Int]) 3); |
4776 | 332 |
(*Transitivity case has a delicate argument involving "cancellation"*) |
333 |
by (rtac leadsTo_Un_duplicate2 2); |
|
334 |
by (etac leadsTo_cancel_Diff1 2); |
|
335 |
by (asm_full_simp_tac (simpset() addsimps [Int_Diff, Diff_triv]) 2); |
|
6714 | 336 |
by (blast_tac (claset() addIs [leadsTo_weaken_L] |
337 |
addDs [constrains_imp_subset]) 2); |
|
4776 | 338 |
(*Basis case*) |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
339 |
by (blast_tac (claset() addIs [leadsTo_Basis, psp_ensures]) 1); |
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
340 |
qed "psp"; |
4776 | 341 |
|
6536 | 342 |
Goal "[| F : A leadsTo A'; F : B co B' |] \ |
6714 | 343 |
\ ==> F : (B' Int A) leadsTo ((B Int A') Un (B' - B))"; |
5536 | 344 |
by (asm_simp_tac (simpset() addsimps psp::Int_ac) 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
345 |
qed "psp2"; |
4776 | 346 |
|
347 |
||
5069 | 348 |
Goalw [unless_def] |
6536 | 349 |
"[| F : A leadsTo A'; F : B unless B' |] \ |
350 |
\ ==> F : (A Int B) leadsTo ((A' Int B) Un B')"; |
|
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
351 |
by (dtac psp 1); |
4776 | 352 |
by (assume_tac 1); |
6714 | 353 |
by (blast_tac (claset() addIs [leadsTo_weaken]) 1); |
5277
e4297d03e5d2
A higher-level treatment of LeadsTo, minimizing use of "reachable"
paulson
parents:
5257
diff
changeset
|
354 |
qed "psp_unless"; |
4776 | 355 |
|
356 |
||
357 |
(*** Proving the induction rules ***) |
|
358 |
||
5257 | 359 |
(** The most general rule: r is any wf relation; f is any variant function **) |
360 |
||
5239 | 361 |
Goal "[| wf r; \ |
6536 | 362 |
\ ALL m. F : (A Int f-``{m}) leadsTo \ |
7524 | 363 |
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ |
6536 | 364 |
\ ==> F : (A Int f-``{m}) leadsTo B"; |
4776 | 365 |
by (eres_inst_tac [("a","m")] wf_induct 1); |
6536 | 366 |
by (subgoal_tac "F : (A Int (f -`` (r^-1 ^^ {x}))) leadsTo B" 1); |
4776 | 367 |
by (stac vimage_eq_UN 2); |
368 |
by (asm_simp_tac (HOL_ss addsimps (UN_simps RL [sym])) 2); |
|
369 |
by (blast_tac (claset() addIs [leadsTo_UN]) 2); |
|
370 |
by (blast_tac (claset() addIs [leadsTo_cancel1, leadsTo_Un_duplicate]) 1); |
|
371 |
val lemma = result(); |
|
372 |
||
373 |
||
374 |
(** Meta or object quantifier ????? **) |
|
5239 | 375 |
Goal "[| wf r; \ |
6536 | 376 |
\ ALL m. F : (A Int f-``{m}) leadsTo \ |
7524 | 377 |
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ |
6536 | 378 |
\ ==> F : A leadsTo B"; |
4776 | 379 |
by (res_inst_tac [("t", "A")] subst 1); |
380 |
by (rtac leadsTo_UN 2); |
|
381 |
by (etac lemma 2); |
|
382 |
by (REPEAT (assume_tac 2)); |
|
383 |
by (Fast_tac 1); (*Blast_tac: Function unknown's argument not a parameter*) |
|
384 |
qed "leadsTo_wf_induct"; |
|
385 |
||
386 |
||
5239 | 387 |
Goal "[| wf r; \ |
6536 | 388 |
\ ALL m:I. F : (A Int f-``{m}) leadsTo \ |
7524 | 389 |
\ ((A Int f-``(r^-1 ^^ {m})) Un B) |] \ |
6536 | 390 |
\ ==> F : A leadsTo ((A - (f-``I)) Un B)"; |
4776 | 391 |
by (etac leadsTo_wf_induct 1); |
392 |
by Safe_tac; |
|
393 |
by (case_tac "m:I" 1); |
|
394 |
by (blast_tac (claset() addIs [leadsTo_weaken]) 1); |
|
395 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
|
396 |
qed "bounded_induct"; |
|
397 |
||
398 |
||
6536 | 399 |
(*Alternative proof is via the lemma F : (A Int f-``(lessThan m)) leadsTo B*) |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8122
diff
changeset
|
400 |
val prems = |
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8122
diff
changeset
|
401 |
Goal "[| !!m. F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \ |
6536 | 402 |
\ ==> F : A leadsTo B"; |
4776 | 403 |
by (rtac (wf_less_than RS leadsTo_wf_induct) 1); |
404 |
by (Asm_simp_tac 1); |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8122
diff
changeset
|
405 |
by (blast_tac (claset() addIs prems) 1); |
4776 | 406 |
qed "lessThan_induct"; |
407 |
||
7524 | 408 |
Goal "[| ALL m:(greaterThan l). \ |
409 |
\ F : (A Int f-``{m}) leadsTo ((A Int f-``(lessThan m)) Un B) |] \ |
|
6536 | 410 |
\ ==> F : A leadsTo ((A Int (f-``(atMost l))) Un B)"; |
5648 | 411 |
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, |
412 |
Compl_greaterThan RS sym]) 1); |
|
4776 | 413 |
by (rtac (wf_less_than RS bounded_induct) 1); |
414 |
by (Asm_simp_tac 1); |
|
415 |
qed "lessThan_bounded_induct"; |
|
416 |
||
7524 | 417 |
Goal "[| ALL m:(lessThan l). \ |
418 |
\ F : (A Int f-``{m}) leadsTo ((A Int f-``(greaterThan m)) Un B) |] \ |
|
6536 | 419 |
\ ==> F : A leadsTo ((A Int (f-``(atLeast l))) Un B)"; |
4776 | 420 |
by (res_inst_tac [("f","f"),("f1", "%k. l - k")] |
421 |
(wf_less_than RS wf_inv_image RS leadsTo_wf_induct) 1); |
|
422 |
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1); |
|
423 |
by (Clarify_tac 1); |
|
424 |
by (case_tac "m<l" 1); |
|
425 |
by (blast_tac (claset() addIs [not_leE, subset_imp_leadsTo]) 2); |
|
426 |
by (blast_tac (claset() addIs [leadsTo_weaken_R, diff_less_mono2]) 1); |
|
427 |
qed "greaterThan_bounded_induct"; |
|
428 |
||
429 |
||
430 |
(*** wlt ****) |
|
431 |
||
432 |
(*Misra's property W3*) |
|
6536 | 433 |
Goalw [wlt_def] "F : (wlt F B) leadsTo B"; |
4776 | 434 |
by (blast_tac (claset() addSIs [leadsTo_Union]) 1); |
435 |
qed "wlt_leadsTo"; |
|
436 |
||
6536 | 437 |
Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt F B"; |
4776 | 438 |
by (blast_tac (claset() addSIs [leadsTo_Union]) 1); |
439 |
qed "leadsTo_subset"; |
|
440 |
||
441 |
(*Misra's property W2*) |
|
6536 | 442 |
Goal "F : A leadsTo B = (A <= wlt F B)"; |
4776 | 443 |
by (blast_tac (claset() addSIs [leadsTo_subset, |
444 |
wlt_leadsTo RS leadsTo_weaken_L]) 1); |
|
445 |
qed "leadsTo_eq_subset_wlt"; |
|
446 |
||
447 |
(*Misra's property W4*) |
|
5648 | 448 |
Goal "B <= wlt F B"; |
4776 | 449 |
by (asm_simp_tac (simpset() addsimps [leadsTo_eq_subset_wlt RS sym, |
450 |
subset_imp_leadsTo]) 1); |
|
451 |
qed "wlt_increasing"; |
|
452 |
||
453 |
||
454 |
(*Used in the Trans case below*) |
|
5069 | 455 |
Goalw [constrains_def] |
5111 | 456 |
"[| B <= A2; \ |
6536 | 457 |
\ F : (A1 - B) co (A1 Un B); \ |
458 |
\ F : (A2 - C) co (A2 Un C) |] \ |
|
459 |
\ ==> F : (A1 Un A2 - C) co (A1 Un A2 Un C)"; |
|
5669 | 460 |
by (Clarify_tac 1); |
5620 | 461 |
by (Blast_tac 1); |
4776 | 462 |
val lemma1 = result(); |
463 |
||
464 |
||
465 |
(*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*) |
|
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
466 |
Goal "F : A leadsTo A' \ |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
467 |
\ ==> EX B. A<=B & F : B leadsTo A' & F : (B-A') co (B Un A')"; |
4776 | 468 |
by (etac leadsTo_induct 1); |
469 |
(*Basis*) |
|
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
470 |
by (blast_tac (claset() addIs [leadsTo_Basis] addDs [ensuresD]) 1); |
4776 | 471 |
(*Trans*) |
472 |
by (Clarify_tac 1); |
|
473 |
by (res_inst_tac [("x", "Ba Un Bb")] exI 1); |
|
474 |
by (blast_tac (claset() addIs [lemma1, leadsTo_Un_Un, leadsTo_cancel1, |
|
475 |
leadsTo_Un_duplicate]) 1); |
|
476 |
(*Union*) |
|
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
477 |
by (clarify_tac (claset() addSDs [ball_conj_distrib RS iffD1, bchoice]) 1);; |
4776 | 478 |
by (res_inst_tac [("x", "UN A:S. f A")] exI 1); |
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
479 |
by (auto_tac (claset() addIs [leadsTo_UN], simpset())); |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
480 |
(*Blast_tac says PROOF FAILED*) |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
481 |
by (deepen_tac (claset() addIs [constrains_UN RS constrains_weaken]) 0 1); |
4776 | 482 |
qed "leadsTo_123"; |
483 |
||
484 |
||
485 |
(*Misra's property W5*) |
|
6536 | 486 |
Goal "F : (wlt F B - B) co (wlt F B)"; |
5648 | 487 |
by (cut_inst_tac [("F","F")] (wlt_leadsTo RS leadsTo_123) 1); |
4776 | 488 |
by (Clarify_tac 1); |
5648 | 489 |
by (subgoal_tac "Ba = wlt F B" 1); |
490 |
by (blast_tac (claset() addDs [leadsTo_eq_subset_wlt RS iffD1]) 2); |
|
4776 | 491 |
by (Clarify_tac 1); |
492 |
by (asm_full_simp_tac (simpset() addsimps [wlt_increasing, Un_absorb2]) 1); |
|
493 |
qed "wlt_constrains_wlt"; |
|
494 |
||
495 |
||
496 |
(*** Completion: Binary and General Finite versions ***) |
|
497 |
||
5648 | 498 |
Goal "[| W = wlt F (B' Un C); \ |
6536 | 499 |
\ F : A leadsTo (A' Un C); F : A' co (A' Un C); \ |
500 |
\ F : B leadsTo (B' Un C); F : B' co (B' Un C) |] \ |
|
501 |
\ ==> F : (A Int B) leadsTo ((A' Int B') Un C)"; |
|
502 |
by (subgoal_tac "F : (W-C) co (W Un B' Un C)" 1); |
|
4776 | 503 |
by (blast_tac (claset() addIs [[asm_rl, wlt_constrains_wlt] |
504 |
MRS constrains_Un RS constrains_weaken]) 2); |
|
6536 | 505 |
by (subgoal_tac "F : (W-C) co W" 1); |
4776 | 506 |
by (asm_full_simp_tac |
507 |
(simpset() addsimps [wlt_increasing, Un_assoc, Un_absorb2]) 2); |
|
6536 | 508 |
by (subgoal_tac "F : (A Int W - C) leadsTo (A' Int W Un C)" 1); |
6714 | 509 |
by (blast_tac (claset() addIs [wlt_leadsTo, psp RS leadsTo_weaken]) 2); |
7963 | 510 |
(** LEVEL 6 **) |
6536 | 511 |
by (subgoal_tac "F : (A' Int W Un C) leadsTo (A' Int B' Un C)" 1); |
6714 | 512 |
by (rtac leadsTo_Un_duplicate2 2); |
513 |
by (blast_tac (claset() addIs [leadsTo_Un_Un, |
|
514 |
wlt_leadsTo RS psp2 RS leadsTo_weaken, |
|
8112
efbe50e2bef9
new theorem leadsTo_refl and induction rule leadsTo_induct_pre
paulson
parents:
8041
diff
changeset
|
515 |
leadsTo_refl]) 2); |
4776 | 516 |
by (dtac leadsTo_Diff 1); |
517 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); |
|
518 |
by (subgoal_tac "A Int B <= A Int W" 1); |
|
5456 | 519 |
by (blast_tac (claset() addSDs [leadsTo_subset] |
520 |
addSIs [subset_refl RS Int_mono]) 2); |
|
4776 | 521 |
by (blast_tac (claset() addIs [leadsTo_Trans, subset_imp_leadsTo]) 1); |
522 |
bind_thm("completion", refl RS result()); |
|
523 |
||
524 |
||
6536 | 525 |
Goal "finite I ==> (ALL i:I. F : (A i) leadsTo (A' i Un C)) --> \ |
526 |
\ (ALL i:I. F : (A' i) co (A' i Un C)) --> \ |
|
527 |
\ F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"; |
|
4776 | 528 |
by (etac finite_induct 1); |
7963 | 529 |
by Auto_tac; |
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
530 |
by (rtac completion 1); |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
531 |
by (simp_tac (HOL_ss addsimps (INT_simps RL [sym])) 4); |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
532 |
by (rtac constrains_INT 4); |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
533 |
by Auto_tac; |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
534 |
val lemma = result(); |
4776 | 535 |
|
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
536 |
val prems = Goal |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
537 |
"[| finite I; \ |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
538 |
\ !!i. i:I ==> F : (A i) leadsTo (A' i Un C); \ |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
539 |
\ !!i. i:I ==> F : (A' i) co (A' i Un C) |] \ |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
540 |
\ ==> F : (INT i:I. A i) leadsTo ((INT i:I. A' i) Un C)"; |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
541 |
by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1); |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
542 |
qed "finite_completion"; |
7963 | 543 |
|
544 |
Goalw [stable_def] |
|
545 |
"[| F : A leadsTo A'; F : stable A'; \ |
|
546 |
\ F : B leadsTo B'; F : stable B' |] \ |
|
547 |
\ ==> F : (A Int B) leadsTo (A' Int B')"; |
|
548 |
by (res_inst_tac [("C1", "{}")] (completion RS leadsTo_weaken_R) 1); |
|
549 |
by (REPEAT (Force_tac 1)); |
|
550 |
qed "stable_completion"; |
|
551 |
||
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
552 |
val prems = Goalw [stable_def] |
7963 | 553 |
"[| finite I; \ |
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
554 |
\ !!i. i:I ==> F : (A i) leadsTo (A' i); \ |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
555 |
\ !!i. i:I ==> F : stable (A' i) |] \ |
7963 | 556 |
\ ==> F : (INT i:I. A i) leadsTo (INT i:I. A' i)"; |
557 |
by (res_inst_tac [("C1", "{}")] (finite_completion RS leadsTo_weaken_R) 1); |
|
8334
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
558 |
by (ALLGOALS Asm_simp_tac); |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
559 |
by (ALLGOALS (blast_tac (claset() addIs prems))); |
7896bcbd8641
Added Tanja's Detects and Reachability theories. Also
paulson
parents:
8251
diff
changeset
|
560 |
qed "finite_stable_completion"; |
7963 | 561 |
|
562 |