947 *} |
947 *} |
948 |
948 |
949 |
949 |
950 section {* Cleaning of the theorem *} |
950 section {* Cleaning of the theorem *} |
951 |
951 |
952 ML {* |
|
953 fun applic_prs lthy absrep (rty, qty) = |
|
954 let |
|
955 fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm; |
|
956 fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm; |
|
957 val (raty, rgty) = Term.strip_type rty; |
|
958 val (qaty, qgty) = Term.strip_type qty; |
|
959 val vs = map (fn _ => "x") qaty; |
|
960 val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; |
|
961 val f = Free (fname, qaty ---> qgty); |
|
962 val args = map Free (vfs ~~ qaty); |
|
963 val rhs = list_comb(f, args); |
|
964 val largs = map2 mk_rep (raty ~~ qaty) args; |
|
965 val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs)); |
|
966 val llhs = Syntax.check_term lthy lhs; |
|
967 val eq = Logic.mk_equals (llhs, rhs); |
|
968 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
|
969 val sctxt = HOL_ss addsimps (@{thms fun_map.simps id_simps} @ absrep); |
|
970 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
|
971 val t_id = MetaSimplifier.rewrite_rule @{thms id_simps} t; |
|
972 in |
|
973 singleton (ProofContext.export lthy' lthy) t_id |
|
974 end |
|
975 *} |
|
976 |
|
977 ML {* |
|
978 fun find_aps_all rtm qtm = |
|
979 case (rtm, qtm) of |
|
980 (Abs(_, T1, s1), Abs(_, T2, s2)) => |
|
981 find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2)) |
|
982 | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) => |
|
983 let |
|
984 val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2) |
|
985 in |
|
986 if T1 = T2 then sub else (T1, T2) :: sub |
|
987 end |
|
988 | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2) |
|
989 | _ => []; |
|
990 |
|
991 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm) |
|
992 *} |
|
993 |
952 |
994 (* TODO: This is slow *) |
953 (* TODO: This is slow *) |
995 ML {* |
954 ML {* |
996 fun allex_prs_tac lthy quot = |
955 fun allex_prs_tac lthy quot = |
997 (EqSubst.eqsubst_tac lthy [0] @{thms all_prs ex_prs}) THEN' (quotient_tac quot) |
956 (EqSubst.eqsubst_tac lthy [0] @{thms all_prs ex_prs}) THEN' (quotient_tac quot) |
1084 The first one is implemented as a conversion (fast). |
1043 The first one is implemented as a conversion (fast). |
1085 The second one is an EqSubst (slow). |
1044 The second one is an EqSubst (slow). |
1086 The rest are a simp_tac and are fast. |
1045 The rest are a simp_tac and are fast. |
1087 *) |
1046 *) |
1088 ML {* |
1047 ML {* |
1089 fun clean_tac lthy quot defs aps = |
1048 fun clean_tac lthy quot defs = |
1090 let |
1049 let |
1091 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1050 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1092 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1051 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1093 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1052 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1094 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1053 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1208 THEN' gen_frees_tac lthy |
1167 THEN' gen_frees_tac lthy |
1209 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1168 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1210 let |
1169 let |
1211 val rthm' = atomize_thm rthm |
1170 val rthm' = atomize_thm rthm |
1212 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1171 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1213 val aps = find_aps (prop_of rthm') (term_of concl) |
|
1214 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv |
1172 val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv |
1215 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv |
1173 val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv |
1216 in |
1174 in |
1217 EVERY1 |
1175 EVERY1 |
1218 [rtac rule, |
1176 [rtac rule, |
1219 RANGE [rtac rthm', |
1177 RANGE [rtac rthm', |
1220 regularize_tac lthy rel_eqv, |
1178 regularize_tac lthy rel_eqv, |
1221 all_inj_repabs_tac lthy rty quot rel_refl trans2, |
1179 all_inj_repabs_tac lthy rty quot rel_refl trans2, |
1222 clean_tac lthy quot defs aps]] |
1180 clean_tac lthy quot defs]] |
1223 end) lthy |
1181 end) lthy |
1224 *} |
1182 *} |
1225 |
1183 |
1226 end |
1184 end |
1227 |
1185 |