# HG changeset patch
# User wenzelm
# Date 1123004832 -7200
# Node ID fb9261990ffe734746e0215aec2e284118953e4d
# Parent  51ff2bc327741d337f0b30f9229d7391bd1af25d
simprocs: Simplifier.inherit_bounds;

diff -r 51ff2bc32774 -r fb9261990ffe src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Tue Aug 02 19:47:11 2005 +0200
+++ b/src/FOL/simpdata.ML	Tue Aug 02 19:47:12 2005 +0200
@@ -267,11 +267,11 @@
 end;
 
 val defEX_regroup =
-  Simplifier.simproc (Theory.sign_of (the_context ()))
+  Simplifier.simproc (the_context ())
     "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
 
 val defALL_regroup =
-  Simplifier.simproc (Theory.sign_of (the_context ()))
+  Simplifier.simproc (the_context ())
     "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
 
 
@@ -337,6 +337,10 @@
   setmksimps (mksimps mksimps_pairs)
   setmkcong mk_meta_cong;
 
+fun unfold_tac ss ths =
+  ALLGOALS (full_simp_tac
+    (Simplifier.inherit_bounds ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
+
 
 (*intuitionistic simprules only*)
 val IFOL_ss = FOL_basic_ss
diff -r 51ff2bc32774 -r fb9261990ffe src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Aug 02 19:47:11 2005 +0200
+++ b/src/HOL/Product_Type.thy	Tue Aug 02 19:47:12 2005 +0200
@@ -412,9 +412,9 @@
   fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE
   |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
   |   split_pat tp i _ = NONE;
-  fun metaeq sg lhs rhs = mk_meta_eq (Tactic.prove sg [] []
+  fun metaeq thy ss lhs rhs = mk_meta_eq (Tactic.prove thy [] []
         (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
-        (K (simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1)));
+        (K (simp_tac (Simplifier.inherit_bounds ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
 
   fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
   |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
@@ -426,14 +426,14 @@
   |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
                               else (subst arg k i t $ subst arg k i u)
   |   subst arg k i t = t;
-  fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
+  fun beta_proc thy ss (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
         (case split_pat beta_term_pat 1 t of
-        SOME (i,f) => SOME (metaeq sg s (subst arg 0 i f))
+        SOME (i,f) => SOME (metaeq thy ss s (subst arg 0 i f))
         | NONE => NONE)
   |   beta_proc _ _ _ = NONE;
-  fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) =
+  fun eta_proc thy ss (s as Const ("split", _) $ Abs (_, _, t)) =
         (case split_pat eta_term_pat 1 t of
-          SOME (_,ft) => SOME (metaeq sg s (let val (f $ arg) = ft in f end))
+          SOME (_,ft) => SOME (metaeq thy ss s (let val (f $ arg) = ft in f end))
         | NONE => NONE)
   |   eta_proc _ _ _ = NONE;
 in
diff -r 51ff2bc32774 -r fb9261990ffe src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Aug 02 19:47:11 2005 +0200
+++ b/src/HOL/Set.thy	Tue Aug 02 19:47:12 2005 +0200
@@ -424,12 +424,16 @@
     val Ball_def = thm "Ball_def";
     val Bex_def = thm "Bex_def";
 
-    val prove_bex_tac =
-      rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
+    val simpset = Simplifier.clear_ss HOL_basic_ss;
+    fun unfold_tac ss th =
+      ALLGOALS (full_simp_tac (Simplifier.inherit_bounds ss simpset addsimps [th]));
+
+    fun prove_bex_tac ss =
+      unfold_tac ss Bex_def THEN Quantifier1.prove_one_point_ex_tac;
     val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
 
-    val prove_ball_tac =
-      rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
+    fun prove_ball_tac ss =
+      unfold_tac ss Ball_def THEN Quantifier1.prove_one_point_all_tac;
     val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
   in
     val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
diff -r 51ff2bc32774 -r fb9261990ffe src/Provers/quantifier1.ML
--- a/src/Provers/quantifier1.ML	Tue Aug 02 19:47:11 2005 +0200
+++ b/src/Provers/quantifier1.ML	Tue Aug 02 19:47:12 2005 +0200
@@ -57,10 +57,10 @@
 sig
   val prove_one_point_all_tac: tactic
   val prove_one_point_ex_tac: tactic
-  val rearrange_all: Sign.sg -> simpset -> term -> thm option
-  val rearrange_ex:  Sign.sg -> simpset -> term -> thm option
-  val rearrange_ball: tactic -> Sign.sg -> simpset -> term -> thm option
-  val rearrange_bex:  tactic -> Sign.sg -> simpset -> term -> thm option
+  val rearrange_all: theory -> simpset -> term -> thm option
+  val rearrange_ex:  theory -> simpset -> term -> thm option
+  val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
+  val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
 end;
 
 functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
@@ -103,8 +103,8 @@
         | exqu xs P = extract xs P
   in exqu end;
 
-fun prove_conv tac sg tu =
-  Tactic.prove sg [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
+fun prove_conv tac thy tu =
+  Tactic.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
 
 fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
 
@@ -145,35 +145,35 @@
       val Q = if n=0 then P else renumber 0 n P
   in quant xs (qC $ Abs(x,T,Q)) end;
 
-fun rearrange_all sg _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
+fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
      (case extract_quant extract_imp q [] P of
         NONE => NONE
       | SOME(xs,eq,Q) =>
           let val R = quantify all x T xs (imp $ eq $ Q)
-          in SOME(prove_conv prove_one_point_all_tac sg (F,R)) end)
+          in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end)
   | rearrange_all _ _ _ = NONE;
 
-fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
+fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) =
      (case extract_imp [] P of
         NONE => NONE
       | SOME(xs,eq,Q) => if not(null xs) then NONE else
           let val R = imp $ eq $ Q
-          in SOME(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
+          in SOME(prove_conv (tac ss) thy (F,Ball $ A $ Abs(x,T,R))) end)
   | rearrange_ball _ _ _ _ = NONE;
 
-fun rearrange_ex sg _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
+fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
      (case extract_quant extract_conj q [] P of
         NONE => NONE
       | SOME(xs,eq,Q) =>
           let val R = quantify ex x T xs (conj $ eq $ Q)
-          in SOME(prove_conv prove_one_point_ex_tac sg (F,R)) end)
+          in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end)
   | rearrange_ex _ _ _ = NONE;
 
-fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
+fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) =
      (case extract_conj [] P of
         NONE => NONE
       | SOME(xs,eq,Q) => if not(null xs) then NONE else
-          SOME(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
+          SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
   | rearrange_bex _ _ _ _ = NONE;
 
 end;
diff -r 51ff2bc32774 -r fb9261990ffe src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Tue Aug 02 19:47:11 2005 +0200
+++ b/src/ZF/OrdQuant.thy	Tue Aug 02 19:47:12 2005 +0200
@@ -400,17 +400,17 @@
 ML_setup {*
 local
 
-val prove_rex_tac = rewtac rex_def THEN Quantifier1.prove_one_point_ex_tac;
+fun prove_rex_tac ss = unfold_tac ss [rex_def] THEN Quantifier1.prove_one_point_ex_tac;
 val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
 
-val prove_rall_tac = rewtac rall_def THEN Quantifier1.prove_one_point_all_tac;
+fun prove_rall_tac ss = unfold_tac ss [rall_def] THEN Quantifier1.prove_one_point_all_tac;
 val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
 
 in
 
-val defREX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+val defREX_regroup = Simplifier.simproc (the_context ())
   "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
-val defRALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+val defRALL_regroup = Simplifier.simproc (the_context ())
   "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
 
 end;
diff -r 51ff2bc32774 -r fb9261990ffe src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Tue Aug 02 19:47:11 2005 +0200
+++ b/src/ZF/simpdata.ML	Tue Aug 02 19:47:12 2005 +0200
@@ -53,22 +53,20 @@
   addcongs [if_weak_cong]
   setSolver type_solver;
 
-
-
 local
 
-val prove_bex_tac = rewtac Bex_def THEN Quantifier1.prove_one_point_ex_tac;
+fun prove_bex_tac ss = unfold_tac ss [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
 
-val prove_ball_tac = rewtac Ball_def THEN Quantifier1.prove_one_point_all_tac;
+fun prove_ball_tac ss = unfold_tac ss [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
 
 in
 
-val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+val defBEX_regroup = Simplifier.simproc (the_context ())
   "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
 
-val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+val defBALL_regroup = Simplifier.simproc (the_context ())
   "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
 
 end;