875 |
875 |
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 {* |
|
881 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
|
882 (FIRST' [resolve_tac trans2, |
|
883 lambda_res_tac ctxt, |
|
884 rtac @{thm RES_FORALL_RSP}, |
|
885 ball_rsp_tac ctxt, |
|
886 rtac @{thm RES_EXISTS_RSP}, |
|
887 bex_rsp_tac ctxt, |
|
888 resolve_tac rsp_thms, |
|
889 rtac @{thm refl}, |
|
890 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' |
|
891 (RANGE [SOLVES' (quotient_tac quot_thms)])), |
|
892 (APPLY_RSP_TAC rty ctxt THEN' |
|
893 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])), |
|
894 Cong_Tac.cong_tac @{thm cong}, |
|
895 rtac @{thm ext}, |
|
896 resolve_tac rel_refl, |
|
897 atac, |
|
898 (*seems not necessary:: SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),*) |
|
899 weak_lambda_res_tac ctxt, |
|
900 CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]) |
|
901 |
|
902 fun all_inj_repabs_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 *} |
|
905 |
|
906 (* |
880 (* |
907 To prove that the regularised theorem implies the abs/rep injected, |
881 To prove that the regularised theorem implies the abs/rep injected, |
908 we try: |
882 we try: |
909 |
883 |
910 1) theorems 'trans2' from the appropriate QUOT_TYPE |
884 1) theorems 'trans2' from the appropriate QUOT_TYPE |
925 E) simplifying (= ===> =) for simpler respectfulness |
899 E) simplifying (= ===> =) for simpler respectfulness |
926 |
900 |
927 *) |
901 *) |
928 |
902 |
929 ML {* |
903 ML {* |
930 fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
904 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
931 (FIRST' [ |
905 (FIRST' [ |
932 (K (print_tac "start")) THEN' (K no_tac), |
906 (*(K (print_tac "start")) THEN' (K no_tac), *) |
933 |
907 |
934 (* "cong" rule of the of the relation *) |
908 (* "cong" rule of the of the relation *) |
935 (* a \<approx> b = c \<approx> d ----> \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> *) |
909 (* a \<approx> b = c \<approx> d ----> \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> *) |
936 DT ctxt "1" (resolve_tac trans2), |
910 NDT ctxt "1" (resolve_tac trans2), |
937 |
911 |
938 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
912 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
939 DT ctxt "2" (lambda_res_tac ctxt), |
913 NDT ctxt "2" (lambda_res_tac ctxt), |
940 |
914 |
941 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
915 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
942 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
916 NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
943 |
917 |
944 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
918 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
945 DT ctxt "4" (ball_rsp_tac ctxt), |
919 NDT ctxt "4" (ball_rsp_tac ctxt), |
946 |
920 |
947 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
921 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
948 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
922 NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
949 |
923 |
950 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
924 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
951 DT ctxt "6" (bex_rsp_tac ctxt), |
925 NDT ctxt "6" (bex_rsp_tac ctxt), |
952 |
926 |
953 (* respectfulness of constants *) |
927 (* respectfulness of constants *) |
954 DT ctxt "7" (resolve_tac rsp_thms), |
928 NDT ctxt "7" (resolve_tac rsp_thms), |
955 |
929 |
956 (* reflexivity of operators arising from Cong_tac *) |
930 (* reflexivity of operators arising from Cong_tac *) |
957 DT ctxt "8" (rtac @{thm refl}), |
931 NDT ctxt "8" (rtac @{thm refl}), |
958 |
932 |
959 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
933 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
960 (* observe ---> *) |
934 (* observe ---> *) |
961 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
935 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
962 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
936 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
963 |
937 |
964 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
938 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
965 DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
939 NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
966 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
940 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
967 |
941 |
968 (* (op =) (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided type of t does not need lifting *) |
942 (* (op =) (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided type of t does not need lifting *) |
969 (* merge with previous tactic *) |
943 (* merge with previous tactic *) |
970 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
944 NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
971 |
945 |
972 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
946 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
973 DT ctxt "C" (rtac @{thm ext}), |
947 NDT ctxt "C" (rtac @{thm ext}), |
974 |
948 |
975 (* reflexivity of the basic relations *) |
949 (* reflexivity of the basic relations *) |
976 DT ctxt "D" (resolve_tac rel_refl), |
950 NDT ctxt "D" (resolve_tac rel_refl), |
977 |
951 |
978 (* resolving with R x y assumptions *) |
952 (* resolving with R x y assumptions *) |
979 DT ctxt "E" (atac), |
953 NDT ctxt "E" (atac), |
980 |
954 |
981 (* seems not necessay:: DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*) |
955 (* seems not necessay:: NDT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*) |
982 |
956 |
983 (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
957 (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
984 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
958 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
985 DT ctxt "G" (weak_lambda_res_tac ctxt), |
959 NDT ctxt "G" (weak_lambda_res_tac ctxt), |
986 |
960 |
987 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
961 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
988 (* global simplification *) |
962 (* global simplification *) |
989 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
963 NDT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
990 *} |
964 *} |
991 |
965 |
992 ML {* |
966 ML {* |
993 fun all_inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
967 fun all_inj_repabs_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) |
968 REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms) |
995 *} |
969 *} |
996 |
970 |
997 |
971 |
998 section {* Cleaning of the theorem *} |
972 section {* Cleaning of the theorem *} |
999 |
973 |