926 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
926 REPEAT_ALL_NEW (inj_repabs_tac ctxt) |
927 *} |
927 *} |
928 |
928 |
929 section {* Cleaning of the Theorem *} |
929 section {* Cleaning of the Theorem *} |
930 |
930 |
|
931 ML {* |
|
932 fun fun_map_simple_conv xs ctxt ctrm = |
|
933 case (term_of ctrm) of |
|
934 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
|
935 if (member (op=) xs h) |
|
936 then Conv.all_conv ctrm |
|
937 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm |
|
938 | _ => Conv.all_conv ctrm |
|
939 |
|
940 fun fun_map_conv xs ctxt ctrm = |
|
941 case (term_of ctrm) of |
|
942 _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv |
|
943 fun_map_simple_conv xs ctxt) ctrm |
|
944 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
|
945 | _ => Conv.all_conv ctrm |
|
946 |
|
947 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
|
948 *} |
|
949 |
931 (* Since the patterns for the lhs are different; there are 3 different make-insts *) |
950 (* Since the patterns for the lhs are different; there are 3 different make-insts *) |
932 (* 1: does ? \<rightarrow> id *) |
951 (* 1: does ? \<rightarrow> id *) |
933 (* 2: does id \<rightarrow> ? *) |
952 (* 2: does id \<rightarrow> ? *) |
934 (* 3: does ? \<rightarrow> ? *) |
953 (* 3: does ? \<rightarrow> ? *) |
935 ML {* |
954 ML {* |
947 in (f, Abs ("x", T, mk_abs 0 g)) end; |
966 in (f, Abs ("x", T, mk_abs 0 g)) end; |
948 *} |
967 *} |
949 |
968 |
950 ML {* |
969 ML {* |
951 fun make_inst2 lhs t = |
970 fun make_inst2 lhs t = |
952 let |
|
953 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
|
954 val _ $ (Abs (_, _, (_ $ g))) = t; |
|
955 fun mk_abs i t = |
|
956 if incr_boundvars i u aconv t then Bound i |
|
957 else (case t of |
|
958 t1 $ t2 => mk_abs i t1 $ mk_abs i t2 |
|
959 | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') |
|
960 | Bound j => if i = j then error "make_inst" else t |
|
961 | _ => t); |
|
962 in (f, Abs ("x", T, mk_abs 0 g)) end; |
|
963 *} |
|
964 |
|
965 ML {* |
|
966 fun make_inst3 lhs t = |
|
967 let |
971 let |
968 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
972 val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; |
969 val _ $ (Abs (_, _, (_ $ g))) = t; |
973 val _ $ (Abs (_, _, (_ $ g))) = t; |
970 fun mk_abs i t = |
974 fun mk_abs i t = |
971 if incr_boundvars i u aconv t then Bound i |
975 if incr_boundvars i u aconv t then Bound i |
1003 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1007 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of ts)) (term_of ctrm) |
1004 in |
1008 in |
1005 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1009 Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts |
1006 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
1010 end handle _ => (* TODO handle only Bind | Error "make_inst" *) |
1007 let |
1011 let |
1008 val (insp, inst) = make_inst3 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1012 val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm) |
1009 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
1013 val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te |
1010 in |
1014 in |
1011 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
1015 MetaSimplifier.rewrite_rule (id_simps_get ctxt) td |
1012 end); |
1016 end); |
1013 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
1017 val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then |
1030 More_Conv.top_conv lambda_prs_simple_conv |
1034 More_Conv.top_conv lambda_prs_simple_conv |
1031 |
1035 |
1032 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
1036 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) |
1033 *} |
1037 *} |
1034 |
1038 |
1035 (* 1. conversion (is not a pattern) *) |
1039 (* 1. folding of definitions and preservation lemmas; *) |
|
1040 (* and simplification with *) |
|
1041 thm babs_prs all_prs ex_prs |
|
1042 (* 2. unfolding of ---> in front of everything, except *) |
|
1043 (* bound variables *) |
|
1044 thm fun_map.simps |
|
1045 (* 3. simplification with *) |
1036 thm lambda_prs |
1046 thm lambda_prs |
1037 (* 2. folding of definitions: (rep ---> abs) oldConst == newconst *) |
1047 (* 4. simplification with *) |
1038 (* prservation lemma *) |
1048 thm Quotient_abs_rep Quotient_rel_rep id_simps |
1039 (* and simplification with *) |
1049 (* 5. Test for refl *) |
1040 thm all_prs ex_prs |
|
1041 (* 3. simplification with *) |
|
1042 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps |
|
1043 (* 4. Test for refl *) |
|
1044 |
|
1045 ML {* |
|
1046 fun fun_map_conv xs ctxt ctrm = |
|
1047 case (term_of ctrm) of |
|
1048 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
|
1049 (Conv.binop_conv (fun_map_conv xs ctxt) then_conv |
|
1050 (if (member (op=) xs h) |
|
1051 then Conv.all_conv |
|
1052 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]})) ctrm |
|
1053 | _ $ _ => Conv.comb_conv (fun_map_conv xs ctxt) ctrm |
|
1054 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
|
1055 | _ => Conv.all_conv ctrm |
|
1056 |
|
1057 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
|
1058 *} |
|
1059 |
1050 |
1060 ML {* |
1051 ML {* |
1061 fun clean_tac lthy = |
1052 fun clean_tac lthy = |
1062 let |
1053 let |
1063 val thy = ProofContext.theory_of lthy; |
1054 val thy = ProofContext.theory_of lthy; |
1064 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1055 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
1065 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
1056 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
|
1057 |
1066 val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} |
1058 val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} |
1067 val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
1059 val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) |
1068 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1060 fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
1069 in |
1061 in |
1070 EVERY' [simp_tac (simps thms1), |
1062 EVERY' [simp_tac (simps thms1), |
1071 TRY o REPEAT_ALL_NEW (CHANGED o (fun_map_tac lthy)), |
1063 fun_map_tac lthy, |
1072 lambda_prs_tac lthy, |
1064 lambda_prs_tac lthy, |
1073 simp_tac (simps thms2), |
1065 simp_tac (simps thms2), |
1074 TRY o rtac refl] |
1066 TRY o rtac refl] |
1075 end |
1067 end |
1076 *} |
1068 *} |