182 "[| i<k; !!x.[| x<k; ALL y<x. P(y) |] ==> P(x) |] ==> P(i)" |
184 "[| i<k; !!x.[| x<k; ALL y<x. P(y) |] ==> P(x) |] ==> P(i)" |
183 apply (simp add: lt_def oall_def) |
185 apply (simp add: lt_def oall_def) |
184 apply (erule conjE) |
186 apply (erule conjE) |
185 apply (erule Ord_induct, assumption, blast) |
187 apply (erule Ord_induct, assumption, blast) |
186 done |
188 done |
|
189 |
|
190 |
|
191 subsection {*Quantification over a class*} |
|
192 |
|
193 constdefs |
|
194 "rall" :: "[i=>o, i=>o] => o" |
|
195 "rall(M, P) == ALL x. M(x) --> P(x)" |
|
196 |
|
197 "rex" :: "[i=>o, i=>o] => o" |
|
198 "rex(M, P) == EX x. M(x) & P(x)" |
|
199 |
|
200 syntax |
|
201 "@rall" :: "[pttrn, i=>o, o] => o" ("(3ALL _[_]./ _)" 10) |
|
202 "@rex" :: "[pttrn, i=>o, o] => o" ("(3EX _[_]./ _)" 10) |
|
203 |
|
204 syntax (xsymbols) |
|
205 "@rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10) |
|
206 "@rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10) |
|
207 |
|
208 translations |
|
209 "ALL x[M]. P" == "rall(M, %x. P)" |
|
210 "EX x[M]. P" == "rex(M, %x. P)" |
|
211 |
|
212 (*** Relativized universal quantifier ***) |
|
213 |
|
214 lemma rallI [intro!]: "[| !!x. M(x) ==> P(x) |] ==> ALL x[M]. P(x)" |
|
215 by (simp add: rall_def) |
|
216 |
|
217 lemma rspec: "[| ALL x[M]. P(x); M(x) |] ==> P(x)" |
|
218 by (simp add: rall_def) |
|
219 |
|
220 (*Instantiates x first: better for automatic theorem proving?*) |
|
221 lemma rev_rallE [elim]: |
|
222 "[| ALL x[M]. P(x); ~ M(x) ==> Q; P(x) ==> Q |] ==> Q" |
|
223 by (simp add: rall_def, blast) |
|
224 |
|
225 lemma rallE: "[| ALL x[M]. P(x); P(x) ==> Q; ~ M(x) ==> Q |] ==> Q" |
|
226 by blast |
|
227 |
|
228 (*Trival rewrite rule; (ALL x[M].P)<->P holds only if A is nonempty!*) |
|
229 lemma rall_triv [simp]: "(ALL x[M]. P) <-> ((EX x. M(x)) --> P)" |
|
230 by (simp add: rall_def) |
|
231 |
|
232 (*Congruence rule for rewriting*) |
|
233 lemma rall_cong [cong]: |
|
234 "(!!x. M(x) ==> P(x) <-> P'(x)) ==> rall(M,P) <-> rall(M,P')" |
|
235 by (simp add: rall_def) |
|
236 |
|
237 (*** Relativized existential quantifier ***) |
|
238 |
|
239 lemma rexI [intro]: "[| P(x); M(x) |] ==> EX x[M]. P(x)" |
|
240 by (simp add: rex_def, blast) |
|
241 |
|
242 (*The best argument order when there is only one M(x)*) |
|
243 lemma rev_rexI: "[| M(x); P(x) |] ==> EX x[M]. P(x)" |
|
244 by blast |
|
245 |
|
246 (*Not of the general form for such rules; ~EX has become ALL~ *) |
|
247 lemma rexCI: "[| ALL x[M]. ~P(x) ==> P(a); M(a) |] ==> EX x[M]. P(x)" |
|
248 by blast |
|
249 |
|
250 lemma rexE [elim!]: "[| EX x[M]. P(x); !!x. [| M(x); P(x) |] ==> Q |] ==> Q" |
|
251 by (simp add: rex_def, blast) |
|
252 |
|
253 (*We do not even have (EX x[M]. True) <-> True unless A is nonempty!!*) |
|
254 lemma rex_triv [simp]: "(EX x[M]. P) <-> ((EX x. M(x)) & P)" |
|
255 by (simp add: rex_def) |
|
256 |
|
257 lemma rex_cong [cong]: |
|
258 "(!!x. M(x) ==> P(x) <-> P'(x)) ==> rex(M,P) <-> rex(M,P')" |
|
259 by (simp add: rex_def cong: conj_cong) |
|
260 |
|
261 lemma atomize_rall: "(!!x. M(x) ==> P(x)) == Trueprop (ALL x[M]. P(x))"; |
|
262 by (simp add: rall_def atomize_all atomize_imp) |
|
263 |
|
264 declare atomize_rall [symmetric, rulify] |
|
265 |
|
266 lemma rall_simps1: |
|
267 "(ALL x[M]. P(x) & Q) <-> (ALL x[M]. P(x)) & ((ALL x[M]. False) | Q)" |
|
268 "(ALL x[M]. P(x) | Q) <-> ((ALL x[M]. P(x)) | Q)" |
|
269 "(ALL x[M]. P(x) --> Q) <-> ((EX x[M]. P(x)) --> Q)" |
|
270 "(~(ALL x[M]. P(x))) <-> (EX x[M]. ~P(x))" |
|
271 by blast+ |
|
272 |
|
273 lemma rall_simps2: |
|
274 "(ALL x[M]. P & Q(x)) <-> ((ALL x[M]. False) | P) & (ALL x[M]. Q(x))" |
|
275 "(ALL x[M]. P | Q(x)) <-> (P | (ALL x[M]. Q(x)))" |
|
276 "(ALL x[M]. P --> Q(x)) <-> (P --> (ALL x[M]. Q(x)))" |
|
277 by blast+ |
|
278 |
|
279 lemmas rall_simps = rall_simps1 rall_simps2 |
|
280 |
|
281 lemma rall_conj_distrib: |
|
282 "(ALL x[M]. P(x) & Q(x)) <-> ((ALL x[M]. P(x)) & (ALL x[M]. Q(x)))" |
|
283 by blast |
|
284 |
|
285 lemma rex_simps1: |
|
286 "(EX x[M]. P(x) & Q) <-> ((EX x[M]. P(x)) & Q)" |
|
287 "(EX x[M]. P(x) | Q) <-> (EX x[M]. P(x)) | ((EX x[M]. True) & Q)" |
|
288 "(EX x[M]. P(x) --> Q) <-> ((ALL x[M]. P(x)) --> ((EX x[M]. True) & Q))" |
|
289 "(~(EX x[M]. P(x))) <-> (ALL x[M]. ~P(x))" |
|
290 by blast+ |
|
291 |
|
292 lemma rex_simps2: |
|
293 "(EX x[M]. P & Q(x)) <-> (P & (EX x[M]. Q(x)))" |
|
294 "(EX x[M]. P | Q(x)) <-> ((EX x[M]. True) & P) | (EX x[M]. Q(x))" |
|
295 "(EX x[M]. P --> Q(x)) <-> (((ALL x[M]. False) | P) --> (EX x[M]. Q(x)))" |
|
296 by blast+ |
|
297 |
|
298 lemmas rex_simps = rex_simps1 rex_simps2 |
|
299 |
|
300 lemma rex_disj_distrib: |
|
301 "(EX x[M]. P(x) | Q(x)) <-> ((EX x[M]. P(x)) | (EX x[M]. Q(x)))" |
|
302 by blast |
|
303 |
|
304 |
|
305 (** One-point rule for bounded quantifiers: see HOL/Set.ML **) |
|
306 |
|
307 lemma rex_triv_one_point1 [simp]: "(EX x[M]. x=a) <-> ( M(a))" |
|
308 by blast |
|
309 |
|
310 lemma rex_triv_one_point2 [simp]: "(EX x[M]. a=x) <-> ( M(a))" |
|
311 by blast |
|
312 |
|
313 lemma rex_one_point1 [simp]: "(EX x[M]. x=a & P(x)) <-> ( M(a) & P(a))" |
|
314 by blast |
|
315 |
|
316 lemma rex_one_point2 [simp]: "(EX x[M]. a=x & P(x)) <-> ( M(a) & P(a))" |
|
317 by blast |
|
318 |
|
319 lemma rall_one_point1 [simp]: "(ALL x[M]. x=a --> P(x)) <-> ( M(a) --> P(a))" |
|
320 by blast |
|
321 |
|
322 lemma rall_one_point2 [simp]: "(ALL x[M]. a=x --> P(x)) <-> ( M(a) --> P(a))" |
|
323 by blast |
|
324 |
187 |
325 |
188 ML |
326 ML |
189 {* |
327 {* |
190 val oall_def = thm "oall_def" |
328 val oall_def = thm "oall_def" |
191 val oex_def = thm "oex_def" |
329 val oex_def = thm "oex_def" |
205 val OUN_E = thm "OUN_E"; |
343 val OUN_E = thm "OUN_E"; |
206 val OUN_iff = thm "OUN_iff"; |
344 val OUN_iff = thm "OUN_iff"; |
207 val OUN_cong = thm "OUN_cong"; |
345 val OUN_cong = thm "OUN_cong"; |
208 val lt_induct = thm "lt_induct"; |
346 val lt_induct = thm "lt_induct"; |
209 |
347 |
|
348 val rall_def = thm "rall_def" |
|
349 val rex_def = thm "rex_def" |
|
350 |
|
351 val rallI = thm "rallI"; |
|
352 val rspec = thm "rspec"; |
|
353 val rallE = thm "rallE"; |
|
354 val rev_oallE = thm "rev_oallE"; |
|
355 val rall_cong = thm "rall_cong"; |
|
356 val rexI = thm "rexI"; |
|
357 val rexCI = thm "rexCI"; |
|
358 val rexE = thm "rexE"; |
|
359 val rex_cong = thm "rex_cong"; |
|
360 |
210 val Ord_atomize = |
361 val Ord_atomize = |
211 atomize (("OrdQuant.oall", [ospec])::ZF_conn_pairs, ZF_mem_pairs); |
362 atomize ([("OrdQuant.oall", [ospec]),("OrdQuant.rall", [rspec])]@ |
|
363 ZF_conn_pairs, |
|
364 ZF_mem_pairs); |
212 simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all); |
365 simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all); |
213 *} |
366 *} |
214 |
367 |
|
368 text{*Setting up the one-point-rule simproc*} |
|
369 ML |
|
370 {* |
|
371 |
|
372 let |
|
373 val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
|
374 ("EX x[M]. P(x) & Q(x)", FOLogic.oT) |
|
375 |
|
376 val prove_rex_tac = rewtac rex_def THEN |
|
377 Quantifier1.prove_one_point_ex_tac; |
|
378 |
|
379 val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac; |
|
380 |
|
381 val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) |
|
382 ("ALL x[M]. P(x) --> Q(x)", FOLogic.oT) |
|
383 |
|
384 val prove_rall_tac = rewtac rall_def THEN |
|
385 Quantifier1.prove_one_point_all_tac; |
|
386 |
|
387 val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac; |
|
388 |
|
389 val defREX_regroup = mk_simproc "defined REX" [ex_pattern] rearrange_bex; |
|
390 val defRALL_regroup = mk_simproc "defined RALL" [all_pattern] rearrange_ball; |
|
391 in |
|
392 |
|
393 Addsimprocs [defRALL_regroup,defREX_regroup] |
|
394 |
|
395 end; |
|
396 *} |
|
397 |
215 end |
398 end |