paulson@4776
|
1 |
(* Title: HOL/UNITY/SubstAx
|
paulson@4776
|
2 |
ID: $Id$
|
paulson@4776
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
paulson@4776
|
4 |
Copyright 1998 University of Cambridge
|
paulson@4776
|
5 |
|
paulson@5277
|
6 |
LeadsTo relation, restricted to the set of reachable states.
|
paulson@4776
|
7 |
*)
|
paulson@4776
|
8 |
|
paulson@6536
|
9 |
overload_1st_set "SubstAx.op LeadsTo";
|
paulson@5277
|
10 |
|
paulson@4776
|
11 |
|
paulson@6575
|
12 |
(*Resembles the previous definition of LeadsTo*)
|
paulson@6575
|
13 |
Goalw [LeadsTo_def]
|
paulson@6575
|
14 |
"A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}";
|
paulson@8069
|
15 |
by (blast_tac (claset() addDs [psp_stable2] addIs [leadsTo_weaken]) 1);
|
paulson@6575
|
16 |
qed "LeadsTo_eq_leadsTo";
|
paulson@6575
|
17 |
|
paulson@6575
|
18 |
|
paulson@5277
|
19 |
(*** Specialized laws for handling invariants ***)
|
paulson@5277
|
20 |
|
paulson@6570
|
21 |
(** Conjoining an Always property **)
|
paulson@5544
|
22 |
|
paulson@6811
|
23 |
Goal "F : Always INV ==> (F : (INV Int A) LeadsTo A') = (F : A LeadsTo A')";
|
paulson@5277
|
24 |
by (asm_full_simp_tac
|
paulson@6570
|
25 |
(simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable,
|
paulson@6570
|
26 |
Int_absorb2, Int_assoc RS sym]) 1);
|
paulson@6811
|
27 |
qed "Always_LeadsTo_pre";
|
paulson@5544
|
28 |
|
paulson@6811
|
29 |
Goal "F : Always INV ==> (F : A LeadsTo (INV Int A')) = (F : A LeadsTo A')";
|
paulson@5544
|
30 |
by (asm_full_simp_tac
|
paulson@6575
|
31 |
(simpset() addsimps [LeadsTo_eq_leadsTo, Always_eq_includes_reachable,
|
paulson@6570
|
32 |
Int_absorb2, Int_assoc RS sym]) 1);
|
paulson@6811
|
33 |
qed "Always_LeadsTo_post";
|
paulson@6811
|
34 |
|
paulson@6811
|
35 |
(* [| F : Always C; F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
|
paulson@6811
|
36 |
bind_thm ("Always_LeadsToI", Always_LeadsTo_pre RS iffD1);
|
paulson@6811
|
37 |
|
paulson@6811
|
38 |
(* [| F : Always INV; F : A LeadsTo A' |] ==> F : A LeadsTo (INV Int A') *)
|
paulson@6811
|
39 |
bind_thm ("Always_LeadsToD", Always_LeadsTo_post RS iffD2);
|
paulson@5277
|
40 |
|
paulson@5277
|
41 |
|
paulson@4776
|
42 |
(*** Introduction rules: Basis, Trans, Union ***)
|
paulson@4776
|
43 |
|
paulson@6536
|
44 |
Goal "F : A leadsTo B ==> F : A LeadsTo B";
|
paulson@5111
|
45 |
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
|
paulson@6575
|
46 |
by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
|
paulson@4776
|
47 |
qed "leadsTo_imp_LeadsTo";
|
paulson@4776
|
48 |
|
paulson@6536
|
49 |
Goal "[| F : A LeadsTo B; F : B LeadsTo C |] ==> F : A LeadsTo C";
|
paulson@6575
|
50 |
by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1);
|
paulson@4776
|
51 |
by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
|
paulson@4776
|
52 |
qed "LeadsTo_Trans";
|
paulson@4776
|
53 |
|
paulson@5648
|
54 |
val prems = Goalw [LeadsTo_def]
|
paulson@6536
|
55 |
"(!!A. A : S ==> F : A LeadsTo B) ==> F : (Union S) LeadsTo B";
|
paulson@5111
|
56 |
by (Simp_tac 1);
|
paulson@4776
|
57 |
by (stac Int_Union 1);
|
paulson@5648
|
58 |
by (blast_tac (claset() addIs [leadsTo_UN] addDs prems) 1);
|
paulson@4776
|
59 |
qed "LeadsTo_Union";
|
paulson@4776
|
60 |
|
paulson@4776
|
61 |
|
paulson@4776
|
62 |
(*** Derived rules ***)
|
paulson@4776
|
63 |
|
paulson@6536
|
64 |
Goal "F : A LeadsTo UNIV";
|
paulson@6575
|
65 |
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
|
paulson@4776
|
66 |
qed "LeadsTo_UNIV";
|
paulson@4776
|
67 |
Addsimps [LeadsTo_UNIV];
|
paulson@4776
|
68 |
|
paulson@4776
|
69 |
(*Useful with cancellation, disjunction*)
|
paulson@6536
|
70 |
Goal "F : A LeadsTo (A' Un A') ==> F : A LeadsTo A'";
|
paulson@4776
|
71 |
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
|
paulson@4776
|
72 |
qed "LeadsTo_Un_duplicate";
|
paulson@4776
|
73 |
|
paulson@6536
|
74 |
Goal "F : A LeadsTo (A' Un C Un C) ==> F : A LeadsTo (A' Un C)";
|
paulson@4776
|
75 |
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
|
paulson@4776
|
76 |
qed "LeadsTo_Un_duplicate2";
|
paulson@4776
|
77 |
|
paulson@5277
|
78 |
val prems =
|
paulson@6536
|
79 |
Goal "(!!i. i : I ==> F : (A i) LeadsTo B) ==> F : (UN i:I. A i) LeadsTo B";
|
paulson@6295
|
80 |
by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
|
paulson@4776
|
81 |
by (blast_tac (claset() addIs (LeadsTo_Union::prems)) 1);
|
paulson@4776
|
82 |
qed "LeadsTo_UN";
|
paulson@4776
|
83 |
|
paulson@4776
|
84 |
(*Binary union introduction rule*)
|
paulson@6536
|
85 |
Goal "[| F : A LeadsTo C; F : B LeadsTo C |] ==> F : (A Un B) LeadsTo C";
|
paulson@4776
|
86 |
by (stac Un_eq_Union 1);
|
paulson@4776
|
87 |
by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
|
paulson@4776
|
88 |
qed "LeadsTo_Un";
|
paulson@4776
|
89 |
|
paulson@6710
|
90 |
(*Lets us look at the starting state*)
|
paulson@6710
|
91 |
val prems =
|
paulson@6710
|
92 |
Goal "(!!s. s : A ==> F : {s} LeadsTo B) ==> F : A LeadsTo B";
|
paulson@6710
|
93 |
by (stac (UN_singleton RS sym) 1 THEN rtac LeadsTo_UN 1);
|
paulson@6710
|
94 |
by (blast_tac (claset() addIs prems) 1);
|
paulson@6710
|
95 |
qed "single_LeadsTo_I";
|
paulson@6710
|
96 |
|
paulson@6536
|
97 |
Goal "A <= B ==> F : A LeadsTo B";
|
paulson@5111
|
98 |
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
|
paulson@4776
|
99 |
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
|
paulson@4776
|
100 |
qed "subset_imp_LeadsTo";
|
paulson@4776
|
101 |
|
paulson@4776
|
102 |
bind_thm ("empty_LeadsTo", empty_subsetI RS subset_imp_LeadsTo);
|
paulson@4776
|
103 |
Addsimps [empty_LeadsTo];
|
paulson@4776
|
104 |
|
paulson@6536
|
105 |
Goal "[| F : A LeadsTo A'; A' <= B' |] ==> F : A LeadsTo B'";
|
paulson@5111
|
106 |
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
|
paulson@4776
|
107 |
by (blast_tac (claset() addIs [leadsTo_weaken_R]) 1);
|
paulson@4776
|
108 |
qed_spec_mp "LeadsTo_weaken_R";
|
paulson@4776
|
109 |
|
paulson@6536
|
110 |
Goal "[| F : A LeadsTo A'; B <= A |] \
|
paulson@6536
|
111 |
\ ==> F : B LeadsTo A'";
|
paulson@5111
|
112 |
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
|
paulson@4776
|
113 |
by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1);
|
paulson@4776
|
114 |
qed_spec_mp "LeadsTo_weaken_L";
|
paulson@4776
|
115 |
|
paulson@6536
|
116 |
Goal "[| F : A LeadsTo A'; \
|
paulson@5340
|
117 |
\ B <= A; A' <= B' |] \
|
paulson@6536
|
118 |
\ ==> F : B LeadsTo B'";
|
paulson@5340
|
119 |
by (blast_tac (claset() addIs [LeadsTo_weaken_R, LeadsTo_weaken_L,
|
paulson@5340
|
120 |
LeadsTo_Trans]) 1);
|
paulson@5340
|
121 |
qed "LeadsTo_weaken";
|
paulson@4776
|
122 |
|
paulson@6570
|
123 |
Goal "[| F : Always C; F : A LeadsTo A'; \
|
paulson@5544
|
124 |
\ C Int B <= A; C Int A' <= B' |] \
|
paulson@6536
|
125 |
\ ==> F : B LeadsTo B'";
|
paulson@6570
|
126 |
by (blast_tac (claset() addDs [Always_LeadsToI] addIs[LeadsTo_weaken]
|
paulson@6570
|
127 |
addIs [Always_LeadsToD]) 1);
|
paulson@6570
|
128 |
qed "Always_LeadsTo_weaken";
|
paulson@5340
|
129 |
|
paulson@5340
|
130 |
(** Two theorems for "proof lattices" **)
|
paulson@5340
|
131 |
|
paulson@8216
|
132 |
Goal "F : A LeadsTo B ==> F : (A Un B) LeadsTo B";
|
paulson@5340
|
133 |
by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1);
|
paulson@5340
|
134 |
qed "LeadsTo_Un_post";
|
paulson@5340
|
135 |
|
paulson@6536
|
136 |
Goal "[| F : A LeadsTo B; F : B LeadsTo C |] \
|
paulson@6536
|
137 |
\ ==> F : (A Un B) LeadsTo C";
|
paulson@5340
|
138 |
by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo,
|
paulson@5340
|
139 |
LeadsTo_weaken_L, LeadsTo_Trans]) 1);
|
paulson@5340
|
140 |
qed "LeadsTo_Trans_Un";
|
paulson@5340
|
141 |
|
paulson@5340
|
142 |
|
paulson@5340
|
143 |
(** Distributive laws **)
|
paulson@5340
|
144 |
|
paulson@6536
|
145 |
Goal "(F : (A Un B) LeadsTo C) = (F : A LeadsTo C & F : B LeadsTo C)";
|
paulson@4776
|
146 |
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken_L]) 1);
|
paulson@4776
|
147 |
qed "LeadsTo_Un_distrib";
|
paulson@4776
|
148 |
|
paulson@6536
|
149 |
Goal "(F : (UN i:I. A i) LeadsTo B) = (ALL i : I. F : (A i) LeadsTo B)";
|
paulson@4776
|
150 |
by (blast_tac (claset() addIs [LeadsTo_UN, LeadsTo_weaken_L]) 1);
|
paulson@4776
|
151 |
qed "LeadsTo_UN_distrib";
|
paulson@4776
|
152 |
|
paulson@6536
|
153 |
Goal "(F : (Union S) LeadsTo B) = (ALL A : S. F : A LeadsTo B)";
|
paulson@4776
|
154 |
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_L]) 1);
|
paulson@4776
|
155 |
qed "LeadsTo_Union_distrib";
|
paulson@4776
|
156 |
|
paulson@4776
|
157 |
|
paulson@6570
|
158 |
(** More rules using the premise "Always INV" **)
|
paulson@5277
|
159 |
|
paulson@8122
|
160 |
Goal "F : A Ensures B ==> F : A LeadsTo B";
|
paulson@6575
|
161 |
by (asm_full_simp_tac
|
paulson@8122
|
162 |
(simpset() addsimps [Ensures_def, LeadsTo_def, leadsTo_Basis]) 1);
|
paulson@5313
|
163 |
qed "LeadsTo_Basis";
|
paulson@5313
|
164 |
|
paulson@8122
|
165 |
Goal "[| F : (A-B) Co (A Un B); F : transient (A-B) |] \
|
paulson@8122
|
166 |
\ ==> F : A Ensures B";
|
paulson@8122
|
167 |
by (asm_full_simp_tac
|
paulson@8122
|
168 |
(simpset() addsimps [Ensures_def, Constrains_eq_constrains]) 1);
|
paulson@8122
|
169 |
by (blast_tac (claset() addIs [ensuresI, constrains_weaken,
|
paulson@8122
|
170 |
transient_strengthen]) 1);
|
paulson@8122
|
171 |
qed "EnsuresI";
|
paulson@8122
|
172 |
|
paulson@6570
|
173 |
Goal "[| F : Always INV; \
|
paulson@6536
|
174 |
\ F : (INV Int (A-A')) Co (A Un A'); \
|
paulson@5648
|
175 |
\ F : transient (INV Int (A-A')) |] \
|
paulson@6536
|
176 |
\ ==> F : A LeadsTo A'";
|
paulson@6570
|
177 |
by (rtac Always_LeadsToI 1);
|
paulson@5313
|
178 |
by (assume_tac 1);
|
paulson@8122
|
179 |
by (blast_tac (claset() addIs [EnsuresI, LeadsTo_Basis,
|
paulson@8122
|
180 |
Always_ConstrainsD RS Constrains_weaken,
|
paulson@8122
|
181 |
transient_strengthen]) 1);
|
paulson@6570
|
182 |
qed "Always_LeadsTo_Basis";
|
paulson@5277
|
183 |
|
paulson@5253
|
184 |
(*Set difference: maybe combine with leadsTo_weaken_L??
|
paulson@5253
|
185 |
This is the most useful form of the "disjunction" rule*)
|
paulson@6536
|
186 |
Goal "[| F : (A-B) LeadsTo C; F : (A Int B) LeadsTo C |] \
|
paulson@6536
|
187 |
\ ==> F : A LeadsTo C";
|
paulson@5479
|
188 |
by (blast_tac (claset() addIs [LeadsTo_Un, LeadsTo_weaken]) 1);
|
paulson@4776
|
189 |
qed "LeadsTo_Diff";
|
paulson@4776
|
190 |
|
paulson@4776
|
191 |
|
paulson@5277
|
192 |
val prems =
|
paulson@6536
|
193 |
Goal "(!! i. i:I ==> F : (A i) LeadsTo (A' i)) \
|
paulson@6536
|
194 |
\ ==> F : (UN i:I. A i) LeadsTo (UN i:I. A' i)";
|
paulson@6295
|
195 |
by (simp_tac (HOL_ss addsimps [Union_image_eq RS sym]) 1);
|
paulson@4776
|
196 |
by (blast_tac (claset() addIs [LeadsTo_Union, LeadsTo_weaken_R]
|
paulson@4776
|
197 |
addIs prems) 1);
|
paulson@4776
|
198 |
qed "LeadsTo_UN_UN";
|
paulson@4776
|
199 |
|
paulson@4776
|
200 |
|
paulson@4776
|
201 |
(*Version with no index set*)
|
paulson@5257
|
202 |
val prems =
|
paulson@6536
|
203 |
Goal "(!! i. F : (A i) LeadsTo (A' i)) \
|
paulson@6536
|
204 |
\ ==> F : (UN i. A i) LeadsTo (UN i. A' i)";
|
paulson@4776
|
205 |
by (blast_tac (claset() addIs [LeadsTo_UN_UN]
|
paulson@4776
|
206 |
addIs prems) 1);
|
paulson@4776
|
207 |
qed "LeadsTo_UN_UN_noindex";
|
paulson@4776
|
208 |
|
paulson@4776
|
209 |
(*Version with no index set*)
|
paulson@6536
|
210 |
Goal "ALL i. F : (A i) LeadsTo (A' i) \
|
paulson@6536
|
211 |
\ ==> F : (UN i. A i) LeadsTo (UN i. A' i)";
|
paulson@4776
|
212 |
by (blast_tac (claset() addIs [LeadsTo_UN_UN]) 1);
|
paulson@4776
|
213 |
qed "all_LeadsTo_UN_UN";
|
paulson@4776
|
214 |
|
paulson@4776
|
215 |
|
paulson@4776
|
216 |
(*Binary union version*)
|
paulson@6536
|
217 |
Goal "[| F : A LeadsTo A'; F : B LeadsTo B' |] \
|
paulson@6536
|
218 |
\ ==> F : (A Un B) LeadsTo (A' Un B')";
|
paulson@4776
|
219 |
by (blast_tac (claset() addIs [LeadsTo_Un,
|
paulson@4776
|
220 |
LeadsTo_weaken_R]) 1);
|
paulson@4776
|
221 |
qed "LeadsTo_Un_Un";
|
paulson@4776
|
222 |
|
paulson@4776
|
223 |
|
paulson@4776
|
224 |
(** The cancellation law **)
|
paulson@4776
|
225 |
|
paulson@6536
|
226 |
Goal "[| F : A LeadsTo (A' Un B); F : B LeadsTo B' |] \
|
paulson@6536
|
227 |
\ ==> F : A LeadsTo (A' Un B')";
|
paulson@4776
|
228 |
by (blast_tac (claset() addIs [LeadsTo_Un_Un,
|
paulson@4776
|
229 |
subset_imp_LeadsTo, LeadsTo_Trans]) 1);
|
paulson@4776
|
230 |
qed "LeadsTo_cancel2";
|
paulson@4776
|
231 |
|
paulson@6536
|
232 |
Goal "[| F : A LeadsTo (A' Un B); F : (B-A') LeadsTo B' |] \
|
paulson@6536
|
233 |
\ ==> F : A LeadsTo (A' Un B')";
|
paulson@4776
|
234 |
by (rtac LeadsTo_cancel2 1);
|
paulson@4776
|
235 |
by (assume_tac 2);
|
paulson@4776
|
236 |
by (ALLGOALS Asm_simp_tac);
|
paulson@4776
|
237 |
qed "LeadsTo_cancel_Diff2";
|
paulson@4776
|
238 |
|
paulson@6536
|
239 |
Goal "[| F : A LeadsTo (B Un A'); F : B LeadsTo B' |] \
|
paulson@6536
|
240 |
\ ==> F : A LeadsTo (B' Un A')";
|
paulson@4776
|
241 |
by (asm_full_simp_tac (simpset() addsimps [Un_commute]) 1);
|
paulson@4776
|
242 |
by (blast_tac (claset() addSIs [LeadsTo_cancel2]) 1);
|
paulson@4776
|
243 |
qed "LeadsTo_cancel1";
|
paulson@4776
|
244 |
|
paulson@6536
|
245 |
Goal "[| F : A LeadsTo (B Un A'); F : (B-A') LeadsTo B' |] \
|
paulson@6536
|
246 |
\ ==> F : A LeadsTo (B' Un A')";
|
paulson@4776
|
247 |
by (rtac LeadsTo_cancel1 1);
|
paulson@4776
|
248 |
by (assume_tac 2);
|
paulson@4776
|
249 |
by (ALLGOALS Asm_simp_tac);
|
paulson@4776
|
250 |
qed "LeadsTo_cancel_Diff1";
|
paulson@4776
|
251 |
|
paulson@4776
|
252 |
|
paulson@4776
|
253 |
(** The impossibility law **)
|
paulson@4776
|
254 |
|
paulson@5277
|
255 |
(*The set "A" may be non-empty, but it contains no reachable states*)
|
paulson@6570
|
256 |
Goal "F : A LeadsTo {} ==> F : Always (-A)";
|
paulson@6570
|
257 |
by (full_simp_tac (simpset() addsimps [LeadsTo_def,
|
paulson@6570
|
258 |
Always_eq_includes_reachable]) 1);
|
paulson@6570
|
259 |
by (dtac leadsTo_empty 1);
|
paulson@6570
|
260 |
by Auto_tac;
|
paulson@4776
|
261 |
qed "LeadsTo_empty";
|
paulson@4776
|
262 |
|
paulson@4776
|
263 |
|
paulson@4776
|
264 |
(** PSP: Progress-Safety-Progress **)
|
paulson@4776
|
265 |
|
paulson@5639
|
266 |
(*Special case of PSP: Misra's "stable conjunction"*)
|
paulson@6536
|
267 |
Goal "[| F : A LeadsTo A'; F : Stable B |] \
|
paulson@6536
|
268 |
\ ==> F : (A Int B) LeadsTo (A' Int B)";
|
paulson@6575
|
269 |
by (full_simp_tac
|
paulson@6575
|
270 |
(simpset() addsimps [LeadsTo_eq_leadsTo, Stable_eq_stable]) 1);
|
paulson@5313
|
271 |
by (dtac psp_stable 1);
|
paulson@5313
|
272 |
by (assume_tac 1);
|
paulson@5313
|
273 |
by (asm_full_simp_tac (simpset() addsimps Int_ac) 1);
|
paulson@6710
|
274 |
qed "PSP_Stable";
|
paulson@4776
|
275 |
|
paulson@6536
|
276 |
Goal "[| F : A LeadsTo A'; F : Stable B |] \
|
paulson@6536
|
277 |
\ ==> F : (B Int A) LeadsTo (B Int A')";
|
paulson@6710
|
278 |
by (asm_simp_tac (simpset() addsimps PSP_Stable::Int_ac) 1);
|
paulson@6710
|
279 |
qed "PSP_Stable2";
|
paulson@4776
|
280 |
|
paulson@6575
|
281 |
Goal "[| F : A LeadsTo A'; F : B Co B' |] \
|
paulson@6710
|
282 |
\ ==> F : (A Int B') LeadsTo ((A' Int B) Un (B' - B))";
|
paulson@6575
|
283 |
by (full_simp_tac
|
paulson@6575
|
284 |
(simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1);
|
paulson@5313
|
285 |
by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
|
paulson@5277
|
286 |
qed "PSP";
|
paulson@4776
|
287 |
|
paulson@6536
|
288 |
Goal "[| F : A LeadsTo A'; F : B Co B' |] \
|
paulson@6710
|
289 |
\ ==> F : (B' Int A) LeadsTo ((B Int A') Un (B' - B))";
|
paulson@5536
|
290 |
by (asm_simp_tac (simpset() addsimps PSP::Int_ac) 1);
|
paulson@5277
|
291 |
qed "PSP2";
|
paulson@4776
|
292 |
|
paulson@5313
|
293 |
Goalw [Unless_def]
|
paulson@6536
|
294 |
"[| F : A LeadsTo A'; F : B Unless B' |] \
|
paulson@6536
|
295 |
\ ==> F : (A Int B) LeadsTo ((A' Int B) Un B')";
|
paulson@5277
|
296 |
by (dtac PSP 1);
|
paulson@4776
|
297 |
by (assume_tac 1);
|
paulson@5313
|
298 |
by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken,
|
paulson@5584
|
299 |
subset_imp_LeadsTo]) 1);
|
paulson@5313
|
300 |
qed "PSP_Unless";
|
paulson@4776
|
301 |
|
paulson@4776
|
302 |
|
paulson@5804
|
303 |
Goal "[| F : Stable A; F : transient C; \
|
paulson@6570
|
304 |
\ F : Always (-A Un B Un C) |] ==> F : A LeadsTo B";
|
paulson@6570
|
305 |
by (etac Always_LeadsTo_weaken 1);
|
paulson@5804
|
306 |
by (rtac LeadsTo_Diff 1);
|
paulson@6710
|
307 |
by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_Stable2) 2);
|
paulson@5804
|
308 |
by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
|
paulson@6570
|
309 |
qed "Stable_transient_Always_LeadsTo";
|
paulson@5804
|
310 |
|
paulson@5804
|
311 |
|
paulson@4776
|
312 |
(*** Induction rules ***)
|
paulson@4776
|
313 |
|
paulson@4776
|
314 |
(** Meta or object quantifier ????? **)
|
paulson@5232
|
315 |
Goal "[| wf r; \
|
nipkow@10834
|
316 |
\ ALL m. F : (A Int f-`{m}) LeadsTo \
|
nipkow@10834
|
317 |
\ ((A Int f-`(r^-1 `` {m})) Un B) |] \
|
paulson@6536
|
318 |
\ ==> F : A LeadsTo B";
|
paulson@6575
|
319 |
by (full_simp_tac (simpset() addsimps [LeadsTo_eq_leadsTo]) 1);
|
paulson@4776
|
320 |
by (etac leadsTo_wf_induct 1);
|
paulson@4776
|
321 |
by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
|
paulson@4776
|
322 |
qed "LeadsTo_wf_induct";
|
paulson@4776
|
323 |
|
paulson@4776
|
324 |
|
paulson@5232
|
325 |
Goal "[| wf r; \
|
nipkow@10834
|
326 |
\ ALL m:I. F : (A Int f-`{m}) LeadsTo \
|
nipkow@10834
|
327 |
\ ((A Int f-`(r^-1 `` {m})) Un B) |] \
|
nipkow@10834
|
328 |
\ ==> F : A LeadsTo ((A - (f-`I)) Un B)";
|
paulson@4776
|
329 |
by (etac LeadsTo_wf_induct 1);
|
paulson@4776
|
330 |
by Safe_tac;
|
paulson@4776
|
331 |
by (case_tac "m:I" 1);
|
paulson@4776
|
332 |
by (blast_tac (claset() addIs [LeadsTo_weaken]) 1);
|
paulson@4776
|
333 |
by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 1);
|
paulson@5277
|
334 |
qed "Bounded_induct";
|
paulson@4776
|
335 |
|
paulson@4776
|
336 |
|
paulson@8216
|
337 |
val prems =
|
nipkow@10834
|
338 |
Goal "(!!m::nat. F : (A Int f-`{m}) LeadsTo ((A Int f-`(lessThan m)) Un B)) \
|
paulson@6536
|
339 |
\ ==> F : A LeadsTo B";
|
paulson@4776
|
340 |
by (rtac (wf_less_than RS LeadsTo_wf_induct) 1);
|
paulson@8216
|
341 |
by (auto_tac (claset() addIs prems, simpset()));
|
paulson@5277
|
342 |
qed "LessThan_induct";
|
paulson@4776
|
343 |
|
wenzelm@11701
|
344 |
(*Integer version. Could generalize from Numeral0 to any lower bound*)
|
paulson@5584
|
345 |
val [reach, prem] =
|
wenzelm@11701
|
346 |
Goal "[| F : Always {s. (Numeral0::int) <= f s}; \
|
paulson@6536
|
347 |
\ !! z. F : (A Int {s. f s = z}) LeadsTo \
|
paulson@5584
|
348 |
\ ((A Int {s. f s < z}) Un B) |] \
|
paulson@6536
|
349 |
\ ==> F : A LeadsTo B";
|
paulson@8216
|
350 |
by (res_inst_tac [("f", "nat o f")] LessThan_induct 1);
|
paulson@5544
|
351 |
by (simp_tac (simpset() addsimps [vimage_def]) 1);
|
paulson@6570
|
352 |
by (rtac ([reach, prem] MRS Always_LeadsTo_weaken) 1);
|
paulson@5584
|
353 |
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
|
paulson@5544
|
354 |
qed "integ_0_le_induct";
|
paulson@5544
|
355 |
|
nipkow@10834
|
356 |
Goal "!!l::nat. [| ALL m:(greaterThan l). F : (A Int f-`{m}) LeadsTo \
|
nipkow@10834
|
357 |
\ ((A Int f-`(lessThan m)) Un B) |] \
|
nipkow@10834
|
358 |
\ ==> F : A LeadsTo ((A Int (f-`(atMost l))) Un B)";
|
paulson@4776
|
359 |
by (simp_tac (HOL_ss addsimps [Diff_eq RS sym, vimage_Compl, Compl_greaterThan RS sym]) 1);
|
paulson@5277
|
360 |
by (rtac (wf_less_than RS Bounded_induct) 1);
|
paulson@4776
|
361 |
by (Asm_simp_tac 1);
|
paulson@5277
|
362 |
qed "LessThan_bounded_induct";
|
paulson@4776
|
363 |
|
nipkow@10834
|
364 |
Goal "!!l::nat. [| ALL m:(lessThan l). F : (A Int f-`{m}) LeadsTo \
|
nipkow@10834
|
365 |
\ ((A Int f-`(greaterThan m)) Un B) |] \
|
nipkow@10834
|
366 |
\ ==> F : A LeadsTo ((A Int (f-`(atLeast l))) Un B)";
|
paulson@4776
|
367 |
by (res_inst_tac [("f","f"),("f1", "%k. l - k")]
|
paulson@4776
|
368 |
(wf_less_than RS wf_inv_image RS LeadsTo_wf_induct) 1);
|
paulson@4776
|
369 |
by (simp_tac (simpset() addsimps [inv_image_def, Image_singleton]) 1);
|
paulson@4776
|
370 |
by (Clarify_tac 1);
|
paulson@4776
|
371 |
by (case_tac "m<l" 1);
|
paulson@4776
|
372 |
by (blast_tac (claset() addIs [not_leE, subset_imp_LeadsTo]) 2);
|
paulson@4776
|
373 |
by (blast_tac (claset() addIs [LeadsTo_weaken_R, diff_less_mono2]) 1);
|
paulson@5277
|
374 |
qed "GreaterThan_bounded_induct";
|
paulson@4776
|
375 |
|
paulson@4776
|
376 |
|
paulson@4776
|
377 |
(*** Completion: Binary and General Finite versions ***)
|
paulson@4776
|
378 |
|
paulson@6536
|
379 |
Goal "[| F : A LeadsTo (A' Un C); F : A' Co (A' Un C); \
|
paulson@6536
|
380 |
\ F : B LeadsTo (B' Un C); F : B' Co (B' Un C) |] \
|
paulson@6536
|
381 |
\ ==> F : (A Int B) LeadsTo ((A' Int B') Un C)";
|
paulson@6575
|
382 |
by (full_simp_tac
|
paulson@6575
|
383 |
(simpset() addsimps [LeadsTo_eq_leadsTo, Constrains_eq_constrains,
|
paulson@5313
|
384 |
Int_Un_distrib]) 1);
|
paulson@5313
|
385 |
by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
|
paulson@5277
|
386 |
qed "Completion";
|
paulson@4776
|
387 |
|
paulson@6564
|
388 |
Goal "finite I \
|
paulson@6536
|
389 |
\ ==> (ALL i:I. F : (A i) LeadsTo (A' i Un C)) --> \
|
paulson@6536
|
390 |
\ (ALL i:I. F : (A' i) Co (A' i Un C)) --> \
|
paulson@6536
|
391 |
\ F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)";
|
paulson@4776
|
392 |
by (etac finite_induct 1);
|
paulson@8334
|
393 |
by Auto_tac;
|
paulson@8334
|
394 |
by (rtac Completion 1);
|
paulson@8334
|
395 |
by (simp_tac (HOL_ss addsimps (INT_simps RL [sym])) 4);
|
paulson@8334
|
396 |
by (rtac Constrains_INT 4);
|
paulson@8334
|
397 |
by Auto_tac;
|
paulson@8334
|
398 |
val lemma = result();
|
paulson@8334
|
399 |
|
paulson@8334
|
400 |
val prems = Goal
|
paulson@8334
|
401 |
"[| finite I; \
|
paulson@8334
|
402 |
\ !!i. i:I ==> F : (A i) LeadsTo (A' i Un C); \
|
paulson@8334
|
403 |
\ !!i. i:I ==> F : (A' i) Co (A' i Un C) |] \
|
paulson@8334
|
404 |
\ ==> F : (INT i:I. A i) LeadsTo ((INT i:I. A' i) Un C)";
|
paulson@8334
|
405 |
by (blast_tac (claset() addIs (lemma RS mp RS mp)::prems) 1);
|
paulson@8334
|
406 |
qed "Finite_completion";
|
paulson@8334
|
407 |
|
paulson@8334
|
408 |
Goalw [Stable_def]
|
paulson@8334
|
409 |
"[| F : A LeadsTo A'; F : Stable A'; \
|
paulson@8334
|
410 |
\ F : B LeadsTo B'; F : Stable B' |] \
|
paulson@8334
|
411 |
\ ==> F : (A Int B) LeadsTo (A' Int B')";
|
paulson@8334
|
412 |
by (res_inst_tac [("C1", "{}")] (Completion RS LeadsTo_weaken_R) 1);
|
paulson@8334
|
413 |
by (REPEAT (Force_tac 1));
|
paulson@8334
|
414 |
qed "Stable_completion";
|
paulson@8334
|
415 |
|
paulson@8334
|
416 |
val prems = Goalw [Stable_def]
|
paulson@8334
|
417 |
"[| finite I; \
|
paulson@8334
|
418 |
\ !!i. i:I ==> F : (A i) LeadsTo (A' i); \
|
paulson@8334
|
419 |
\ !!i. i:I ==> F : Stable (A' i) |] \
|
paulson@8334
|
420 |
\ ==> F : (INT i:I. A i) LeadsTo (INT i:I. A' i)";
|
paulson@8334
|
421 |
by (res_inst_tac [("C1", "{}")] (Finite_completion RS LeadsTo_weaken_R) 1);
|
paulson@4776
|
422 |
by (ALLGOALS Asm_simp_tac);
|
paulson@8334
|
423 |
by (ALLGOALS (blast_tac (claset() addIs prems)));
|
paulson@8334
|
424 |
qed "Finite_stable_completion";
|
paulson@5240
|
425 |
|
paulson@5240
|
426 |
|
paulson@5313
|
427 |
(*proves "ensures/leadsTo" properties when the program is specified*)
|
paulson@5426
|
428 |
fun ensures_tac sact =
|
paulson@5240
|
429 |
SELECT_GOAL
|
paulson@6570
|
430 |
(EVERY [REPEAT (Always_Int_tac 1),
|
paulson@6570
|
431 |
etac Always_LeadsTo_Basis 1
|
paulson@5240
|
432 |
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
|
paulson@7522
|
433 |
REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
|
paulson@8122
|
434 |
EnsuresI, ensuresI] 1),
|
paulson@6536
|
435 |
(*now there are two subgoals: co & transient*)
|
paulson@5648
|
436 |
simp_tac (simpset() addsimps !program_defs_ref) 2,
|
paulson@8041
|
437 |
res_inst_tac [("act", sact)] transientI 2,
|
paulson@5340
|
438 |
(*simplify the command's domain*)
|
paulson@5426
|
439 |
simp_tac (simpset() addsimps [Domain_def]) 3,
|
paulson@5426
|
440 |
constrains_tac 1,
|
paulson@5240
|
441 |
ALLGOALS Clarify_tac,
|
paulson@5422
|
442 |
ALLGOALS Asm_full_simp_tac]);
|