author | paulson |
Tue, 31 Aug 1999 15:56:56 +0200 | |
changeset 7399 | cf780c2bcccf |
parent 7361 | 477e1bdf230f |
child 7482 | 7badd511844d |
permissions | -rw-r--r-- |
7186 | 1 |
(* Title: HOL/UNITY/Lift_prog.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
*) |
|
6 |
||
7 |
||
8 |
(*** Basic properties ***) |
|
9 |
||
10 |
(** lift_set and drop_set **) |
|
11 |
||
12 |
Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)"; |
|
13 |
by Auto_tac; |
|
14 |
qed "lift_set_iff"; |
|
15 |
AddIffs [lift_set_iff]; |
|
16 |
||
17 |
Goalw [lift_set_def] "lift_set i (A Int B) = lift_set i A Int lift_set i B"; |
|
18 |
by Auto_tac; |
|
19 |
qed "lift_set_Int"; |
|
20 |
||
21 |
(*Converse fails*) |
|
22 |
Goalw [drop_set_def] "f : A ==> f i : drop_set i A"; |
|
23 |
by Auto_tac; |
|
24 |
qed "drop_set_I"; |
|
25 |
||
26 |
(** lift_act and drop_act **) |
|
27 |
||
28 |
Goalw [lift_act_def] "lift_act i Id = Id"; |
|
29 |
by Auto_tac; |
|
30 |
by (etac rev_mp 1); |
|
31 |
by (dtac sym 1); |
|
32 |
by (asm_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1); |
|
33 |
qed "lift_act_Id"; |
|
34 |
Addsimps [lift_act_Id]; |
|
35 |
||
36 |
Goalw [drop_act_def] "(s, s') : act ==> (s i, s' i) : drop_act i act"; |
|
37 |
by (auto_tac (claset() addSIs [image_eqI], simpset())); |
|
38 |
qed "drop_act_I"; |
|
39 |
||
40 |
Goalw [drop_act_def] "drop_act i Id = Id"; |
|
41 |
by Auto_tac; |
|
42 |
by (res_inst_tac [("x", "((%u. x), (%u. x))")] image_eqI 1); |
|
43 |
by Auto_tac; |
|
44 |
qed "drop_act_Id"; |
|
45 |
Addsimps [drop_act_Id]; |
|
46 |
||
47 |
(** lift_prog and drop_prog **) |
|
48 |
||
49 |
Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)"; |
|
50 |
by Auto_tac; |
|
51 |
qed "Init_lift_prog"; |
|
52 |
Addsimps [Init_lift_prog]; |
|
53 |
||
54 |
Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F"; |
|
55 |
by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset())); |
|
56 |
qed "Acts_lift_prog"; |
|
57 |
Addsimps [Acts_lift_prog]; |
|
58 |
||
59 |
Goalw [drop_prog_def] "Init (drop_prog i F) = drop_set i (Init F)"; |
|
60 |
by Auto_tac; |
|
61 |
qed "Init_drop_prog"; |
|
62 |
Addsimps [Init_drop_prog]; |
|
63 |
||
64 |
Goalw [drop_prog_def] "Acts (drop_prog i F) = drop_act i `` Acts F"; |
|
65 |
by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset())); |
|
66 |
qed "Acts_drop_prog"; |
|
67 |
Addsimps [Acts_drop_prog]; |
|
68 |
||
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
69 |
(** These monotonicity results look natural but are UNUSED **) |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
70 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7361
diff
changeset
|
71 |
Goal "F <= G ==> lift_prog i F <= lift_prog i G"; |
7186 | 72 |
by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); |
73 |
by Auto_tac; |
|
74 |
qed "lift_prog_mono"; |
|
75 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7361
diff
changeset
|
76 |
Goal "F <= G ==> drop_prog i F <= drop_prog i G"; |
7186 | 77 |
by (full_simp_tac (simpset() addsimps [component_eq_subset, drop_set_def]) 1); |
78 |
by Auto_tac; |
|
79 |
qed "drop_prog_mono"; |
|
80 |
||
81 |
Goal "lift_prog i SKIP = SKIP"; |
|
82 |
by (auto_tac (claset() addSIs [program_equalityI], |
|
83 |
simpset() addsimps [SKIP_def, lift_prog_def])); |
|
84 |
qed "lift_prog_SKIP"; |
|
85 |
||
86 |
Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)"; |
|
87 |
by (rtac program_equalityI 1); |
|
88 |
by (auto_tac (claset(), simpset() addsimps [Acts_Join])); |
|
89 |
qed "lift_prog_Join"; |
|
90 |
||
91 |
Goal "lift_prog i (JOIN I F) = (JN j:I. lift_prog i (F j))"; |
|
92 |
by (rtac program_equalityI 1); |
|
93 |
by (auto_tac (claset(), simpset() addsimps [Acts_JN])); |
|
94 |
qed "lift_prog_JN"; |
|
95 |
||
96 |
Goal "drop_prog i SKIP = SKIP"; |
|
97 |
by (auto_tac (claset() addSIs [program_equalityI], |
|
98 |
simpset() addsimps [SKIP_def, drop_set_def, drop_prog_def])); |
|
99 |
qed "drop_prog_SKIP"; |
|
100 |
||
101 |
||
102 |
(** Injectivity of lift_set, lift_act, lift_prog **) |
|
103 |
||
104 |
Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F"; |
|
105 |
by Auto_tac; |
|
106 |
qed "lift_set_inverse"; |
|
107 |
Addsimps [lift_set_inverse]; |
|
108 |
||
109 |
Goal "inj (lift_set i)"; |
|
110 |
by (rtac inj_on_inverseI 1); |
|
111 |
by (rtac lift_set_inverse 1); |
|
112 |
qed "inj_lift_set"; |
|
113 |
||
114 |
(*Because A and B could differ outside i, cannot generalize result to |
|
115 |
drop_set i (A Int B) = drop_set i A Int drop_set i B |
|
116 |
*) |
|
117 |
Goalw [lift_set_def, drop_set_def] |
|
118 |
"drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)"; |
|
119 |
by Auto_tac; |
|
120 |
qed "drop_set_lift_set_Int"; |
|
121 |
||
122 |
Goalw [lift_set_def, drop_set_def] |
|
123 |
"drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A"; |
|
124 |
by Auto_tac; |
|
125 |
qed "drop_set_lift_set_Int2"; |
|
126 |
||
127 |
Goalw [drop_set_def] |
|
128 |
"i : I ==> drop_set i (INT j:I. lift_set j A) = A"; |
|
129 |
by Auto_tac; |
|
130 |
qed "drop_set_INT"; |
|
131 |
||
132 |
Goalw [lift_act_def, drop_act_def] "drop_act i (lift_act i act) = act"; |
|
133 |
by Auto_tac; |
|
134 |
by (res_inst_tac [("x", "f(i:=a)")] exI 1); |
|
135 |
by (Asm_simp_tac 1); |
|
136 |
by (res_inst_tac [("x", "f(i:=b)")] exI 1); |
|
137 |
by (Asm_simp_tac 1); |
|
138 |
by (rtac ext 1); |
|
139 |
by (Asm_simp_tac 1); |
|
140 |
qed "lift_act_inverse"; |
|
141 |
Addsimps [lift_act_inverse]; |
|
142 |
||
143 |
Goal "inj (lift_act i)"; |
|
144 |
by (rtac inj_on_inverseI 1); |
|
145 |
by (rtac lift_act_inverse 1); |
|
146 |
qed "inj_lift_act"; |
|
147 |
||
148 |
Goal "drop_prog i (lift_prog i F) = F"; |
|
149 |
by (simp_tac (simpset() addsimps [lift_prog_def, drop_prog_def]) 1); |
|
150 |
by (rtac program_equalityI 1); |
|
151 |
by (simp_tac (simpset() addsimps [image_compose RS sym, o_def]) 2); |
|
152 |
by (Simp_tac 1); |
|
153 |
qed "lift_prog_inverse"; |
|
154 |
Addsimps [lift_prog_inverse]; |
|
155 |
||
156 |
Goal "inj (lift_prog i)"; |
|
157 |
by (rtac inj_on_inverseI 1); |
|
158 |
by (rtac lift_prog_inverse 1); |
|
159 |
qed "inj_lift_prog"; |
|
160 |
||
161 |
||
162 |
(*For compatibility with the original definition and perhaps simpler proofs*) |
|
163 |
Goalw [lift_act_def] |
|
164 |
"((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)"; |
|
165 |
by Auto_tac; |
|
166 |
by (rtac exI 1); |
|
167 |
by Auto_tac; |
|
168 |
qed "lift_act_eq"; |
|
169 |
AddIffs [lift_act_eq]; |
|
170 |
||
171 |
||
172 |
(*** Safety: co, stable, invariant ***) |
|
173 |
||
174 |
(** Safety and lift_prog **) |
|
175 |
||
176 |
Goal "(lift_prog i F : (lift_set i A) co (lift_set i B)) = \ |
|
177 |
\ (F : A co B)"; |
|
178 |
by (auto_tac (claset(), |
|
179 |
simpset() addsimps [constrains_def])); |
|
180 |
by (Blast_tac 2); |
|
181 |
by (Force_tac 1); |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
182 |
qed "lift_prog_constrains"; |
7186 | 183 |
|
184 |
Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)"; |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
185 |
by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains]) 1); |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
186 |
qed "lift_prog_stable"; |
7186 | 187 |
|
188 |
Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)"; |
|
189 |
by (auto_tac (claset(), |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
190 |
simpset() addsimps [invariant_def, lift_prog_stable])); |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
191 |
qed "lift_prog_invariant"; |
7186 | 192 |
|
193 |
(*This one looks strange! Proof probably is by case analysis on i=j. |
|
194 |
If i~=j then lift_prog j (F j) does nothing to lift_set i, and the |
|
195 |
premise ensures A<=B.*) |
|
196 |
Goal "F i : A co B \ |
|
197 |
\ ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)"; |
|
198 |
by (auto_tac (claset(), |
|
199 |
simpset() addsimps [constrains_def])); |
|
200 |
by (REPEAT (Blast_tac 1)); |
|
201 |
qed "constrains_imp_lift_prog_constrains"; |
|
202 |
||
203 |
||
204 |
(** Safety and drop_prog **) |
|
205 |
||
206 |
Goalw [constrains_def] |
|
207 |
"(drop_prog i F : A co B) = (F : (lift_set i A) co (lift_set i B))"; |
|
208 |
by Auto_tac; |
|
209 |
by (force_tac (claset(), |
|
210 |
simpset() addsimps [drop_act_def]) 2); |
|
211 |
by (blast_tac (claset() addIs [drop_act_I]) 1); |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
212 |
qed "drop_prog_constrains"; |
7186 | 213 |
|
214 |
Goal "(drop_prog i F : stable A) = (F : stable (lift_set i A))"; |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
215 |
by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1); |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
216 |
qed "drop_prog_stable"; |
7186 | 217 |
|
218 |
||
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
219 |
(*** Diff, needed for localTo ***) |
7186 | 220 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7361
diff
changeset
|
221 |
(** THESE PROOFS CAN BE GENERALIZED AS IN EXTEND.ML **) |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7361
diff
changeset
|
222 |
|
7186 | 223 |
Goal "Diff G (lift_act i `` Acts F) : (lift_set i A) co (lift_set i B) \ |
224 |
\ ==> Diff (drop_prog i G) (Acts F) : A co B"; |
|
225 |
by (auto_tac (claset(), |
|
226 |
simpset() addsimps [constrains_def, Diff_def])); |
|
227 |
by (dtac bspec 1); |
|
228 |
by (Force_tac 1); |
|
229 |
by (auto_tac (claset(), simpset() addsimps [drop_act_def])); |
|
230 |
by (auto_tac (claset(), simpset() addsimps [lift_set_def])); |
|
231 |
qed "Diff_drop_prog_co"; |
|
232 |
||
233 |
Goalw [stable_def] |
|
234 |
"Diff G (lift_act i `` Acts F) : stable (lift_set i A) \ |
|
235 |
\ ==> Diff (drop_prog i G) (Acts F) : stable A"; |
|
236 |
by (etac Diff_drop_prog_co 1); |
|
237 |
qed "Diff_drop_prog_stable"; |
|
238 |
||
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
239 |
Goalw [constrains_def, Diff_def] |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
240 |
"Diff G (Acts F) : A co B \ |
7186 | 241 |
\ ==> Diff (lift_prog i G) (lift_act i `` Acts F) \ |
242 |
\ : (lift_set i A) co (lift_set i B)"; |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
243 |
by Auto_tac; |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
244 |
by (Blast_tac 1); |
7186 | 245 |
qed "Diff_lift_prog_co"; |
246 |
||
247 |
Goalw [stable_def] |
|
248 |
"Diff G (Acts F) : stable A \ |
|
249 |
\ ==> Diff (lift_prog i G) (lift_act i `` Acts F) : stable (lift_set i A)"; |
|
250 |
by (etac Diff_lift_prog_co 1); |
|
251 |
qed "Diff_lift_prog_stable"; |
|
252 |
||
253 |
||
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
254 |
(*** Weak safety primitives: Co, Stable ***) |
7186 | 255 |
|
256 |
(** Reachability **) |
|
257 |
||
258 |
Goal "s : reachable F ==> f(i:=s) : reachable (lift_prog i F)"; |
|
259 |
by (etac reachable.induct 1); |
|
260 |
by (force_tac (claset() addIs [reachable.Acts, ext], |
|
261 |
simpset()) 2); |
|
262 |
by (force_tac (claset() addIs [reachable.Init], simpset()) 1); |
|
263 |
qed "reachable_lift_progI"; |
|
264 |
||
265 |
Goal "f : reachable (lift_prog i F) ==> f i : reachable F"; |
|
266 |
by (etac reachable.induct 1); |
|
267 |
by Auto_tac; |
|
268 |
by (ALLGOALS (blast_tac (claset() addIs reachable.intrs))); |
|
269 |
qed "reachable_lift_progD"; |
|
270 |
||
271 |
Goal "reachable (lift_prog i F) = lift_set i (reachable F)"; |
|
272 |
by Auto_tac; |
|
273 |
by (etac reachable_lift_progD 1); |
|
274 |
ren "f" 1; |
|
275 |
by (dres_inst_tac [("f","f"),("i","i")] reachable_lift_progI 1); |
|
276 |
by Auto_tac; |
|
277 |
qed "reachable_lift_prog"; |
|
278 |
||
279 |
Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B)) = \ |
|
280 |
\ (F : A Co B)"; |
|
281 |
by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog, |
|
282 |
lift_set_Int RS sym, |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
283 |
lift_prog_constrains]) 1); |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
284 |
qed "lift_prog_Constrains"; |
7186 | 285 |
|
286 |
Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)"; |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
287 |
by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1); |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
288 |
qed "lift_prog_Stable"; |
7186 | 289 |
|
290 |
(** Reachability and drop_prog **) |
|
291 |
||
292 |
Goal "f : reachable F ==> f i : reachable (drop_prog i F)"; |
|
293 |
by (etac reachable.induct 1); |
|
294 |
by (force_tac (claset() addIs [reachable.Acts, drop_act_I], |
|
295 |
simpset()) 2); |
|
296 |
by (force_tac (claset() addIs [reachable.Init, drop_set_I], |
|
297 |
simpset()) 1); |
|
298 |
qed "reachable_imp_reachable_drop_prog"; |
|
299 |
||
300 |
(*Converse fails because it would require |
|
301 |
[| s i : reachable (drop_prog i F); s i : A |] ==> s : reachable F |
|
302 |
*) |
|
303 |
Goalw [Constrains_def] |
|
304 |
"drop_prog i F : A Co B ==> F : (lift_set i A) Co (lift_set i B)"; |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
305 |
by (full_simp_tac (simpset() addsimps [drop_prog_constrains]) 1); |
7186 | 306 |
by (etac constrains_weaken_L 1); |
307 |
by Auto_tac; |
|
308 |
by (etac reachable_imp_reachable_drop_prog 1); |
|
309 |
qed "drop_prog_Constrains_D"; |
|
310 |
||
311 |
Goalw [Stable_def] |
|
312 |
"drop_prog i F : Stable A ==> F : Stable (lift_set i A)"; |
|
313 |
by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1); |
|
314 |
qed "drop_prog_Stable_D"; |
|
315 |
||
316 |
||
317 |
(*** Programs of the form lift_prog i F Join G |
|
318 |
in other words programs containing a replicated component ***) |
|
319 |
||
320 |
Goal "drop_prog i ((lift_prog i F) Join G) = F Join (drop_prog i G)"; |
|
321 |
by (rtac program_equalityI 1); |
|
322 |
by (simp_tac (simpset() addsimps [Acts_Join, image_Un, |
|
323 |
image_compose RS sym, o_def]) 2); |
|
324 |
by (simp_tac (simpset() addsimps [drop_set_lift_set_Int]) 1); |
|
325 |
qed "drop_prog_lift_prog_Join"; |
|
326 |
||
327 |
Goal "(lift_prog i F) Join G = lift_prog i H \ |
|
328 |
\ ==> H = F Join (drop_prog i G)"; |
|
329 |
by (dres_inst_tac [("f", "drop_prog i")] arg_cong 1); |
|
330 |
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1); |
|
331 |
by (etac sym 1); |
|
332 |
qed "lift_prog_Join_eq_lift_prog_D"; |
|
333 |
||
334 |
Goal "f : reachable (lift_prog i F Join G) \ |
|
335 |
\ ==> f i : reachable (F Join drop_prog i G)"; |
|
336 |
by (etac reachable.induct 1); |
|
337 |
by (force_tac (claset() addIs [reachable.Init, drop_set_I], simpset()) 1); |
|
338 |
(*By case analysis on whether the action is of lift_prog i F or G*) |
|
339 |
by (force_tac (claset() addIs [reachable.Acts, drop_act_I], |
|
340 |
simpset() addsimps [Acts_Join, image_iff]) 1); |
|
341 |
qed "reachable_lift_prog_Join_D"; |
|
342 |
||
343 |
(*Opposite inclusion fails, even for the initial state: lift_set i includes |
|
344 |
ALL functions determined only by their value at i.*) |
|
345 |
Goal "reachable (lift_prog i F Join G) <= \ |
|
346 |
\ lift_set i (reachable (F Join drop_prog i G))"; |
|
347 |
by Auto_tac; |
|
348 |
by (etac reachable_lift_prog_Join_D 1); |
|
349 |
qed "reachable_lift_prog_Join_subset"; |
|
350 |
||
7361 | 351 |
Goalw [Constrains_def] |
352 |
"F Join drop_prog i G : A Co B \ |
|
353 |
\ ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)"; |
|
7186 | 354 |
by (subgoal_tac |
355 |
"lift_prog i F Join G : lift_set i (reachable (F Join drop_prog i G)) Int \ |
|
356 |
\ lift_set i A \ |
|
7361 | 357 |
\ co lift_set i B" 1); |
7186 | 358 |
by (asm_full_simp_tac |
359 |
(simpset() addsimps [lift_set_Int RS sym, |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
360 |
lift_prog_constrains, |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
361 |
drop_prog_constrains RS sym, |
7186 | 362 |
drop_prog_lift_prog_Join]) 2); |
363 |
by (blast_tac (claset() addIs [constrains_weaken, |
|
364 |
reachable_lift_prog_Join_D]) 1); |
|
7361 | 365 |
qed "lift_prog_Join_Constrains"; |
366 |
||
367 |
Goal "F Join drop_prog i G : Stable A \ |
|
368 |
\ ==> lift_prog i F Join G : Stable (lift_set i A)"; |
|
369 |
by (asm_full_simp_tac (simpset() addsimps [Stable_def, |
|
370 |
lift_prog_Join_Constrains]) 1); |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
371 |
qed "lift_prog_Join_Stable"; |
7186 | 372 |
|
373 |
||
374 |
(*** guarantees properties ***) |
|
375 |
||
376 |
(** It seems that neither of these can be proved from the other. **) |
|
377 |
||
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
378 |
(*Strong precondition and postcondition; doesn't seem very useful. |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
379 |
Probably can be strengthened to an equivalance.*) |
7361 | 380 |
Goal "F : X guarantees Y \ |
381 |
\ ==> lift_prog i F : (lift_prog i `` X) guarantees (lift_prog i `` Y)"; |
|
7186 | 382 |
by (rtac guaranteesI 1); |
383 |
by Auto_tac; |
|
384 |
by (blast_tac (claset() addDs [lift_prog_Join_eq_lift_prog_D, guaranteesD]) 1); |
|
385 |
qed "lift_prog_guarantees"; |
|
386 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7361
diff
changeset
|
387 |
(*Weak precondition and postcondition; this is the good one! |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7361
diff
changeset
|
388 |
CAN WEAKEN 2ND PREMISE TO |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7361
diff
changeset
|
389 |
!!G. extend h F Join G : XX ==> F Join project h G : X; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7361
diff
changeset
|
390 |
*) |
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
391 |
val [xguary,drop_prog,lift_prog] = |
7361 | 392 |
Goal "[| F : X guarantees Y; \ |
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
393 |
\ !!H. H : XX ==> drop_prog i H : X; \ |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
394 |
\ !!G. F Join drop_prog i G : Y ==> lift_prog i F Join G : YY |] \ |
7361 | 395 |
\ ==> lift_prog i F : XX guarantees YY"; |
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
396 |
by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1); |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
397 |
by (dtac drop_prog 1); |
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
398 |
by (full_simp_tac (simpset() addsimps [drop_prog_lift_prog_Join]) 1); |
7186 | 399 |
qed "drop_prog_guarantees"; |
400 |
||
401 |
||
402 |
(*** sub ***) |
|
403 |
||
404 |
Addsimps [sub_def]; |
|
405 |
||
406 |
Goal "lift_set i {s. P s} = {s. P (sub i s)}"; |
|
407 |
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1); |
|
408 |
qed "lift_set_sub"; |
|
409 |
||
410 |
Goal "{s. P (s i)} = lift_set i {s. P s}"; |
|
411 |
by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1); |
|
412 |
qed "Collect_eq_lift_set"; |
|
413 |
||
414 |
||
415 |
(** Are these two useful?? **) |
|
416 |
||
417 |
(*The other direction fails: having FF : Stable {s. z <= f (s i)} does not |
|
418 |
ensure that F has the form lift_prog i F for some F.*) |
|
419 |
Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}"; |
|
420 |
by Auto_tac; |
|
421 |
by (stac Collect_eq_lift_set 1); |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
422 |
by (asm_simp_tac (simpset() addsimps [lift_prog_Stable]) 1); |
7186 | 423 |
qed "image_lift_prog_Stable"; |
424 |
||
425 |
Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)"; |
|
426 |
by (simp_tac (simpset() addsimps [Increasing_def, |
|
427 |
inj_lift_prog RS image_INT]) 1); |
|
428 |
by (blast_tac (claset() addIs [impOfSubs image_lift_prog_Stable]) 1); |
|
429 |
qed "image_lift_prog_Increasing"; |
|
430 |
||
431 |
||
432 |
(*** guarantees corollaries ***) |
|
433 |
||
434 |
Goalw [increasing_def] |
|
7361 | 435 |
"F : UNIV guarantees increasing f \ |
436 |
\ ==> lift_prog i F : UNIV guarantees increasing (f o sub i)"; |
|
7186 | 437 |
by (etac drop_prog_guarantees 1); |
438 |
by Auto_tac; |
|
439 |
by (stac Collect_eq_lift_set 1); |
|
440 |
by (asm_full_simp_tac |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
441 |
(simpset() addsimps [lift_prog_stable, drop_prog_stable, |
7186 | 442 |
stable_Join]) 1); |
443 |
qed "lift_prog_guar_increasing"; |
|
444 |
||
445 |
Goalw [Increasing_def] |
|
7361 | 446 |
"F : UNIV guarantees Increasing f \ |
447 |
\ ==> lift_prog i F : UNIV guarantees Increasing (f o sub i)"; |
|
7186 | 448 |
by (etac drop_prog_guarantees 1); |
449 |
by Auto_tac; |
|
450 |
by (stac Collect_eq_lift_set 1); |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
451 |
by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable]) 1); |
7186 | 452 |
qed "lift_prog_guar_Increasing"; |
453 |
||
454 |
Goalw [localTo_def, increasing_def] |
|
7361 | 455 |
"F : (f localTo F) guarantees increasing f \ |
7186 | 456 |
\ ==> lift_prog i F : (f o sub i) localTo (lift_prog i F) \ |
7361 | 457 |
\ guarantees increasing (f o sub i)"; |
7186 | 458 |
by (etac drop_prog_guarantees 1); |
459 |
by Auto_tac; |
|
460 |
by (stac Collect_eq_lift_set 2); |
|
461 |
(*the "increasing" guarantee*) |
|
462 |
by (asm_full_simp_tac |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
463 |
(simpset() addsimps [lift_prog_stable, drop_prog_stable, |
7186 | 464 |
stable_Join]) 2); |
465 |
(*the "localTo" requirement*) |
|
466 |
by (asm_simp_tac |
|
467 |
(simpset() addsimps [Diff_drop_prog_stable, |
|
468 |
Collect_eq_lift_set RS sym]) 1); |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
469 |
qed "lift_prog_localTo_guar_increasing"; |
7186 | 470 |
|
471 |
Goalw [localTo_def, Increasing_def] |
|
7361 | 472 |
"F : (f localTo F) guarantees Increasing f \ |
7186 | 473 |
\ ==> lift_prog i F : (f o sub i) localTo (lift_prog i F) \ |
7361 | 474 |
\ guarantees Increasing (f o sub i)"; |
7186 | 475 |
by (etac drop_prog_guarantees 1); |
476 |
by Auto_tac; |
|
477 |
by (stac Collect_eq_lift_set 2); |
|
478 |
(*the "Increasing" guarantee*) |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
479 |
by (asm_simp_tac (simpset() addsimps [lift_prog_Join_Stable]) 2); |
7186 | 480 |
(*the "localTo" requirement*) |
481 |
by (asm_simp_tac |
|
482 |
(simpset() addsimps [Diff_drop_prog_stable, |
|
483 |
Collect_eq_lift_set RS sym]) 1); |
|
7343
4fa705cedbdb
renamed some theorems; also better natural deduction style for old ones
paulson
parents:
7186
diff
changeset
|
484 |
qed "lift_prog_localTo_guar_Increasing"; |
7186 | 485 |
|
486 |
(*Converse fails. Useful?*) |
|
487 |
Goal "lift_prog i `` (f localTo F) <= (f o sub i) localTo (lift_prog i F)"; |
|
488 |
by (simp_tac (simpset() addsimps [localTo_def]) 1); |
|
489 |
by Auto_tac; |
|
490 |
by (stac Collect_eq_lift_set 1); |
|
491 |
by (asm_simp_tac (simpset() addsimps [Diff_lift_prog_stable]) 1); |
|
492 |
qed "localTo_lift_prog_I"; |