1081 *} |
1081 *} |
1082 |
1082 |
1083 ML {* |
1083 ML {* |
1084 fun lambda_prs_simple_conv ctxt ctrm = |
1084 fun lambda_prs_simple_conv ctxt ctrm = |
1085 case (term_of ctrm) of |
1085 case (term_of ctrm) of |
1086 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1086 ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) => |
1087 let |
1087 let |
1088 val thy = ProofContext.theory_of ctxt |
1088 val thy = ProofContext.theory_of ctxt |
1089 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
1089 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
1090 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
1090 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
1091 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1091 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1094 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1094 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1095 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1095 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1096 val tl = Thm.lhs_of ts |
1096 val tl = Thm.lhs_of ts |
1097 val (insp, inst) = make_inst (term_of tl) (term_of ctrm) |
1097 val (insp, inst) = make_inst (term_of tl) (term_of ctrm) |
1098 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1098 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1099 (*val _ = tracing "lambda_prs" |
1099 val _ = if not (s = @{const_name "id"}) then |
1100 val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))) |
1100 (tracing "lambda_prs"; |
1101 val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*) |
1101 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
|
1102 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
|
1103 tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
|
1104 tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts))); |
|
1105 tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) |
|
1106 else () |
1102 in |
1107 in |
1103 Conv.rewr_conv ti ctrm |
1108 Conv.rewr_conv ti ctrm |
1104 end |
1109 end |
1105 | _ => Conv.all_conv ctrm |
1110 | _ => Conv.all_conv ctrm |
1106 *} |
1111 *} |