892 *) |
892 *) |
893 |
893 |
894 ML {* |
894 ML {* |
895 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
895 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
896 (FIRST' [ |
896 (FIRST' [ |
897 (* "cong" rule of the of the relation *) |
897 (* "cong" rule of the of the relation / transitivity*) |
898 (* a \<approx> b = c \<approx> d ----> \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> *) |
898 (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) |
899 NDT ctxt "1" (resolve_tac trans2), |
899 NDT ctxt "1" (resolve_tac trans2), |
900 |
900 |
901 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
901 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
902 NDT ctxt "2" (lambda_res_tac ctxt), |
902 NDT ctxt "2" (lambda_res_tac ctxt), |
903 |
903 |
912 |
912 |
913 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
913 (* (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), |
914 NDT ctxt "6" (bex_rsp_tac ctxt), |
915 |
915 |
916 (* respectfulness of constants *) |
916 (* respectfulness of constants *) |
917 NDT ctxt "7" (resolve_tac rsp_thms), |
917 DT ctxt "7" (resolve_tac rsp_thms), |
918 |
918 |
919 (* reflexivity of operators arising from Cong_tac *) |
919 (* reflexivity of operators arising from Cong_tac *) |
920 NDT ctxt "8" (rtac @{thm refl}), |
920 NDT ctxt "8" (rtac @{thm refl}), |
921 |
921 |
922 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
922 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
923 (* observe ---> *) |
923 (* observe ---> *) |
924 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
924 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
925 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
925 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
926 |
926 |
927 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
927 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
928 NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
928 NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
929 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
929 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
930 |
930 |
931 (* (op =) (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided type of t does not need lifting *) |
931 (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) |
932 (* merge with previous tactic *) |
932 (* merge with previous tactic *) |
933 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
933 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
934 |
934 |
935 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
935 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
936 NDT ctxt "C" (rtac @{thm ext}), |
936 NDT ctxt "C" (rtac @{thm ext}), |
937 |
937 |
938 (* reflexivity of the basic relations *) |
938 (* reflexivity of the basic relations *) |
|
939 (* R \<dots> \<dots> *) |
939 NDT ctxt "D" (resolve_tac rel_refl), |
940 NDT ctxt "D" (resolve_tac rel_refl), |
940 |
941 |
941 (* resolving with R x y assumptions *) |
942 (* resolving with R x y assumptions *) |
942 NDT ctxt "E" (atac), |
943 NDT ctxt "E" (atac), |
943 |
944 |