795 ML {* |
795 ML {* |
796 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
796 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
797 (FIRST' [ |
797 (FIRST' [ |
798 rtac trans_thm, |
798 rtac trans_thm, |
799 LAMBDA_RES_TAC ctxt, |
799 LAMBDA_RES_TAC ctxt, |
|
800 rtac @{thm RES_FORALL_RSP}, |
800 ball_rsp_tac ctxt, |
801 ball_rsp_tac ctxt, |
|
802 rtac @{thm RES_EXISTS_RSP}, |
801 bex_rsp_tac ctxt, |
803 bex_rsp_tac ctxt, |
802 FIRST' (map rtac rsp_thms), |
804 FIRST' (map rtac rsp_thms), |
803 rtac refl, |
805 rtac refl, |
804 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])), |
806 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])), |
805 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])), |
807 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])), |
906 get_fun flag qenv lthy xchg_ty |
908 get_fun flag qenv lthy xchg_ty |
907 end |
909 end |
908 *} |
910 *} |
909 |
911 |
910 ML {* |
912 ML {* |
911 fun applic_prs lthy rty qty absrep ty = |
913 fun applic_prs_old lthy rty qty absrep ty = |
912 let |
914 let |
913 val rty = Logic.varifyT rty; |
915 val rty = Logic.varifyT rty; |
914 val qty = Logic.varifyT qty; |
916 val qty = Logic.varifyT qty; |
915 fun absty ty = |
917 fun absty ty = |
916 exchange_ty lthy rty qty ty |
918 exchange_ty lthy rty qty ty |
939 in |
941 in |
940 singleton (ProofContext.export lthy' lthy) t_id |
942 singleton (ProofContext.export lthy' lthy) t_id |
941 end |
943 end |
942 *} |
944 *} |
943 |
945 |
|
946 ML {* |
|
947 fun applic_prs lthy absrep (rty, qty) = |
|
948 let |
|
949 fun mk_rep (T, T') tm = (Quotient_Def.get_fun repF lthy (T, T')) $ tm; |
|
950 fun mk_abs (T, T') tm = (Quotient_Def.get_fun absF lthy (T, T')) $ tm; |
|
951 val (raty, rgty) = Term.strip_type rty; |
|
952 val (qaty, qgty) = Term.strip_type qty; |
|
953 val vs = map (fn _ => "x") qaty; |
|
954 val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; |
|
955 val f = Free (fname, qaty ---> qgty); |
|
956 val args = map Free (vfs ~~ qaty); |
|
957 val rhs = list_comb(f, args); |
|
958 val largs = map2 mk_rep (raty ~~ qaty) args; |
|
959 val lhs = mk_abs (rgty, qgty) (list_comb((mk_rep (raty ---> rgty, qaty ---> qgty) f), largs)); |
|
960 val llhs = Syntax.check_term lthy lhs; |
|
961 val eq = Logic.mk_equals (llhs, rhs); |
|
962 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
|
963 val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps map_id id_apply}); |
|
964 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
|
965 val t_id = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply] id_def_sym} t; |
|
966 in |
|
967 singleton (ProofContext.export lthy' lthy) t_id |
|
968 end |
|
969 *} |
944 |
970 |
945 ML {* |
971 ML {* |
946 fun findaps_all rty tm = |
972 fun findaps_all rty tm = |
947 case tm of |
973 case tm of |
948 Abs(_, T, b) => |
974 Abs(_, T, b) => |
952 (if needs_lift rty T then [T] else []) |
978 (if needs_lift rty T then [T] else []) |
953 | _ => []; |
979 | _ => []; |
954 fun findaps rty tm = distinct (op =) (findaps_all rty tm) |
980 fun findaps rty tm = distinct (op =) (findaps_all rty tm) |
955 *} |
981 *} |
956 |
982 |
|
983 |
|
984 ML {* |
|
985 fun find_aps_all rtm qtm = |
|
986 case (rtm, qtm) of |
|
987 (Abs(_, T1, s1), Abs(_, T2, s2)) => |
|
988 find_aps_all (subst_bound ((Free ("x", T1)), s1)) (subst_bound ((Free ("x", T2)), s2)) |
|
989 | (((f1 as (Free (_, T1))) $ a1), ((f2 as (Free (_, T2))) $ a2)) => |
|
990 let |
|
991 val sub = (find_aps_all f1 f2) @ (find_aps_all a1 a2) |
|
992 in |
|
993 if T1 = T2 then sub else (T1, T2) :: sub |
|
994 end |
|
995 | ((f1 $ a1), (f2 $ a2)) => (find_aps_all f1 f2) @ (find_aps_all a1 a2) |
|
996 | _ => []; |
|
997 |
|
998 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm) |
|
999 *} |
957 |
1000 |
958 ML {* |
1001 ML {* |
959 (* FIXME: allex_prs and lambda_prs can be one function *) |
1002 (* FIXME: allex_prs and lambda_prs can be one function *) |
960 fun allex_prs_tac lthy quot = |
1003 fun allex_prs_tac lthy quot = |
961 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
1004 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
1046 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1089 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1047 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1090 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1048 *} |
1091 *} |
1049 |
1092 |
1050 ML {* |
1093 ML {* |
1051 fun clean_tac lthy quot defs reps_same = |
1094 fun clean_tac lthy quot defs reps_same absrep aps = |
1052 let |
1095 let |
1053 val lower = flat (map (add_lower_defs lthy) defs) |
1096 val lower = flat (map (add_lower_defs lthy) defs) |
|
1097 val aps_thms = map (applic_prs lthy absrep) aps |
1054 in |
1098 in |
1055 EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1099 EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), |
1056 lambda_prs_tac lthy quot, |
1100 lambda_prs_tac lthy quot, |
1057 (* TODO: cleaning according to app_prs *) |
1101 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms), |
1058 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower), |
1102 TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower), |
1059 simp_tac (HOL_ss addsimps [reps_same])] |
1103 simp_tac (HOL_ss addsimps [reps_same])] |
1060 end |
1104 end |
1061 *} |
1105 *} |
1062 |
1106 |
1143 SOME (cterm_of thy reg_goal), |
1187 SOME (cterm_of thy reg_goal), |
1144 SOME (cterm_of thy inj_goal)] |
1188 SOME (cterm_of thy inj_goal)] |
1145 @{thm procedure} |
1189 @{thm procedure} |
1146 end |
1190 end |
1147 *} |
1191 *} |
1148 |
1192 |
1149 ML {* |
1193 (* Left for debugging *) |
1150 fun procedure_tac rthm ctxt = |
1194 ML {* |
1151 ObjectLogic.full_atomize_tac |
1195 fun procedure_tac lthy rthm = |
1152 THEN' gen_frees_tac ctxt |
1196 ObjectLogic.full_atomize_tac |
|
1197 THEN' gen_frees_tac lthy |
1153 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1198 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1154 let |
1199 let |
1155 val rthm' = atomize_thm rthm |
1200 val rthm' = atomize_thm rthm |
1156 val rule = procedure_inst context (prop_of rthm') (Envir.beta_norm (term_of concl)) |
1201 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1157 in |
1202 in |
1158 EVERY1 [rtac rule, rtac rthm'] |
1203 rtac rule THEN' rtac rthm' |
1159 end) ctxt |
1204 end 1) lthy |
1160 *} |
1205 *} |
1161 |
1206 |
1162 ML {* |
1207 ML {* |
1163 fun lift_tac lthy thm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs = |
1208 fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs = |
1164 procedure_tac thm lthy THEN' |
1209 ObjectLogic.full_atomize_tac |
1165 RANGE [regularize_tac lthy rel_eqv rel_refl, |
1210 THEN' gen_frees_tac lthy |
1166 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1211 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1167 clean_tac lthy quot defs reps_same] |
1212 let |
1168 *} |
1213 val rthm' = atomize_thm rthm |
1169 |
1214 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1170 |
1215 val aps = find_aps (prop_of rthm') (term_of concl) |
|
1216 in |
|
1217 rtac rule THEN' RANGE [ |
|
1218 rtac rthm', |
|
1219 regularize_tac lthy rel_eqv rel_refl, |
|
1220 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
|
1221 clean_tac lthy quot defs reps_same absrep aps |
|
1222 ] |
|
1223 end 1) lthy |
|
1224 *} |
1171 |
1225 |
1172 end |
1226 end |
1173 |
1227 |
1174 |
1228 |