424 lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)" |
424 lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)" |
425 by blast |
425 by blast |
426 |
426 |
427 ML_setup {* |
427 ML_setup {* |
428 local |
428 local |
429 val Ball_def = thm "Ball_def"; |
429 val unfold_bex_tac = unfold_tac [thm "Bex_def"]; |
430 val Bex_def = thm "Bex_def"; |
430 fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; |
431 |
|
432 val simpset = Simplifier.clear_ss HOL_basic_ss; |
|
433 fun unfold_tac ss th = |
|
434 ALLGOALS (full_simp_tac (Simplifier.inherit_context ss simpset addsimps [th])); |
|
435 |
|
436 fun prove_bex_tac ss = |
|
437 unfold_tac ss Bex_def THEN Quantifier1.prove_one_point_ex_tac; |
|
438 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; |
431 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; |
439 |
432 |
440 fun prove_ball_tac ss = |
433 val unfold_ball_tac = unfold_tac [thm "Ball_def"]; |
441 unfold_tac ss Ball_def THEN Quantifier1.prove_one_point_all_tac; |
434 fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; |
442 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; |
435 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; |
443 in |
436 in |
444 val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ())) |
437 val defBEX_regroup = Simplifier.simproc (the_context ()) |
445 "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex; |
438 "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex; |
446 val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ())) |
439 val defBALL_regroup = Simplifier.simproc (the_context ()) |
447 "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball; |
440 "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball; |
448 end; |
441 end; |
449 |
442 |
450 Addsimprocs [defBALL_regroup, defBEX_regroup]; |
443 Addsimprocs [defBALL_regroup, defBEX_regroup]; |
451 *} |
444 *} |