|
1 (* Title: HOL/UNITY/Rename.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 2000 University of Cambridge |
|
5 |
|
6 *) |
|
7 |
|
8 Addsimps [image_inv_f_f, image_surj_f_inv_f]; |
|
9 |
|
10 Goal "bij h ==> good_map (%(x,u). h x)"; |
|
11 by (rtac good_mapI 1); |
|
12 by (rewrite_goals_tac [bij_def, inj_on_def, surj_def]); |
|
13 by Auto_tac; |
|
14 qed "good_map_bij"; |
|
15 Addsimps [good_map_bij]; |
|
16 |
|
17 fun bij_export th = good_map_bij RS export th |> simplify (simpset()); |
|
18 |
|
19 Goalw [bij_def, split_def] "bij h ==> fst (inv (%(x,u). h x) s) = inv h s"; |
|
20 by (Clarify_tac 1); |
|
21 by (subgoal_tac "surj (%p. h (fst p))" 1); |
|
22 by (asm_full_simp_tac (simpset() addsimps [surj_def]) 2); |
|
23 by (etac injD 1); |
|
24 by (asm_simp_tac (simpset() addsimps [surj_f_inv_f]) 1); |
|
25 by (etac surj_f_inv_f 1); |
|
26 qed "fst_o_inv_eq_inv"; |
|
27 |
|
28 Goal "bij h ==> z : h``A = (inv h z : A)"; |
|
29 by (auto_tac (claset() addSIs [image_eqI], |
|
30 simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f])); |
|
31 qed "mem_rename_set_iff"; |
|
32 |
|
33 Goal "bij h ==> h``{s. P s} = {s. P (inv h s)}"; |
|
34 by (auto_tac (claset() addSIs [exI], |
|
35 simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f])); |
|
36 qed "rename_set_eq_Collect"; |
|
37 |
|
38 Goal "extend_set (%(x,u). h x) A = h``A"; |
|
39 by (auto_tac (claset() addSIs [image_eqI], |
|
40 simpset() addsimps [extend_set_def])); |
|
41 qed "extend_set_eq_image"; |
|
42 Addsimps [extend_set_eq_image]; |
|
43 |
|
44 Goalw [rename_def] "Init (rename h F) = h``(Init F)"; |
|
45 by (Simp_tac 1); |
|
46 qed "Init_rename"; |
|
47 |
|
48 Goalw [rename_def, rename_act_def] |
|
49 "bij h ==> Acts (rename h F) = (rename_act h `` Acts F)"; |
|
50 by (asm_simp_tac (simpset() addsimps [export Acts_extend]) 1); |
|
51 qed "Acts_rename"; |
|
52 |
|
53 Addsimps [Init_rename, Acts_rename]; |
|
54 |
|
55 Goalw [rename_act_def, extend_act_def] |
|
56 "(s,s') : act ==> (h s, h s') : rename_act h act"; |
|
57 by Auto_tac; |
|
58 qed "rename_actI"; |
|
59 |
|
60 Goalw [rename_act_def] |
|
61 "bij h ==> ((s,s') : rename_act h act) = ((inv h s, inv h s') : act)"; |
|
62 by (rtac trans 1); |
|
63 by (etac (bij_export mem_extend_act_iff) 2); |
|
64 by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 1); |
|
65 qed "mem_rename_act_iff"; |
|
66 |
|
67 Goalw [rename_act_def] "Domain (rename_act h act) = h``(Domain act)"; |
|
68 by (asm_simp_tac (simpset() addsimps [export Domain_extend_act]) 1); |
|
69 qed "Domain_rename_act"; |
|
70 |
|
71 (*** inverse properties ***) |
|
72 |
|
73 Goalw [bij_def] |
|
74 "bij h \ |
|
75 \ ==> extend_set (%(x,u::'c). inv h x) = project_set (%(x,u::'c). h x)"; |
|
76 by (rtac ext 1); |
|
77 by (auto_tac (claset() addSIs [image_eqI], |
|
78 simpset() addsimps [extend_set_def, project_set_def, |
|
79 surj_f_inv_f])); |
|
80 qed "extend_set_inv"; |
|
81 |
|
82 (** for "rename" (programs) **) |
|
83 |
|
84 Goal "bij h \ |
|
85 \ ==> extend_act (%(x,u::'c). inv h x) = project_act (%(x,u::'c). h x)"; |
|
86 by (rtac ext 1); |
|
87 by (auto_tac (claset() addSIs [image_eqI], |
|
88 simpset() addsimps [extend_act_def, project_act_def, bij_def, |
|
89 surj_f_inv_f])); |
|
90 qed "extend_act_inv"; |
|
91 |
|
92 Goal "bij h \ |
|
93 \ ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV"; |
|
94 by (ftac bij_imp_bij_inv 1); |
|
95 by (rtac ext 1); |
|
96 by (rtac program_equalityI 1); |
|
97 by (asm_simp_tac |
|
98 (simpset() addsimps [export project_act_Id, export Acts_extend, |
|
99 insert_Id_image_Acts, extend_act_inv]) 2); |
|
100 by (asm_simp_tac (simpset() addsimps [extend_set_inv]) 1); |
|
101 qed "extend_inv"; |
|
102 |
|
103 Goal "bij h ==> rename (inv h) (rename h F) = F"; |
|
104 by (asm_simp_tac (simpset() addsimps [rename_def, extend_inv, |
|
105 export extend_inverse]) 1); |
|
106 qed "rename_inv_rename"; |
|
107 Addsimps [rename_inv_rename]; |
|
108 |
|
109 Goal "bij h ==> rename h (rename (inv h) F) = F"; |
|
110 by (ftac bij_imp_bij_inv 1); |
|
111 by (etac (inv_inv_eq RS subst) 1 THEN etac rename_inv_rename 1); |
|
112 qed "rename_rename_inv"; |
|
113 Addsimps [rename_rename_inv]; |
|
114 |
|
115 Goal "bij h ==> rename (inv h) = inv (rename h)"; |
|
116 by (rtac (inv_equality RS sym) 1); |
|
117 by Auto_tac; |
|
118 qed "rename_inv_eq"; |
|
119 |
|
120 |
|
121 (*** the lattice operations ***) |
|
122 |
|
123 Goalw [rename_def] "bij h ==> rename h SKIP = SKIP"; |
|
124 by (Asm_simp_tac 1); |
|
125 qed "rename_SKIP"; |
|
126 Addsimps [rename_SKIP]; |
|
127 |
|
128 Goalw [rename_def] "bij h ==> inj (rename h)"; |
|
129 by (asm_simp_tac (simpset() addsimps [export inj_extend]) 1); |
|
130 qed "inj_rename"; |
|
131 |
|
132 Goalw [rename_def] |
|
133 "bij h ==> rename h (F Join G) = rename h F Join rename h G"; |
|
134 by (asm_simp_tac (simpset() addsimps [export extend_Join]) 1); |
|
135 qed "rename_Join"; |
|
136 Addsimps [rename_Join]; |
|
137 |
|
138 Goalw [rename_def] "bij h ==> rename h (JOIN I F) = (JN i:I. rename h (F i))"; |
|
139 by (asm_simp_tac (simpset() addsimps [export extend_JN]) 1); |
|
140 qed "rename_JN"; |
|
141 Addsimps [rename_JN]; |
|
142 |
|
143 (*** Safety: co, stable ***) |
|
144 |
|
145 Goalw [rename_def] |
|
146 "bij h ==> (rename h F : (h``A) co (h``B)) = (F : A co B)"; |
|
147 by (REPEAT (stac (extend_set_eq_image RS sym) 1)); |
|
148 by (etac (good_map_bij RS export extend_constrains) 1); |
|
149 qed "rename_constrains"; |
|
150 |
|
151 Goalw [stable_def] |
|
152 "bij h ==> (rename h F : stable (h``A)) = (F : stable A)"; |
|
153 by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1); |
|
154 qed "rename_stable"; |
|
155 |
|
156 Goal "bij h ==> (rename h F : invariant (h``A)) = (F : invariant A)"; |
|
157 by (asm_simp_tac (simpset() addsimps [invariant_def, rename_stable, |
|
158 bij_is_inj RS inj_image_subset_iff]) 1); |
|
159 qed "rename_invariant"; |
|
160 |
|
161 Goalw [rename_def] |
|
162 "bij h ==> reachable (rename h F) = h `` (reachable F)"; |
|
163 by (asm_simp_tac (simpset() addsimps [export reachable_extend_eq]) 1); |
|
164 qed "reachable_rename_eq"; |
|
165 |
|
166 Goal "bij h ==> (rename h F : (h``A) Co (h``B)) = (F : A Co B)"; |
|
167 by (asm_simp_tac |
|
168 (simpset() addsimps [Constrains_def, reachable_rename_eq, |
|
169 rename_constrains, bij_is_inj, image_Int RS sym]) 1); |
|
170 qed "rename_Constrains"; |
|
171 |
|
172 Goalw [Stable_def] |
|
173 "bij h ==> (rename h F : Stable (h``A)) = (F : Stable A)"; |
|
174 by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1); |
|
175 qed "rename_Stable"; |
|
176 |
|
177 Goal "bij h ==> (rename h F : Always (h``A)) = (F : Always A)"; |
|
178 by (asm_simp_tac (simpset() addsimps [Always_def, rename_Stable, |
|
179 bij_is_inj RS inj_image_subset_iff]) 1); |
|
180 qed "rename_Always"; |
|
181 |
|
182 |
|
183 (*** Progress: transient, ensures ***) |
|
184 |
|
185 Goalw [rename_def] |
|
186 "bij h ==> (rename h F : transient (h``A)) = (F : transient A)"; |
|
187 by (stac (extend_set_eq_image RS sym) 1); |
|
188 by (etac (good_map_bij RS export extend_transient) 1); |
|
189 qed "rename_transient"; |
|
190 |
|
191 Goalw [rename_def] |
|
192 "bij h ==> (rename h F : (h``A) ensures (h``B)) = (F : A ensures B)"; |
|
193 by (REPEAT (stac (extend_set_eq_image RS sym) 1)); |
|
194 by (etac (good_map_bij RS export extend_ensures) 1); |
|
195 qed "rename_ensures"; |
|
196 |
|
197 Goalw [rename_def] |
|
198 "bij h ==> (rename h F : (h``A) leadsTo (h``B)) = (F : A leadsTo B)"; |
|
199 by (REPEAT (stac (extend_set_eq_image RS sym) 1)); |
|
200 by (etac (good_map_bij RS export extend_leadsTo) 1); |
|
201 qed "rename_leadsTo"; |
|
202 |
|
203 Goalw [rename_def] |
|
204 "bij h ==> (rename h F : (h``A) LeadsTo (h``B)) = (F : A LeadsTo B)"; |
|
205 by (REPEAT (stac (extend_set_eq_image RS sym) 1)); |
|
206 by (etac (good_map_bij RS export extend_LeadsTo) 1); |
|
207 qed "rename_LeadsTo"; |
|
208 |
|
209 Goalw [rename_def] |
|
210 "bij h ==> (rename h F : (rename h `` X) guarantees[v o inv h] \ |
|
211 \ (rename h `` Y)) = \ |
|
212 \ (F : X guarantees[v] Y)"; |
|
213 by (stac (good_map_bij RS export extend_guarantees_eq RS sym) 1); |
|
214 by (assume_tac 1); |
|
215 by (asm_simp_tac (simpset() addsimps [fst_o_inv_eq_inv, o_def]) 1); |
|
216 qed "rename_rename_guarantees_eq"; |
|
217 |
|
218 Goal "bij h ==> (rename h F : X guarantees[v] Y) = \ |
|
219 \ (F : (rename (inv h) `` X) guarantees[v o h] \ |
|
220 \ (rename (inv h) `` Y))"; |
|
221 by (stac (rename_rename_guarantees_eq RS sym) 1); |
|
222 by (assume_tac 1); |
|
223 by (asm_simp_tac |
|
224 (simpset() addsimps [image_eq_UN, o_def, bij_is_surj RS surj_f_inv_f]) 1); |
|
225 qed "rename_guarantees_eq_rename_inv"; |
|
226 |
|
227 Goal "bij h ==> (rename h G : preserves v) = (G : preserves (v o h))"; |
|
228 by (stac (good_map_bij RS export extend_preserves RS sym) 1); |
|
229 by (assume_tac 1); |
|
230 by (asm_simp_tac (simpset() addsimps [o_def, fst_o_inv_eq_inv, rename_def, |
|
231 bij_is_surj RS surj_f_inv_f]) 1); |
|
232 qed "rename_preserves"; |
|
233 |
|
234 |
|
235 (** junk |
|
236 |
|
237 |
|
238 Goalw [extend_act_def, project_act_def, surj_def] |
|
239 "surj h ==> extend_act (%(x,u). h x) (project_act (%(x,u). h x) act) = act"; |
|
240 by Auto_tac; |
|
241 by (forw_inst_tac [("x", "a")] spec 1); |
|
242 by (dres_inst_tac [("x", "b")] spec 1); |
|
243 by Auto_tac; |
|
244 qed "project_act_inverse"; |
|
245 |
|
246 Goal "bij h ==> rename h (rename (inv h) F) = F"; |
|
247 by (rtac program_equalityI 1); |
|
248 by (Asm_simp_tac 1); |
|
249 by (asm_simp_tac |
|
250 (simpset() addsimps [rename_def, inverse_def, export Acts_extend, |
|
251 image_eq_UN, export extend_act_Id, |
|
252 bij_is_surj RS project_act_inverse]) 1); |
|
253 qed "rename_rename_inv"; |
|
254 Addsimps [rename_rename_inv]; |
|
255 |
|
256 |
|
257 |
|
258 Goalw [bij_def] |
|
259 "bij h \ |
|
260 \ ==> extend_set (%(x,u::'c). inv h x) = inv (extend_set (%(x,u::'c). h x))"; |
|
261 by (rtac ext 1); |
|
262 by (auto_tac (claset() addSIs [image_eqI], |
|
263 simpset() addsimps [extend_set_def, project_set_def, |
|
264 surj_f_inv_f])); |
|
265 qed "extend_set_inv"; |
|
266 |
|
267 |
|
268 ***) |