1 (* Title: QuotMain.thy |
|
2 Author: Cezary Kaliszyk and Christian Urban |
|
3 *) |
|
4 |
|
5 theory QuotMain |
|
6 imports Plain ATP_Linkup |
|
7 uses |
|
8 ("quotient_info.ML") |
|
9 ("quotient_typ.ML") |
|
10 ("quotient_def.ML") |
|
11 ("quotient_term.ML") |
|
12 ("quotient_tacs.ML") |
|
13 begin |
|
14 |
|
15 text {* |
|
16 Basic definition for equivalence relations |
|
17 that are represented by predicates. |
|
18 *} |
|
19 |
|
20 definition |
|
21 "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))" |
|
22 |
|
23 definition |
|
24 "reflp E \<longleftrightarrow> (\<forall>x. E x x)" |
|
25 |
|
26 definition |
|
27 "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)" |
|
28 |
|
29 definition |
|
30 "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)" |
|
31 |
|
32 lemma equivp_reflp_symp_transp: |
|
33 shows "equivp E = (reflp E \<and> symp E \<and> transp E)" |
|
34 unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq |
|
35 by blast |
|
36 |
|
37 lemma equivp_reflp: |
|
38 shows "equivp E \<Longrightarrow> E x x" |
|
39 by (simp only: equivp_reflp_symp_transp reflp_def) |
|
40 |
|
41 lemma equivp_symp: |
|
42 shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x" |
|
43 by (metis equivp_reflp_symp_transp symp_def) |
|
44 |
|
45 lemma equivp_transp: |
|
46 shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z" |
|
47 by (metis equivp_reflp_symp_transp transp_def) |
|
48 |
|
49 lemma equivpI: |
|
50 assumes "reflp R" "symp R" "transp R" |
|
51 shows "equivp R" |
|
52 using assms by (simp add: equivp_reflp_symp_transp) |
|
53 |
|
54 lemma eq_imp_rel: |
|
55 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
|
56 by (simp add: equivp_reflp) |
|
57 |
|
58 lemma identity_equivp: |
|
59 shows "equivp (op =)" |
|
60 unfolding equivp_def |
|
61 by auto |
|
62 |
|
63 |
|
64 text {* Partial equivalences: not yet used anywhere *} |
|
65 definition |
|
66 "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y))))" |
|
67 |
|
68 lemma equivp_implies_part_equivp: |
|
69 assumes a: "equivp E" |
|
70 shows "part_equivp E" |
|
71 using a |
|
72 unfolding equivp_def part_equivp_def |
|
73 by auto |
|
74 |
|
75 text {* Composition of Relations *} |
|
76 |
|
77 abbreviation |
|
78 rel_conj (infixr "OOO" 75) |
|
79 where |
|
80 "r1 OOO r2 \<equiv> r1 OO r2 OO r1" |
|
81 |
|
82 lemma eq_comp_r: |
|
83 shows "((op =) OOO R) = R" |
|
84 by (auto simp add: expand_fun_eq) |
|
85 |
|
86 section {* Respects predicate *} |
|
87 |
|
88 definition |
|
89 Respects |
|
90 where |
|
91 "Respects R x \<longleftrightarrow> (R x x)" |
|
92 |
|
93 lemma in_respects: |
|
94 shows "(x \<in> Respects R) = R x x" |
|
95 unfolding mem_def Respects_def |
|
96 by simp |
|
97 |
|
98 section {* Function map and function relation *} |
|
99 |
|
100 definition |
|
101 fun_map (infixr "--->" 55) |
|
102 where |
|
103 [simp]: "fun_map f g h x = g (h (f x))" |
|
104 |
|
105 definition |
|
106 fun_rel (infixr "===>" 55) |
|
107 where |
|
108 [simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))" |
|
109 |
|
110 |
|
111 lemma fun_map_id: |
|
112 shows "(id ---> id) = id" |
|
113 by (simp add: expand_fun_eq id_def) |
|
114 |
|
115 lemma fun_rel_eq: |
|
116 shows "((op =) ===> (op =)) = (op =)" |
|
117 by (simp add: expand_fun_eq) |
|
118 |
|
119 lemma fun_rel_id: |
|
120 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
|
121 shows "(R1 ===> R2) f g" |
|
122 using a by simp |
|
123 |
|
124 lemma fun_rel_id_asm: |
|
125 assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))" |
|
126 shows "A \<longrightarrow> (R1 ===> R2) f g" |
|
127 using a by auto |
|
128 |
|
129 |
|
130 section {* Quotient Predicate *} |
|
131 |
|
132 definition |
|
133 "Quotient E Abs Rep \<longleftrightarrow> |
|
134 (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and> |
|
135 (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))" |
|
136 |
|
137 lemma Quotient_abs_rep: |
|
138 assumes a: "Quotient E Abs Rep" |
|
139 shows "Abs (Rep a) = a" |
|
140 using a |
|
141 unfolding Quotient_def |
|
142 by simp |
|
143 |
|
144 lemma Quotient_rep_reflp: |
|
145 assumes a: "Quotient E Abs Rep" |
|
146 shows "E (Rep a) (Rep a)" |
|
147 using a |
|
148 unfolding Quotient_def |
|
149 by blast |
|
150 |
|
151 lemma Quotient_rel: |
|
152 assumes a: "Quotient E Abs Rep" |
|
153 shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))" |
|
154 using a |
|
155 unfolding Quotient_def |
|
156 by blast |
|
157 |
|
158 lemma Quotient_rel_rep: |
|
159 assumes a: "Quotient R Abs Rep" |
|
160 shows "R (Rep a) (Rep b) = (a = b)" |
|
161 using a |
|
162 unfolding Quotient_def |
|
163 by metis |
|
164 |
|
165 lemma Quotient_rep_abs: |
|
166 assumes a: "Quotient R Abs Rep" |
|
167 shows "R r r \<Longrightarrow> R (Rep (Abs r)) r" |
|
168 using a unfolding Quotient_def |
|
169 by blast |
|
170 |
|
171 lemma Quotient_rel_abs: |
|
172 assumes a: "Quotient E Abs Rep" |
|
173 shows "E r s \<Longrightarrow> Abs r = Abs s" |
|
174 using a unfolding Quotient_def |
|
175 by blast |
|
176 |
|
177 lemma Quotient_symp: |
|
178 assumes a: "Quotient E Abs Rep" |
|
179 shows "symp E" |
|
180 using a unfolding Quotient_def symp_def |
|
181 by metis |
|
182 |
|
183 lemma Quotient_transp: |
|
184 assumes a: "Quotient E Abs Rep" |
|
185 shows "transp E" |
|
186 using a unfolding Quotient_def transp_def |
|
187 by metis |
|
188 |
|
189 lemma identity_quotient: |
|
190 shows "Quotient (op =) id id" |
|
191 unfolding Quotient_def id_def |
|
192 by blast |
|
193 |
|
194 lemma fun_quotient: |
|
195 assumes q1: "Quotient R1 abs1 rep1" |
|
196 and q2: "Quotient R2 abs2 rep2" |
|
197 shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
|
198 proof - |
|
199 have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" |
|
200 using q1 q2 |
|
201 unfolding Quotient_def |
|
202 unfolding expand_fun_eq |
|
203 by simp |
|
204 moreover |
|
205 have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" |
|
206 using q1 q2 |
|
207 unfolding Quotient_def |
|
208 by (simp (no_asm)) (metis) |
|
209 moreover |
|
210 have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> |
|
211 (rep1 ---> abs2) r = (rep1 ---> abs2) s)" |
|
212 unfolding expand_fun_eq |
|
213 apply(auto) |
|
214 using q1 q2 unfolding Quotient_def |
|
215 apply(metis) |
|
216 using q1 q2 unfolding Quotient_def |
|
217 apply(metis) |
|
218 using q1 q2 unfolding Quotient_def |
|
219 apply(metis) |
|
220 using q1 q2 unfolding Quotient_def |
|
221 apply(metis) |
|
222 done |
|
223 ultimately |
|
224 show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
|
225 unfolding Quotient_def by blast |
|
226 qed |
|
227 |
|
228 lemma abs_o_rep: |
|
229 assumes a: "Quotient R Abs Rep" |
|
230 shows "Abs o Rep = id" |
|
231 unfolding expand_fun_eq |
|
232 by (simp add: Quotient_abs_rep[OF a]) |
|
233 |
|
234 lemma equals_rsp: |
|
235 assumes q: "Quotient R Abs Rep" |
|
236 and a: "R xa xb" "R ya yb" |
|
237 shows "R xa ya = R xb yb" |
|
238 using a Quotient_symp[OF q] Quotient_transp[OF q] |
|
239 unfolding symp_def transp_def |
|
240 by blast |
|
241 |
|
242 lemma lambda_prs: |
|
243 assumes q1: "Quotient R1 Abs1 Rep1" |
|
244 and q2: "Quotient R2 Abs2 Rep2" |
|
245 shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)" |
|
246 unfolding expand_fun_eq |
|
247 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] |
|
248 by simp |
|
249 |
|
250 lemma lambda_prs1: |
|
251 assumes q1: "Quotient R1 Abs1 Rep1" |
|
252 and q2: "Quotient R2 Abs2 Rep2" |
|
253 shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)" |
|
254 unfolding expand_fun_eq |
|
255 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] |
|
256 by simp |
|
257 |
|
258 lemma rep_abs_rsp: |
|
259 assumes q: "Quotient R Abs Rep" |
|
260 and a: "R x1 x2" |
|
261 shows "R x1 (Rep (Abs x2))" |
|
262 using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] |
|
263 by metis |
|
264 |
|
265 lemma rep_abs_rsp_left: |
|
266 assumes q: "Quotient R Abs Rep" |
|
267 and a: "R x1 x2" |
|
268 shows "R (Rep (Abs x1)) x2" |
|
269 using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q] |
|
270 by metis |
|
271 |
|
272 text{* |
|
273 In the following theorem R1 can be instantiated with anything, |
|
274 but we know some of the types of the Rep and Abs functions; |
|
275 so by solving Quotient assumptions we can get a unique R1 that |
|
276 will be provable; which is why we need to use apply_rsp and |
|
277 not the primed version *} |
|
278 |
|
279 lemma apply_rsp: |
|
280 fixes f g::"'a \<Rightarrow> 'c" |
|
281 assumes q: "Quotient R1 Abs1 Rep1" |
|
282 and a: "(R1 ===> R2) f g" "R1 x y" |
|
283 shows "R2 (f x) (g y)" |
|
284 using a by simp |
|
285 |
|
286 lemma apply_rsp': |
|
287 assumes a: "(R1 ===> R2) f g" "R1 x y" |
|
288 shows "R2 (f x) (g y)" |
|
289 using a by simp |
|
290 |
|
291 section {* lemmas for regularisation of ball and bex *} |
|
292 |
|
293 lemma ball_reg_eqv: |
|
294 fixes P :: "'a \<Rightarrow> bool" |
|
295 assumes a: "equivp R" |
|
296 shows "Ball (Respects R) P = (All P)" |
|
297 using a |
|
298 unfolding equivp_def |
|
299 by (auto simp add: in_respects) |
|
300 |
|
301 lemma bex_reg_eqv: |
|
302 fixes P :: "'a \<Rightarrow> bool" |
|
303 assumes a: "equivp R" |
|
304 shows "Bex (Respects R) P = (Ex P)" |
|
305 using a |
|
306 unfolding equivp_def |
|
307 by (auto simp add: in_respects) |
|
308 |
|
309 lemma ball_reg_right: |
|
310 assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x" |
|
311 shows "All P \<longrightarrow> Ball R Q" |
|
312 using a by (metis COMBC_def Collect_def Collect_mem_eq) |
|
313 |
|
314 lemma bex_reg_left: |
|
315 assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x" |
|
316 shows "Bex R Q \<longrightarrow> Ex P" |
|
317 using a by (metis COMBC_def Collect_def Collect_mem_eq) |
|
318 |
|
319 lemma ball_reg_left: |
|
320 assumes a: "equivp R" |
|
321 shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P" |
|
322 using a by (metis equivp_reflp in_respects) |
|
323 |
|
324 lemma bex_reg_right: |
|
325 assumes a: "equivp R" |
|
326 shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P" |
|
327 using a by (metis equivp_reflp in_respects) |
|
328 |
|
329 lemma ball_reg_eqv_range: |
|
330 fixes P::"'a \<Rightarrow> bool" |
|
331 and x::"'a" |
|
332 assumes a: "equivp R2" |
|
333 shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))" |
|
334 apply(rule iffI) |
|
335 apply(rule allI) |
|
336 apply(drule_tac x="\<lambda>y. f x" in bspec) |
|
337 apply(simp add: in_respects) |
|
338 apply(rule impI) |
|
339 using a equivp_reflp_symp_transp[of "R2"] |
|
340 apply(simp add: reflp_def) |
|
341 apply(simp) |
|
342 apply(simp) |
|
343 done |
|
344 |
|
345 lemma bex_reg_eqv_range: |
|
346 assumes a: "equivp R2" |
|
347 shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))" |
|
348 apply(auto) |
|
349 apply(rule_tac x="\<lambda>y. f x" in bexI) |
|
350 apply(simp) |
|
351 apply(simp add: Respects_def in_respects) |
|
352 apply(rule impI) |
|
353 using a equivp_reflp_symp_transp[of "R2"] |
|
354 apply(simp add: reflp_def) |
|
355 done |
|
356 |
|
357 lemma all_reg: |
|
358 assumes a: "!x :: 'a. (P x --> Q x)" |
|
359 and b: "All P" |
|
360 shows "All Q" |
|
361 using a b by (metis) |
|
362 |
|
363 lemma ex_reg: |
|
364 assumes a: "!x :: 'a. (P x --> Q x)" |
|
365 and b: "Ex P" |
|
366 shows "Ex Q" |
|
367 using a b by metis |
|
368 |
|
369 lemma ball_reg: |
|
370 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
|
371 and b: "Ball R P" |
|
372 shows "Ball R Q" |
|
373 using a b by (metis COMBC_def Collect_def Collect_mem_eq) |
|
374 |
|
375 lemma bex_reg: |
|
376 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
|
377 and b: "Bex R P" |
|
378 shows "Bex R Q" |
|
379 using a b by (metis COMBC_def Collect_def Collect_mem_eq) |
|
380 |
|
381 lemma ball_all_comm: |
|
382 assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)" |
|
383 shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)" |
|
384 using assms by auto |
|
385 |
|
386 lemma bex_ex_comm: |
|
387 assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)" |
|
388 shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)" |
|
389 using assms by auto |
|
390 |
|
391 section {* Bounded abstraction *} |
|
392 |
|
393 definition |
|
394 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
395 where |
|
396 "x \<in> p \<Longrightarrow> Babs p m x = m x" |
|
397 |
|
398 lemma babs_rsp: |
|
399 assumes q: "Quotient R1 Abs1 Rep1" |
|
400 and a: "(R1 ===> R2) f g" |
|
401 shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" |
|
402 apply (auto simp add: Babs_def in_respects) |
|
403 apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") |
|
404 using a apply (simp add: Babs_def) |
|
405 apply (simp add: in_respects) |
|
406 using Quotient_rel[OF q] |
|
407 by metis |
|
408 |
|
409 lemma babs_prs: |
|
410 assumes q1: "Quotient R1 Abs1 Rep1" |
|
411 and q2: "Quotient R2 Abs2 Rep2" |
|
412 shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f" |
|
413 apply (rule ext) |
|
414 apply (simp) |
|
415 apply (subgoal_tac "Rep1 x \<in> Respects R1") |
|
416 apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
|
417 apply (simp add: in_respects Quotient_rel_rep[OF q1]) |
|
418 done |
|
419 |
|
420 lemma babs_simp: |
|
421 assumes q: "Quotient R1 Abs Rep" |
|
422 shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)" |
|
423 apply(rule iffI) |
|
424 apply(simp_all only: babs_rsp[OF q]) |
|
425 apply(auto simp add: Babs_def) |
|
426 apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1") |
|
427 apply(metis Babs_def) |
|
428 apply (simp add: in_respects) |
|
429 using Quotient_rel[OF q] |
|
430 by metis |
|
431 |
|
432 (* If a user proves that a particular functional relation |
|
433 is an equivalence this may be useful in regularising *) |
|
434 lemma babs_reg_eqv: |
|
435 shows "equivp R \<Longrightarrow> Babs (Respects R) P = P" |
|
436 by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) |
|
437 |
|
438 |
|
439 (* 3 lemmas needed for proving repabs_inj *) |
|
440 lemma ball_rsp: |
|
441 assumes a: "(R ===> (op =)) f g" |
|
442 shows "Ball (Respects R) f = Ball (Respects R) g" |
|
443 using a by (simp add: Ball_def in_respects) |
|
444 |
|
445 lemma bex_rsp: |
|
446 assumes a: "(R ===> (op =)) f g" |
|
447 shows "(Bex (Respects R) f = Bex (Respects R) g)" |
|
448 using a by (simp add: Bex_def in_respects) |
|
449 |
|
450 lemma bex1_rsp: |
|
451 assumes a: "(R ===> (op =)) f g" |
|
452 shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)" |
|
453 using a |
|
454 by (simp add: Ex1_def in_respects) auto |
|
455 |
|
456 (* 2 lemmas needed for cleaning of quantifiers *) |
|
457 lemma all_prs: |
|
458 assumes a: "Quotient R absf repf" |
|
459 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
|
460 using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply |
|
461 by metis |
|
462 |
|
463 lemma ex_prs: |
|
464 assumes a: "Quotient R absf repf" |
|
465 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
|
466 using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply |
|
467 by metis |
|
468 |
|
469 section {* Bex1_rel quantifier *} |
|
470 |
|
471 definition |
|
472 Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
|
473 where |
|
474 "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))" |
|
475 |
|
476 lemma bex1_rel_aux: |
|
477 "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y" |
|
478 unfolding Bex1_rel_def |
|
479 apply (erule conjE)+ |
|
480 apply (erule bexE) |
|
481 apply rule |
|
482 apply (rule_tac x="xa" in bexI) |
|
483 apply metis |
|
484 apply metis |
|
485 apply rule+ |
|
486 apply (erule_tac x="xaa" in ballE) |
|
487 prefer 2 |
|
488 apply (metis) |
|
489 apply (erule_tac x="ya" in ballE) |
|
490 prefer 2 |
|
491 apply (metis) |
|
492 apply (metis in_respects) |
|
493 done |
|
494 |
|
495 lemma bex1_rel_aux2: |
|
496 "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x" |
|
497 unfolding Bex1_rel_def |
|
498 apply (erule conjE)+ |
|
499 apply (erule bexE) |
|
500 apply rule |
|
501 apply (rule_tac x="xa" in bexI) |
|
502 apply metis |
|
503 apply metis |
|
504 apply rule+ |
|
505 apply (erule_tac x="xaa" in ballE) |
|
506 prefer 2 |
|
507 apply (metis) |
|
508 apply (erule_tac x="ya" in ballE) |
|
509 prefer 2 |
|
510 apply (metis) |
|
511 apply (metis in_respects) |
|
512 done |
|
513 |
|
514 lemma bex1_rel_rsp: |
|
515 assumes a: "Quotient R absf repf" |
|
516 shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)" |
|
517 apply simp |
|
518 apply clarify |
|
519 apply rule |
|
520 apply (simp_all add: bex1_rel_aux bex1_rel_aux2) |
|
521 apply (erule bex1_rel_aux2) |
|
522 apply assumption |
|
523 done |
|
524 |
|
525 |
|
526 lemma ex1_prs: |
|
527 assumes a: "Quotient R absf repf" |
|
528 shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" |
|
529 apply simp |
|
530 apply (subst Bex1_rel_def) |
|
531 apply (subst Bex_def) |
|
532 apply (subst Ex1_def) |
|
533 apply simp |
|
534 apply rule |
|
535 apply (erule conjE)+ |
|
536 apply (erule_tac exE) |
|
537 apply (erule conjE) |
|
538 apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y") |
|
539 apply (rule_tac x="absf x" in exI) |
|
540 apply (simp) |
|
541 apply rule+ |
|
542 using a unfolding Quotient_def |
|
543 apply metis |
|
544 apply rule+ |
|
545 apply (erule_tac x="x" in ballE) |
|
546 apply (erule_tac x="y" in ballE) |
|
547 apply simp |
|
548 apply (simp add: in_respects) |
|
549 apply (simp add: in_respects) |
|
550 apply (erule_tac exE) |
|
551 apply rule |
|
552 apply (rule_tac x="repf x" in exI) |
|
553 apply (simp only: in_respects) |
|
554 apply rule |
|
555 apply (metis Quotient_rel_rep[OF a]) |
|
556 using a unfolding Quotient_def apply (simp) |
|
557 apply rule+ |
|
558 using a unfolding Quotient_def in_respects |
|
559 apply metis |
|
560 done |
|
561 |
|
562 lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))" |
|
563 apply (simp add: Ex1_def Bex1_rel_def in_respects) |
|
564 apply clarify |
|
565 apply auto |
|
566 apply (rule bexI) |
|
567 apply assumption |
|
568 apply (simp add: in_respects) |
|
569 apply (simp add: in_respects) |
|
570 apply auto |
|
571 done |
|
572 |
|
573 section {* Various respects and preserve lemmas *} |
|
574 |
|
575 lemma quot_rel_rsp: |
|
576 assumes a: "Quotient R Abs Rep" |
|
577 shows "(R ===> R ===> op =) R R" |
|
578 apply(rule fun_rel_id)+ |
|
579 apply(rule equals_rsp[OF a]) |
|
580 apply(assumption)+ |
|
581 done |
|
582 |
|
583 lemma o_prs: |
|
584 assumes q1: "Quotient R1 Abs1 Rep1" |
|
585 and q2: "Quotient R2 Abs2 Rep2" |
|
586 and q3: "Quotient R3 Abs3 Rep3" |
|
587 shows "(Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g)) = f o g" |
|
588 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3] |
|
589 unfolding o_def expand_fun_eq by simp |
|
590 |
|
591 lemma o_rsp: |
|
592 assumes q1: "Quotient R1 Abs1 Rep1" |
|
593 and q2: "Quotient R2 Abs2 Rep2" |
|
594 and q3: "Quotient R3 Abs3 Rep3" |
|
595 and a1: "(R2 ===> R3) f1 f2" |
|
596 and a2: "(R1 ===> R2) g1 g2" |
|
597 shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" |
|
598 using a1 a2 unfolding o_def expand_fun_eq |
|
599 by (auto) |
|
600 |
|
601 lemma cond_prs: |
|
602 assumes a: "Quotient R absf repf" |
|
603 shows "absf (if a then repf b else repf c) = (if a then b else c)" |
|
604 using a unfolding Quotient_def by auto |
|
605 |
|
606 lemma if_prs: |
|
607 assumes q: "Quotient R Abs Rep" |
|
608 shows "Abs (If a (Rep b) (Rep c)) = If a b c" |
|
609 using Quotient_abs_rep[OF q] by auto |
|
610 |
|
611 (* q not used *) |
|
612 lemma if_rsp: |
|
613 assumes q: "Quotient R Abs Rep" |
|
614 and a: "a1 = a2" "R b1 b2" "R c1 c2" |
|
615 shows "R (If a1 b1 c1) (If a2 b2 c2)" |
|
616 using a by auto |
|
617 |
|
618 lemma let_prs: |
|
619 assumes q1: "Quotient R1 Abs1 Rep1" |
|
620 and q2: "Quotient R2 Abs2 Rep2" |
|
621 shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f" |
|
622 using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto |
|
623 |
|
624 lemma let_rsp: |
|
625 assumes q1: "Quotient R1 Abs1 Rep1" |
|
626 and a1: "(R1 ===> R2) f g" |
|
627 and a2: "R1 x y" |
|
628 shows "R2 ((Let x f)::'c) ((Let y g)::'c)" |
|
629 using apply_rsp[OF q1 a1] a2 by auto |
|
630 |
|
631 locale quot_type = |
|
632 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
633 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
|
634 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
|
635 assumes equivp: "equivp R" |
|
636 and rep_prop: "\<And>y. \<exists>x. Rep y = R x" |
|
637 and rep_inverse: "\<And>x. Abs (Rep x) = x" |
|
638 and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)" |
|
639 and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" |
|
640 begin |
|
641 |
|
642 definition |
|
643 abs::"'a \<Rightarrow> 'b" |
|
644 where |
|
645 "abs x \<equiv> Abs (R x)" |
|
646 |
|
647 definition |
|
648 rep::"'b \<Rightarrow> 'a" |
|
649 where |
|
650 "rep a = Eps (Rep a)" |
|
651 |
|
652 lemma homeier_lem9: |
|
653 shows "R (Eps (R x)) = R x" |
|
654 proof - |
|
655 have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def) |
|
656 then have "R x (Eps (R x))" by (rule someI) |
|
657 then show "R (Eps (R x)) = R x" |
|
658 using equivp unfolding equivp_def by simp |
|
659 qed |
|
660 |
|
661 theorem homeier_thm10: |
|
662 shows "abs (rep a) = a" |
|
663 unfolding abs_def rep_def |
|
664 proof - |
|
665 from rep_prop |
|
666 obtain x where eq: "Rep a = R x" by auto |
|
667 have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp |
|
668 also have "\<dots> = Abs (R x)" using homeier_lem9 by simp |
|
669 also have "\<dots> = Abs (Rep a)" using eq by simp |
|
670 also have "\<dots> = a" using rep_inverse by simp |
|
671 finally |
|
672 show "Abs (R (Eps (Rep a))) = a" by simp |
|
673 qed |
|
674 |
|
675 lemma homeier_lem7: |
|
676 shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS") |
|
677 proof - |
|
678 have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject) |
|
679 also have "\<dots> = ?LHS" by (simp add: abs_inverse) |
|
680 finally show "?LHS = ?RHS" by simp |
|
681 qed |
|
682 |
|
683 theorem homeier_thm11: |
|
684 shows "R r r' = (abs r = abs r')" |
|
685 unfolding abs_def |
|
686 by (simp only: equivp[simplified equivp_def] homeier_lem7) |
|
687 |
|
688 lemma rep_refl: |
|
689 shows "R (rep a) (rep a)" |
|
690 unfolding rep_def |
|
691 by (simp add: equivp[simplified equivp_def]) |
|
692 |
|
693 |
|
694 lemma rep_abs_rsp: |
|
695 shows "R f (rep (abs g)) = R f g" |
|
696 and "R (rep (abs g)) f = R g f" |
|
697 by (simp_all add: homeier_thm10 homeier_thm11) |
|
698 |
|
699 lemma Quotient: |
|
700 shows "Quotient R abs rep" |
|
701 unfolding Quotient_def |
|
702 apply(simp add: homeier_thm10) |
|
703 apply(simp add: rep_refl) |
|
704 apply(subst homeier_thm11[symmetric]) |
|
705 apply(simp add: equivp[simplified equivp_def]) |
|
706 done |
|
707 |
|
708 end |
|
709 |
|
710 section {* ML setup *} |
|
711 |
|
712 text {* Auxiliary data for the quotient package *} |
|
713 |
|
714 use "quotient_info.ML" |
|
715 |
|
716 declare [[map "fun" = (fun_map, fun_rel)]] |
|
717 |
|
718 lemmas [quot_thm] = fun_quotient |
|
719 lemmas [quot_respect] = quot_rel_rsp |
|
720 lemmas [quot_equiv] = identity_equivp |
|
721 |
|
722 |
|
723 text {* Lemmas about simplifying id's. *} |
|
724 lemmas [id_simps] = |
|
725 id_def[symmetric] |
|
726 fun_map_id |
|
727 id_apply |
|
728 id_o |
|
729 o_id |
|
730 eq_comp_r |
|
731 |
|
732 text {* Translation functions for the lifting process. *} |
|
733 use "quotient_term.ML" |
|
734 |
|
735 |
|
736 text {* Definitions of the quotient types. *} |
|
737 use "quotient_typ.ML" |
|
738 |
|
739 |
|
740 text {* Definitions for quotient constants. *} |
|
741 use "quotient_def.ML" |
|
742 |
|
743 |
|
744 text {* |
|
745 An auxiliary constant for recording some information |
|
746 about the lifted theorem in a tactic. |
|
747 *} |
|
748 definition |
|
749 "Quot_True x \<equiv> True" |
|
750 |
|
751 lemma |
|
752 shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P" |
|
753 and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P" |
|
754 and QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P" |
|
755 and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))" |
|
756 and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)" |
|
757 by (simp_all add: Quot_True_def ext) |
|
758 |
|
759 lemma QT_imp: "Quot_True a \<equiv> Quot_True b" |
|
760 by (simp add: Quot_True_def) |
|
761 |
|
762 |
|
763 text {* Tactics for proving the lifted theorems *} |
|
764 use "quotient_tacs.ML" |
|
765 |
|
766 section {* Methods / Interface *} |
|
767 |
|
768 (* TODO inline *) |
|
769 ML {* |
|
770 fun mk_method1 tac thms ctxt = |
|
771 SIMPLE_METHOD (HEADGOAL (tac ctxt thms)) |
|
772 |
|
773 fun mk_method2 tac ctxt = |
|
774 SIMPLE_METHOD (HEADGOAL (tac ctxt)) |
|
775 *} |
|
776 |
|
777 method_setup lifting = |
|
778 {* Attrib.thms >> (mk_method1 Quotient_Tacs.lift_tac) *} |
|
779 {* lifts theorems to quotient types *} |
|
780 |
|
781 method_setup lifting_setup = |
|
782 {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *} |
|
783 {* sets up the three goals for the quotient lifting procedure *} |
|
784 |
|
785 method_setup regularize = |
|
786 {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *} |
|
787 {* proves the regularization goals from the quotient lifting procedure *} |
|
788 |
|
789 method_setup injection = |
|
790 {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *} |
|
791 {* proves the rep/abs injection goals from the quotient lifting procedure *} |
|
792 |
|
793 method_setup cleaning = |
|
794 {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} |
|
795 {* proves the cleaning goals from the quotient lifting procedure *} |
|
796 |
|
797 attribute_setup quot_lifted = |
|
798 {* Scan.succeed Quotient_Tacs.lifted_attrib *} |
|
799 {* lifts theorems to quotient types *} |
|
800 |
|
801 end |
|
802 |
|