978 | Bound j => if i = j then error "make_inst" else t |
978 | Bound j => if i = j then error "make_inst" else t |
979 | _ => t); |
979 | _ => t); |
980 in (f, Abs ("x", T, mk_abs 0 g)) end; |
980 in (f, Abs ("x", T, mk_abs 0 g)) end; |
981 *} |
981 *} |
982 |
982 |
|
983 (* Since the patterns for the lhs are different; there are 2 different make-insts *) |
|
984 ML {* |
|
985 fun make_inst2 lhs t = |
|
986 let |
|
987 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
|
988 val _ = tracing "a"; |
|
989 val _ $ (Abs (_, _, (_ $ g))) = t; |
|
990 fun mk_abs i t = |
|
991 if incr_boundvars i u aconv t then Bound i |
|
992 else (case t of |
|
993 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
|
994 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
|
995 | Bound j => if i = j then error "make_inst" else t |
|
996 | _ => t); |
|
997 in (f, Abs ("x", T, mk_abs 0 g)) end; |
|
998 *} |
|
999 |
983 ML {* |
1000 ML {* |
984 fun lambda_prs_simple_conv ctxt ctrm = |
1001 fun lambda_prs_simple_conv ctxt ctrm = |
985 case (term_of ctrm) of |
1002 case (term_of ctrm) of |
986 ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) => |
1003 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
987 let |
1004 let |
988 val thy = ProofContext.theory_of ctxt |
1005 val thy = ProofContext.theory_of ctxt |
989 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
1006 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
990 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
1007 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
991 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1008 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
992 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1009 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
993 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
1010 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
994 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1011 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
995 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
|
996 val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
1012 val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
997 val tl = Thm.lhs_of ts |
1013 val ti = |
998 val (insp, inst) = make_inst (term_of tl) (term_of ctrm) |
1014 (let |
999 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1015 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1000 val _ = if not (s = @{const_name "id"}) then |
1016 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
|
1017 in |
|
1018 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
|
1019 end handle Bind => |
|
1020 let |
|
1021 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
|
1022 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
|
1023 in |
|
1024 MetaSimplifier.rewrite_rule @{thms id_simps} td |
|
1025 end); |
|
1026 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
1001 (tracing "lambda_prs"; |
1027 (tracing "lambda_prs"; |
1002 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
1028 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
1003 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
1029 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
1004 tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
1030 tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
1005 tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts))); |
1031 tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) |
1006 tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) |
|
1007 else () |
1032 else () |
1008 in |
1033 in |
1009 Conv.rewr_conv ti ctrm |
1034 Conv.rewr_conv ti ctrm |
1010 end |
1035 end |
1011 | _ => Conv.all_conv ctrm |
1036 | _ => Conv.all_conv ctrm |