# 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 <a,b> 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};