929 ML {* |
929 ML {* |
930 fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
930 fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
931 (FIRST' [ |
931 (FIRST' [ |
932 (K (print_tac "start")) THEN' (K no_tac), |
932 (K (print_tac "start")) THEN' (K no_tac), |
933 |
933 |
934 (* "cong" rule of the of the relation *) |
934 (* "cong" rule of the of the relation *) |
935 (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> a \<approx> b = c \<approx> d *) |
935 (* a \<approx> b = c \<approx> d ----> \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> *) |
936 DT ctxt "1" (resolve_tac trans2), |
936 DT ctxt "1" (resolve_tac trans2), |
937 |
937 |
938 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
938 (* (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), |
939 DT ctxt "2" (lambda_res_tac ctxt), |
940 |
940 |
941 (* = (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *) |
941 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
942 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
942 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
943 |
943 |
944 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
944 (* (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), |
945 DT ctxt "4" (ball_rsp_tac ctxt), |
946 |
946 |
947 (* = (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *) |
947 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
948 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
948 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
949 |
949 |
950 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
950 (* (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), |
951 DT ctxt "6" (bex_rsp_tac ctxt), |
952 |
952 |
953 (* respectfulness of constants *) |
953 (* respectfulness of constants *) |
954 DT ctxt "7" (resolve_tac rsp_thms), |
954 DT ctxt "7" (resolve_tac rsp_thms), |
955 |
955 |
956 (* reflexivity of operators arising from Cong_tac *) |
956 (* reflexivity of operators arising from Cong_tac *) |
957 DT ctxt "8" (rtac @{thm refl}), |
957 DT ctxt "8" (rtac @{thm refl}), |
958 |
958 |
959 (* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *) |
959 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
960 (* observe ---> *) |
960 (* observe ---> *) |
961 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
961 DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
962 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
962 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
963 |
963 |
964 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
964 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *) |
966 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
966 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
967 |
967 |
968 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *) |
968 (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *) |
969 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
969 DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), |
970 |
970 |
971 (* = (\<lambda>x\<dots>) (\<lambda>x\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *) |
971 (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
972 DT ctxt "C" (rtac @{thm ext}), |
972 DT ctxt "C" (rtac @{thm ext}), |
973 |
973 |
974 (* reflexivity of the basic relations *) |
974 (* reflexivity of the basic relations *) |
975 DT ctxt "D" (resolve_tac rel_refl), |
975 DT ctxt "D" (resolve_tac rel_refl), |
976 |
976 |
977 (* resolving with R x y assumptions *) |
977 (* resolving with R x y assumptions *) |
978 DT ctxt "E" (atac), |
978 DT ctxt "E" (atac), |
979 |
979 |
980 (* seems not necessay:: DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*) |
980 (* seems not necessay:: DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*) |
|
981 |
|
982 (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
|
983 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
981 DT ctxt "G" (weak_lambda_res_tac ctxt), |
984 DT ctxt "G" (weak_lambda_res_tac ctxt), |
982 |
985 |
983 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed to apply respectfulness theorems *) |
986 (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) |
984 (* works globally *) |
987 (* global simplification *) |
985 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
988 DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]) |
986 |
989 *} |
|
990 |
|
991 ML {* |
987 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
992 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms = |
988 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
993 REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms) |
989 *} |
994 *} |
990 |
995 |
991 |
996 |