935 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
935 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
936 | dest_fun_type _ = error "dest_fun_type" |
936 | dest_fun_type _ = error "dest_fun_type" |
937 *} |
937 *} |
938 |
938 |
939 ML {* |
939 ML {* |
940 val rep_abs_rsp_tac = |
940 fun rep_abs_rsp_tac ctxt = |
941 Subgoal.FOCUS (fn {concl, context, ...} => |
941 SUBGOAL (fn (goal, i) => |
942 case HOLogic.dest_Trueprop (term_of concl) of (rel $ lhs $ (rep $ (abs $ rhs))) => |
942 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of (rel $ _ $ (rep $ (abs $ _))) => |
943 (let |
943 (let |
944 val thy = ProofContext.theory_of context; |
944 val thy = ProofContext.theory_of ctxt; |
945 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
945 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
946 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
946 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
947 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
947 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
948 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
948 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
949 val te = solve_quotient_assums context thm |
949 val te = solve_quotient_assums ctxt thm |
950 val t_inst = map (SOME o (cterm_of thy)) [lhs, rhs]; |
|
951 val thm = Drule.instantiate' [] t_inst te |
|
952 in |
950 in |
953 compose_tac (false, thm, 1) 1 |
951 rtac te i |
954 end |
952 end |
955 handle _ => no_tac) |
953 handle _ => no_tac) |
956 | _ => no_tac) |
954 | _ => no_tac) |
957 *} |
955 *} |
958 |
956 |
1238 end |
1236 end |
1239 *} |
1237 *} |
1240 |
1238 |
1241 (* Left for debugging *) |
1239 (* Left for debugging *) |
1242 ML {* |
1240 ML {* |
1243 fun procedure_tac lthy rthm = |
1241 fun procedure_tac ctxt rthm = |
1244 ObjectLogic.full_atomize_tac |
1242 ObjectLogic.full_atomize_tac |
1245 THEN' gen_frees_tac lthy |
1243 THEN' gen_frees_tac ctxt |
1246 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1244 THEN' CSUBGOAL (fn (gl, i) => |
1247 let |
1245 let |
1248 val rthm' = atomize_thm rthm |
1246 val rthm' = atomize_thm rthm |
1249 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1247 val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) |
1250 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} |
1248 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} |
1251 in |
1249 in |
1252 EVERY1 [rtac rule, rtac rthm'] THEN RANGE [(fn _ => all_tac), rtac thm] 1 |
1250 (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i |
1253 end) lthy |
1251 end) |
1254 *} |
1252 *} |
1255 |
1253 |
1256 ML {* |
1254 ML {* |
1257 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1255 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1258 |
1256 |
1259 fun lift_tac lthy rthm rel_eqv = |
1257 fun lift_tac ctxt rthm rel_eqv = |
1260 ObjectLogic.full_atomize_tac |
1258 ObjectLogic.full_atomize_tac |
1261 THEN' gen_frees_tac lthy |
1259 THEN' gen_frees_tac ctxt |
1262 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1260 THEN' CSUBGOAL (fn (gl, i) => |
1263 let |
1261 let |
1264 val rthm' = atomize_thm rthm |
1262 val rthm' = atomize_thm rthm |
1265 val rule = procedure_inst context (prop_of rthm') (term_of concl) |
1263 val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) |
1266 val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv |
1264 val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv |
1267 val quotients = quotient_rules_get lthy |
1265 val quotients = quotient_rules_get ctxt |
1268 val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients |
1266 val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients |
1269 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} |
1267 val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} |
1270 in |
1268 in |
1271 EVERY1 |
1269 (rtac rule THEN' |
1272 [rtac rule, |
1270 RANGE [rtac rthm', |
1273 RANGE [rtac rthm', |
1271 regularize_tac ctxt rel_eqv, |
1274 regularize_tac lthy rel_eqv, |
1272 rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2, |
1275 rtac thm THEN' all_inj_repabs_tac lthy rel_refl trans2, |
1273 clean_tac ctxt]) i |
1276 clean_tac lthy]] |
1274 end) |
1277 end) lthy |
|
1278 *} |
1275 *} |
1279 |
1276 |
1280 end |
1277 end |
1281 |
1278 |