# HG changeset patch
# User nipkow
# Date 880699026 -3600
# Node ID 24d9e6639cd4bf080f311d4d3e35d7b8b4421198
# Parent  afb60b8bf15e2f5bc8a1d8e50c3c900ef23c18ec
Moved the quantifier elimination simp procs into Provers.

diff -r afb60b8bf15e -r 24d9e6639cd4 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri Nov 28 07:35:47 1997 +0100
+++ b/src/HOL/ROOT.ML	Fri Nov 28 07:37:06 1997 +0100
@@ -24,6 +24,7 @@
 use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
 use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
 use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
+use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
 
 use "thy_data.ML";
 
diff -r afb60b8bf15e -r 24d9e6639cd4 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Nov 28 07:35:47 1997 +0100
+++ b/src/HOL/simpdata.ML	Fri Nov 28 07:37:06 1997 +0100
@@ -52,6 +52,31 @@
 val DelIffs = seq delIff
 end;
 
+(** instantiate generic simp procs for `quantifier elimination': **)
+structure Quantifier1 = Quantifier1Fun(
+struct
+  (*abstract syntax*)
+  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
+    | dest_eq _ = None;
+  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
+    | dest_conj _ = None;
+  val conj = HOLogic.conj
+  val imp  = HOLogic.imp
+  (*rules*)
+  val iff_reflection = eq_reflection
+  val iffI = iffI
+  val sym  = sym
+  val conjI= conjI
+  val conjE= conjE
+  val impI = impI
+  val impE = impE
+  val mp   = mp
+  val exI  = exI
+  val exE  = exE
+  val allI = allI
+  val allE = allE
+end);
+
 
 local
 
@@ -160,7 +185,6 @@
 NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"
    "!x. x=t --> P(x)" and "!x. t=x --> P(x)"
    must be taken care of by ordinary rewrite rules.
-***)
 
 local
 
@@ -227,6 +251,9 @@
 val defEX_regroup = mk_simproc "defined EX" [ex_pattern] rearrange_ex;
 val defALL_regroup = mk_simproc "defined ALL" [all_pattern] rearrange_all;
 end;
+***)
+
+
 
 
 (* elimination of existential quantifiers in assumptions *)
@@ -355,7 +382,20 @@
                    "(if P then Q else R) = ((P-->Q) & (~P-->R))"
                    (fn _ => [rtac expand_if 1]);
 
+(** make simp procs for quantifier elimination **)
+local
+val ex_pattern =
+  read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
 
+val all_pattern =
+  read_cterm (sign_of HOL.thy) ("! x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
+
+in
+val defEX_regroup =
+  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
+val defALL_regroup =
+  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
+end;
 
 (** Case splitting **)