863 |
863 |
864 ML {* |
864 ML {* |
865 val APPLY_RSP1_TAC' = |
865 val APPLY_RSP1_TAC' = |
866 Subgoal.FOCUS (fn {concl, asms, context,...} => |
866 Subgoal.FOCUS (fn {concl, asms, context,...} => |
867 case ((HOLogic.dest_Trueprop (term_of concl))) of |
867 case ((HOLogic.dest_Trueprop (term_of concl))) of |
868 ((R2 $ (f $ x) $ (g $ y))) => |
868 ((R2 $ (f $ x) $ (g $ y))) => |
869 let |
869 let |
870 val (asmf, asma) = find_qt_asm (map term_of asms); |
870 val (asmf, asma) = find_qt_asm (map term_of asms); |
|
871 in |
|
872 if (fastype_of asmf) = (fastype_of f) then no_tac else let |
|
873 val ty_a = fastype_of x; |
|
874 val ty_b = fastype_of asma; |
|
875 val ty_c = range_type (type_of f); |
|
876 val thy = ProofContext.theory_of context; |
|
877 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; |
|
878 val thm = Drule.instantiate' ty_inst [] @{thm APPLY_RSP1} |
|
879 val te = solve_quotient_assums context thm |
|
880 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
|
881 val thm = Drule.instantiate' [] t_inst te |
871 in |
882 in |
872 if (fastype_of asmf) = (fastype_of f) then no_tac else let |
883 compose_tac (false, thm, 2) 1 |
873 val ty_a = fastype_of x; |
|
874 val ty_b = fastype_of asma; |
|
875 val ty_c = range_type (type_of f); |
|
876 val thy = ProofContext.theory_of context; |
|
877 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; |
|
878 val thm = Drule.instantiate' ty_inst [] @{thm APPLY_RSP1} |
|
879 val te = solve_quotient_assums context thm |
|
880 val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; |
|
881 val thm = Drule.instantiate' [] t_inst te |
|
882 in |
|
883 (* TODO try sth like: compose_tac (false, thm, 1) 1 *) |
|
884 rtac thm 1 |
|
885 end |
|
886 end |
884 end |
887 | _ => no_tac) |
885 end |
|
886 | _ => no_tac) |
888 *} |
887 *} |
889 |
888 |
890 ML {* |
889 ML {* |
891 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
890 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
892 *} |
891 *} |
1117 | _ => t); |
1116 | _ => t); |
1118 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1117 in (f, Abs ("x", T, mk_abs 0 g)) end; |
1119 *} |
1118 *} |
1120 |
1119 |
1121 ML {* |
1120 ML {* |
|
1121 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
|
1122 | dest_fun_type _ = error "dest_fun_type" |
|
1123 *} |
|
1124 |
|
1125 |
|
1126 ML {* |
1122 fun lambda_allex_prs_simple_conv ctxt ctrm = |
1127 fun lambda_allex_prs_simple_conv ctxt ctrm = |
1123 case (term_of ctrm) of |
1128 case (term_of ctrm) of |
1124 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1129 ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) => |
1125 let |
1130 let |
1126 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
1131 val (ty_b, ty_a) = dest_fun_type (fastype_of r1); |
1127 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); |
1132 val (ty_c, ty_d) = dest_fun_type (fastype_of a2); |
1128 val thy = ProofContext.theory_of ctxt; |
1133 val thy = ProofContext.theory_of ctxt; |
1129 val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d] |
1134 val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] |
1130 val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; |
|
1131 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1135 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
1132 val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; |
1136 val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; |
1133 val te = @{thm eq_reflection} OF [solve_quotient_assum 2 ctxt lpi] |
1137 val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] |
1134 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1138 val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te |
1135 val tl = Thm.lhs_of ts; |
1139 val tl = Thm.lhs_of ts; |
1136 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
1140 val (insp, inst) = make_inst (term_of tl) (term_of ctrm); |
1137 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1141 val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts; |
1138 in |
1142 in |
1139 Conv.rewr_conv ti ctrm |
1143 Conv.rewr_conv ti ctrm |
1140 end |
1144 end |
1141 | (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
1145 | (Const (@{const_name Ball}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
1142 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
1146 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
1143 let |
1147 let |
1144 val (_, [ty_a, ty_b]) = dest_Type (fastype_of absf); |
1148 val (ty_a, ty_b) = dest_fun_type (fastype_of absf); |
1145 val thy = ProofContext.theory_of ctxt; |
1149 val thy = ProofContext.theory_of ctxt; |
1146 val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
1150 val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
1147 val tyinst = [SOME cty_a, SOME cty_b]; |
1151 val tyinst = [SOME cty_a, SOME cty_b]; |
1148 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1152 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1149 val thm = Drule.instantiate' tyinst tinst @{thm all_prs}; |
1153 val thm = Drule.instantiate' tyinst tinst @{thm all_prs}; |
1150 val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm]; |
1154 val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; |
1151 in |
1155 in |
1152 Conv.rewr_conv ti ctrm |
1156 Conv.rewr_conv ti ctrm |
1153 end |
1157 end |
1154 | (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
1158 | (Const (@{const_name Bex}, _) $ (Const (@{const_name Respects}, _) $ R) $ |
1155 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
1159 (((Const (@{const_name fun_map}, _) $ absf $ (Const (@{const_name id}, _)))) $ f)) => |
1156 let |
1160 let |
1157 val (_, [ty_a, ty_b]) = dest_Type (fastype_of absf); |
1161 val (ty_a, ty_b) = dest_fun_type (fastype_of absf); |
1158 val thy = ProofContext.theory_of ctxt; |
1162 val thy = ProofContext.theory_of ctxt; |
1159 val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
1163 val (cty_a, cty_b) = (ctyp_of thy ty_a, ctyp_of thy ty_b); |
1160 val tyinst = [SOME cty_a, SOME cty_b]; |
1164 val tyinst = [SOME cty_a, SOME cty_b]; |
1161 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1165 val tinst = [SOME (cterm_of thy R), SOME (cterm_of thy absf), NONE, SOME (cterm_of thy f)]; |
1162 val thm = Drule.instantiate' tyinst tinst @{thm ex_prs}; |
1166 val thm = Drule.instantiate' tyinst tinst @{thm ex_prs}; |
1163 val ti = @{thm eq_reflection} OF [solve_quotient_assum 1 ctxt thm]; |
1167 val ti = @{thm eq_reflection} OF [solve_quotient_assums ctxt thm]; |
1164 in |
1168 in |
1165 Conv.rewr_conv ti ctrm |
1169 Conv.rewr_conv ti ctrm |
1166 end |
1170 end |
1167 | _ => Conv.all_conv ctrm |
1171 | _ => Conv.all_conv ctrm |
1168 *} |
1172 *} |
1169 |
1173 |
1170 (* quot stands for the QUOTIENT theorems: *) |
|
1171 (* could be potentially all of them *) |
|
1172 ML {* |
1174 ML {* |
1173 val lambda_allex_prs_conv = |
1175 val lambda_allex_prs_conv = |
1174 More_Conv.top_conv lambda_allex_prs_simple_conv |
1176 More_Conv.top_conv lambda_allex_prs_simple_conv |
1175 *} |
1177 *} |
1176 |
1178 |
1177 ML {* |
1179 ML {* |
1178 fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt) |
1180 fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt) |
1179 *} |
1181 *} |