equal
deleted
inserted
replaced
876 ML {* |
876 ML {* |
877 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
877 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
878 *} |
878 *} |
879 |
879 |
880 ML {* |
880 ML {* |
881 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
881 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
882 (FIRST' [resolve_tac trans2, |
882 (FIRST' [resolve_tac trans2, |
883 lambda_res_tac ctxt, |
883 lambda_res_tac ctxt, |
884 rtac @{thm RES_FORALL_RSP}, |
884 rtac @{thm RES_FORALL_RSP}, |
885 ball_rsp_tac ctxt, |
885 ball_rsp_tac ctxt, |
886 rtac @{thm RES_EXISTS_RSP}, |
886 rtac @{thm RES_EXISTS_RSP}, |
897 atac, |
897 atac, |
898 (*seems not necessary:: SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),*) |
898 (*seems not necessary:: SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),*) |
899 weak_lambda_res_tac ctxt, |
899 weak_lambda_res_tac ctxt, |
900 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]) |
900 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]) |
901 |
901 |
902 fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
902 fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
903 REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms) |
903 REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms) |
904 *} |
904 *} |
905 |
905 |
906 (* |
906 (* |
907 To prove that the regularised theorem implies the abs/rep injected, |
907 To prove that the regularised theorem implies the abs/rep injected, |
908 we try: |
908 we try: |
925 E) simplifying (= ===> =) for simpler respectfulness |
925 E) simplifying (= ===> =) for simpler respectfulness |
926 |
926 |
927 *) |
927 *) |
928 |
928 |
929 ML {* |
929 ML {* |
930 fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
930 fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
931 (FIRST' [ |
931 (FIRST' [ |
932 (K (print_tac "start")) THEN' (K no_tac), |
932 (K (print_tac "start")) THEN' (K no_tac), |
933 |
933 |
934 (* "cong" rule of the of the relation *) |
934 (* "cong" rule of the of the relation *) |
935 (* a \<approx> b = c \<approx> d ----> \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> *) |
935 (* a \<approx> b = c \<approx> d ----> \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> *) |
988 (* global simplification *) |
988 (* global simplification *) |
989 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
989 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
990 *} |
990 *} |
991 |
991 |
992 ML {* |
992 ML {* |
993 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
993 fun all_inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
994 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
994 REPEAT_ALL_NEW (inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
995 *} |
995 *} |
996 |
996 |
997 |
997 |
998 section {* Cleaning of the theorem *} |
998 section {* Cleaning of the theorem *} |
999 |
999 |
1243 in |
1243 in |
1244 EVERY1 |
1244 EVERY1 |
1245 [rtac rule, |
1245 [rtac rule, |
1246 RANGE [rtac rthm', |
1246 RANGE [rtac rthm', |
1247 regularize_tac lthy rel_eqv, |
1247 regularize_tac lthy rel_eqv, |
1248 REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms), |
1248 all_inj_repabs_tac lthy rty quot rel_refl trans2 rsp_thms, |
1249 clean_tac lthy quot defs aps]] |
1249 clean_tac lthy quot defs aps]] |
1250 end) lthy |
1250 end) lthy |
1251 *} |
1251 *} |
1252 |
1252 |
1253 end |
1253 end |