235 *} |
235 *} |
236 |
236 |
237 section {* Debugging infrastructure for testing tactics *} |
237 section {* Debugging infrastructure for testing tactics *} |
238 |
238 |
239 ML {* |
239 ML {* |
|
240 fun fst_prem_str ctxt [] = "No subgoals" |
|
241 | fst_prem_str ctxt thms = (hd thms) |> Syntax.string_of_term ctxt |
|
242 *} |
|
243 |
|
244 ML {* |
240 fun my_print_tac ctxt s thm = |
245 fun my_print_tac ctxt s thm = |
241 let |
246 let |
242 val prems_str = prems_of thm |
247 val _ = tracing (s ^ "\n" ^ (fst_prem_str ctxt (prems_of thm))) |
243 |> map (Syntax.string_of_term ctxt) |
|
244 |> cat_lines |
|
245 val _ = tracing (s ^ "\n" ^ prems_str) |
|
246 in |
248 in |
247 Seq.single thm |
249 Seq.single thm |
248 end |
250 end |
249 |
251 *} |
250 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] |
252 |
251 |
253 ML {* |
252 fun NDT ctxt s tac = tac |
254 fun DT ctxt s tac i thm = |
|
255 let |
|
256 val fst_goal_start = fst_prem_str ctxt (prems_of thm) |
|
257 in |
|
258 EVERY [tac i, |
|
259 my_print_tac ctxt (cat_lines ["before: " ^ s, fst_goal_start, "after: " ^ s])] thm |
|
260 end |
|
261 |
|
262 fun NDT ctxt s tac thm = tac thm |
253 *} |
263 *} |
254 |
264 |
255 section {* Infrastructure about definitions *} |
265 section {* Infrastructure about definitions *} |
256 |
266 |
257 (* Does the same as 'subst' in a given theorem *) |
267 (* Does the same as 'subst' in a given theorem *) |
901 *) |
911 *) |
902 |
912 |
903 ML {* |
913 ML {* |
904 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
914 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
905 (FIRST' [ |
915 (FIRST' [ |
906 (*(K (print_tac "start")) THEN' (K no_tac), *) |
|
907 |
|
908 (* "cong" rule of the of the relation *) |
916 (* "cong" rule of the of the relation *) |
909 (* a \<approx> b = c \<approx> d ----> \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> *) |
917 (* a \<approx> b = c \<approx> d ----> \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> *) |
910 NDT ctxt "1" (resolve_tac trans2), |
918 NDT ctxt "1" (resolve_tac trans2), |
911 |
919 |
912 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
920 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
913 NDT ctxt "2" (lambda_res_tac ctxt), |
921 NDT ctxt "2" (lambda_res_tac ctxt), |
914 |
922 |
915 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
923 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
916 NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
924 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
917 |
925 |
918 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
926 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
919 NDT ctxt "4" (ball_rsp_tac ctxt), |
927 DT ctxt "4" (ball_rsp_tac ctxt), |
920 |
928 |
921 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
929 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
922 NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
930 NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
923 |
931 |
924 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
932 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |