158 then show "A = B" using * by auto |
155 then show "A = B" using * by auto |
159 qed |
156 qed |
160 then show "A \<equiv> B" by (rule eq_reflection) |
157 then show "A \<equiv> B" by (rule eq_reflection) |
161 qed |
158 qed |
162 |
159 |
163 ML {* |
|
164 fun atomize_thm thm = |
|
165 let |
|
166 val thm' = Thm.freezeT (forall_intr_vars thm) |
|
167 val thm'' = ObjectLogic.atomize (cprop_of thm') |
|
168 in |
|
169 @{thm equal_elim_rule1} OF [thm'', thm'] |
|
170 end |
|
171 *} |
|
172 |
|
173 section {* Infrastructure about id *} |
160 section {* Infrastructure about id *} |
174 |
161 |
175 lemmas [id_simps] = |
162 lemmas [id_simps] = |
176 fun_map_id[THEN eq_reflection] |
163 fun_map_id[THEN eq_reflection] |
177 id_apply[THEN eq_reflection] |
164 id_apply[THEN eq_reflection] |
178 id_def[THEN eq_reflection,symmetric] |
165 id_def[THEN eq_reflection,symmetric] |
179 |
|
180 section {* Computation of the Regularize Goal *} |
|
181 |
|
182 (* |
|
183 Regularizing an rtrm means: |
|
184 - quantifiers over a type that needs lifting are replaced by |
|
185 bounded quantifiers, for example: |
|
186 \<forall>x. P \<Longrightarrow> \<forall>x \<in> (Respects R). P / All (Respects R) P |
|
187 |
|
188 the relation R is given by the rty and qty; |
|
189 |
|
190 - abstractions over a type that needs lifting are replaced |
|
191 by bounded abstractions: |
|
192 \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P) |
|
193 |
|
194 - equalities over the type being lifted are replaced by |
|
195 corresponding relations: |
|
196 A = B \<Longrightarrow> A \<approx> B |
|
197 |
|
198 example with more complicated types of A, B: |
|
199 A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A B |
|
200 *) |
|
201 |
|
202 ML {* |
|
203 (* builds the relation that is the argument of respects *) |
|
204 fun mk_resp_arg lthy (rty, qty) = |
|
205 let |
|
206 val thy = ProofContext.theory_of lthy |
|
207 in |
|
208 if rty = qty |
|
209 then HOLogic.eq_const rty |
|
210 else |
|
211 case (rty, qty) of |
|
212 (Type (s, tys), Type (s', tys')) => |
|
213 if s = s' |
|
214 then let |
|
215 val SOME map_info = maps_lookup thy s |
|
216 val args = map (mk_resp_arg lthy) (tys ~~ tys') |
|
217 in |
|
218 list_comb (Const (#relfun map_info, dummyT), args) |
|
219 end |
|
220 else let |
|
221 val SOME qinfo = quotdata_lookup_thy thy s' |
|
222 (* FIXME: check in this case that the rty and qty *) |
|
223 (* FIXME: correspond to each other *) |
|
224 val (s, _) = dest_Const (#rel qinfo) |
|
225 (* FIXME: the relation should only be the string *) |
|
226 (* FIXME: and the type needs to be calculated as below; *) |
|
227 (* FIXME: maybe one should actually have a term *) |
|
228 (* FIXME: and one needs to force it to have this type *) |
|
229 in |
|
230 Const (s, rty --> rty --> @{typ bool}) |
|
231 end |
|
232 | _ => HOLogic.eq_const dummyT |
|
233 (* FIXME: check that the types correspond to each other? *) |
|
234 end |
|
235 *} |
|
236 |
|
237 ML {* |
|
238 val mk_babs = Const (@{const_name Babs}, dummyT) |
|
239 val mk_ball = Const (@{const_name Ball}, dummyT) |
|
240 val mk_bex = Const (@{const_name Bex}, dummyT) |
|
241 val mk_resp = Const (@{const_name Respects}, dummyT) |
|
242 *} |
|
243 |
|
244 ML {* |
|
245 (* - applies f to the subterm of an abstraction, *) |
|
246 (* otherwise to the given term, *) |
|
247 (* - used by regularize, therefore abstracted *) |
|
248 (* variables do not have to be treated specially *) |
|
249 |
|
250 fun apply_subt f trm1 trm2 = |
|
251 case (trm1, trm2) of |
|
252 (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t') |
|
253 | _ => f trm1 trm2 |
|
254 |
|
255 (* the major type of All and Ex quantifiers *) |
|
256 fun qnt_typ ty = domain_type (domain_type ty) |
|
257 *} |
|
258 |
|
259 ML {* |
|
260 (* produces a regularized version of rtrm *) |
|
261 (* - the result is contains dummyT *) |
|
262 (* - does not need any special treatment of *) |
|
263 (* bound variables *) |
|
264 |
|
265 fun regularize_trm lthy rtrm qtrm = |
|
266 case (rtrm, qtrm) of |
|
267 (Abs (x, ty, t), Abs (x', ty', t')) => |
|
268 let |
|
269 val subtrm = Abs(x, ty, regularize_trm lthy t t') |
|
270 in |
|
271 if ty = ty' then subtrm |
|
272 else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm |
|
273 end |
|
274 |
|
275 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
|
276 let |
|
277 val subtrm = apply_subt (regularize_trm lthy) t t' |
|
278 in |
|
279 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
|
280 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
281 end |
|
282 |
|
283 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
|
284 let |
|
285 val subtrm = apply_subt (regularize_trm lthy) t t' |
|
286 in |
|
287 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
|
288 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
289 end |
|
290 |
|
291 | (* equalities need to be replaced by appropriate equivalence relations *) |
|
292 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
|
293 if ty = ty' then rtrm |
|
294 else mk_resp_arg lthy (domain_type ty, domain_type ty') |
|
295 |
|
296 | (* in this case we check whether the given equivalence relation is correct *) |
|
297 (rel, Const (@{const_name "op ="}, ty')) => |
|
298 let |
|
299 val exc = LIFT_MATCH "regularise (relation mismatch)" |
|
300 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
|
301 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
|
302 in |
|
303 if rel' = rel then rtrm else raise exc |
|
304 end |
|
305 |
|
306 | (_, Const _) => |
|
307 let |
|
308 fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*) |
|
309 | same_name _ _ = false |
|
310 (* TODO/FIXME: This test is not enough. *) |
|
311 (* Why? *) |
|
312 (* Because constants can have the same name but not be the same |
|
313 constant. All overloaded constants have the same name but because |
|
314 of different types they do differ. |
|
315 |
|
316 This code will let one write a theorem where plus on nat is |
|
317 matched to plus on int, even if the latter is defined differently. |
|
318 |
|
319 This would result in hard to understand failures in injection and |
|
320 cleaning. *) |
|
321 (* cu: if I also test the type, then something else breaks *) |
|
322 in |
|
323 if same_name rtrm qtrm then rtrm |
|
324 else |
|
325 let |
|
326 val thy = ProofContext.theory_of lthy |
|
327 val qtrm_str = Syntax.string_of_term lthy qtrm |
|
328 val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") |
|
329 val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") |
|
330 val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 |
|
331 in |
|
332 if Pattern.matches thy (rtrm', rtrm) |
|
333 then rtrm else raise exc2 |
|
334 end |
|
335 end |
|
336 |
|
337 | (t1 $ t2, t1' $ t2') => |
|
338 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
|
339 |
|
340 | (Free (x, ty), Free (x', ty')) => |
|
341 (* this case cannot arrise as we start with two fully atomized terms *) |
|
342 raise (LIFT_MATCH "regularize (frees)") |
|
343 |
|
344 | (Bound i, Bound i') => |
|
345 if i = i' then rtrm |
|
346 else raise (LIFT_MATCH "regularize (bounds mismatch)") |
|
347 |
|
348 | _ => |
|
349 let |
|
350 val rtrm_str = Syntax.string_of_term lthy rtrm |
|
351 val qtrm_str = Syntax.string_of_term lthy qtrm |
|
352 in |
|
353 raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) |
|
354 end |
|
355 *} |
|
356 |
|
357 section {* Regularize Tactic *} |
|
358 |
|
359 ML {* |
|
360 fun equiv_tac ctxt = |
|
361 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
|
362 |
|
363 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
|
364 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
|
365 *} |
|
366 |
|
367 ML {* |
|
368 fun prep_trm thy (x, (T, t)) = |
|
369 (cterm_of thy (Var (x, T)), cterm_of thy t) |
|
370 |
|
371 fun prep_ty thy (x, (S, ty)) = |
|
372 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
|
373 *} |
|
374 |
|
375 ML {* |
|
376 fun matching_prs thy pat trm = |
|
377 let |
|
378 val univ = Unify.matchers thy [(pat, trm)] |
|
379 val SOME (env, _) = Seq.pull univ |
|
380 val tenv = Vartab.dest (Envir.term_env env) |
|
381 val tyenv = Vartab.dest (Envir.type_env env) |
|
382 in |
|
383 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
|
384 end |
|
385 *} |
|
386 |
|
387 ML {* |
|
388 fun calculate_instance ctxt thm redex R1 R2 = |
|
389 let |
|
390 val thy = ProofContext.theory_of ctxt |
|
391 val goal = Const (@{const_name "equivp"}, dummyT) $ R2 |
|
392 |> Syntax.check_term ctxt |
|
393 |> HOLogic.mk_Trueprop |
|
394 val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1) |
|
395 val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) |
|
396 val R1c = cterm_of thy R1 |
|
397 val thmi = Drule.instantiate' [] [SOME R1c] thm |
|
398 val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex |
|
399 val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) |
|
400 in |
|
401 SOME thm2 |
|
402 end |
|
403 handle _ => NONE |
|
404 (* FIXME/TODO: what is the place where the exception is raised: matching_prs? *) |
|
405 *} |
|
406 |
|
407 ML {* |
|
408 fun ball_bex_range_simproc ss redex = |
|
409 let |
|
410 val ctxt = Simplifier.the_context ss |
|
411 in |
|
412 case redex of |
|
413 (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ |
|
414 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
|
415 calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 |
|
416 |
|
417 | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ |
|
418 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
|
419 calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 |
|
420 | _ => NONE |
|
421 end |
|
422 *} |
|
423 |
|
424 lemma eq_imp_rel: |
|
425 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
|
426 by (simp add: equivp_reflp) |
|
427 |
|
428 ML {* |
|
429 (* test whether DETERM makes any difference *) |
|
430 fun quotient_tac ctxt = SOLVES' |
|
431 (REPEAT_ALL_NEW (FIRST' |
|
432 [rtac @{thm identity_quotient}, |
|
433 resolve_tac (quotient_rules_get ctxt)])) |
|
434 |
|
435 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
|
436 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
|
437 *} |
|
438 |
|
439 ML {* |
|
440 fun solve_quotient_assum ctxt thm = |
|
441 case Seq.pull (quotient_tac ctxt 1 thm) of |
|
442 SOME (t, _) => t |
|
443 | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing" |
|
444 *} |
|
445 |
|
446 |
|
447 (* 0. preliminary simplification step according to *) |
|
448 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv |
|
449 ball_reg_eqv_range bex_reg_eqv_range |
|
450 (* 1. eliminating simple Ball/Bex instances*) |
|
451 thm ball_reg_right bex_reg_left |
|
452 (* 2. monos *) |
|
453 (* 3. commutation rules for ball and bex *) |
|
454 thm ball_all_comm bex_ex_comm |
|
455 (* 4. then rel-equality (which need to be instantiated to avoid loops) *) |
|
456 thm eq_imp_rel |
|
457 (* 5. then simplification like 0 *) |
|
458 (* finally jump back to 1 *) |
|
459 |
|
460 ML {* |
|
461 fun regularize_tac ctxt = |
|
462 let |
|
463 val thy = ProofContext.theory_of ctxt |
|
464 val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} |
|
465 val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} |
|
466 val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) |
|
467 val simpset = (mk_minimal_ss ctxt) |
|
468 addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} |
|
469 addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver |
|
470 val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) |
|
471 in |
|
472 simp_tac simpset THEN' |
|
473 REPEAT_ALL_NEW (CHANGED o FIRST' [ |
|
474 resolve_tac @{thms ball_reg_right bex_reg_left}, |
|
475 resolve_tac (Inductive.get_monos ctxt), |
|
476 resolve_tac @{thms ball_all_comm bex_ex_comm}, |
|
477 resolve_tac eq_eqvs, |
|
478 simp_tac simpset]) |
|
479 end |
|
480 *} |
|
481 |
|
482 section {* Calculation of the Injected Goal *} |
|
483 |
|
484 (* |
|
485 Injecting repabs means: |
|
486 |
|
487 For abstractions: |
|
488 * If the type of the abstraction doesn't need lifting we recurse. |
|
489 * If it does we add RepAbs around the whole term and check if the |
|
490 variable needs lifting. |
|
491 * If it doesn't then we recurse |
|
492 * If it does we recurse and put 'RepAbs' around all occurences |
|
493 of the variable in the obtained subterm. This in combination |
|
494 with the RepAbs above will let us change the type of the |
|
495 abstraction with rewriting. |
|
496 For applications: |
|
497 * If the term is 'Respects' applied to anything we leave it unchanged |
|
498 * If the term needs lifting and the head is a constant that we know |
|
499 how to lift, we put a RepAbs and recurse |
|
500 * If the term needs lifting and the head is a free applied to subterms |
|
501 (if it is not applied we treated it in Abs branch) then we |
|
502 put RepAbs and recurse |
|
503 * Otherwise just recurse. |
|
504 *) |
|
505 |
|
506 ML {* |
|
507 fun mk_repabs lthy (T, T') trm = |
|
508 Quotient_Def.get_fun repF lthy (T, T') |
|
509 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
|
510 *} |
|
511 |
|
512 ML {* |
|
513 (* bound variables need to be treated properly, *) |
|
514 (* as the type of subterms need to be calculated *) |
|
515 (* in the abstraction case *) |
|
516 |
|
517 fun inj_repabs_trm lthy (rtrm, qtrm) = |
|
518 case (rtrm, qtrm) of |
|
519 (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
|
520 Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
|
521 |
|
522 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
|
523 Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) |
|
524 |
|
525 | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => |
|
526 let |
|
527 val rty = fastype_of rtrm |
|
528 val qty = fastype_of qtrm |
|
529 in |
|
530 mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))) |
|
531 end |
|
532 |
|
533 | (Abs (x, T, t), Abs (x', T', t')) => |
|
534 let |
|
535 val rty = fastype_of rtrm |
|
536 val qty = fastype_of qtrm |
|
537 val (y, s) = Term.dest_abs (x, T, t) |
|
538 val (_, s') = Term.dest_abs (x', T', t') |
|
539 val yvar = Free (y, T) |
|
540 val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) |
|
541 in |
|
542 if rty = qty then result |
|
543 else mk_repabs lthy (rty, qty) result |
|
544 end |
|
545 |
|
546 | (t $ s, t' $ s') => |
|
547 (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s')) |
|
548 |
|
549 | (Free (_, T), Free (_, T')) => |
|
550 if T = T' then rtrm |
|
551 else mk_repabs lthy (T, T') rtrm |
|
552 |
|
553 | (_, Const (@{const_name "op ="}, _)) => rtrm |
|
554 |
|
555 | (_, Const (_, T')) => |
|
556 let |
|
557 val rty = fastype_of rtrm |
|
558 in |
|
559 if rty = T' then rtrm |
|
560 else mk_repabs lthy (rty, T') rtrm |
|
561 end |
|
562 |
|
563 | _ => raise (LIFT_MATCH "injection") |
|
564 *} |
|
565 |
|
566 section {* Injection Tactic *} |
|
567 |
|
568 definition |
|
569 "QUOT_TRUE x \<equiv> True" |
|
570 |
|
571 ML {* |
|
572 (* looks for QUOT_TRUE assumtions, and in case its argument *) |
|
573 (* is an application, it returns the function and the argument *) |
|
574 fun find_qt_asm asms = |
|
575 let |
|
576 fun find_fun trm = |
|
577 case trm of |
|
578 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
|
579 | _ => false |
|
580 in |
|
581 case find_first find_fun asms of |
|
582 SOME (_ $ (_ $ (f $ a))) => SOME (f, a) |
|
583 | _ => NONE |
|
584 end |
|
585 *} |
|
586 |
|
587 text {* |
|
588 To prove that the regularised theorem implies the abs/rep injected, |
|
589 we try: |
|
590 |
|
591 1) theorems 'trans2' from the appropriate QUOT_TYPE |
|
592 2) remove lambdas from both sides: lambda_rsp_tac |
|
593 3) remove Ball/Bex from the right hand side |
|
594 4) use user-supplied RSP theorems |
|
595 5) remove rep_abs from the right side |
|
596 6) reflexivity of equality |
|
597 7) split applications of lifted type (apply_rsp) |
|
598 8) split applications of non-lifted type (cong_tac) |
|
599 9) apply extentionality |
|
600 A) reflexivity of the relation |
|
601 B) assumption |
|
602 (Lambdas under respects may have left us some assumptions) |
|
603 C) proving obvious higher order equalities by simplifying fun_rel |
|
604 (not sure if it is still needed?) |
|
605 D) unfolding lambda on one side |
|
606 E) simplifying (= ===> =) for simpler respectfulness |
|
607 *} |
|
608 |
|
609 lemma quot_true_dests: |
|
610 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
|
611 and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
|
612 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
|
613 and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
|
614 by (simp_all add: QUOT_TRUE_def ext) |
|
615 |
|
616 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
|
617 by (simp add: QUOT_TRUE_def) |
|
618 |
|
619 lemma regularize_to_injection: "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y" |
|
620 by(auto simp add: QUOT_TRUE_def) |
|
621 |
|
622 ML {* |
|
623 fun quot_true_simple_conv ctxt fnctn ctrm = |
|
624 case (term_of ctrm) of |
|
625 (Const (@{const_name QUOT_TRUE}, _) $ x) => |
|
626 let |
|
627 val fx = fnctn x; |
|
628 val thy = ProofContext.theory_of ctxt; |
|
629 val cx = cterm_of thy x; |
|
630 val cfx = cterm_of thy fx; |
|
631 val cxt = ctyp_of thy (fastype_of x); |
|
632 val cfxt = ctyp_of thy (fastype_of fx); |
|
633 val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} |
|
634 in |
|
635 Conv.rewr_conv thm ctrm |
|
636 end |
|
637 *} |
|
638 |
|
639 ML {* |
|
640 fun quot_true_conv ctxt fnctn ctrm = |
|
641 case (term_of ctrm) of |
|
642 (Const (@{const_name QUOT_TRUE}, _) $ _) => |
|
643 quot_true_simple_conv ctxt fnctn ctrm |
|
644 | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm |
|
645 | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm |
|
646 | _ => Conv.all_conv ctrm |
|
647 *} |
|
648 |
|
649 ML {* |
|
650 fun quot_true_tac ctxt fnctn = |
|
651 CONVERSION |
|
652 ((Conv.params_conv ~1 (fn ctxt => |
|
653 (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) |
|
654 *} |
|
655 |
|
656 ML {* fun dest_comb (f $ a) = (f, a) *} |
|
657 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} |
|
658 (* TODO: Can this be done easier? *) |
|
659 ML {* |
|
660 fun unlam t = |
|
661 case t of |
|
662 (Abs a) => snd (Term.dest_abs a) |
|
663 | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) |
|
664 *} |
|
665 |
|
666 ML {* |
|
667 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
|
668 | dest_fun_type _ = error "dest_fun_type" |
|
669 *} |
|
670 |
|
671 ML {* |
|
672 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
|
673 *} |
|
674 |
|
675 ML {* |
|
676 (* we apply apply_rsp only in case if the type needs lifting, *) |
|
677 (* which is the case if the type of the data in the QUOT_TRUE *) |
|
678 (* assumption is different from the corresponding type in the goal *) |
|
679 val apply_rsp_tac = |
|
680 Subgoal.FOCUS (fn {concl, asms, context,...} => |
|
681 let |
|
682 val bare_concl = HOLogic.dest_Trueprop (term_of concl) |
|
683 val qt_asm = find_qt_asm (map term_of asms) |
|
684 in |
|
685 case (bare_concl, qt_asm) of |
|
686 (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => |
|
687 if (fastype_of qt_fun) = (fastype_of f) |
|
688 then no_tac |
|
689 else |
|
690 let |
|
691 val ty_x = fastype_of x |
|
692 val ty_b = fastype_of qt_arg |
|
693 val ty_f = range_type (fastype_of f) |
|
694 val thy = ProofContext.theory_of context |
|
695 val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] |
|
696 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
|
697 val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} |
|
698 in |
|
699 (rtac inst_thm THEN' quotient_tac context) 1 |
|
700 end |
|
701 | _ => no_tac |
|
702 end) |
|
703 *} |
|
704 |
|
705 thm equals_rsp |
|
706 |
|
707 ML {* |
|
708 fun equals_rsp_tac R ctxt = |
|
709 let |
|
710 val ty = domain_type (fastype_of R); |
|
711 val thy = ProofContext.theory_of ctxt |
|
712 val thm = Drule.instantiate' |
|
713 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} |
|
714 in |
|
715 rtac thm THEN' quotient_tac ctxt |
|
716 end |
|
717 (* raised by instantiate' *) |
|
718 handle THM _ => K no_tac |
|
719 | TYPE _ => K no_tac |
|
720 | TERM _ => K no_tac |
|
721 *} |
|
722 |
|
723 ML {* |
|
724 fun rep_abs_rsp_tac ctxt = |
|
725 SUBGOAL (fn (goal, i) => |
|
726 case (bare_concl goal) of |
|
727 (rel $ _ $ (rep $ (abs $ _))) => |
|
728 (let |
|
729 val thy = ProofContext.theory_of ctxt; |
|
730 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
|
731 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
|
732 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
|
733 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
|
734 in |
|
735 (rtac inst_thm THEN' quotient_tac ctxt) i |
|
736 end |
|
737 handle THM _ => no_tac | TYPE _ => no_tac) |
|
738 | _ => no_tac) |
|
739 *} |
|
740 |
|
741 ML {* |
|
742 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
|
743 (case (bare_concl goal) of |
|
744 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
|
745 (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) |
|
746 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
747 |
|
748 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
749 | (Const (@{const_name "op ="},_) $ |
|
750 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
751 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
|
752 => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} |
|
753 |
|
754 (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *) |
|
755 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
756 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
757 (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
758 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
759 |
|
760 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
761 | Const (@{const_name "op ="},_) $ |
|
762 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
763 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
764 => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} |
|
765 |
|
766 (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *) |
|
767 | (Const (@{const_name fun_rel}, _) $ _ $ _) $ |
|
768 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
769 (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) |
|
770 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
|
771 |
|
772 | (_ $ |
|
773 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ |
|
774 (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) |
|
775 => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] |
|
776 |
|
777 | Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => |
|
778 (rtac @{thm refl} ORELSE' |
|
779 (equals_rsp_tac R ctxt THEN' RANGE [ |
|
780 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) |
|
781 |
|
782 (* reflexivity of operators arising from Cong_tac *) |
|
783 | Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl} |
|
784 |
|
785 (* respectfulness of constants; in particular of a simple relation *) |
|
786 | _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) |
|
787 => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt |
|
788 |
|
789 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
|
790 (* observe ---> *) |
|
791 | _ $ _ $ _ |
|
792 => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) |
|
793 ORELSE' rep_abs_rsp_tac ctxt |
|
794 |
|
795 | _ => K no_tac |
|
796 ) i) |
|
797 *} |
|
798 |
|
799 ML {* |
|
800 fun inj_repabs_step_tac ctxt rel_refl = |
|
801 (FIRST' [ |
|
802 inj_repabs_tac_match ctxt, |
|
803 (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *) |
|
804 |
|
805 apply_rsp_tac ctxt THEN' |
|
806 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
|
807 |
|
808 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
|
809 (* merge with previous tactic *) |
|
810 Cong_Tac.cong_tac @{thm cong} THEN' |
|
811 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
|
812 |
|
813 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
|
814 rtac @{thm ext} THEN' quot_true_tac ctxt unlam, |
|
815 |
|
816 (* resolving with R x y assumptions *) |
|
817 atac, |
|
818 |
|
819 (* reflexivity of the basic relations *) |
|
820 (* R \<dots> \<dots> *) |
|
821 resolve_tac rel_refl]) |
|
822 *} |
|
823 |
|
824 ML {* |
|
825 fun inj_repabs_tac ctxt = |
|
826 let |
|
827 val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) |
|
828 in |
|
829 inj_repabs_step_tac ctxt rel_refl |
|
830 end |
|
831 |
|
832 fun all_inj_repabs_tac ctxt = |
|
833 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
|
834 *} |
|
835 |
|
836 section {* Cleaning of the Theorem *} |
|
837 |
|
838 ML {* |
|
839 (* expands all fun_maps, except in front of bound variables *) |
|
840 |
|
841 fun fun_map_simple_conv xs ctxt ctrm = |
|
842 case (term_of ctrm) of |
|
843 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
|
844 if (member (op=) xs h) |
|
845 then Conv.all_conv ctrm |
|
846 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm |
|
847 | _ => Conv.all_conv ctrm |
|
848 |
|
849 fun fun_map_conv xs ctxt ctrm = |
|
850 case (term_of ctrm) of |
|
851 _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv |
|
852 fun_map_simple_conv xs ctxt) ctrm |
|
853 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
|
854 | _ => Conv.all_conv ctrm |
|
855 |
|
856 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
|
857 *} |
|
858 |
|
859 ML {* |
|
860 fun mk_abs u i t = |
|
861 if incr_boundvars i u aconv t then Bound i |
|
862 else (case t of |
|
863 t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) |
|
864 | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') |
|
865 | Bound j => if i = j then error "make_inst" else t |
|
866 | _ => t) |
|
867 |
|
868 fun make_inst lhs t = |
|
869 let |
|
870 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
|
871 val _ $ (Abs (_, _, (_ $ g))) = t; |
|
872 in |
|
873 (f, Abs ("x", T, mk_abs u 0 g)) |
|
874 end |
|
875 |
|
876 fun make_inst_id lhs t = |
|
877 let |
|
878 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
|
879 val _ $ (Abs (_, _, g)) = t; |
|
880 in |
|
881 (f, Abs ("x", T, mk_abs u 0 g)) |
|
882 end |
|
883 *} |
|
884 |
|
885 ML {* |
|
886 (* Simplifies a redex using the 'lambda_prs' theorem. *) |
|
887 (* First instantiates the types and known subterms. *) |
|
888 (* Then solves the quotient assumptions to get Rep2 and Abs1 *) |
|
889 (* Finally instantiates the function f using make_inst *) |
|
890 (* If Rep2 is identity then the pattern is simpler and make_inst_id is used *) |
|
891 fun lambda_prs_simple_conv ctxt ctrm = |
|
892 case (term_of ctrm) of |
|
893 (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => |
|
894 (let |
|
895 val thy = ProofContext.theory_of ctxt |
|
896 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
|
897 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
|
898 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
|
899 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
|
900 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
|
901 val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)] |
|
902 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
|
903 val make_inst = if ty_c = ty_d then make_inst_id else make_inst |
|
904 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
|
905 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
|
906 in |
|
907 Conv.rewr_conv ti ctrm |
|
908 end |
|
909 handle _ => Conv.all_conv ctrm) |
|
910 | _ => Conv.all_conv ctrm |
|
911 *} |
|
912 |
|
913 ML {* |
|
914 val lambda_prs_conv = |
|
915 More_Conv.top_conv lambda_prs_simple_conv |
|
916 |
|
917 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
|
918 *} |
|
919 |
|
920 (* 1. folding of definitions and preservation lemmas; *) |
|
921 (* and simplification with *) |
|
922 thm babs_prs all_prs ex_prs |
|
923 (* 2. unfolding of ---> in front of everything, except *) |
|
924 (* bound variables (this prevents lambda_prs from *) |
|
925 (* becoming stuck *) |
|
926 thm fun_map.simps |
|
927 (* 3. simplification with *) |
|
928 thm lambda_prs |
|
929 (* 4. simplification with *) |
|
930 thm Quotient_abs_rep Quotient_rel_rep id_simps |
|
931 (* 5. Test for refl *) |
|
932 |
|
933 ML {* |
|
934 fun clean_tac lthy = |
|
935 let |
|
936 val thy = ProofContext.theory_of lthy; |
|
937 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
|
938 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
|
939 |
|
940 val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} |
|
941 val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
|
942 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
|
943 in |
|
944 EVERY' [simp_tac (simps thms1), |
|
945 fun_map_tac lthy, |
|
946 lambda_prs_tac lthy, |
|
947 simp_tac (simps thms2), |
|
948 TRY o rtac refl] |
|
949 end |
|
950 *} |
|
951 |
|
952 section {* Tactic for Genralisation of Free Variables in a Goal *} |
|
953 |
|
954 ML {* |
|
955 fun inst_spec ctrm = |
|
956 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} |
|
957 |
|
958 fun inst_spec_tac ctrms = |
|
959 EVERY' (map (dtac o inst_spec) ctrms) |
|
960 |
|
961 fun all_list xs trm = |
|
962 fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm |
|
963 |
|
964 fun apply_under_Trueprop f = |
|
965 HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop |
|
966 |
|
967 fun gen_frees_tac ctxt = |
|
968 SUBGOAL (fn (concl, i) => |
|
969 let |
|
970 val thy = ProofContext.theory_of ctxt |
|
971 val vrs = Term.add_frees concl [] |
|
972 val cvrs = map (cterm_of thy o Free) vrs |
|
973 val concl' = apply_under_Trueprop (all_list vrs) concl |
|
974 val goal = Logic.mk_implies (concl', concl) |
|
975 val rule = Goal.prove ctxt [] [] goal |
|
976 (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) |
|
977 in |
|
978 rtac rule i |
|
979 end) |
|
980 *} |
|
981 |
|
982 section {* The General Shape of the Lifting Procedure *} |
|
983 |
|
984 (* - A is the original raw theorem *) |
|
985 (* - B is the regularized theorem *) |
|
986 (* - C is the rep/abs injected version of B *) |
|
987 (* - D is the lifted theorem *) |
|
988 (* *) |
|
989 (* - 1st prem is the regularization step *) |
|
990 (* - 2nd prem is the rep/abs injection step *) |
|
991 (* - 3rd prem is the cleaning part *) |
|
992 (* *) |
|
993 (* the QUOT_TRUE premise in 2 records the lifted theorem *) |
|
994 |
|
995 ML {* |
|
996 val lifting_procedure = |
|
997 @{lemma "\<lbrakk>A; |
|
998 A \<longrightarrow> B; |
|
999 QUOT_TRUE D \<Longrightarrow> B = C; |
|
1000 C = D\<rbrakk> \<Longrightarrow> D" |
|
1001 by (simp add: QUOT_TRUE_def)} |
|
1002 *} |
|
1003 |
|
1004 ML {* |
|
1005 fun lift_match_error ctxt fun_str rtrm qtrm = |
|
1006 let |
|
1007 val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
1008 val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
1009 val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, |
|
1010 "", "does not match with original theorem", rtrm_str] |
|
1011 in |
|
1012 error msg |
|
1013 end |
|
1014 *} |
|
1015 |
|
1016 ML {* |
|
1017 fun procedure_inst ctxt rtrm qtrm = |
|
1018 let |
|
1019 val thy = ProofContext.theory_of ctxt |
|
1020 val rtrm' = HOLogic.dest_Trueprop rtrm |
|
1021 val qtrm' = HOLogic.dest_Trueprop qtrm |
|
1022 val reg_goal = |
|
1023 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
|
1024 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
|
1025 val inj_goal = |
|
1026 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
|
1027 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
|
1028 in |
|
1029 Drule.instantiate' [] |
|
1030 [SOME (cterm_of thy rtrm'), |
|
1031 SOME (cterm_of thy reg_goal), |
|
1032 NONE, |
|
1033 SOME (cterm_of thy inj_goal)] lifting_procedure |
|
1034 end |
|
1035 *} |
|
1036 |
|
1037 ML {* |
|
1038 (* the tactic leaves three subgoals to be proved *) |
|
1039 fun procedure_tac ctxt rthm = |
|
1040 ObjectLogic.full_atomize_tac |
|
1041 THEN' gen_frees_tac ctxt |
|
1042 THEN' CSUBGOAL (fn (goal, i) => |
|
1043 let |
|
1044 val rthm' = atomize_thm rthm |
|
1045 val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) |
|
1046 in |
|
1047 (rtac rule THEN' rtac rthm') i |
|
1048 end) |
|
1049 *} |
|
1050 |
|
1051 section {* Automatic Proofs *} |
|
1052 |
|
1053 |
|
1054 ML {* |
|
1055 local |
|
1056 |
|
1057 val msg1 = "Regularize proof failed." |
|
1058 val msg2 = cat_lines ["Injection proof failed.", |
|
1059 "This is probably due to missing respects lemmas.", |
|
1060 "Try invoking the injection method manually to see", |
|
1061 "which lemmas are missing."] |
|
1062 val msg3 = "Cleaning proof failed." |
|
1063 |
|
1064 in |
|
1065 |
|
1066 fun lift_tac ctxt rthm = |
|
1067 procedure_tac ctxt rthm |
|
1068 THEN' RANGE_WARN |
|
1069 [(regularize_tac ctxt, msg1), |
|
1070 (all_inj_repabs_tac ctxt, msg2), |
|
1071 (clean_tac ctxt, msg3)] |
|
1072 |
|
1073 end |
|
1074 *} |
|
1075 |
166 |
1076 section {* Methods / Interface *} |
167 section {* Methods / Interface *} |
1077 |
168 |
1078 ML {* |
169 ML {* |
1079 fun mk_method1 tac thm ctxt = |
170 fun mk_method1 tac thm ctxt = |