1183 end |
1183 end |
1184 *} |
1184 *} |
1185 |
1185 |
1186 (* Left for debugging *) |
1186 (* Left for debugging *) |
1187 ML {* |
1187 ML {* |
1188 fun procedure_tac lthy rthm = |
1188 fun procedure_tac ctxt rthm = |
1189 ObjectLogic.full_atomize_tac |
1189 ObjectLogic.full_atomize_tac |
1190 THEN' gen_frees_tac lthy |
1190 THEN' gen_frees_tac ctxt |
1191 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1191 THEN' CSUBGOAL (fn (gl, i) => |
1192 let |
1192 let |
1193 val rthm' = atomize_thm rthm |
1193 val rthm' = atomize_thm rthm |
1194 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1194 val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) |
1195 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} |
1195 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} |
1196 in |
1196 in |
1197 EVERY1 [rtac rule, rtac rthm'] THEN RANGE [(fn _ => all_tac), rtac thm] 1 |
1197 (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i |
1198 end) lthy |
1198 end) |
1199 *} |
1199 *} |
1200 |
1200 |
1201 ML {* |
1201 ML {* |
1202 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1202 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1203 |
1203 |
1204 fun lift_tac lthy rthm rel_eqv = |
1204 fun lift_tac ctxt rthm rel_eqv = |
1205 ObjectLogic.full_atomize_tac |
1205 ObjectLogic.full_atomize_tac |
1206 THEN' gen_frees_tac lthy |
1206 THEN' gen_frees_tac ctxt |
1207 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1207 THEN' CSUBGOAL (fn (gl, i) => |
1208 let |
1208 let |
1209 val rthm' = atomize_thm rthm |
1209 val rthm' = atomize_thm rthm |
1210 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1210 val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) |
1211 val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv |
1211 val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv |
1212 val quotients = quotient_rules_get lthy |
1212 val quotients = quotient_rules_get ctxt |
1213 val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients |
1213 val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients |
1214 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} |
1214 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} |
1215 in |
1215 in |
1216 EVERY1 |
1216 (rtac rule THEN' |
1217 [rtac rule, |
1217 RANGE [rtac rthm', |
1218 RANGE [rtac rthm', |
1218 regularize_tac ctxt rel_eqv, |
1219 regularize_tac lthy rel_eqv, |
1219 rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2, |
1220 rtac thm THEN' all_inj_repabs_tac lthy rel_refl trans2, |
1220 clean_tac ctxt]) i |
1221 clean_tac lthy]] |
1221 end) |
1222 end) lthy |
|
1223 *} |
1222 *} |
1224 |
1223 |
1225 end |
1224 end |
1226 |
1225 |