equal
deleted
inserted
replaced
1086 The second one is an EqSubst (slow). |
1086 The second one is an EqSubst (slow). |
1087 The rest are a simp_tac and are fast. |
1087 The rest are a simp_tac and are fast. |
1088 *) |
1088 *) |
1089 |
1089 |
1090 ML {* |
1090 ML {* |
1091 fun clean_tac lthy quot defs = |
1091 fun clean_tac lthy quot = |
1092 let |
1092 let |
|
1093 val thy = ProofContext.theory_of lthy; |
|
1094 val defs = map (#def) (qconsts_dest thy); |
1093 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1095 val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot |
1094 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1096 val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; |
1095 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1097 val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot |
1096 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1098 val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same |
1097 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1099 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1211 *} |
1213 *} |
1212 |
1214 |
1213 ML {* |
1215 ML {* |
1214 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1216 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1215 |
1217 |
1216 fun lift_tac lthy rthm rel_eqv quot defs = |
1218 fun lift_tac lthy rthm rel_eqv quot = |
1217 ObjectLogic.full_atomize_tac |
1219 ObjectLogic.full_atomize_tac |
1218 THEN' gen_frees_tac lthy |
1220 THEN' gen_frees_tac lthy |
1219 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1221 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1220 let |
1222 let |
1221 val rthm' = atomize_thm rthm |
1223 val rthm' = atomize_thm rthm |
1227 EVERY1 |
1229 EVERY1 |
1228 [rtac rule, |
1230 [rtac rule, |
1229 RANGE [rtac rthm', |
1231 RANGE [rtac rthm', |
1230 regularize_tac lthy rel_eqv, |
1232 regularize_tac lthy rel_eqv, |
1231 rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2, |
1233 rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2, |
1232 clean_tac lthy quot defs]] |
1234 clean_tac lthy quot]] |
1233 end) lthy |
1235 end) lthy |
1234 *} |
1236 *} |
1235 |
1237 |
|
1238 print_quotients |
|
1239 |
|
1240 |
1236 end |
1241 end |
1237 |
1242 |