equal
deleted
inserted
replaced
988 (* global simplification *) |
988 (* global simplification *) |
989 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
989 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
990 *} |
990 *} |
991 |
991 |
992 ML {* |
992 ML {* |
993 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
993 fun inj_repabs_tac ctxt quot_thms rel_refl trans2 = |
994 (FIRST' [ |
994 (FIRST' [ |
995 (* "cong" rule of the of the relation / transitivity*) |
995 (* "cong" rule of the of the relation / transitivity*) |
996 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
996 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
997 NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [ |
997 NDT ctxt "1" (resolve_tac trans2 THEN' RANGE [ |
998 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), |
998 quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]), |
1048 (* global simplification *) |
1048 (* global simplification *) |
1049 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
1049 NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))]) |
1050 *} |
1050 *} |
1051 |
1051 |
1052 ML {* |
1052 ML {* |
1053 fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
1053 fun all_inj_repabs_tac ctxt quot_thms rel_refl trans2 = |
1054 REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2) |
1054 REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2) |
1055 *} |
1055 *} |
1056 |
1056 |
1057 section {* Cleaning of the theorem *} |
1057 section {* Cleaning of the theorem *} |
1058 |
1058 |
1059 |
1059 |
1274 end) lthy |
1274 end) lthy |
1275 *} |
1275 *} |
1276 |
1276 |
1277 ML {* |
1277 ML {* |
1278 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1278 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1279 fun lift_tac lthy rthm rel_eqv rty quot defs = |
1279 |
|
1280 fun lift_tac lthy rthm rel_eqv quot defs = |
1280 ObjectLogic.full_atomize_tac |
1281 ObjectLogic.full_atomize_tac |
1281 THEN' gen_frees_tac lthy |
1282 THEN' gen_frees_tac lthy |
1282 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1283 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1283 let |
1284 let |
1284 val rthm' = atomize_thm rthm |
1285 val rthm' = atomize_thm rthm |
1289 in |
1290 in |
1290 EVERY1 |
1291 EVERY1 |
1291 [rtac rule, |
1292 [rtac rule, |
1292 RANGE [rtac rthm', |
1293 RANGE [rtac rthm', |
1293 regularize_tac lthy rel_eqv, |
1294 regularize_tac lthy rel_eqv, |
1294 rtac thm THEN' all_inj_repabs_tac lthy rty quot rel_refl trans2, |
1295 rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2, |
1295 clean_tac lthy quot defs]] |
1296 clean_tac lthy quot defs]] |
1296 end) lthy |
1297 end) lthy |
1297 *} |
1298 *} |
1298 |
1299 |
1299 end |
1300 end |