815 ML {* |
815 ML {* |
816 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
816 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
817 (FIRST' [ |
817 (FIRST' [ |
818 rtac trans_thm, |
818 rtac trans_thm, |
819 LAMBDA_RES_TAC ctxt, |
819 LAMBDA_RES_TAC ctxt, |
|
820 rtac @{thm RES_FORALL_RSP}, |
820 ball_rsp_tac ctxt, |
821 ball_rsp_tac ctxt, |
|
822 rtac @{thm RES_EXISTS_RSP}, |
821 bex_rsp_tac ctxt, |
823 bex_rsp_tac ctxt, |
822 FIRST' (map rtac rsp_thms), |
824 FIRST' (map rtac rsp_thms), |
823 rtac refl, |
825 rtac refl, |
824 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])), |
826 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])), |
825 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])), |
827 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])), |
926 get_fun flag qenv lthy xchg_ty |
928 get_fun flag qenv lthy xchg_ty |
927 end |
929 end |
928 *} |
930 *} |
929 |
931 |
930 ML {* |
932 ML {* |
931 fun applic_prs lthy rty qty absrep ty = |
933 fun applic_prs_old lthy rty qty absrep ty = |
932 let |
934 let |
933 val rty = Logic.varifyT rty; |
935 val rty = Logic.varifyT rty; |
934 val qty = Logic.varifyT qty; |
936 val qty = Logic.varifyT qty; |
935 fun absty ty = |
937 fun absty ty = |
936 exchange_ty lthy rty qty ty |
938 exchange_ty lthy rty qty ty |
959 in |
961 in |
960 singleton (ProofContext.export lthy' lthy) t_id |
962 singleton (ProofContext.export lthy' lthy) t_id |
961 end |
963 end |
962 *} |
964 *} |
963 |
965 |
|
966 ML {* |
|
967 fun applic_prs lthy absrep (rty, qty) = |
|
968 let |
|
969 fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm; |
|
970 fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm; |
|
971 val (raty, rgty) = Term.strip_type rty; |
|
972 val (qaty, qgty) = Term.strip_type qty; |
|
973 val vs = map (fn _ => "x") qaty; |
|
974 val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; |
|
975 val f = Free (fname, qaty ---> qgty); |
|
976 val args = map Free (vfs ~~ qaty); |
|
977 val rhs = list_comb(f, args); |
|
978 val largs = map2 mk_rep (raty ~~ qaty) args; |
|
979 val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs)); |
|
980 val llhs = Syntax.check_term lthy lhs; |
|
981 val eq = Logic.mk_equals (llhs, rhs); |
|
982 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
|
983 val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply}); |
|
984 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
|
985 val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t; |
|
986 in |
|
987 singleton (ProofContext.export lthy' lthy) t_id |
|
988 end |
|
989 *} |
964 |
990 |
965 ML {* |
991 ML {* |
966 fun findaps_all rty tm = |
992 fun findaps_all rty tm = |
967 case tm of |
993 case tm of |
968 Abs(_, T, b) => |
994 Abs(_, T, b) => |
972 (if needs_lift rty T then [T] else []) |
998 (if needs_lift rty T then [T] else []) |
973 | _ => []; |
999 | _ => []; |
974 fun findaps rty tm = distinct (op =) (findaps_all rty tm) |
1000 fun findaps rty tm = distinct (op =) (findaps_all rty tm) |
975 *} |
1001 *} |
976 |
1002 |
|
1003 |
|
1004 ML {* |
|
1005 fun find_aps_all rtm qtm = |
|
1006 case (rtm, qtm) of |
|
1007 (Abs(_, T1, s1), Abs(_, T2, s2)) => |
|
1008 find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2)) |
|
1009 | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) => |
|
1010 let |
|
1011 val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2) |
|
1012 in |
|
1013 if T1 = T2 then sub else (T1, T2) :: sub |
|
1014 end |
|
1015 | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2) |
|
1016 | _ => []; |
|
1017 |
|
1018 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm) |
|
1019 *} |
977 |
1020 |
978 ML {* |
1021 ML {* |
979 (* FIXME: allex_prs and lambda_prs can be one function *) |
1022 (* FIXME: allex_prs and lambda_prs can be one function *) |
980 fun allex_prs_tac lthy quot = |
1023 fun allex_prs_tac lthy quot = |
981 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
1024 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
1066 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1109 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1067 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1110 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1068 *} |
1111 *} |
1069 |
1112 |
1070 ML {* |
1113 ML {* |
1071 fun clean_tac lthy quot defs reps_same = |
1114 fun clean_tac lthy quot defs reps_same absrep aps = |
1072 let |
1115 let |
1073 val lower = flat (map (add_lower_defs lthy) defs) |
1116 val lower = flat (map (add_lower_defs lthy) defs) |
|
1117 val aps_thms = map (applic_prs lthy absrep) aps |
1074 in |
1118 in |
1075 EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1119 EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1076 lambda_prs_tac lthy quot, |
1120 lambda_prs_tac lthy quot, |
1077 (* TODO: cleaning according to app_prs *) |
1121 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), |
1078 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower), |
1122 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower), |
1079 simp_tac (HOL_ss addsimps [reps_same])] |
1123 simp_tac (HOL_ss addsimps [reps_same])] |
1080 end |
1124 end |
1081 *} |
1125 *} |
1082 |
1126 |
1163 SOME (cterm_of thy reg_goal), |
1207 SOME (cterm_of thy reg_goal), |
1164 SOME (cterm_of thy inj_goal)] |
1208 SOME (cterm_of thy inj_goal)] |
1165 @{thm procedure} |
1209 @{thm procedure} |
1166 end |
1210 end |
1167 *} |
1211 *} |
1168 |
1212 |
1169 ML {* |
1213 (* Left for debugging *) |
1170 fun procedure_tac rthm ctxt = |
1214 ML {* |
1171 ObjectLogic.full_atomize_tac |
1215 fun procedure_tac lthy rthm = |
1172 THEN' gen_frees_tac ctxt |
1216 ObjectLogic.full_atomize_tac |
|
1217 THEN' gen_frees_tac lthy |
1173 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1218 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1174 let |
1219 let |
1175 val rthm' = atomize_thm rthm |
1220 val rthm' = atomize_thm rthm |
1176 val rule = procedure_inst context (prop_of rthm') (Envir.beta_norm (term_of concl)) |
1221 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1177 in |
1222 in |
1178 EVERY1 [rtac rule, rtac rthm'] |
1223 rtac rule THEN' rtac rthm' |
1179 end) ctxt |
1224 end 1) lthy |
1180 *} |
1225 *} |
1181 |
1226 |
1182 ML {* |
1227 ML {* |
1183 fun lift_tac lthy thm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs = |
1228 fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs = |
1184 procedure_tac thm lthy THEN' |
1229 ObjectLogic.full_atomize_tac |
1185 RANGE [regularize_tac lthy rel_eqv rel_refl, |
1230 THEN' gen_frees_tac lthy |
1186 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1231 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1187 clean_tac lthy quot defs reps_same] |
1232 let |
1188 *} |
1233 val rthm' = atomize_thm rthm |
1189 |
1234 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1190 |
1235 val aps = find_aps (prop_of rthm') (term_of concl) |
|
1236 in |
|
1237 rtac rule THEN' RANGE [ |
|
1238 rtac rthm', |
|
1239 regularize_tac lthy rel_eqv rel_refl, |
|
1240 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
|
1241 clean_tac lthy quot defs reps_same absrep aps |
|
1242 ] |
|
1243 end 1) lthy |
|
1244 *} |
1191 |
1245 |
1192 end |
1246 end |
1193 |
1247 |
1194 |
1248 |