equal
deleted
inserted
replaced
1004 |
1004 |
1005 ML {* |
1005 ML {* |
1006 fun lambda_prs_simple_conv ctxt ctrm = |
1006 fun lambda_prs_simple_conv ctxt ctrm = |
1007 case (term_of ctrm) of |
1007 case (term_of ctrm) of |
1008 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1008 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1009 let |
1009 (let |
1010 val thy = ProofContext.theory_of ctxt |
1010 val thy = ProofContext.theory_of ctxt |
1011 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
1011 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
1012 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
1012 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
1013 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1013 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1014 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1014 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1019 (let |
1019 (let |
1020 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1020 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1021 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1021 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1022 in |
1022 in |
1023 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1023 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1024 end handle Bind => |
1024 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
1025 let |
1025 let |
1026 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1026 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1027 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
1027 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
1028 in |
1028 in |
1029 MetaSimplifier.rewrite_rule @{thms id_simps} td |
1029 MetaSimplifier.rewrite_rule @{thms id_simps} td |
1036 tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) |
1036 tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) |
1037 else () |
1037 else () |
1038 in |
1038 in |
1039 Conv.rewr_conv ti ctrm |
1039 Conv.rewr_conv ti ctrm |
1040 end |
1040 end |
|
1041 handle _ => Conv.all_conv ctrm) |
1041 | _ => Conv.all_conv ctrm |
1042 | _ => Conv.all_conv ctrm |
1042 *} |
1043 *} |
1043 |
1044 |
1044 ML {* |
1045 ML {* |
1045 val lambda_prs_conv = |
1046 val lambda_prs_conv = |