233 MetaSimplifier.rewrite_rule @{thms id_simps} thm |
233 MetaSimplifier.rewrite_rule @{thms id_simps} thm |
234 *} |
234 *} |
235 |
235 |
236 section {* Debugging infrastructure for testing tactics *} |
236 section {* Debugging infrastructure for testing tactics *} |
237 |
237 |
238 ML {* |
238 |
239 fun fst_prem_str ctxt [] = "No subgoals" |
239 |
240 | fst_prem_str ctxt thms = (hd thms) |> Syntax.string_of_term ctxt |
240 ML {* |
241 *} |
241 fun my_print_tac ctxt s i thm = |
242 |
|
243 ML {* |
|
244 fun my_print_tac ctxt s thm = |
|
245 let |
242 let |
246 val _ = tracing (s ^ "\n" ^ (fst_prem_str ctxt (prems_of thm))) |
243 val prem_str = nth (prems_of thm) (i - 1) |
|
244 |> Syntax.string_of_term ctxt |
|
245 handle Subscript => "no subgoal" |
|
246 val _ = tracing (s ^ "\n" ^ prem_str) |
247 in |
247 in |
248 Seq.single thm |
248 Seq.single thm |
|
249 end *} |
|
250 |
|
251 |
|
252 ML {* |
|
253 fun DT ctxt s tac i thm = |
|
254 let |
|
255 val before_goal = nth (prems_of thm) (i - 1) |
|
256 |> Syntax.string_of_term ctxt |
|
257 val before_msg = ["before: " ^ s, before_goal, "after: " ^ s] |
|
258 |> cat_lines |
|
259 in |
|
260 EVERY [tac i, my_print_tac ctxt before_msg i] thm |
249 end |
261 end |
250 *} |
|
251 |
|
252 ML {* |
|
253 fun DT ctxt s tac i thm = |
|
254 let |
|
255 val fst_goal_start = fst_prem_str ctxt (prems_of thm) |
|
256 in |
|
257 EVERY [tac i, |
|
258 my_print_tac ctxt (cat_lines ["before: " ^ s, fst_goal_start, "after: " ^ s])] thm |
|
259 end |
|
260 |
262 |
261 fun NDT ctxt s tac thm = tac thm |
263 fun NDT ctxt s tac thm = tac thm |
262 *} |
264 *} |
263 |
265 |
264 section {* Infrastructure about definitions *} |
266 section {* Infrastructure about definitions *} |
890 E) simplifying (= ===> =) for simpler respectfulness |
892 E) simplifying (= ===> =) for simpler respectfulness |
891 |
893 |
892 *) |
894 *) |
893 |
895 |
894 ML {* |
896 ML {* |
895 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
897 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
896 (FIRST' [ |
898 (FIRST' [ |
897 (* "cong" rule of the of the relation / transitivity*) |
899 (* "cong" rule of the of the relation / transitivity*) |
898 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
900 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
899 NDT ctxt "1" (resolve_tac trans2), |
901 NDT ctxt "1" (resolve_tac trans2), |
900 |
902 |
912 |
914 |
913 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
915 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
914 NDT ctxt "6" (bex_rsp_tac ctxt), |
916 NDT ctxt "6" (bex_rsp_tac ctxt), |
915 |
917 |
916 (* respectfulness of constants *) |
918 (* respectfulness of constants *) |
917 DT ctxt "7" (resolve_tac rsp_thms), |
919 NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)), |
918 |
920 |
919 (* reflexivity of operators arising from Cong_tac *) |
921 (* reflexivity of operators arising from Cong_tac *) |
920 NDT ctxt "8" (rtac @{thm refl}), |
922 NDT ctxt "8" (rtac @{thm refl}), |
921 |
923 |
922 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
924 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
952 (* global simplification *) |
954 (* global simplification *) |
953 NDT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
955 NDT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
954 *} |
956 *} |
955 |
957 |
956 ML {* |
958 ML {* |
957 fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
959 fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = |
958 REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms) |
960 REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2) |
959 *} |
961 *} |
960 |
962 |
961 |
963 |
962 section {* Cleaning of the theorem *} |
964 section {* Cleaning of the theorem *} |
963 |
965 |
1192 end) lthy |
1194 end) lthy |
1193 *} |
1195 *} |
1194 |
1196 |
1195 ML {* |
1197 ML {* |
1196 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1198 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *) |
1197 fun lift_tac lthy rthm rel_eqv rty quot rsp_thms defs = |
1199 fun lift_tac lthy rthm rel_eqv rty quot defs = |
1198 ObjectLogic.full_atomize_tac |
1200 ObjectLogic.full_atomize_tac |
1199 THEN' gen_frees_tac lthy |
1201 THEN' gen_frees_tac lthy |
1200 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1202 THEN' Subgoal.FOCUS (fn {context, concl, ...} => |
1201 let |
1203 let |
1202 val rthm' = atomize_thm rthm |
1204 val rthm' = atomize_thm rthm |