equal
deleted
inserted
replaced
67 Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"} |
67 Simproc for pulling @{text "x=t"} in @{text "{x. \<dots> & x=t & \<dots>}"} |
68 to the front (and similarly for @{text "t=x"}): |
68 to the front (and similarly for @{text "t=x"}): |
69 *} |
69 *} |
70 |
70 |
71 simproc_setup defined_Collect ("{x. P x & Q x}") = {* |
71 simproc_setup defined_Collect ("{x. P x & Q x}") = {* |
72 fn _ => |
72 fn _ => Quantifier1.rearrange_Collect |
73 Quantifier1.rearrange_Collect |
73 (fn _ => |
74 (rtac @{thm Collect_cong} 1 THEN |
74 rtac @{thm Collect_cong} 1 THEN |
75 rtac @{thm iffI} 1 THEN |
75 rtac @{thm iffI} 1 THEN |
76 ALLGOALS |
76 ALLGOALS |
77 (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}])) |
77 (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}])) |
78 *} |
78 *} |
79 |
79 |
353 end; |
353 end; |
354 in [(@{const_syntax Collect}, setcompr_tr')] end; |
354 in [(@{const_syntax Collect}, setcompr_tr')] end; |
355 *} |
355 *} |
356 |
356 |
357 simproc_setup defined_Bex ("EX x:A. P x & Q x") = {* |
357 simproc_setup defined_Bex ("EX x:A. P x & Q x") = {* |
358 let |
358 fn _ => Quantifier1.rearrange_bex |
359 val unfold_bex_tac = unfold_tac @{thms Bex_def}; |
359 (fn ctxt => |
360 fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; |
360 unfold_tac ctxt @{thms Bex_def} THEN |
361 in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end |
361 Quantifier1.prove_one_point_ex_tac) |
362 *} |
362 *} |
363 |
363 |
364 simproc_setup defined_All ("ALL x:A. P x --> Q x") = {* |
364 simproc_setup defined_All ("ALL x:A. P x --> Q x") = {* |
365 let |
365 fn _ => Quantifier1.rearrange_ball |
366 val unfold_ball_tac = unfold_tac @{thms Ball_def}; |
366 (fn ctxt => |
367 fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; |
367 unfold_tac ctxt @{thms Ball_def} THEN |
368 in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end |
368 Quantifier1.prove_one_point_all_tac) |
369 *} |
369 *} |
370 |
370 |
371 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x" |
371 lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x" |
372 by (simp add: Ball_def) |
372 by (simp add: Ball_def) |
373 |
373 |