925 |
926 |
926 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
927 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
927 NDT ctxt "2" (lambda_res_tac ctxt), |
928 NDT ctxt "2" (lambda_res_tac ctxt), |
928 |
929 |
929 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
930 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
930 NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
931 NDT ctxt "3" (rtac @{thm ball_rsp}), |
931 |
932 |
932 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
933 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
933 NDT ctxt "4" (ball_rsp_tac ctxt), |
934 NDT ctxt "4" (ball_rsp_tac ctxt), |
934 |
935 |
935 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
936 (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
936 NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
937 NDT ctxt "5" (rtac @{thm bex_rsp}), |
937 |
938 |
938 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
939 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
939 NDT ctxt "6" (bex_rsp_tac ctxt), |
940 NDT ctxt "6" (bex_rsp_tac ctxt), |
940 |
941 |
941 (* respectfulness of constants *) |
942 (* respectfulness of constants *) |
944 (* reflexivity of operators arising from Cong_tac *) |
945 (* reflexivity of operators arising from Cong_tac *) |
945 NDT ctxt "8" (rtac @{thm refl}), |
946 NDT ctxt "8" (rtac @{thm refl}), |
946 |
947 |
947 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
948 (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) |
948 (* observe ---> *) |
949 (* observe ---> *) |
949 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt |
950 NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt |
950 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
951 THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))), |
951 |
952 |
952 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
953 (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) |
953 NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
954 NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' |
954 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
955 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))), |
1028 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm) |
1029 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm) |
1029 *} |
1030 *} |
1030 |
1031 |
1031 ML {* |
1032 ML {* |
1032 fun allex_prs_tac lthy quot = |
1033 fun allex_prs_tac lthy quot = |
1033 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
1034 (EqSubst.eqsubst_tac lthy [0] @{thms all_prs ex_prs}) THEN' (quotient_tac quot) |
1034 THEN' (quotient_tac quot) |
|
1035 *} |
1035 *} |
1036 |
1036 |
1037 (* Rewrites the term with LAMBDA_PRS thm. |
1037 (* Rewrites the term with LAMBDA_PRS thm. |
1038 |
1038 |
1039 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) |
1039 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) |
1100 (Conv.params_conv ~1 (fn ctxt => |
1100 (Conv.params_conv ~1 (fn ctxt => |
1101 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1101 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
1102 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1102 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
1103 *} |
1103 *} |
1104 |
1104 |
|
1105 (* |
|
1106 Cleaning the theorem consists of 5 kinds of rewrites. |
|
1107 These rewrites can be done independently and in any order. |
|
1108 |
|
1109 - LAMBDA_PRS: |
|
1110 (Rep1 ---> Abs2) (\<lambda>x. Rep2 (?f (Abs1 x))) \<equiv> ?f |
|
1111 - Rewriting with definitions from the argument defs |
|
1112 (Abs) OldConst (Rep Args) \<equiv> NewConst Args |
|
1113 - QUOTIENT_REL_REP: |
|
1114 Rel (Rep x) (Rep y) \<equiv> x = y |
|
1115 - FORALL_PRS (and the same for exists: EXISTS_PRS) |
|
1116 \<forall>x\<in>Respects R. (abs ---> id) ?f \<equiv> \<forall>x. ?f |
|
1117 - applic_prs |
|
1118 Abs1 ((Abs2 --> Rep1) f (Rep2 args)) \<equiv> f args |
|
1119 |
|
1120 The first one is implemented as a conversion (fast). |
|
1121 The second and third one are a simp_tac (fast). |
|
1122 The last two are EqSubst (slow). |
|
1123 *) |
1105 ML {* |
1124 ML {* |
1106 fun clean_tac lthy quot defs aps = |
1125 fun clean_tac lthy quot defs aps = |
1107 let |
1126 let |
1108 val lower = flat (map (add_lower_defs lthy) defs) |
1127 val lower = flat (map (add_lower_defs lthy) defs) |
1109 val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower |
1128 val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower |