1042 |
1042 |
1043 ML {* |
1043 ML {* |
1044 fun lambda_allex_prs_simple_conv ctxt ctrm = |
1044 fun lambda_allex_prs_simple_conv ctxt ctrm = |
1045 case (term_of ctrm) of |
1045 case (term_of ctrm) of |
1046 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1046 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1047 let |
1047 let |
1048 val (ty_b, ty_a) = dest_fun_type (fastype_of r1); |
1048 val (ty_b, ty_a) = dest_fun_type (fastype_of r1); |
1049 val (ty_c, ty_d) = dest_fun_type (fastype_of a2); |
1049 val (ty_c, ty_d) = dest_fun_type (fastype_of a2); |
1050 val thy = ProofContext.theory_of ctxt; |
1050 val thy = ProofContext.theory_of ctxt; |
1051 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1051 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1052 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1052 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1053 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}; |
1053 val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}; |
1054 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1054 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1055 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1055 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1056 val tl = Thm.lhs_of ts; |
1056 val tl = Thm.lhs_of ts; |
1057 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
1057 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
1058 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1058 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1059 in |
1059 in |
1060 Conv.rewr_conv ti ctrm |
1060 Conv.rewr_conv ti ctrm |
1061 end |
1061 end |
1062 | (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
|
1063 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
|
1064 let |
|
1065 val (ty_a, ty_b) = dest_fun_type (fastype_of absf); |
|
1066 val thy = ProofContext.theory_of ctxt; |
|
1067 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
|
1068 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
|
1069 val thm = Drule.instantiate' tyinst tinst @{thm all_prs}; |
|
1070 val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; |
|
1071 in |
|
1072 Conv.rewr_conv ti ctrm |
|
1073 end |
|
1074 | (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
|
1075 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
|
1076 let |
|
1077 val (ty_a, ty_b) = dest_fun_type (fastype_of absf); |
|
1078 val thy = ProofContext.theory_of ctxt; |
|
1079 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
|
1080 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
|
1081 val thm = Drule.instantiate' tyinst tinst @{thm ex_prs}; |
|
1082 val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; |
|
1083 in |
|
1084 Conv.rewr_conv ti ctrm |
|
1085 end |
|
1086 | _ => Conv.all_conv ctrm |
1062 | _ => Conv.all_conv ctrm |
1087 *} |
1063 *} |
1088 |
1064 |
1089 ML {* |
1065 ML {* |
1090 val lambda_allex_prs_conv = |
1066 val lambda_allex_prs_conv = |
1091 More_Conv.top_conv lambda_allex_prs_simple_conv |
1067 More_Conv.top_conv lambda_allex_prs_simple_conv |
1092 *} |
1068 |
1093 |
|
1094 ML {* |
|
1095 fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt) |
1069 fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt) |
1096 *} |
1070 *} |
1097 |
1071 |
1098 (* |
1072 (* |
1099 Cleaning the theorem consists of 6 kinds of rewrites. |
1073 Cleaning the theorem consists of 6 kinds of rewrites. |
1119 The first one is implemented as a conversion (fast). |
1093 The first one is implemented as a conversion (fast). |
1120 The second one is an EqSubst (slow). |
1094 The second one is an EqSubst (slow). |
1121 The rest are a simp_tac and are fast. |
1095 The rest are a simp_tac and are fast. |
1122 *) |
1096 *) |
1123 |
1097 |
1124 ML {* fun OF1 thm1 thm2 = thm2 RS thm1 *} |
|
1125 ML {* |
1098 ML {* |
1126 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
1099 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
1127 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
1100 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
1128 *} |
1101 *} |
1129 |
1102 |
1130 ML {* |
1103 ML {* |
1131 fun clean_tac lthy = |
1104 fun clean_tac lthy = |
1132 let |
1105 let |
1133 val thy = ProofContext.theory_of lthy; |
1106 val thy = ProofContext.theory_of lthy; |
1134 val defs = map (Thm.varifyT o #def) (qconsts_dest thy) |
1107 val defs = map (Thm.varifyT o #def) (qconsts_dest thy) |
1135 val thms = @{thms eq_reflection[OF fun_map.simps]} |
1108 val thms1 = @{thms all_prs ex_prs} |
1136 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1109 val thms2 = @{thms eq_reflection[OF fun_map.simps]} |
1137 @ defs |
1110 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1138 val simp_ctxt = HOL_basic_ss addsimps thms addSolver quotient_solver |
1111 @ defs |
|
1112 fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver |
|
1113 (* FIXME: use of someting smaller than HOL_basic_ss *) |
1139 in |
1114 in |
1140 EVERY' [ |
1115 EVERY' [ |
1141 (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x))) ----> f *) |
1116 (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x))) ----> f *) |
|
1117 NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), |
|
1118 |
1142 (* Ball (Respects R) ((abs ---> id) f) ----> All f *) |
1119 (* Ball (Respects R) ((abs ---> id) f) ----> All f *) |
1143 NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), |
1120 NDT lthy "b" (simp_tac (simp_ctxt thms1)), |
1144 |
1121 |
1145 (* NewConst -----> (rep ---> abs) oldConst *) |
1122 (* NewConst -----> (rep ---> abs) oldConst *) |
1146 (* abs (rep x) -----> x *) |
1123 (* abs (rep x) -----> x *) |
1147 (* R (Rep x) (Rep y) -----> x = y *) |
1124 (* R (Rep x) (Rep y) -----> x = y *) |
1148 (* id_simps; fun_map.simps *) |
1125 (* id_simps; fun_map.simps *) |
1149 NDT lthy "c" (TRY o simp_tac simp_ctxt), |
1126 NDT lthy "c" (simp_tac (simp_ctxt thms2)), |
1150 |
1127 |
1151 (* final step *) |
1128 (* final step *) |
1152 NDT lthy "d" (TRY o rtac refl) |
1129 NDT lthy "d" (TRY o rtac refl) |
1153 ] |
1130 ] |
1154 end |
1131 end |
1223 val rtrm' = HOLogic.dest_Trueprop rtrm |
1200 val rtrm' = HOLogic.dest_Trueprop rtrm |
1224 val qtrm' = HOLogic.dest_Trueprop qtrm |
1201 val qtrm' = HOLogic.dest_Trueprop qtrm |
1225 val reg_goal = |
1202 val reg_goal = |
1226 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
1203 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
1227 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1204 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1228 val _ = tracing "Regularization done." |
1205 val _ = warning "Regularization done." |
1229 val inj_goal = |
1206 val inj_goal = |
1230 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
1207 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
1231 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1208 handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm |
1232 val _ = tracing "RepAbs Injection done." |
1209 val _ = warning "RepAbs Injection done." |
1233 in |
1210 in |
1234 Drule.instantiate' [] |
1211 Drule.instantiate' [] |
1235 [SOME (cterm_of thy rtrm'), |
1212 [SOME (cterm_of thy rtrm'), |
1236 SOME (cterm_of thy reg_goal), |
1213 SOME (cterm_of thy reg_goal), |
1237 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |
1214 SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} |