179 val n = length xs; |
179 val n = length xs; |
180 val Q = if n = 0 then P else renumber 0 n P; |
180 val Q = if n = 0 then P else renumber 0 n P; |
181 in quant xs (qC $ Abs (x, T, Q)) end; |
181 in quant xs (qC $ Abs (x, T, Q)) end; |
182 |
182 |
183 fun rearrange_all ctxt ct = |
183 fun rearrange_all ctxt ct = |
184 (case term_of ct of |
184 (case Thm.term_of ct of |
185 F as (all as Const (q, _)) $ Abs (x, T, P) => |
185 F as (all as Const (q, _)) $ Abs (x, T, P) => |
186 (case extract_quant extract_imp q P of |
186 (case extract_quant extract_imp q P of |
187 NONE => NONE |
187 NONE => NONE |
188 | SOME (xs, eq, Q) => |
188 | SOME (xs, eq, Q) => |
189 let val R = quantify all x T xs (Data.imp $ eq $ Q) |
189 let val R = quantify all x T xs (Data.imp $ eq $ Q) |
190 in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end) |
190 in SOME (prove_conv ctxt (F, R) prove_one_point_all_tac) end) |
191 | _ => NONE); |
191 | _ => NONE); |
192 |
192 |
193 fun rearrange_ball tac ctxt ct = |
193 fun rearrange_ball tac ctxt ct = |
194 (case term_of ct of |
194 (case Thm.term_of ct of |
195 F as Ball $ A $ Abs (x, T, P) => |
195 F as Ball $ A $ Abs (x, T, P) => |
196 (case extract_imp true [] P of |
196 (case extract_imp true [] P of |
197 NONE => NONE |
197 NONE => NONE |
198 | SOME (xs, eq, Q) => |
198 | SOME (xs, eq, Q) => |
199 if not (null xs) then NONE |
199 if not (null xs) then NONE |
201 let val R = Data.imp $ eq $ Q |
201 let val R = Data.imp $ eq $ Q |
202 in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end) |
202 in SOME (prove_conv ctxt (F, Ball $ A $ Abs (x, T, R)) tac) end) |
203 | _ => NONE); |
203 | _ => NONE); |
204 |
204 |
205 fun rearrange_ex ctxt ct = |
205 fun rearrange_ex ctxt ct = |
206 (case term_of ct of |
206 (case Thm.term_of ct of |
207 F as (ex as Const (q, _)) $ Abs (x, T, P) => |
207 F as (ex as Const (q, _)) $ Abs (x, T, P) => |
208 (case extract_quant extract_conj q P of |
208 (case extract_quant extract_conj q P of |
209 NONE => NONE |
209 NONE => NONE |
210 | SOME (xs, eq, Q) => |
210 | SOME (xs, eq, Q) => |
211 let val R = quantify ex x T xs (Data.conj $ eq $ Q) |
211 let val R = quantify ex x T xs (Data.conj $ eq $ Q) |
212 in SOME (prove_conv ctxt (F, R) prove_one_point_ex_tac) end) |
212 in SOME (prove_conv ctxt (F, R) prove_one_point_ex_tac) end) |
213 | _ => NONE); |
213 | _ => NONE); |
214 |
214 |
215 fun rearrange_bex tac ctxt ct = |
215 fun rearrange_bex tac ctxt ct = |
216 (case term_of ct of |
216 (case Thm.term_of ct of |
217 F as Bex $ A $ Abs (x, T, P) => |
217 F as Bex $ A $ Abs (x, T, P) => |
218 (case extract_conj true [] P of |
218 (case extract_conj true [] P of |
219 NONE => NONE |
219 NONE => NONE |
220 | SOME (xs, eq, Q) => |
220 | SOME (xs, eq, Q) => |
221 if not (null xs) then NONE |
221 if not (null xs) then NONE |
222 else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac)) |
222 else SOME (prove_conv ctxt (F, Bex $ A $ Abs (x, T, Data.conj $ eq $ Q)) tac)) |
223 | _ => NONE); |
223 | _ => NONE); |
224 |
224 |
225 fun rearrange_Collect tac ctxt ct = |
225 fun rearrange_Collect tac ctxt ct = |
226 (case term_of ct of |
226 (case Thm.term_of ct of |
227 F as Collect $ Abs (x, T, P) => |
227 F as Collect $ Abs (x, T, P) => |
228 (case extract_conj true [] P of |
228 (case extract_conj true [] P of |
229 NONE => NONE |
229 NONE => NONE |
230 | SOME (_, eq, Q) => |
230 | SOME (_, eq, Q) => |
231 let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q) |
231 let val R = Collect $ Abs (x, T, Data.conj $ eq $ Q) |