1 theory QuotMainNew |
|
2 imports QuotScript QuotList Prove |
|
3 uses ("quotient_info.ML") |
|
4 ("quotient.ML") |
|
5 ("quotient_def.ML") |
|
6 begin |
|
7 |
|
8 locale QUOT_TYPE = |
|
9 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
10 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
|
11 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
|
12 assumes equiv: "EQUIV R" |
|
13 and rep_prop: "\<And>y. \<exists>x. Rep y = R x" |
|
14 and rep_inverse: "\<And>x. Abs (Rep x) = x" |
|
15 and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)" |
|
16 and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" |
|
17 begin |
|
18 |
|
19 definition |
|
20 ABS::"'a \<Rightarrow> 'b" |
|
21 where |
|
22 "ABS x \<equiv> Abs (R x)" |
|
23 |
|
24 definition |
|
25 REP::"'b \<Rightarrow> 'a" |
|
26 where |
|
27 "REP a = Eps (Rep a)" |
|
28 |
|
29 lemma lem9: |
|
30 shows "R (Eps (R x)) = R x" |
|
31 proof - |
|
32 have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) |
|
33 then have "R x (Eps (R x))" by (rule someI) |
|
34 then show "R (Eps (R x)) = R x" |
|
35 using equiv unfolding EQUIV_def by simp |
|
36 qed |
|
37 |
|
38 theorem thm10: |
|
39 shows "ABS (REP a) \<equiv> a" |
|
40 apply (rule eq_reflection) |
|
41 unfolding ABS_def REP_def |
|
42 proof - |
|
43 from rep_prop |
|
44 obtain x where eq: "Rep a = R x" by auto |
|
45 have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp |
|
46 also have "\<dots> = Abs (R x)" using lem9 by simp |
|
47 also have "\<dots> = Abs (Rep a)" using eq by simp |
|
48 also have "\<dots> = a" using rep_inverse by simp |
|
49 finally |
|
50 show "Abs (R (Eps (Rep a))) = a" by simp |
|
51 qed |
|
52 |
|
53 lemma REP_refl: |
|
54 shows "R (REP a) (REP a)" |
|
55 unfolding REP_def |
|
56 by (simp add: equiv[simplified EQUIV_def]) |
|
57 |
|
58 lemma lem7: |
|
59 shows "(R x = R y) = (Abs (R x) = Abs (R y))" |
|
60 apply(rule iffI) |
|
61 apply(simp) |
|
62 apply(drule rep_inject[THEN iffD2]) |
|
63 apply(simp add: abs_inverse) |
|
64 done |
|
65 |
|
66 theorem thm11: |
|
67 shows "R r r' = (ABS r = ABS r')" |
|
68 unfolding ABS_def |
|
69 by (simp only: equiv[simplified EQUIV_def] lem7) |
|
70 |
|
71 |
|
72 lemma REP_ABS_rsp: |
|
73 shows "R f (REP (ABS g)) = R f g" |
|
74 and "R (REP (ABS g)) f = R g f" |
|
75 by (simp_all add: thm10 thm11) |
|
76 |
|
77 lemma QUOTIENT: |
|
78 "QUOTIENT R ABS REP" |
|
79 apply(unfold QUOTIENT_def) |
|
80 apply(simp add: thm10) |
|
81 apply(simp add: REP_refl) |
|
82 apply(subst thm11[symmetric]) |
|
83 apply(simp add: equiv[simplified EQUIV_def]) |
|
84 done |
|
85 |
|
86 lemma R_trans: |
|
87 assumes ab: "R a b" |
|
88 and bc: "R b c" |
|
89 shows "R a c" |
|
90 proof - |
|
91 have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
|
92 moreover have ab: "R a b" by fact |
|
93 moreover have bc: "R b c" by fact |
|
94 ultimately show "R a c" unfolding TRANS_def by blast |
|
95 qed |
|
96 |
|
97 lemma R_sym: |
|
98 assumes ab: "R a b" |
|
99 shows "R b a" |
|
100 proof - |
|
101 have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
|
102 then show "R b a" using ab unfolding SYM_def by blast |
|
103 qed |
|
104 |
|
105 lemma R_trans2: |
|
106 assumes ac: "R a c" |
|
107 and bd: "R b d" |
|
108 shows "R a b = R c d" |
|
109 using ac bd |
|
110 by (blast intro: R_trans R_sym) |
|
111 |
|
112 lemma REPS_same: |
|
113 shows "R (REP a) (REP b) \<equiv> (a = b)" |
|
114 proof - |
|
115 have "R (REP a) (REP b) = (a = b)" |
|
116 proof |
|
117 assume as: "R (REP a) (REP b)" |
|
118 from rep_prop |
|
119 obtain x y |
|
120 where eqs: "Rep a = R x" "Rep b = R y" by blast |
|
121 from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp |
|
122 then have "R x (Eps (R y))" using lem9 by simp |
|
123 then have "R (Eps (R y)) x" using R_sym by blast |
|
124 then have "R y x" using lem9 by simp |
|
125 then have "R x y" using R_sym by blast |
|
126 then have "ABS x = ABS y" using thm11 by simp |
|
127 then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp |
|
128 then show "a = b" using rep_inverse by simp |
|
129 next |
|
130 assume ab: "a = b" |
|
131 have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp |
|
132 then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto |
|
133 qed |
|
134 then show "R (REP a) (REP b) \<equiv> (a = b)" by simp |
|
135 qed |
|
136 |
|
137 end |
|
138 |
|
139 lemma equiv_trans2: |
|
140 assumes e: "EQUIV R" |
|
141 and ac: "R a c" |
|
142 and bd: "R b d" |
|
143 shows "R a b = R c d" |
|
144 using ac bd e |
|
145 unfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_def |
|
146 by (blast) |
|
147 |
|
148 section {* type definition for the quotient type *} |
|
149 |
|
150 (* the auxiliary data for the quotient types *) |
|
151 use "quotient_info.ML" |
|
152 |
|
153 declare [[map list = (map, LIST_REL)]] |
|
154 declare [[map * = (prod_fun, prod_rel)]] |
|
155 declare [[map "fun" = (fun_map, FUN_REL)]] |
|
156 |
|
157 ML {* maps_lookup @{theory} "List.list" *} |
|
158 ML {* maps_lookup @{theory} "*" *} |
|
159 ML {* maps_lookup @{theory} "fun" *} |
|
160 |
|
161 |
|
162 (* definition of the quotient types *) |
|
163 (* FIXME: should be called quotient_typ.ML *) |
|
164 use "quotient.ML" |
|
165 |
|
166 |
|
167 (* lifting of constants *) |
|
168 use "quotient_def.ML" |
|
169 |
|
170 (* TODO: Consider defining it with an "if"; sth like: |
|
171 Babs p m = \<lambda>x. if x \<in> p then m x else undefined |
|
172 *) |
|
173 definition |
|
174 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
175 where |
|
176 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
|
177 |
|
178 section {* ATOMIZE *} |
|
179 |
|
180 lemma atomize_eqv[atomize]: |
|
181 shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" |
|
182 proof |
|
183 assume "A \<equiv> B" |
|
184 then show "Trueprop A \<equiv> Trueprop B" by unfold |
|
185 next |
|
186 assume *: "Trueprop A \<equiv> Trueprop B" |
|
187 have "A = B" |
|
188 proof (cases A) |
|
189 case True |
|
190 have "A" by fact |
|
191 then show "A = B" using * by simp |
|
192 next |
|
193 case False |
|
194 have "\<not>A" by fact |
|
195 then show "A = B" using * by auto |
|
196 qed |
|
197 then show "A \<equiv> B" by (rule eq_reflection) |
|
198 qed |
|
199 |
|
200 ML {* |
|
201 fun atomize_thm thm = |
|
202 let |
|
203 val thm' = Thm.freezeT (forall_intr_vars thm) |
|
204 val thm'' = ObjectLogic.atomize (cprop_of thm') |
|
205 in |
|
206 @{thm equal_elim_rule1} OF [thm'', thm'] |
|
207 end |
|
208 *} |
|
209 |
|
210 section {* infrastructure about id *} |
|
211 |
|
212 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
|
213 by (rule eq_reflection) (simp add: prod_fun_def) |
|
214 |
|
215 lemma map_id: "map id \<equiv> id" |
|
216 apply (rule eq_reflection) |
|
217 apply (rule ext) |
|
218 apply (rule_tac list="x" in list.induct) |
|
219 apply (simp_all) |
|
220 done |
|
221 |
|
222 lemmas id_simps = |
|
223 FUN_MAP_I[THEN eq_reflection] |
|
224 id_apply[THEN eq_reflection] |
|
225 id_def[THEN eq_reflection,symmetric] |
|
226 prod_fun_id map_id |
|
227 |
|
228 ML {* |
|
229 fun simp_ids thm = |
|
230 MetaSimplifier.rewrite_rule @{thms id_simps} thm |
|
231 *} |
|
232 |
|
233 section {* Debugging infrastructure for testing tactics *} |
|
234 |
|
235 ML {* |
|
236 fun my_print_tac ctxt s i thm = |
|
237 let |
|
238 val prem_str = nth (prems_of thm) (i - 1) |
|
239 |> Syntax.string_of_term ctxt |
|
240 handle Subscript => "no subgoal" |
|
241 val _ = tracing (s ^ "\n" ^ prem_str) |
|
242 in |
|
243 Seq.single thm |
|
244 end *} |
|
245 |
|
246 |
|
247 ML {* |
|
248 fun DT ctxt s tac i thm = |
|
249 let |
|
250 val before_goal = nth (prems_of thm) (i - 1) |
|
251 |> Syntax.string_of_term ctxt |
|
252 val before_msg = ["before: " ^ s, before_goal, "after: " ^ s] |
|
253 |> cat_lines |
|
254 in |
|
255 EVERY [tac i, my_print_tac ctxt before_msg i] thm |
|
256 end |
|
257 |
|
258 fun NDT ctxt s tac thm = tac thm |
|
259 *} |
|
260 |
|
261 |
|
262 section {* Infrastructure for special quotient identity *} |
|
263 |
|
264 definition |
|
265 "qid TYPE('a) TYPE('b) x \<equiv> x" |
|
266 |
|
267 ML {* |
|
268 fun get_typ_aux (Type ("itself", [T])) = T |
|
269 fun get_typ (Const ("TYPE", T)) = get_typ_aux T |
|
270 fun get_tys (Const (@{const_name "qid"},_) $ ty1 $ ty2) = |
|
271 (get_typ ty1, get_typ ty2) |
|
272 |
|
273 fun is_qid (Const (@{const_name "qid"},_) $ _ $ _) = true |
|
274 | is_qid _ = false |
|
275 |
|
276 |
|
277 fun mk_itself ty = Type ("itself", [ty]) |
|
278 fun mk_TYPE ty = Const ("TYPE", mk_itself ty) |
|
279 fun mk_qid (rty, qty, trm) = |
|
280 Const (@{const_name "qid"}, [mk_itself rty, mk_itself qty, dummyT] ---> dummyT) |
|
281 $ mk_TYPE rty $ mk_TYPE qty $ trm |
|
282 *} |
|
283 |
|
284 ML {* |
|
285 fun insertion_aux (rtrm, qtrm) = |
|
286 case (rtrm, qtrm) of |
|
287 (Abs (x, ty, t), Abs (x', ty', t')) => |
|
288 let |
|
289 val (y, s) = Term.dest_abs (x, ty, t) |
|
290 val (_, s') = Term.dest_abs (x', ty', t') |
|
291 val yvar = Free (y, ty) |
|
292 val result = Term.lambda_name (y, yvar) (insertion_aux (s, s')) |
|
293 in |
|
294 if ty = ty' |
|
295 then result |
|
296 else mk_qid (ty, ty', result) |
|
297 end |
|
298 | (_ $ _, _ $ _) => |
|
299 let |
|
300 val rty = fastype_of rtrm |
|
301 val qty = fastype_of qtrm |
|
302 val (rhead, rargs) = strip_comb rtrm |
|
303 val (qhead, qargs) = strip_comb qtrm |
|
304 val rargs' = map insertion_aux (rargs ~~ qargs) |
|
305 val rhead' = insertion_aux (rhead, qhead) |
|
306 val result = list_comb (rhead', rargs') |
|
307 in |
|
308 if rty = qty |
|
309 then result |
|
310 else mk_qid (rty, qty, result) |
|
311 end |
|
312 | (Free (_, ty), Free (_, ty')) => |
|
313 if ty = ty' |
|
314 then rtrm |
|
315 else mk_qid (ty, ty', rtrm) |
|
316 | (Const (s, ty), Const (s', ty')) => |
|
317 if s = s' |
|
318 then rtrm |
|
319 else mk_qid (ty, ty', rtrm) |
|
320 | (_, _) => raise (LIFT_MATCH "insertion") |
|
321 *} |
|
322 |
|
323 ML {* |
|
324 fun insertion ctxt rtrm qtrm = |
|
325 Syntax.check_term ctxt (insertion_aux (rtrm, qtrm)) |
|
326 *} |
|
327 |
|
328 |
|
329 fun |
|
330 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
|
331 where |
|
332 "intrel (x, y) (u, v) = (x + v = u + y)" |
|
333 |
|
334 quotient my_int = "nat \<times> nat" / intrel |
|
335 apply(unfold EQUIV_def) |
|
336 apply(auto simp add: mem_def expand_fun_eq) |
|
337 done |
|
338 |
|
339 fun |
|
340 my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
341 where |
|
342 "my_plus (x, y) (u, v) = (x + u, y + v)" |
|
343 |
|
344 quotient_def |
|
345 PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
|
346 where |
|
347 "PLUS \<equiv> my_plus" |
|
348 |
|
349 thm PLUS_def |
|
350 |
|
351 ML {* MetaSimplifier.rewrite_term *} |
|
352 |
|
353 ML {* |
|
354 let |
|
355 val rtrm = @{term "\<forall>a b. my_plus a b \<approx> my_plus b a"} |
|
356 val qtrm = @{term "\<forall>a b. PLUS a b = PLUS b a"} |
|
357 val ctxt = @{context} |
|
358 in |
|
359 insertion ctxt rtrm qtrm |
|
360 (*|> Drule.term_rule @{theory} (MetaSimplifier.rewrite_rule [@{thm "qid_def"}])*) |
|
361 |> Syntax.string_of_term ctxt |
|
362 |> writeln |
|
363 end |
|
364 *} |
|
365 |
|
366 section {* Regularization *} |
|
367 |
|
368 (* |
|
369 Regularizing an rtrm means: |
|
370 - quantifiers over a type that needs lifting are replaced by |
|
371 bounded quantifiers, for example: |
|
372 \<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P |
|
373 |
|
374 the relation R is given by the rty and qty; |
|
375 |
|
376 - abstractions over a type that needs lifting are replaced |
|
377 by bounded abstractions: |
|
378 \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P) |
|
379 |
|
380 - equalities over the type being lifted are replaced by |
|
381 corresponding relations: |
|
382 A = B \<Longrightarrow> A \<approx> B |
|
383 |
|
384 example with more complicated types of A, B: |
|
385 A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B |
|
386 *) |
|
387 |
|
388 ML {* |
|
389 (* builds the relation that is the argument of respects *) |
|
390 fun mk_resp_arg lthy (rty, qty) = |
|
391 let |
|
392 val thy = ProofContext.theory_of lthy |
|
393 in |
|
394 if rty = qty |
|
395 then HOLogic.eq_const rty |
|
396 else |
|
397 case (rty, qty) of |
|
398 (Type (s, tys), Type (s', tys')) => |
|
399 if s = s' |
|
400 then let |
|
401 val SOME map_info = maps_lookup thy s |
|
402 val args = map (mk_resp_arg lthy) (tys ~~ tys') |
|
403 in |
|
404 list_comb (Const (#relfun map_info, dummyT), args) |
|
405 end |
|
406 else let |
|
407 val SOME qinfo = quotdata_lookup_thy thy s' |
|
408 (* FIXME: check in this case that the rty and qty *) |
|
409 (* FIXME: correspond to each other *) |
|
410 val (s, _) = dest_Const (#rel qinfo) |
|
411 (* FIXME: the relation should only be the string *) |
|
412 (* FIXME: and the type needs to be calculated as below; *) |
|
413 (* FIXME: maybe one should actually have a term *) |
|
414 (* FIXME: and one needs to force it to have this type *) |
|
415 in |
|
416 Const (s, rty --> rty --> @{typ bool}) |
|
417 end |
|
418 | _ => HOLogic.eq_const dummyT |
|
419 (* FIXME: check that the types correspond to each other? *) |
|
420 end |
|
421 *} |
|
422 |
|
423 ML {* |
|
424 val mk_babs = Const (@{const_name "Babs"}, dummyT) |
|
425 val mk_ball = Const (@{const_name "Ball"}, dummyT) |
|
426 val mk_bex = Const (@{const_name "Bex"}, dummyT) |
|
427 val mk_resp = Const (@{const_name Respects}, dummyT) |
|
428 *} |
|
429 |
|
430 ML {* |
|
431 (* - applies f to the subterm of an abstraction, *) |
|
432 (* otherwise to the given term, *) |
|
433 (* - used by regularize, therefore abstracted *) |
|
434 (* variables do not have to be treated specially *) |
|
435 |
|
436 fun apply_subt f trm = |
|
437 case trm of |
|
438 (Abs (x, T, t)) => Abs (x, T, f t) |
|
439 | _ => f trm |
|
440 |
|
441 (* the major type of All and Ex quantifiers *) |
|
442 fun qnt_typ ty = domain_type (domain_type ty) |
|
443 *} |
|
444 |
|
445 ML {* |
|
446 (* produces a regularized version of trm *) |
|
447 (* - the result is still not completely typed *) |
|
448 (* - does not need any special treatment of *) |
|
449 (* bound variables *) |
|
450 |
|
451 fun regularize_trm lthy trm = |
|
452 case trm of |
|
453 (Const (@{const_name "qid"},_) $ rty' $ qty' $ Abs (x, ty, t)) => |
|
454 let |
|
455 val rty = get_typ rty' |
|
456 val qty = get_typ qty' |
|
457 val subtrm = regularize_trm lthy t |
|
458 in |
|
459 mk_qid (rty, qty, mk_babs $ (mk_resp $ mk_resp_arg lthy (rty, qty)) $ subtrm) |
|
460 end |
|
461 | (Const (@{const_name "qid"},_) $ rty' $ qty' $ (Const (@{const_name "All"}, ty) $ t)) => |
|
462 let |
|
463 val subtrm = apply_subt (regularize_trm lthy) t |
|
464 in |
|
465 if ty = ty' |
|
466 then Const (@{const_name "All"}, ty) $ subtrm |
|
467 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
468 end |
|
469 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
|
470 let |
|
471 val subtrm = apply_subt (regularize_trm lthy) t t' |
|
472 in |
|
473 if ty = ty' |
|
474 then Const (@{const_name "Ex"}, ty) $ subtrm |
|
475 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
476 end |
|
477 (* FIXME: Should = only be replaced, when fully applied? *) |
|
478 (* Then there must be a 2nd argument *) |
|
479 | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => |
|
480 let |
|
481 val subtrm = regularize_trm lthy t t' |
|
482 in |
|
483 if ty = ty' |
|
484 then Const (@{const_name "op ="}, ty) $ subtrm |
|
485 else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm |
|
486 end |
|
487 | (t1 $ t2, t1' $ t2') => |
|
488 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
|
489 | (Free (x, ty), Free (x', ty')) => |
|
490 (* this case cannot arrise as we start with two fully atomized terms *) |
|
491 raise (LIFT_MATCH "regularize (frees)") |
|
492 | (Bound i, Bound i') => |
|
493 if i = i' |
|
494 then rtrm |
|
495 else raise (LIFT_MATCH "regularize (bounds)") |
|
496 | (Const (s, ty), Const (s', ty')) => |
|
497 if s = s' andalso ty = ty' |
|
498 then rtrm |
|
499 else rtrm (* FIXME: check correspondence according to definitions *) |
|
500 | (rt, qt) => |
|
501 raise (LIFT_MATCH "regularize (default)") |
|
502 *} |
|
503 |
|
504 (* |
|
505 FIXME / TODO: needs to be adapted |
|
506 |
|
507 To prove that the raw theorem implies the regularised one, |
|
508 we try in order: |
|
509 |
|
510 - Reflexivity of the relation |
|
511 - Assumption |
|
512 - Elimnating quantifiers on both sides of toplevel implication |
|
513 - Simplifying implications on both sides of toplevel implication |
|
514 - Ball (Respects ?E) ?P = All ?P |
|
515 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
|
516 |
|
517 *) |
|
518 |
|
519 section {* Injections of REP and ABSes *} |
|
520 |
|
521 (* |
|
522 Injecting REPABS means: |
|
523 |
|
524 For abstractions: |
|
525 * If the type of the abstraction doesn't need lifting we recurse. |
|
526 * If it does we add RepAbs around the whole term and check if the |
|
527 variable needs lifting. |
|
528 * If it doesn't then we recurse |
|
529 * If it does we recurse and put 'RepAbs' around all occurences |
|
530 of the variable in the obtained subterm. This in combination |
|
531 with the RepAbs above will let us change the type of the |
|
532 abstraction with rewriting. |
|
533 For applications: |
|
534 * If the term is 'Respects' applied to anything we leave it unchanged |
|
535 * If the term needs lifting and the head is a constant that we know |
|
536 how to lift, we put a RepAbs and recurse |
|
537 * If the term needs lifting and the head is a free applied to subterms |
|
538 (if it is not applied we treated it in Abs branch) then we |
|
539 put RepAbs and recurse |
|
540 * Otherwise just recurse. |
|
541 *) |
|
542 |
|
543 ML {* |
|
544 fun mk_repabs lthy (T, T') trm = |
|
545 Quotient_Def.get_fun repF lthy (T, T') |
|
546 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
|
547 *} |
|
548 |
|
549 ML {* |
|
550 (* bound variables need to be treated properly, *) |
|
551 (* as the type of subterms need to be calculated *) |
|
552 |
|
553 fun inj_repabs_trm lthy (rtrm, qtrm) = |
|
554 let |
|
555 val rty = fastype_of rtrm |
|
556 val qty = fastype_of qtrm |
|
557 in |
|
558 case (rtrm, qtrm) of |
|
559 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
|
560 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
|
561 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
|
562 Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
|
563 | (Const (@{const_name "Babs"}, T) $ r $ t, t') => |
|
564 Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
|
565 | (Abs (x, T, t), Abs (x', T', t')) => |
|
566 let |
|
567 val (y, s) = Term.dest_abs (x, T, t) |
|
568 val (_, s') = Term.dest_abs (x', T', t') |
|
569 val yvar = Free (y, T) |
|
570 val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) |
|
571 in |
|
572 if rty = qty |
|
573 then result |
|
574 else mk_repabs lthy (rty, qty) result |
|
575 end |
|
576 | _ => |
|
577 (* FIXME / TODO: this is a case that needs to be looked at *) |
|
578 (* - variables get a rep-abs insde and outside an application *) |
|
579 (* - constants only get a rep-abs on the outside of the application *) |
|
580 (* - applications get a rep-abs insde and outside an application *) |
|
581 let |
|
582 val (rhead, rargs) = strip_comb rtrm |
|
583 val (qhead, qargs) = strip_comb qtrm |
|
584 val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) |
|
585 in |
|
586 if rty = qty |
|
587 then |
|
588 case (rhead, qhead) of |
|
589 (Free (_, T), Free (_, T')) => |
|
590 if T = T' then list_comb (rhead, rargs') |
|
591 else list_comb (mk_repabs lthy (T, T') rhead, rargs') |
|
592 | _ => list_comb (rhead, rargs') |
|
593 else |
|
594 case (rhead, qhead, length rargs') of |
|
595 (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead |
|
596 | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead |
|
597 | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) |
|
598 | (Free (x, T), Free (x', T'), _) => |
|
599 mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) |
|
600 | (Abs _, Abs _, _ ) => |
|
601 mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) |
|
602 | _ => raise (LIFT_MATCH "injection") |
|
603 end |
|
604 end |
|
605 *} |
|
606 |
|
607 section {* Genralisation of free variables in a goal *} |
|
608 |
|
609 ML {* |
|
610 fun inst_spec ctrm = |
|
611 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
|
612 |
|
613 fun inst_spec_tac ctrms = |
|
614 EVERY' (map (dtac o inst_spec) ctrms) |
|
615 |
|
616 fun all_list xs trm = |
|
617 fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm |
|
618 |
|
619 fun apply_under_Trueprop f = |
|
620 HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop |
|
621 |
|
622 fun gen_frees_tac ctxt = |
|
623 SUBGOAL (fn (concl, i) => |
|
624 let |
|
625 val thy = ProofContext.theory_of ctxt |
|
626 val vrs = Term.add_frees concl [] |
|
627 val cvrs = map (cterm_of thy o Free) vrs |
|
628 val concl' = apply_under_Trueprop (all_list vrs) concl |
|
629 val goal = Logic.mk_implies (concl', concl) |
|
630 val rule = Goal.prove ctxt [] [] goal |
|
631 (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) |
|
632 in |
|
633 rtac rule i |
|
634 end) |
|
635 *} |
|
636 |
|
637 section {* General outline of the lifting procedure *} |
|
638 |
|
639 (* - A is the original raw theorem *) |
|
640 (* - B is the regularized theorem *) |
|
641 (* - C is the rep/abs injected version of B *) |
|
642 (* - D is the lifted theorem *) |
|
643 (* *) |
|
644 (* - b is the regularization step *) |
|
645 (* - c is the rep/abs injection step *) |
|
646 (* - d is the cleaning part *) |
|
647 |
|
648 lemma lifting_procedure: |
|
649 assumes a: "A" |
|
650 and b: "A \<Longrightarrow> B" |
|
651 and c: "B = C" |
|
652 and d: "C = D" |
|
653 shows "D" |
|
654 using a b c d |
|
655 by simp |
|
656 |
|
657 ML {* |
|
658 fun lift_match_error ctxt fun_str rtrm qtrm = |
|
659 let |
|
660 val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
661 val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
662 val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, |
|
663 "and the lifted theorem\n", rtrm_str, "do not match"] |
|
664 in |
|
665 error (space_implode " " msg) |
|
666 end |
|
667 *} |
|
668 |
|
669 ML {* |
|
670 fun procedure_inst ctxt rtrm qtrm = |
|
671 let |
|
672 val thy = ProofContext.theory_of ctxt |
|
673 val rtrm' = HOLogic.dest_Trueprop rtrm |
|
674 val qtrm' = HOLogic.dest_Trueprop qtrm |
|
675 val reg_goal = |
|
676 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
|
677 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
|
678 val inj_goal = |
|
679 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
|
680 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
|
681 in |
|
682 Drule.instantiate' [] |
|
683 [SOME (cterm_of thy rtrm'), |
|
684 SOME (cterm_of thy reg_goal), |
|
685 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |
|
686 end |
|
687 *} |
|
688 |
|
689 (* Left for debugging *) |
|
690 ML {* |
|
691 fun procedure_tac lthy rthm = |
|
692 ObjectLogic.full_atomize_tac |
|
693 THEN' gen_frees_tac lthy |
|
694 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
|
695 let |
|
696 val rthm' = atomize_thm rthm |
|
697 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
|
698 in |
|
699 EVERY1 [rtac rule, rtac rthm'] |
|
700 end) lthy |
|
701 *} |
|
702 |
|
703 ML {* |
|
704 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
|
705 fun lift_tac lthy rthm rel_eqv rty quot defs = |
|
706 ObjectLogic.full_atomize_tac |
|
707 THEN' gen_frees_tac lthy |
|
708 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
|
709 let |
|
710 val rthm' = atomize_thm rthm |
|
711 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
|
712 val aps = find_aps (prop_of rthm') (term_of concl) |
|
713 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv |
|
714 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv |
|
715 in |
|
716 EVERY1 |
|
717 [rtac rule, rtac rthm'] |
|
718 end) lthy |
|
719 *} |
|
720 |
|
721 end |
|
722 |
|
723 |
|