equal
deleted
inserted
replaced
788 | _ => error "find_qt_asm" |
788 | _ => error "find_qt_asm" |
789 end |
789 end |
790 *} |
790 *} |
791 |
791 |
792 ML {* |
792 ML {* |
793 fun APPLY_RSP_TAC rty = |
793 val APPLY_RSP_TAC = |
794 Subgoal.FOCUS (fn {concl, asms, ...} => |
|
795 case ((HOLogic.dest_Trueprop (term_of concl))) of |
|
796 ((_ $ (f $ _) $ (_ $ _))) => |
|
797 let |
|
798 val (asmf, asma) = find_qt_asm (map term_of asms); |
|
799 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
|
800 val insts = Thm.first_order_match (pat, concl) |
|
801 in |
|
802 if (fastype_of asmf) = (fastype_of f) |
|
803 then no_tac |
|
804 else rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
|
805 end |
|
806 | _ => no_tac) |
|
807 *} |
|
808 |
|
809 ML {* |
|
810 val APPLY_RSP_TAC' = |
|
811 Subgoal.FOCUS (fn {concl, asms, context,...} => |
794 Subgoal.FOCUS (fn {concl, asms, context,...} => |
812 case ((HOLogic.dest_Trueprop (term_of concl))) of |
795 case ((HOLogic.dest_Trueprop (term_of concl))) of |
813 ((R2 $ (f $ x) $ (g $ y))) => |
796 ((R2 $ (f $ x) $ (g $ y))) => |
814 let |
797 let |
815 val (asmf, asma) = find_qt_asm (map term_of asms); |
798 val (asmf, asma) = find_qt_asm (map term_of asms); |
951 (* observe ---> *) |
934 (* observe ---> *) |
952 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
935 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
953 THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), |
936 THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), |
954 |
937 |
955 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
938 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
956 NDT ctxt "A" (APPLY_RSP_TAC' ctxt THEN' |
939 NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN' |
957 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), |
940 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms), |
958 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
941 quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
959 |
942 |
960 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
943 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
961 (* merge with previous tactic *) |
944 (* merge with previous tactic *) |
1105 The second one is an EqSubst (slow). |
1088 The second one is an EqSubst (slow). |
1106 The rest are a simp_tac and are fast. |
1089 The rest are a simp_tac and are fast. |
1107 *) |
1090 *) |
1108 |
1091 |
1109 ML {* |
1092 ML {* |
1110 fun clean_tac lthy quot defs = |
1093 fun clean_tac lthy quot = |
1111 let |
1094 let |
|
1095 val thy = ProofContext.theory_of lthy; |
|
1096 val defs = map (Thm.varifyT o #def) (qconsts_dest thy); |
1112 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1097 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1113 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1098 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1114 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1099 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1115 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1100 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1116 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1101 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1230 *} |
1215 *} |
1231 |
1216 |
1232 ML {* |
1217 ML {* |
1233 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1218 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1234 |
1219 |
1235 fun lift_tac lthy rthm rel_eqv quot defs = |
1220 fun lift_tac lthy rthm rel_eqv quot = |
1236 ObjectLogic.full_atomize_tac |
1221 ObjectLogic.full_atomize_tac |
1237 THEN' gen_frees_tac lthy |
1222 THEN' gen_frees_tac lthy |
1238 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1223 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1239 let |
1224 let |
1240 val rthm' = atomize_thm rthm |
1225 val rthm' = atomize_thm rthm |
1246 EVERY1 |
1231 EVERY1 |
1247 [rtac rule, |
1232 [rtac rule, |
1248 RANGE [rtac rthm', |
1233 RANGE [rtac rthm', |
1249 regularize_tac lthy rel_eqv, |
1234 regularize_tac lthy rel_eqv, |
1250 rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2, |
1235 rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2, |
1251 clean_tac lthy quot defs]] |
1236 clean_tac lthy quot]] |
1252 end) lthy |
1237 end) lthy |
1253 *} |
1238 *} |
1254 |
1239 |
1255 end |
1240 end |
1256 |
1241 |