871 | Bound j => if i = j then error "make_inst" else t |
865 | Bound j => if i = j then error "make_inst" else t |
872 | _ => t) |
866 | _ => t) |
873 |
867 |
874 fun make_inst lhs t = |
868 fun make_inst lhs t = |
875 let |
869 let |
|
870 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
|
871 val _ $ (Abs (_, _, (_ $ g))) = t; |
|
872 in |
|
873 (f, Abs ("x", T, mk_abs u 0 g)) |
|
874 end |
|
875 |
|
876 fun make_inst_id lhs t = |
|
877 let |
876 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
878 val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; |
877 val _ $ (Abs (_, _, g)) = t; |
879 val _ $ (Abs (_, _, g)) = t; |
878 in |
880 in |
879 (f, Abs ("x", T, mk_abs u 0 g)) |
881 (f, Abs ("x", T, mk_abs u 0 g)) |
880 end |
882 end |
881 |
883 *} |
882 fun make_inst2 lhs t = |
884 |
883 let |
885 ML {* |
884 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
886 (* Simplifies a redex using the 'lambda_prs' theorem. *) |
885 val _ $ (Abs (_, _, (_ $ g))) = t; |
887 (* First instantiates the types and known subterms. *) |
886 in |
888 (* Then solves the quotient assumptions to get Rep2 and Abs1 *) |
887 (f, Abs ("x", T, mk_abs u 0 g)) |
889 (* Finally instantiates the function f using make_inst *) |
888 end |
890 (* If Rep2 is identity then the pattern is simpler and make_inst_id is used *) |
889 *} |
|
890 |
|
891 ML {* |
|
892 (* FIXME / TODO this needs to be clarified *) |
|
893 |
|
894 fun lambda_prs_simple_conv ctxt ctrm = |
891 fun lambda_prs_simple_conv ctxt ctrm = |
895 case (term_of ctrm) of |
892 case (term_of ctrm) of |
896 (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => |
893 (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => |
897 (let |
894 (let |
898 val thy = ProofContext.theory_of ctxt |
895 val thy = ProofContext.theory_of ctxt |
899 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
896 val (ty_b, ty_a) = dest_fun_type (fastype_of r1) |
900 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
897 val (ty_c, ty_d) = dest_fun_type (fastype_of a2) |
901 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
898 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
902 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
899 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
903 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
900 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} |
904 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
901 val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)] |
905 val ti = |
902 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
906 (let |
903 val make_inst = if ty_c = ty_d then make_inst_id else make_inst |
907 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
904 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
908 val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) |
905 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
909 in |
|
910 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
|
911 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
|
912 let |
|
913 val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te |
|
914 val _ = tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts))); |
|
915 val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
|
916 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm) |
|
917 in |
|
918 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
|
919 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
|
920 let |
|
921 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
|
922 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
|
923 in |
|
924 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
|
925 end) |
|
926 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
|
927 (tracing "lambda_prs"; |
|
928 tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); |
|
929 tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); |
|
930 tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); |
|
931 tracing ("ti rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) |
|
932 else () |
|
933 |
|
934 in |
906 in |
935 Conv.rewr_conv ti ctrm |
907 Conv.rewr_conv ti ctrm |
936 end |
908 end |
937 handle _ => Conv.all_conv ctrm) |
909 handle _ => Conv.all_conv ctrm) |
938 | _ => Conv.all_conv ctrm |
910 | _ => Conv.all_conv ctrm |