975 | _ => t); |
975 | _ => t); |
976 in (f, Abs ("x", T, mk_abs 0 g)) end; |
976 in (f, Abs ("x", T, mk_abs 0 g)) end; |
977 *} |
977 *} |
978 |
978 |
979 ML {* |
979 ML {* |
980 fun make_inst3 lhs t = |
|
981 let |
|
982 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
|
983 val _ $ (Abs (_, _, (_ $ g))) = t; |
|
984 fun mk_abs i t = |
|
985 if incr_boundvars i u aconv t then Bound i |
|
986 else (case t of |
|
987 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
|
988 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
|
989 | Bound j => if i = j then error "make_inst" else t |
|
990 | _ => t); |
|
991 in (f, Abs ("x", T, mk_abs 0 g)) end; |
|
992 *} |
|
993 |
|
994 ML {* |
|
995 fun lambda_prs_simple_conv ctxt ctrm = |
980 fun lambda_prs_simple_conv ctxt ctrm = |
996 case (term_of ctrm) of |
981 case (term_of ctrm) of |
997 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
982 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
998 (let |
983 (let |
999 val thy = ProofContext.theory_of ctxt |
984 val thy = ProofContext.theory_of ctxt |
1017 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1002 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1018 in |
1003 in |
1019 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1004 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1020 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
1005 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
1021 let |
1006 let |
1022 val (insp, inst) = make_inst3 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1007 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1023 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
1008 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
1024 in |
1009 in |
1025 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
1010 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
1026 end); |
1011 end); |
1027 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
1012 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |