938 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
938 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
939 *} |
939 *} |
940 |
940 |
941 section {* Cleaning of the Theorem *} |
941 section {* Cleaning of the Theorem *} |
942 |
942 |
|
943 (* Since the patterns for the lhs are different; there are 3 different make-insts *) |
|
944 (* 1: does ? \<rightarrow> id *) |
|
945 (* 2: does id \<rightarrow> ? *) |
|
946 (* 3: does ? \<rightarrow> ? *) |
943 ML {* |
947 ML {* |
944 fun make_inst lhs t = |
948 fun make_inst lhs t = |
945 let |
949 let |
946 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
950 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
947 val _ $ (Abs (_, _, g)) = t; |
951 val _ $ (Abs (_, _, g)) = t; |
953 | Bound j => if i = j then error "make_inst" else t |
957 | Bound j => if i = j then error "make_inst" else t |
954 | _ => t); |
958 | _ => t); |
955 in (f, Abs ("x", T, mk_abs 0 g)) end; |
959 in (f, Abs ("x", T, mk_abs 0 g)) end; |
956 *} |
960 *} |
957 |
961 |
958 (* Since the patterns for the lhs are different; there are 2 different make-insts *) |
|
959 ML {* |
962 ML {* |
960 fun make_inst2 lhs t = |
963 fun make_inst2 lhs t = |
961 let |
964 let |
962 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
965 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
963 val _ = tracing "a"; |
966 val _ $ (Abs (_, _, (_ $ g))) = t; |
|
967 fun mk_abs i t = |
|
968 if incr_boundvars i u aconv t then Bound i |
|
969 else (case t of |
|
970 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
|
971 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
|
972 | Bound j => if i = j then error "make_inst" else t |
|
973 | _ => t); |
|
974 in (f, Abs ("x", T, mk_abs 0 g)) end; |
|
975 *} |
|
976 |
|
977 ML {* |
|
978 fun make_inst3 lhs t = |
|
979 let |
|
980 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
964 val _ $ (Abs (_, _, (_ $ g))) = t; |
981 val _ $ (Abs (_, _, (_ $ g))) = t; |
965 fun mk_abs i t = |
982 fun mk_abs i t = |
966 if incr_boundvars i u aconv t then Bound i |
983 if incr_boundvars i u aconv t then Bound i |
967 else (case t of |
984 else (case t of |
968 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
985 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
982 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
999 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
983 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1000 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
984 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1001 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
985 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
1002 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
986 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1003 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
987 val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
|
988 val ti = |
1004 val ti = |
989 (let |
1005 (let |
990 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
1006 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
991 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1007 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
992 in |
1008 in |
993 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1009 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
994 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
1010 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
995 let |
1011 let |
996 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1012 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
|
1013 val _ = tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts))); |
|
1014 val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
|
1015 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm) |
|
1016 in |
|
1017 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
|
1018 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
|
1019 let |
|
1020 val (insp, inst) = make_inst3 (term_of (Thm.lhs_of te)) (term_of ctrm) |
997 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 |
998 in |
1022 in |
999 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
1023 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
1000 end); |
1024 end); |
1001 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
1025 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
1003 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
1027 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
1004 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
1028 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
1005 tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
1029 tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
1006 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)))) |
1007 else () |
1031 else () |
|
1032 |
1008 in |
1033 in |
1009 Conv.rewr_conv ti ctrm |
1034 Conv.rewr_conv ti ctrm |
1010 end |
1035 end |
1011 handle _ => Conv.all_conv ctrm) |
1036 handle _ => Conv.all_conv ctrm) |
1012 | _ => Conv.all_conv ctrm |
1037 | _ => Conv.all_conv ctrm |