1 (* Title: HOL/UNITY/Lift_prog.ML |
1 (* Title: HOL/UNITY/Lift_prog.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 Arrays of processes. Many results are instances of those in Extend & Project. |
6 Arrays of processes. |
7 *) |
7 *) |
8 |
8 |
9 |
9 Addsimps [insert_map_def, delete_map_def]; |
10 (*** Basic properties ***) |
10 |
11 |
11 Goal "delete_map i (insert_map i x f) = f"; |
12 (** lift_set and drop_set **) |
12 by (rtac ext 1); |
13 |
13 by (Simp_tac 1); |
14 Goalw [lift_set_def] "(f : lift_set i A) = (f i : A)"; |
14 qed "insert_map_inverse"; |
15 by Auto_tac; |
15 |
16 qed "lift_set_iff"; |
16 Goal "(insert_map i x (delete_map i g)) = g(i:=x)"; |
17 AddIffs [lift_set_iff]; |
17 by (rtac ext 1); |
18 |
18 by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
19 Goalw [lift_set_def] "lift_set i A Int lift_set i B = lift_set i (A Int B)"; |
19 by (exhaust_tac "d" 1); |
20 by Auto_tac; |
20 by (ALLGOALS Asm_simp_tac); |
21 qed "Int_lift_set"; |
21 qed "insert_map_delete_map_eq"; |
22 |
22 |
23 Goalw [lift_set_def] "lift_set i A Un lift_set i B = lift_set i (A Un B)"; |
23 (*** Injectiveness proof ***) |
24 by Auto_tac; |
24 |
25 qed "Un_lift_set"; |
25 Goal "(insert_map i x f) = (insert_map i y g) ==> x=y"; |
26 |
26 by (dres_inst_tac [("x","i")] fun_cong 1); |
27 Goalw [lift_set_def] "lift_set i A - lift_set i B = lift_set i (A-B)"; |
27 by (Full_simp_tac 1); |
28 by Auto_tac; |
28 qed "insert_map_inject1"; |
29 qed "Diff_lift_set"; |
29 |
30 |
30 Goal "(insert_map i x f) = (insert_map i y g) ==> f=g"; |
31 Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set]; |
31 by (dres_inst_tac [("f", "delete_map i")] arg_cong 1); |
32 |
32 by (full_simp_tac (simpset() addsimps [insert_map_inverse]) 1); |
33 (** lift_act and drop_act **) |
33 qed "insert_map_inject2"; |
34 |
34 |
35 (*For compatibility with the original definition and perhaps simpler proofs*) |
35 Goal "(insert_map i x f) = (insert_map i y g) ==> x=y & f=g"; |
36 Goalw [lift_act_def] |
36 by (blast_tac (claset() addDs [insert_map_inject1, insert_map_inject2]) 1); |
37 "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)"; |
37 bind_thm ("insert_map_inject", result() RS conjE); |
38 by Auto_tac; |
38 AddSEs [insert_map_inject]; |
39 by (rtac exI 1); |
39 |
40 by Auto_tac; |
40 (*The general case: we don't assume i=i'*) |
41 qed "lift_act_eq"; |
41 Goalw [lift_map_def] |
42 AddIffs [lift_act_eq]; |
42 "(lift_map i (s,(f,uu)) = lift_map i' (s',(f',uu'))) \ |
43 |
43 \ = (uu = uu' & insert_map i s f = insert_map i' s' f')"; |
44 (** lift_prog and drop_prog **) |
44 by Auto_tac; |
45 |
45 qed "lift_map_eq_iff"; |
46 Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)"; |
46 AddIffs [lift_map_eq_iff]; |
47 by Auto_tac; |
47 |
48 qed "Init_lift_prog"; |
48 Goalw [lift_map_def, drop_map_def] "!!s. drop_map i (lift_map i s) = s"; |
49 Addsimps [Init_lift_prog]; |
49 by (force_tac (claset() addIs [insert_map_inverse], simpset()) 1); |
50 |
50 qed "drop_map_lift_map_eq"; |
51 Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F"; |
51 |
52 by (auto_tac (claset() addIs [rev_image_eqI], simpset())); |
52 Goalw [lift_map_def] "inj (lift_map i)"; |
53 qed "Acts_lift_prog"; |
53 by (rtac injI 1); |
54 Addsimps [Acts_lift_prog]; |
54 by Auto_tac; |
55 |
55 qed "inj_lift_map"; |
56 Goalw [drop_prog_def] "Init (drop_prog i C F) = drop_set i (Init F)"; |
56 |
57 by Auto_tac; |
57 (*** Surjectiveness proof ***) |
58 qed "Init_drop_prog"; |
58 |
59 Addsimps [Init_drop_prog]; |
59 Goalw [lift_map_def, drop_map_def] "!!s. lift_map i (drop_map i s) = s"; |
60 |
60 by (force_tac (claset(), simpset() addsimps [insert_map_delete_map_eq]) 1); |
61 Goal "Acts (drop_prog i C F) = insert Id (drop_act i `` Restrict C `` Acts F)"; |
61 qed "lift_map_drop_map_eq"; |
62 by (auto_tac (claset() addIs [image_eqI], |
62 |
63 simpset() addsimps [drop_prog_def])); |
63 Goal "(drop_map i s) = (drop_map i s') ==> s=s'"; |
64 qed "Acts_drop_prog"; |
64 by (dres_inst_tac [("f", "lift_map i")] arg_cong 1); |
65 Addsimps [Acts_drop_prog]; |
65 by (full_simp_tac (simpset() addsimps [lift_map_drop_map_eq]) 1); |
66 |
66 qed "drop_map_inject"; |
|
67 AddSDs [drop_map_inject]; |
|
68 |
|
69 Goal "surj (lift_map i)"; |
|
70 by (rtac surjI 1); |
|
71 by (rtac lift_map_drop_map_eq 1); |
|
72 qed "surj_lift_map"; |
|
73 |
|
74 Goal "bij (lift_map i)"; |
|
75 by (simp_tac (simpset() addsimps [bij_def, inj_lift_map, surj_lift_map]) 1); |
|
76 qed "bij_lift_map"; |
|
77 AddIffs [bij_lift_map]; |
|
78 |
|
79 AddIffs [bij_lift_map RS mem_rename_act_iff]; |
|
80 |
|
81 Goal "inv (lift_map i) = drop_map i"; |
|
82 by (rtac inv_equality 1); |
|
83 by (rtac lift_map_drop_map_eq 2); |
|
84 by (rtac drop_map_lift_map_eq 1); |
|
85 qed "inv_lift_map_eq"; |
|
86 Addsimps [inv_lift_map_eq]; |
67 |
87 |
68 (*** sub ***) |
88 (*** sub ***) |
69 |
89 |
70 Goal "sub i f = f i"; |
90 Goal "sub i f = f i"; |
71 by (simp_tac (simpset() addsimps [sub_def]) 1); |
91 by (simp_tac (simpset() addsimps [sub_def]) 1); |
72 qed "sub_apply"; |
92 qed "sub_apply"; |
73 Addsimps [sub_apply]; |
93 Addsimps [sub_apply]; |
74 |
94 |
75 Goal "lift_set i {s. P s} = {s. P (sub i s)}"; |
95 Goal "lift_set i {s. P s} = {s. P (drop_map i s)}"; |
76 by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1); |
96 by (rtac set_ext 1); |
77 qed "lift_set_sub"; |
97 by (asm_simp_tac (simpset() delsimps [image_Collect] |
78 |
98 addsimps [lift_set_def, rename_set_eq_Collect]) 1); |
79 Goal "{s. P (s i)} = lift_set i {s. P s}"; |
99 qed "lift_set_eq_Collect"; |
80 by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1); |
100 |
81 qed "Collect_eq_lift_set"; |
101 Goalw [lift_set_def] "lift_set i {} = {}"; |
82 |
102 by Auto_tac; |
83 Goal "sub i -`` A = lift_set i A"; |
103 qed "lift_set_empty"; |
|
104 Addsimps [lift_set_empty]; |
|
105 |
|
106 Goalw [lift_set_def] "(lift_map i x : lift_set i A) = (x : A)"; |
|
107 by (rtac (inj_lift_map RS inj_image_mem_iff) 1); |
|
108 qed "lift_set_iff"; |
|
109 AddIffs [lift_set_iff]; |
|
110 |
|
111 Goal "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)"; |
|
112 by (asm_simp_tac (simpset() addsimps [lift_set_def, |
|
113 mem_rename_set_iff, drop_map_def]) 1); |
|
114 qed "lift_set_iff"; |
|
115 AddIffs [lift_set_iff]; |
|
116 |
|
117 Goalw [lift_set_def] "A<=B ==> lift_set i A <= lift_set i B"; |
|
118 by (etac image_mono 1); |
|
119 qed "lift_set_mono"; |
|
120 |
|
121 Goalw [lift_set_def] "lift_set i (A Un B) = lift_set i A Un lift_set i B"; |
|
122 by (asm_simp_tac (simpset() addsimps [image_Un]) 1); |
|
123 qed "lift_set_Un_distrib"; |
|
124 |
|
125 Goalw [lift_set_def] "lift_set i (A-B) = lift_set i A - lift_set i B"; |
|
126 by (rtac (inj_lift_map RS image_set_diff) 1); |
|
127 qed "lift_set_Diff_distrib"; |
|
128 |
|
129 |
|
130 (*** the lattice operations ***) |
|
131 |
|
132 Goalw [lift_def] "lift i SKIP = SKIP"; |
|
133 by (Asm_simp_tac 1); |
|
134 qed "lift_SKIP"; |
|
135 Addsimps [lift_SKIP]; |
|
136 |
|
137 Goalw [lift_def] "lift i (F Join G) = lift i F Join lift i G"; |
|
138 by (Asm_simp_tac 1); |
|
139 qed "lift_Join"; |
|
140 Addsimps [lift_Join]; |
|
141 |
|
142 Goalw [lift_def] "lift j (JOIN I F) = (JN i:I. lift j (F i))"; |
|
143 by (Asm_simp_tac 1); |
|
144 qed "lift_JN"; |
|
145 Addsimps [lift_JN]; |
|
146 |
|
147 (*** Safety: co, stable, invariant ***) |
|
148 |
|
149 Goalw [lift_def, lift_set_def] |
|
150 "(lift i F : (lift_set i A) co (lift_set i B)) = (F : A co B)"; |
|
151 by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1); |
|
152 qed "lift_constrains"; |
|
153 |
|
154 Goalw [lift_def, lift_set_def] |
|
155 "(lift i F : stable (lift_set i A)) = (F : stable A)"; |
|
156 by (asm_simp_tac (simpset() addsimps [rename_stable]) 1); |
|
157 qed "lift_stable"; |
|
158 |
|
159 Goalw [lift_def, lift_set_def] |
|
160 "(lift i F : invariant (lift_set i A)) = (F : invariant A)"; |
|
161 by (asm_simp_tac (simpset() addsimps [rename_invariant]) 1); |
|
162 qed "lift_invariant"; |
|
163 |
|
164 Goalw [lift_def, lift_set_def] |
|
165 "(lift i F : (lift_set i A) Co (lift_set i B)) = (F : A Co B)"; |
|
166 by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1); |
|
167 qed "lift_Constrains"; |
|
168 |
|
169 Goalw [lift_def, lift_set_def] |
|
170 "(lift i F : Stable (lift_set i A)) = (F : Stable A)"; |
|
171 by (asm_simp_tac (simpset() addsimps [rename_Stable]) 1); |
|
172 qed "lift_Stable"; |
|
173 |
|
174 Goalw [lift_def, lift_set_def] |
|
175 "(lift i F : Always (lift_set i A)) = (F : Always A)"; |
|
176 by (asm_simp_tac (simpset() addsimps [rename_Always]) 1); |
|
177 qed "lift_Always"; |
|
178 |
|
179 (*** Progress: transient, ensures ***) |
|
180 |
|
181 Goalw [lift_def, lift_set_def] |
|
182 "(lift i F : transient (lift_set i A)) = (F : transient A)"; |
|
183 by (asm_simp_tac (simpset() addsimps [rename_transient]) 1); |
|
184 qed "lift_transient"; |
|
185 |
|
186 Goalw [lift_def, lift_set_def] |
|
187 "(lift i F : (lift_set i A) ensures (lift_set i B)) = \ |
|
188 \ (F : A ensures B)"; |
|
189 by (asm_simp_tac (simpset() addsimps [rename_ensures]) 1); |
|
190 qed "lift_ensures"; |
|
191 |
|
192 Goalw [lift_def, lift_set_def] |
|
193 "(lift i F : (lift_set i A) leadsTo (lift_set i B)) = \ |
|
194 \ (F : A leadsTo B)"; |
|
195 by (asm_simp_tac (simpset() addsimps [rename_leadsTo]) 1); |
|
196 qed "lift_leadsTo"; |
|
197 |
|
198 Goalw [lift_def, lift_set_def] |
|
199 "(lift i F : (lift_set i A) LeadsTo (lift_set i B)) = \ |
|
200 \ (F : A LeadsTo B)"; |
|
201 by (asm_simp_tac (simpset() addsimps [rename_LeadsTo]) 1); |
|
202 qed "lift_LeadsTo"; |
|
203 |
|
204 |
|
205 (** guarantees **) |
|
206 |
|
207 Goalw [lift_def] |
|
208 "(lift i F : (lift i `` X) guarantees[v o drop_map i] (lift i `` Y)) = \ |
|
209 \ (F : X guarantees[v] Y)"; |
|
210 by (stac (bij_lift_map RS rename_rename_guarantees_eq RS sym) 1); |
|
211 by (asm_simp_tac (simpset() addsimps [o_def]) 1); |
|
212 qed "lift_lift_guarantees_eq"; |
|
213 |
|
214 Goal "(lift i F : X guarantees[v] Y) = \ |
|
215 \ (F : (rename (drop_map i) `` X) guarantees[v o lift_map i] \ |
|
216 \ (rename (drop_map i) `` Y))"; |
|
217 by (asm_simp_tac |
|
218 (simpset() addsimps [bij_lift_map RS rename_guarantees_eq_rename_inv, |
|
219 lift_def]) 1); |
|
220 qed "lift_guarantees_eq_lift_inv"; |
|
221 |
|
222 |
|
223 (*To preserve snd means that the second component is there just to allow |
|
224 guarantees properties to be stated. Converse fails, for lift i F can |
|
225 change function components other than i*) |
|
226 Goal "F : preserves snd ==> lift i F : preserves snd"; |
|
227 by (dres_inst_tac [("w1", "snd")] (impOfSubs subset_preserves_o) 1); |
|
228 by (asm_simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1); |
|
229 by (full_simp_tac (simpset() addsimps [lift_map_def, o_def, split_def]) 1); |
|
230 qed "lift_preserves_snd_I"; |
|
231 |
|
232 Goal "(delete_map i g) = (delete_map i g') ==> EX x. g = g'(i:=x)"; |
|
233 by (dres_inst_tac [("f", "insert_map i (g i)")] arg_cong 1); |
|
234 by (full_simp_tac (simpset() addsimps [insert_map_delete_map_eq]) 1); |
|
235 by (etac exI 1); |
|
236 bind_thm ("delete_map_eqE", result() RS exE); |
|
237 AddSEs [delete_map_eqE]; |
|
238 |
|
239 Goal "[| delete_map j g = delete_map j g'; i~=j |] ==> g i = g' i"; |
84 by (Force_tac 1); |
240 by (Force_tac 1); |
85 qed "sub_vimage"; |
241 qed "delete_map_neq_apply"; |
86 Addsimps [sub_vimage]; |
242 |
87 |
243 (*A set of the form (A Times UNIV) ignores the second (dummy) state component*) |
88 (*For tidying the result of "export"*) |
244 |
89 Goal "v o (%z. z i) = v o sub i"; |
245 Goal "(f o fst) -`` A = (f-``A) Times UNIV"; |
90 by (simp_tac (simpset() addsimps [sub_def]) 1); |
246 by Auto_tac; |
91 qed "fold_o_sub"; |
247 qed "vimage_o_fst_eq"; |
92 |
248 |
93 |
249 Goal "(sub i -``A) Times UNIV = lift_set i (A Times UNIV)"; |
94 |
250 by Auto_tac; |
95 (*** lift_prog and the lattice operations ***) |
251 qed "vimage_sub_eq_lift_set"; |
96 |
252 |
97 Goal "lift_prog i SKIP = SKIP"; |
253 Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set]; |
98 by (auto_tac (claset() addSIs [program_equalityI], |
254 |
99 simpset() addsimps [SKIP_def, lift_prog_def])); |
255 Goal "[| F : preserves snd; i~=j |] \ |
100 qed "lift_prog_SKIP"; |
256 \ ==> lift j F : stable (lift_set i (A Times UNIV))"; |
101 |
257 by (auto_tac (claset(), |
102 Goal "lift_prog i (F Join G) = (lift_prog i F) Join (lift_prog i G)"; |
258 simpset() addsimps [lift_def, lift_set_def, |
103 by (rtac program_equalityI 1); |
259 stable_def, constrains_def, |
104 by Auto_tac; |
260 mem_rename_act_iff, mem_rename_set_iff])); |
105 qed "lift_prog_Join"; |
261 by (auto_tac (claset() addSDs [preserves_imp_eq], |
106 |
262 simpset() addsimps [lift_map_def, drop_map_def])); |
107 Goal "lift_prog i (JOIN J F) = (JN j:J. lift_prog i (F j))"; |
263 by (dres_inst_tac [("x", "i")] fun_cong 1); |
108 by (rtac program_equalityI 1); |
264 by Auto_tac; |
109 by Auto_tac; |
265 qed "preserves_snd_lift_stable"; |
110 qed "lift_prog_JN"; |
266 |
111 |
267 (*If i~=j then lift j F does nothing to lift_set i, and the |
112 |
268 premise ensures A<=B.*) |
113 (*** Equivalence with "extend" version ***) |
269 Goal "[| F i : (A Times UNIV) co (B Times UNIV); \ |
114 |
270 \ F j : preserves snd |] \ |
115 Goalw [lift_map_def] "good_map (lift_map i)"; |
271 \ ==> lift j (F j) : (lift_set i (A Times UNIV)) co (lift_set i (B Times UNIV))"; |
116 by (rtac good_mapI 1); |
272 by (case_tac "i=j" 1); |
117 by (res_inst_tac [("f", "%f. (f i, f)")] surjI 1); |
273 by (asm_full_simp_tac (simpset() addsimps [lift_def, lift_set_def, |
118 by Auto_tac; |
274 rename_constrains]) 1); |
119 by (dres_inst_tac [("f", "%f. f i")] arg_cong 1); |
275 by (etac (preserves_snd_lift_stable RS stableD RS constrains_weaken_R) 1); |
120 by Auto_tac; |
276 by (assume_tac 1); |
121 qed "good_map_lift_map"; |
277 by (etac (constrains_imp_subset RS lift_set_mono) 1); |
122 |
278 qed "constrains_imp_lift_constrains"; |
123 fun lift_export0 th = |
279 |
124 good_map_lift_map RS export th |
280 (** Lemmas for the transient theorem **) |
125 |> simplify (simpset() addsimps [fold_o_sub]); |
281 |
126 |
282 Goal "(insert_map i t f)(i := s) = insert_map i s f"; |
127 Goal "fst (inv (lift_map i) g) = g i"; |
|
128 by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1); |
|
129 by (auto_tac (claset(), simpset() addsimps [lift_map_def])); |
|
130 qed "fst_inv_lift_map"; |
|
131 Addsimps [fst_inv_lift_map]; |
|
132 |
|
133 |
|
134 Goal "lift_set i A = extend_set (lift_map i) A"; |
|
135 by (auto_tac (claset(), |
|
136 simpset() addsimps [lift_export0 mem_extend_set_iff])); |
|
137 qed "lift_set_correct"; |
|
138 |
|
139 Goalw [drop_set_def, project_set_def, lift_map_def] |
|
140 "drop_set i A = project_set (lift_map i) A"; |
|
141 by Auto_tac; |
|
142 by (rtac image_eqI 2); |
|
143 by (rtac exI 1); |
|
144 by (stac (refl RS fun_upd_idem) 1); |
|
145 by Auto_tac; |
|
146 qed "drop_set_correct"; |
|
147 |
|
148 Goal "lift_act i = extend_act (lift_map i)"; |
|
149 by (rtac ext 1); |
283 by (rtac ext 1); |
150 by Auto_tac; |
284 by Auto_tac; |
151 by (forward_tac [lift_export0 extend_act_D] 2); |
285 qed "insert_map_upd_same"; |
152 by (auto_tac (claset(), simpset() addsimps [extend_act_def])); |
286 |
153 by (auto_tac (claset(), simpset() addsimps [extend_act_def, lift_map_def])); |
287 Goal "(insert_map j t f)(i := s) = \ |
154 by (rtac bexI 1); |
288 \ (if i=j then insert_map i s f \ |
155 by (auto_tac (claset() addSIs [exI], simpset())); |
289 \ else if i<j then insert_map j t (f(i:=s)) \ |
156 qed "lift_act_correct"; |
290 \ else insert_map j t (f(i-1:=s)))"; |
157 |
|
158 Goal "drop_act i = project_act (lift_map i)"; |
|
159 by (rtac ext 1); |
291 by (rtac ext 1); |
160 by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]); |
292 by (auto_tac (claset(), simpset() addsplits [nat_diff_split'])); |
161 by Auto_tac; |
293 by (ALLGOALS arith_tac); |
162 by (REPEAT_FIRST (ares_tac [exI, conjI])); |
294 qed "insert_map_upd"; |
163 by Auto_tac; |
295 |
164 by (REPEAT_FIRST (assume_tac ORELSE' stac (refl RS fun_upd_idem))); |
296 Goal "[| insert_map i s f = insert_map j t g; i~=j |] \ |
165 qed "drop_act_correct"; |
297 \ ==> EX g'. insert_map i s' f = insert_map j t g'"; |
166 |
298 by (stac (insert_map_upd_same RS sym) 1); |
167 Goal "lift_prog i = extend (lift_map i)"; |
299 by (etac ssubst 1); |
168 by (rtac (program_equalityI RS ext) 1); |
300 by (asm_simp_tac (HOL_ss addsimps [insert_map_upd]) 1); |
169 by (simp_tac (simpset() addsimps [lift_set_correct]) 1); |
301 by (Blast_tac 1); |
170 by (simp_tac (simpset() |
302 qed "insert_map_eq_diff"; |
171 addsimps [lift_export0 Acts_extend, |
303 |
172 lift_act_correct]) 1); |
304 Goalw [lift_map_def] |
173 qed "lift_prog_correct"; |
305 "[| lift_map i (s,(f,uu)) = lift_map j (t,(g,vv)); i~=j |] \ |
174 |
306 \ ==> EX g'. lift_map i (s',(f,uu)) = lift_map j (t,(g',vv))"; |
175 Goal "drop_prog i C = project (lift_map i) C"; |
307 by Auto_tac; |
176 by (rtac (program_equalityI RS ext) 1); |
308 by (blast_tac (claset() addDs [insert_map_eq_diff]) 1); |
177 by (simp_tac (simpset() addsimps [drop_set_correct]) 1); |
309 qed "lift_map_eq_diff"; |
178 by (simp_tac (simpset() |
310 |
179 addsimps [Acts_project, drop_act_correct]) 1); |
311 Goal "F : preserves snd \ |
180 qed "drop_prog_correct"; |
312 \ ==> (lift i F : transient (lift_set j (A Times UNIV))) = \ |
181 |
313 \ (i=j & F : transient (A Times UNIV) | A={})"; |
182 |
314 by (case_tac "i=j" 1); |
183 (** Injectivity of lift_set, lift_act, lift_prog **) |
315 by (auto_tac (claset(), simpset() addsimps [lift_transient])); |
184 |
|
185 Goalw [lift_set_def, drop_set_def] "drop_set i (lift_set i F) = F"; |
|
186 by Auto_tac; |
|
187 qed "lift_set_inverse"; |
|
188 Addsimps [lift_set_inverse]; |
|
189 |
|
190 Goal "inj (lift_set i)"; |
|
191 by (rtac inj_on_inverseI 1); |
|
192 by (rtac lift_set_inverse 1); |
|
193 qed "inj_lift_set"; |
|
194 |
|
195 (*Because A and B could differ outside i, cannot generalize result to |
|
196 drop_set i (A Int B) = drop_set i A Int drop_set i B |
|
197 *) |
|
198 Goalw [lift_set_def, drop_set_def] |
|
199 "drop_set i ((lift_set i A) Int B) = A Int (drop_set i B)"; |
|
200 by Auto_tac; |
|
201 qed "drop_set_Int_lift_set"; |
|
202 |
|
203 Goalw [lift_set_def, drop_set_def] |
|
204 "drop_set i (B Int (lift_set i A)) = (drop_set i B) Int A"; |
|
205 by Auto_tac; |
|
206 qed "drop_set_Int_lift_set2"; |
|
207 |
|
208 Goalw [drop_set_def] |
|
209 "i : I ==> drop_set i (INT j:I. lift_set j A) = A"; |
|
210 by Auto_tac; |
|
211 qed "drop_set_INT"; |
|
212 |
|
213 Goal "lift_set i UNIV = UNIV"; |
|
214 by (simp_tac (simpset() addsimps [lift_set_correct, |
|
215 lift_export0 extend_set_UNIV_eq]) 1); |
|
216 qed "lift_set_UNIV_eq"; |
|
217 Addsimps [lift_set_UNIV_eq]; |
|
218 |
|
219 Goal "inj (lift_prog i)"; |
|
220 by (simp_tac |
|
221 (simpset() addsimps [lift_prog_correct, lift_export0 inj_extend]) 1); |
|
222 qed "inj_lift_prog"; |
|
223 |
|
224 |
|
225 (*** More Lemmas ***) |
|
226 |
|
227 Goal "lift_act i act ^^ lift_set i A = lift_set i (act^^A)"; |
|
228 by (asm_simp_tac (simpset() addsimps [lift_set_correct, lift_act_correct, |
|
229 lift_export0 extend_act_Image]) 1); |
|
230 qed "lift_act_Image"; |
|
231 Addsimps [lift_act_Image]; |
|
232 |
|
233 |
|
234 |
|
235 (*** Safety: co, stable, invariant ***) |
|
236 |
|
237 (** Safety and lift_prog **) |
|
238 |
|
239 Goal "(lift_prog i F : (lift_set i A) co (lift_set i B)) = \ |
|
240 \ (F : A co B)"; |
|
241 by (auto_tac (claset(), |
|
242 simpset() addsimps [constrains_def])); |
|
243 by (Force_tac 1); |
|
244 qed "lift_prog_constrains"; |
|
245 |
|
246 Goal "(lift_prog i F : stable (lift_set i A)) = (F : stable A)"; |
|
247 by (simp_tac (simpset() addsimps [stable_def, lift_prog_constrains]) 1); |
|
248 qed "lift_prog_stable"; |
|
249 |
|
250 Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)"; |
|
251 by (auto_tac (claset(), |
316 by (auto_tac (claset(), |
252 simpset() addsimps [invariant_def, lift_prog_stable])); |
317 simpset() addsimps [lift_def, transient_def, |
253 qed "lift_prog_invariant"; |
318 Domain_rename_act])); |
254 |
319 by (dtac subsetD 1); |
255 Goal "[| lift_prog i F : A co B |] \ |
320 by (Blast_tac 1); |
256 \ ==> F : (drop_set i A) co (drop_set i B)"; |
321 by Auto_tac; |
257 by (asm_full_simp_tac |
322 ren "s f uu s' f' uu'" 1; |
258 (simpset() addsimps [drop_set_correct, lift_prog_correct, |
323 by (subgoal_tac "f'=f & uu'=uu" 1); |
259 lift_export0 extend_constrains_project_set]) 1); |
324 by (force_tac (claset() addSDs [preserves_imp_eq], simpset()) 2); |
260 qed "lift_prog_constrains_drop_set"; |
325 by Auto_tac; |
261 |
326 by (dtac sym 1); |
262 (*This one looks strange! Proof probably is by case analysis on i=j. |
327 by (dtac subsetD 1); |
263 If i~=j then lift_prog j (F j) does nothing to lift_set i, and the |
328 by (rtac ImageI 1); |
264 premise ensures A<=B.*) |
329 by (etac rename_actI 1); |
265 Goal "F i : A co B \ |
330 by (force_tac (claset(), simpset() addsimps [lift_set_def]) 1); |
266 \ ==> lift_prog j (F j) : (lift_set i A) co (lift_set i B)"; |
331 by (etac (lift_map_eq_diff RS exE) 1); |
267 by (auto_tac (claset(), |
332 by (assume_tac 1); |
268 simpset() addsimps [constrains_def])); |
333 by (dtac ComplD 1); |
269 by (REPEAT (Blast_tac 1)); |
334 by (etac notE 1 THEN etac ssubst 1 THEN Fast_tac 1); |
270 qed "constrains_imp_lift_prog_constrains"; |
335 qed "lift_transient_eq_disj"; |
271 |
336 |
272 |
337 (*USELESS??*) |
273 (** Safety and drop_prog **) |
338 Goal "lift_map i `` (A Times UNIV) = \ |
274 |
339 \ (UN s:A. UN f. {insert_map i s f}) Times UNIV"; |
275 Goal "(drop_prog i C F : A co B) = \ |
340 by (auto_tac (claset() addSIs [bexI, image_eqI], |
276 \ (F : (C Int lift_set i A) co (lift_set i B) & A <= B)"; |
341 simpset() addsimps [lift_map_def])); |
277 by (simp_tac |
342 by (rtac (split RS sym) 1); |
278 (simpset() addsimps [drop_prog_correct, lift_set_correct, |
343 qed "lift_map_image_Times"; |
279 lift_export0 project_constrains]) 1); |
344 |
280 qed "drop_prog_constrains"; |
345 Goal "(lift i F : preserves v) = (F : preserves (v o lift_map i))"; |
281 |
346 by (simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1); |
282 Goal "(drop_prog i UNIV F : stable A) = (F : stable (lift_set i A))"; |
347 qed "lift_preserves_eq"; |
283 by (simp_tac (simpset() addsimps [stable_def, drop_prog_constrains]) 1); |
348 |
284 qed "drop_prog_stable"; |
349 Goal "F : preserves snd \ |
285 |
350 \ ==> lift i F : preserves (v o sub j o fst) = \ |
286 |
351 \ (if i=j then F : preserves (v o fst) else True)"; |
287 (*** Weak safety primitives: Co, Stable ***) |
352 by (dtac (impOfSubs subset_preserves_o) 1); |
288 |
353 by (full_simp_tac (simpset() addsimps [lift_preserves_eq, o_def, |
289 (** Reachability **) |
354 drop_map_lift_map_eq]) 1); |
290 |
355 by (asm_simp_tac (simpset() delcongs [if_weak_cong] |
291 Goal "reachable (lift_prog i F) = lift_set i (reachable F)"; |
356 addsimps [lift_map_def, |
292 by (simp_tac |
357 eq_commute, split_def, o_def]) 1); |
293 (simpset() addsimps [lift_prog_correct, lift_set_correct, |
358 by Auto_tac; |
294 lift_export0 reachable_extend_eq]) 1); |
359 qed "lift_preserves_sub"; |
295 qed "reachable_lift_prog"; |
360 |
296 |
361 |
297 Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B)) = \ |
362 |
298 \ (F : A Co B)"; |
363 (*** guarantees corollaries [NOT USED] |
299 by (simp_tac |
|
300 (simpset() addsimps [lift_prog_correct, lift_set_correct, |
|
301 lift_export0 extend_Constrains]) 1); |
|
302 qed "lift_prog_Constrains"; |
|
303 |
|
304 Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)"; |
|
305 by (simp_tac (simpset() addsimps [Stable_def, lift_prog_Constrains]) 1); |
|
306 qed "lift_prog_Stable"; |
|
307 |
|
308 Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : A Co B \ |
|
309 \ ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)"; |
|
310 by (asm_full_simp_tac |
|
311 (simpset() addsimps [lift_prog_correct, drop_prog_correct, |
|
312 lift_set_correct, lift_export0 project_Constrains_D]) 1); |
|
313 qed "drop_prog_Constrains_D"; |
|
314 |
|
315 Goalw [Stable_def] |
|
316 "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Stable A \ |
|
317 \ ==> lift_prog i F Join G : Stable (lift_set i A)"; |
|
318 by (asm_simp_tac (simpset() addsimps [drop_prog_Constrains_D]) 1); |
|
319 qed "drop_prog_Stable_D"; |
|
320 |
|
321 Goal "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Always A \ |
|
322 \ ==> lift_prog i F Join G : Always (lift_set i A)"; |
|
323 by (asm_full_simp_tac |
|
324 (simpset() addsimps [lift_prog_correct, drop_prog_correct, |
|
325 lift_set_correct, lift_export0 project_Always_D]) 1); |
|
326 qed "drop_prog_Always_D"; |
|
327 |
|
328 Goalw [Increasing_def] |
|
329 "F Join drop_prog i (reachable (lift_prog i F Join G)) G : Increasing func \ |
|
330 \ ==> lift_prog i F Join G : Increasing (func o (sub i))"; |
|
331 by Auto_tac; |
|
332 by (stac Collect_eq_lift_set 1); |
|
333 by (asm_simp_tac (simpset() addsimps [drop_prog_Stable_D]) 1); |
|
334 qed "project_Increasing_D"; |
|
335 |
|
336 |
|
337 (*** Progress: transient, ensures ***) |
|
338 |
|
339 Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)"; |
|
340 by (simp_tac (simpset() addsimps [lift_set_correct, lift_prog_correct, |
|
341 lift_export0 extend_transient]) 1); |
|
342 qed "lift_prog_transient"; |
|
343 |
|
344 Goal "(lift_prog i F : transient (lift_set j A)) = \ |
|
345 \ (i=j & F : transient A | A={})"; |
|
346 by (case_tac "i=j" 1); |
|
347 by (auto_tac (claset(), simpset() addsimps [lift_prog_transient])); |
|
348 by (auto_tac (claset(), simpset() addsimps [lift_prog_def, transient_def])); |
|
349 by (Force_tac 1); |
|
350 qed "lift_prog_transient_eq_disj"; |
|
351 |
|
352 |
|
353 (*** guarantees properties ***) |
|
354 |
|
355 Goal "lift_prog i F : preserves (v o sub j) = \ |
|
356 \ (if i=j then F : preserves v else True)"; |
|
357 by (simp_tac (simpset() addsimps [lift_prog_correct, |
|
358 lift_export0 extend_preserves]) 1); |
|
359 by (auto_tac (claset(), |
|
360 simpset() addsimps [preserves_def, extend_def, extend_act_def, |
|
361 stable_def, constrains_def, lift_map_def])); |
|
362 qed "lift_prog_preserves_sub"; |
|
363 |
|
364 Addsimps [lift_prog_preserves_sub]; |
|
365 |
|
366 Goal "G : preserves (v o sub i) ==> drop_prog i C G : preserves v"; |
|
367 by (asm_simp_tac |
|
368 (simpset() addsimps [drop_prog_correct, fold_o_sub, |
|
369 lift_export0 project_preserves_I]) 1); |
|
370 qed "drop_prog_preserves_I"; |
|
371 |
|
372 (*The raw version*) |
|
373 val [xguary,drop_prog,lift_prog] = |
|
374 Goal "[| F : X guarantees[v] Y; \ |
|
375 \ !!G. lift_prog i F Join G : X' ==> F Join drop_prog i (C G) G : X; \ |
|
376 \ !!G. [| F Join drop_prog i (C G) G : Y; lift_prog i F Join G : X'; \ |
|
377 \ G : preserves (v o sub i) |] \ |
|
378 \ ==> lift_prog i F Join G : Y' |] \ |
|
379 \ ==> lift_prog i F : X' guarantees[v o sub i] Y'"; |
|
380 by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1); |
|
381 by (etac drop_prog_preserves_I 1); |
|
382 by (etac drop_prog 1); |
|
383 by Auto_tac; |
|
384 qed "drop_prog_guarantees_raw"; |
|
385 |
|
386 Goal "[| F : X guarantees[v] Y; \ |
|
387 \ projecting C (lift_map i) F X' X; \ |
|
388 \ extending w C (lift_map i) F Y' Y; \ |
|
389 \ preserves w <= preserves (v o sub i) |] \ |
|
390 \ ==> lift_prog i F : X' guarantees[w] Y'"; |
|
391 by (asm_simp_tac |
|
392 (simpset() addsimps [lift_prog_correct, fold_o_sub, |
|
393 lift_export0 project_guarantees]) 1); |
|
394 qed "drop_prog_guarantees"; |
|
395 |
|
396 |
|
397 (** Are these two useful?? **) |
|
398 |
|
399 (*The other direction fails: having FF : Stable {s. z <= f (s i)} does not |
|
400 ensure that F has the form lift_prog i F for some F.*) |
|
401 Goal "lift_prog i `` Stable {s. P (f s)} <= Stable {s. P (f (s i))}"; |
|
402 by Auto_tac; |
|
403 by (stac Collect_eq_lift_set 1); |
|
404 by (asm_simp_tac (simpset() addsimps [lift_prog_Stable]) 1); |
|
405 qed "image_lift_prog_Stable"; |
|
406 |
|
407 Goal "lift_prog i `` Increasing f <= Increasing (f o sub i)"; |
|
408 by (simp_tac (simpset() addsimps [Increasing_def, |
|
409 inj_lift_prog RS image_INT]) 1); |
|
410 by (blast_tac (claset() addIs [impOfSubs image_lift_prog_Stable]) 1); |
|
411 qed "image_lift_prog_Increasing"; |
|
412 |
|
413 |
|
414 (*** guarantees corollaries ***) |
|
415 |
364 |
416 Goal "F : UNIV guarantees[v] increasing func \ |
365 Goal "F : UNIV guarantees[v] increasing func \ |
417 \ ==> lift_prog i F : UNIV guarantees[v o sub i] increasing (func o sub i)"; |
366 \ ==> lift i F : UNIV guarantees[v o sub i] increasing (func o sub i)"; |
418 by (dtac (lift_export0 extend_guar_increasing) 1); |
367 by (dtac (lift_export0 extend_guar_increasing) 1); |
419 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1); |
368 by (asm_full_simp_tac (simpset() addsimps [lift_correct, o_def]) 1); |
420 qed "lift_prog_guar_increasing"; |
369 qed "lift_guar_increasing"; |
421 |
370 |
422 Goal "F : UNIV guarantees[v] Increasing func \ |
371 Goal "F : UNIV guarantees[v] Increasing func \ |
423 \ ==> lift_prog i F : UNIV guarantees[v o sub i] Increasing (func o sub i)"; |
372 \ ==> lift i F : UNIV guarantees[v o sub i] Increasing (func o sub i)"; |
424 by (dtac (lift_export0 extend_guar_Increasing) 1); |
373 by (dtac (lift_export0 extend_guar_Increasing) 1); |
425 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1); |
374 by (asm_full_simp_tac (simpset() addsimps [lift_correct, o_def]) 1); |
426 qed "lift_prog_guar_Increasing"; |
375 qed "lift_guar_Increasing"; |
427 |
376 |
428 Goal "F : Always A guarantees[v] Always B \ |
377 Goal "F : Always A guarantees[v] Always B \ |
429 \ ==> lift_prog i F : \ |
378 \ ==> lift i F : \ |
430 \ Always(lift_set i A) guarantees[v o sub i] Always (lift_set i B)"; |
379 \ Always(lift_set i A) guarantees[v o sub i] Always (lift_set i B)"; |
431 by (asm_simp_tac |
380 by (asm_simp_tac |
432 (simpset() addsimps [lift_set_correct, lift_prog_correct, |
381 (simpset() addsimps [lift_set_correct, lift_correct, |
433 lift_export0 extend_guar_Always]) 1); |
382 lift_export0 extend_guar_Always]) 1); |
434 qed "lift_prog_guar_Always"; |
383 qed "lift_guar_Always"; |
435 |
384 ***) |
436 (*version for outside use*) |
|
437 fun lift_export th = |
|
438 good_map_lift_map RS export th |
|
439 |> simplify |
|
440 (simpset() addsimps [fold_o_sub, |
|
441 drop_set_correct RS sym, |
|
442 lift_set_correct RS sym, |
|
443 drop_prog_correct RS sym, |
|
444 lift_prog_correct RS sym]);; |
|
445 |
|