--- 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
--- 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 ***)
--- 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 {*
--- 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"
--- 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
--- 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;
--- 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
--- 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 <a,b> uniquely determines a and b **)
--- 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};