222 handle Subscript => "no subgoal" |
222 handle Subscript => "no subgoal" |
223 val _ = tracing (s ^ "\n" ^ prem_str) |
223 val _ = tracing (s ^ "\n" ^ prem_str) |
224 in |
224 in |
225 Seq.single thm |
225 Seq.single thm |
226 end *} |
226 end *} |
227 |
|
228 ML {* |
|
229 fun DT ctxt s tac i thm = |
|
230 let |
|
231 val before_goal = nth (prems_of thm) (i - 1) |
|
232 |> Syntax.string_of_term ctxt |
|
233 val before_msg = ["before: " ^ s, before_goal, "after: " ^ s] |
|
234 |> cat_lines |
|
235 in |
|
236 EVERY [tac i, my_print_tac ctxt before_msg i] thm |
|
237 end |
|
238 |
|
239 fun NDT ctxt s tac thm = tac thm |
|
240 *} |
|
241 |
227 |
242 section {* Matching of Terms and Types *} |
228 section {* Matching of Terms and Types *} |
243 |
229 |
244 ML {* |
230 ML {* |
245 fun struct_match_typ (ty, ty') = |
231 fun struct_match_typ (ty, ty') = |
864 *} |
850 *} |
865 |
851 |
866 ML {* |
852 ML {* |
867 fun inj_repabs_step_tac ctxt rel_refl = |
853 fun inj_repabs_step_tac ctxt rel_refl = |
868 (FIRST' [ |
854 (FIRST' [ |
869 NDT ctxt "0" (inj_repabs_tac_match ctxt), |
855 inj_repabs_tac_match ctxt, |
870 (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *) |
856 (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp provided type of t needs lifting *) |
871 |
857 |
872 NDT ctxt "A" (apply_rsp_tac ctxt THEN' |
858 apply_rsp_tac ctxt THEN' |
873 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]), |
859 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
874 |
860 |
875 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
861 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
876 (* merge with previous tactic *) |
862 (* merge with previous tactic *) |
877 NDT ctxt "C" (Cong_Tac.cong_tac @{thm cong} THEN' |
863 Cong_Tac.cong_tac @{thm cong} THEN' |
878 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), |
864 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
879 |
865 |
880 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
866 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
881 NDT ctxt "D" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), |
867 rtac @{thm ext} THEN' quot_true_tac ctxt unlam, |
882 |
868 |
883 (* resolving with R x y assumptions *) |
869 (* resolving with R x y assumptions *) |
884 NDT ctxt "E" (atac), |
870 atac, |
885 |
871 |
886 (* reflexivity of the basic relations *) |
872 (* reflexivity of the basic relations *) |
887 (* R \<dots> \<dots> *) |
873 (* R \<dots> \<dots> *) |
888 NDT ctxt "F" (resolve_tac rel_refl) |
874 resolve_tac rel_refl]) |
889 ]) |
|
890 *} |
875 *} |
891 |
876 |
892 ML {* |
877 ML {* |
893 fun inj_repabs_tac ctxt = |
878 fun inj_repabs_tac ctxt = |
894 let |
879 let |