# HG changeset patch
# User chaieb
# Date 1181552781 -7200
# Node ID 6693a45a226c41c515ac396184dba9ad7f3ee211
# Parent  4ea75351b7cc446cdc4f4c84df174fb917a72e16
Now only contains generic conversion for quantifier elimination in HOL

diff -r 4ea75351b7cc -r 6693a45a226c src/HOL/Tools/Presburger/qelim.ML
--- a/src/HOL/Tools/Presburger/qelim.ML	Mon Jun 11 11:06:19 2007 +0200
+++ b/src/HOL/Tools/Presburger/qelim.ML	Mon Jun 11 11:06:21 2007 +0200
@@ -8,9 +8,6 @@
 
 signature QELIM =
  sig
- val tproof_of_mlift_qelim: theory -> (term -> bool) ->
-   (string list -> term -> thm) -> (term -> thm) ->
-   (term -> thm) -> term -> thm
  val standard_qelim_conv: (cterm list -> cterm -> thm) ->
    (cterm list -> Conv.conv) -> (cterm list -> cterm -> thm) -> cterm -> thm
  val gen_qelim_conv: Conv.conv -> Conv.conv -> Conv.conv ->
@@ -21,51 +18,8 @@
 
 structure Qelim : QELIM =
 struct
-open CooperDec;
-open CooperProof;
 open Conv;
 
-val cboolT = ctyp_of HOL.thy HOLogic.boolT;
-
-(* List of the theorems to be used in the following*)
-
-val qe_ex_conj = thm "qe_ex_conj";
-val qe_ex_nconj = thm "qe_ex_nconj";
-val qe_ALL = thm "qe_ALL";
-
-
-(*============= Compact version =====*)
-
-
-fun decomp_qe is_at afnp nfnp qfnp sg P = 
-   if is_at P then ([], fn [] => afnp [] P) else 
-   case P of
-   (Const("op &",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_conjI)
-   |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
-   |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
-   |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
-   |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
-   |(Const("Ex",_)$Abs(xn,xT,p)) => 
-      let val (xn1,p1) = Syntax.variant_abs(xn,xT,p) 
-      in ([p1],
-        fn [th1_1] => 
-          let val th2 = [th1_1,nfnp (snd (qe_get_terms th1_1))] MRS trans
-              val eth1 = (forall_intr (cterm_of sg (Free(xn1,xT))) th2) COMP  qe_exI
-              val th3 = qfnp (snd(qe_get_terms eth1))
-          in [eth1,th3] MRS trans
-          end )
-      end
-
-   |(Const("All",_)$Abs(xn,xT,p)) => ([(HOLogic.exists_const xT)$Abs(xn,xT,HOLogic.Not $ p)], fn [th] => th RS qe_ALL)
-   | _ => ([],fn [] => instantiate' [SOME (ctyp_of sg (type_of P))] [SOME (cterm_of sg P)] refl);
- 
-
-fun tproof_of_mlift_qelim sg isat afnp nfnp qfnp p = 
-   let val th1 = thm_of sg (decomp_qe isat afnp nfnp qfnp sg) p
-       val th2 = nfnp (snd (qe_get_terms th1))
-    in [th1,th2] MRS trans
-    end;
-
 val is_refl = op aconv o Logic.dest_equals o Thm.prop_of;
 
 fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv  =