# HG changeset patch # User wenzelm # Date 1303473493 -7200 # Node ID 6702c984bf5a6039633b123dd204ee6e8a047515 # Parent 12a752aeee98b7e3f6ec6a50ccfd2a682cc0c01d modernized Quantifier1 simproc setup; diff -r 12a752aeee98 -r 6702c984bf5a src/FOL/FOL.thy --- a/src/FOL/FOL.thy Fri Apr 22 13:07:47 2011 +0200 +++ b/src/FOL/FOL.thy Fri Apr 22 13:58:13 2011 +0200 @@ -305,12 +305,21 @@ use "simpdata.ML" + +simproc_setup defined_Ex ("EX x. P(x)") = {* + fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct) +*} + +simproc_setup defined_All ("ALL x. P(x)") = {* + fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct) +*} + ML {* (*intuitionistic simprules only*) val IFOL_ss = FOL_basic_ss addsimps (@{thms meta_simps} @ @{thms IFOL_simps} @ @{thms int_ex_simps} @ @{thms int_all_simps}) - addsimprocs [defALL_regroup, defEX_regroup] + addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}] addcongs [@{thm imp_cong}]; (*classical simprules too*) @@ -318,6 +327,7 @@ *} setup {* Simplifier.map_simpset (K FOL_ss) *} + setup "Simplifier.method_setup Splitter.split_modifiers" setup Splitter.setup setup clasimp_setup diff -r 12a752aeee98 -r 6702c984bf5a src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Fri Apr 22 13:07:47 2011 +0200 +++ b/src/FOL/simpdata.ML Fri Apr 22 13:58:13 2011 +0200 @@ -80,14 +80,6 @@ val ex_comm = @{thm ex_comm} end); -val defEX_regroup = - Simplifier.simproc_global @{theory} - "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex; - -val defALL_regroup = - Simplifier.simproc_global @{theory} - "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all; - (*** Case splitting ***) diff -r 12a752aeee98 -r 6702c984bf5a src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Apr 22 13:07:47 2011 +0200 +++ b/src/HOL/HOL.thy Fri Apr 22 13:58:13 2011 +0200 @@ -1209,8 +1209,15 @@ use "Tools/simpdata.ML" ML {* open Simpdata *} -setup {* - Simplifier.map_simpset (K (HOL_basic_ss addsimprocs [defALL_regroup, defEX_regroup])) + +setup {* Simplifier.map_simpset (K HOL_basic_ss) *} + +simproc_setup defined_Ex ("EX x. P x") = {* + fn _ => fn ss => fn ct => Quantifier1.rearrange_ex (theory_of_cterm ct) ss (term_of ct) +*} + +simproc_setup defined_All ("ALL x. P x") = {* + fn _ => fn ss => fn ct => Quantifier1.rearrange_all (theory_of_cterm ct) ss (term_of ct) *} setup {* diff -r 12a752aeee98 -r 6702c984bf5a src/HOL/Set.thy --- a/src/HOL/Set.thy Fri Apr 22 13:07:47 2011 +0200 +++ b/src/HOL/Set.thy Fri Apr 22 13:58:13 2011 +0200 @@ -75,17 +75,16 @@ to the front (and similarly for @{text "t=x"}): *} -setup {* -let - val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN - ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}), - DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])]) - val defColl_regroup = Simplifier.simproc_global @{theory} - "defined Collect" ["{x. P x & Q x}"] - (Quantifier1.rearrange_Coll Coll_perm_tac) -in - Simplifier.map_simpset (fn ss => ss addsimprocs [defColl_regroup]) -end +simproc_setup defined_Collect ("{x. P x & Q x}") = {* + let + val Coll_perm_tac = + rtac @{thm Collect_cong} 1 THEN + rtac @{thm iffI} 1 THEN + ALLGOALS (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]); + in + fn _ => fn ss => fn ct => + Quantifier1.rearrange_Coll Coll_perm_tac (theory_of_cterm ct) ss (term_of ct) + end *} lemmas CollectE = CollectD [elim_format] @@ -329,21 +328,24 @@ in [(@{const_syntax Collect}, setcompr_tr')] end; *} -setup {* -let - val unfold_bex_tac = unfold_tac @{thms "Bex_def"}; - fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; - val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; - val unfold_ball_tac = unfold_tac @{thms "Ball_def"}; - fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; - val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; - val defBEX_regroup = Simplifier.simproc_global @{theory} - "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex; - val defBALL_regroup = Simplifier.simproc_global @{theory} - "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball; -in - Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup]) -end +simproc_setup defined_Bex ("EX x:A. P x & Q x") = {* + let + val unfold_bex_tac = unfold_tac @{thms Bex_def}; + fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; + in + fn _ => fn ss => fn ct => + Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct) + end +*} + +simproc_setup defined_All ("ALL x:A. P x --> Q x") = {* + let + val unfold_ball_tac = unfold_tac @{thms Ball_def}; + fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; + in + fn _ => fn ss => fn ct => + Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct) + end *} lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x" diff -r 12a752aeee98 -r 6702c984bf5a src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Fri Apr 22 13:07:47 2011 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Fri Apr 22 13:58:13 2011 +0200 @@ -567,7 +567,7 @@ val nnf_ss = HOL_basic_ss addsimps nnf_extra_simps - addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}]; + addsimprocs [@{simproc defined_All}, @{simproc defined_Ex}, @{simproc neq}, @{simproc let_simp}]; val presimplify = rewrite_rule (map safe_mk_meta_eq nnf_simps) #> simplify nnf_ss diff -r 12a752aeee98 -r 6702c984bf5a src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Fri Apr 22 13:07:47 2011 +0200 +++ b/src/HOL/Tools/simpdata.ML Fri Apr 22 13:58:13 2011 +0200 @@ -183,14 +183,6 @@ let val ss0 = Simplifier.clear_ss HOL_basic_ss addsimps ths in fn ss => ALLGOALS (full_simp_tac (Simplifier.inherit_context ss ss0)) end; -val defALL_regroup = - Simplifier.simproc_global @{theory} - "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all; - -val defEX_regroup = - Simplifier.simproc_global @{theory} - "defined EX" ["EX x. P x"] Quantifier1.rearrange_ex; - end; structure Splitter = Simpdata.Splitter; diff -r 12a752aeee98 -r 6702c984bf5a src/ZF/OrdQuant.thy --- a/src/ZF/OrdQuant.thy Fri Apr 22 13:07:47 2011 +0200 +++ b/src/ZF/OrdQuant.thy Fri Apr 22 13:58:13 2011 +0200 @@ -368,27 +368,24 @@ text {* Setting up the one-point-rule simproc *} -ML {* -local - -val unfold_rex_tac = unfold_tac [@{thm rex_def}]; -fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac; -val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac; - -val unfold_rall_tac = unfold_tac [@{thm rall_def}]; -fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac; -val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac; +simproc_setup defined_rex ("EX x[M]. P(x) & Q(x)") = {* + let + val unfold_rex_tac = unfold_tac @{thms rex_def}; + fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac; + in + fn _ => fn ss => fn ct => + Quantifier1.rearrange_bex prove_rex_tac (theory_of_cterm ct) ss (term_of ct) + end +*} -in - -val defREX_regroup = Simplifier.simproc_global @{theory} - "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex; -val defRALL_regroup = Simplifier.simproc_global @{theory} - "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball; - -end; - -Addsimprocs [defRALL_regroup,defREX_regroup]; +simproc_setup defined_rall ("ALL x[M]. P(x) --> Q(x)") = {* + let + val unfold_rall_tac = unfold_tac @{thms rall_def}; + fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac; + in + fn _ => fn ss => fn ct => + Quantifier1.rearrange_ball prove_rall_tac (theory_of_cterm ct) ss (term_of ct) + end *} end diff -r 12a752aeee98 -r 6702c984bf5a src/ZF/pair.thy --- a/src/ZF/pair.thy Fri Apr 22 13:07:47 2011 +0200 +++ b/src/ZF/pair.thy Fri Apr 22 13:58:13 2011 +0200 @@ -7,7 +7,29 @@ header{*Ordered Pairs*} theory pair imports upair -uses "simpdata.ML" begin +uses "simpdata.ML" +begin + +simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {* + let + val unfold_bex_tac = unfold_tac @{thms Bex_def}; + fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; + in + fn _ => fn ss => fn ct => + Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct) + end +*} + +simproc_setup defined_Ball ("ALL x:A. P(x) --> Q(x)") = {* + let + val unfold_ball_tac = unfold_tac @{thms Ball_def}; + fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; + in + fn _ => fn ss => fn ct => + Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct) + end +*} + (** Lemmas for showing that uniquely determines a and b **) diff -r 12a752aeee98 -r 6702c984bf5a src/ZF/simpdata.ML --- a/src/ZF/simpdata.ML Fri Apr 22 13:07:47 2011 +0200 +++ b/src/ZF/simpdata.ML Fri Apr 22 13:58:13 2011 +0200 @@ -47,28 +47,5 @@ ss setmksimps (K (map mk_eq o ZF_atomize o gen_all)) addcongs [@{thm if_weak_cong}]); -local - -val unfold_bex_tac = unfold_tac [@{thm Bex_def}]; -fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; -val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; - -val unfold_ball_tac = unfold_tac [@{thm Ball_def}]; -fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; -val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; - -in - -val defBEX_regroup = Simplifier.simproc_global @{theory} - "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex; - -val defBALL_regroup = Simplifier.simproc_global @{theory} - "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball; - -end; - -Addsimprocs [defBALL_regroup, defBEX_regroup]; - - val ZF_ss = @{simpset};