equal
deleted
inserted
replaced
998 |
998 |
999 ML {* |
999 ML {* |
1000 fun lambda_prs_simple_conv ctxt ctrm = |
1000 fun lambda_prs_simple_conv ctxt ctrm = |
1001 case (term_of ctrm) of |
1001 case (term_of ctrm) of |
1002 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1002 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1003 let |
1003 (let |
1004 val thy = ProofContext.theory_of ctxt |
1004 val thy = ProofContext.theory_of ctxt |
1005 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
1005 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
1006 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
1006 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
1007 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1007 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1008 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1008 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1013 (let |
1013 (let |
1014 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1014 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1015 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1015 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1016 in |
1016 in |
1017 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1017 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1018 end handle Bind => |
1018 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
1019 let |
1019 let |
1020 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1020 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1021 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
1021 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
1022 in |
1022 in |
1023 MetaSimplifier.rewrite_rule @{thms id_simps} td |
1023 MetaSimplifier.rewrite_rule @{thms id_simps} td |
1030 tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) |
1030 tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) |
1031 else () |
1031 else () |
1032 in |
1032 in |
1033 Conv.rewr_conv ti ctrm |
1033 Conv.rewr_conv ti ctrm |
1034 end |
1034 end |
|
1035 handle _ => Conv.all_conv ctrm) |
1035 | _ => Conv.all_conv ctrm |
1036 | _ => Conv.all_conv ctrm |
1036 *} |
1037 *} |
1037 |
1038 |
1038 ML {* |
1039 ML {* |
1039 val lambda_prs_conv = |
1040 val lambda_prs_conv = |