457 val _ $ (Abs (_, _, g)) = t; |
457 val _ $ (Abs (_, _, g)) = t; |
458 in |
458 in |
459 (f, Abs ("x", T, mk_abs u 0 g)) |
459 (f, Abs ("x", T, mk_abs u 0 g)) |
460 end |
460 end |
461 |
461 |
462 (* Simplifies a redex using the 'lambda_prs' theorem. *) |
462 (* Simplifies a redex using the 'lambda_prs' theorem. |
463 (* First instantiates the types and known subterms. *) |
463 First instantiates the types and known subterms. |
464 (* Then solves the quotient assumptions to get Rep2 and Abs1 *) |
464 Then solves the quotient assumptions to get Rep2 and Abs1 |
465 (* Finally instantiates the function f using make_inst *) |
465 Finally instantiates the function f using make_inst |
466 (* If Rep2 is an identity then the pattern is simpler and *) |
466 If Rep2 is an identity then the pattern is simpler and |
467 (* make_inst_id is used *) |
467 make_inst_id is used *) |
468 fun lambda_prs_simple_conv ctxt ctrm = |
468 fun lambda_prs_simple_conv ctxt ctrm = |
469 case (term_of ctrm) of |
469 case (term_of ctrm) of |
470 (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => |
470 (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => |
471 (let |
471 let |
472 val thy = ProofContext.theory_of ctxt |
472 val thy = ProofContext.theory_of ctxt |
473 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
473 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
474 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
474 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
475 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
475 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
476 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
476 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
477 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} |
477 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]} |
478 val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi) |
478 val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi) |
479 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
479 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
480 val (insp, inst) = |
480 val (insp, inst) = |
481 if ty_c = ty_d |
481 if ty_c = ty_d |
482 then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm) |
482 then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm) |
483 else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
483 else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
484 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
484 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
485 in |
485 in |
486 Conv.rewr_conv ti ctrm |
486 Conv.rewr_conv ti ctrm |
487 end |
487 end |
488 handle _ => Conv.all_conv ctrm) (* TODO: another catch all - can this be improved? *) |
|
489 | _ => Conv.all_conv ctrm |
488 | _ => Conv.all_conv ctrm |
490 |
|
491 |
489 |
492 fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt |
490 fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt |
493 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
491 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
494 |
492 |
495 |
493 |