# HG changeset patch
# User chaieb
# Date 1091634235 -7200
# Node ID f233706d9fcea4ac203caa4c0d512307e1a4cb9c
# Parent  e8cef6993701a74d3c1ac04f56fd5b6b597ed3df
oracle corrected

diff -r e8cef6993701 -r f233706d9fce src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Wed Aug 04 11:25:08 2004 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Wed Aug 04 17:43:55 2004 +0200
@@ -42,6 +42,7 @@
   val plusinf : term -> term -> term
   val onatoms : (term -> term) -> term -> term
   val evalc : term -> term
+  val cooper_w : string list -> term -> (term option * term)
   val integer_qelim : Term.term -> Term.term
   val mk_presburger_oracle : (Sign.sg * exn) -> term
 end;
@@ -197,7 +198,7 @@
  
          else (warning "lint: apparent nonlinearity"; raise COOPER)
          end 
-  |_ =>   (error "COOPER:lint: unknown term  ")
+  |_ =>  error ("COOPER:lint: unknown term  \n");
    
  
  
@@ -414,7 +415,31 @@
 (* ------------------------------------------------------------------------- *) 
 (* Evaluation of constant expressions.                                       *) 
 (* ------------------------------------------------------------------------- *) 
- 
+
+(* An other implementation of divides, that covers more cases*) 
+
+exception DVD_UNKNOWN
+
+fun dvd_op (d, t) = 
+ if not(is_numeral d) then raise DVD_UNKNOWN
+ else let 
+   val dn = dest_numeral d
+   fun coeffs_of x = case x of 
+     Const(p,_) $ tl $ tr => 
+       if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
+          else if p = "op *" 
+	        then if (is_numeral tr) 
+		 then [(dest_numeral tr) * (dest_numeral tl)] 
+		 else [dest_numeral tl]
+	        else []
+    |_ => if (is_numeral t) then [dest_numeral t]  else []
+   val ts = coeffs_of t
+   in case ts of
+     [] => raise DVD_UNKNOWN
+    |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
+   end;
+
+
 val operations = 
   [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), 
    ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; 
@@ -423,22 +448,44 @@
     |applyoperation _ (_, _) = false; 
  
 (*Evaluation of constant atomic formulas*) 
- 
+ (*FIXME : This is an optimation but still incorrect !! *)
+(*
 fun evalc_atom at = case at of  
-      (Const (p,_) $ s $ t) =>(  
-         case assoc (operations,p) of 
-             Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
-              handle _ => at) 
-             | _ =>  at) 
-     |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
-         case assoc (operations,p) of 
-             Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
-	     HOLogic.false_const else HOLogic.true_const)  
-              handle _ => at) 
-             | _ =>  at) 
-     | _ =>  at; 
- 
-(*Function onatoms apllys function f on the atomic formulas involved in a.*) 
+  (Const (p,_) $ s $ t) =>
+   (if p="Divides.op dvd" then 
+     ((if dvd_op(s,t) then HOLogic.true_const
+     else HOLogic.false_const)
+      handle _ => at)
+    else
+  case assoc (operations,p) of 
+    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
+    handle _ => at) 
+      | _ =>  at) 
+      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
+  case assoc (operations,p) of 
+    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
+    HOLogic.false_const else HOLogic.true_const)  
+    handle _ => at) 
+      | _ =>  at) 
+      | _ =>  at; 
+
+*)
+
+fun evalc_atom at = case at of  
+  (Const (p,_) $ s $ t) =>
+   ( case assoc (operations,p) of 
+    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
+    handle _ => at) 
+      | _ =>  at) 
+      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
+  case assoc (operations,p) of 
+    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
+    HOLogic.false_const else HOLogic.true_const)  
+    handle _ => at) 
+      | _ =>  at) 
+      | _ =>  at; 
+
+ (*Function onatoms apllys function f on the atomic formulas involved in a.*) 
  
 fun onatoms f a = if (is_arith_rel a) then f a else case a of 
  
@@ -653,6 +700,48 @@
   | _ => error "cooper: not an existential formula";
   
 
+(* Try to find a withness for the formula *)
+
+fun inf_w mi d vars x p = 
+  let val f = if mi then minusinf else plusinf in
+   case (simpl (minusinf x p)) of
+   Const("True",_)  => (Some (mk_numeral 1), HOLogic.true_const)
+  |Const("False",_) => (None,HOLogic.false_const)
+  |F => 
+      let 
+      fun h n =
+       case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of 
+	Const("True",_) => (Some (mk_numeral n),HOLogic.true_const)
+       |F' => if n=1 then (None,F')
+	     else let val (rw,rf) = h (n-1) in 
+	       (rw,HOLogic.mk_disj(F',rf))
+	     end
+
+      in (h d)
+      end
+  end;
+
+fun set_w d b st vars x p = let 
+    fun h ns = case ns of 
+    [] => (None,HOLogic.false_const)
+   |n::nl => ( case ((simpl o evalc) (linrep vars x n p)) of
+      Const("True",_) => (Some n,HOLogic.true_const)
+      |F' => let val (rw,rf) = h nl 
+             in (rw,HOLogic.mk_disj(F',rf)) 
+	     end)
+    val f = if b then linear_add else linear_sub
+    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
+    in h p_elements
+    end;
+
+fun withness d b st vars x p = case (inf_w b d vars x p) of 
+   (Some n,_) => (Some n,HOLogic.true_const)
+  |(None,Pinf) => (case (set_w d b st vars x p) of 
+    (Some n,_) => (Some n,HOLogic.true_const)
+    |(_,Pst) => (None,HOLogic.mk_disj(Pinf,Pst)));
+
+
+
 
 (*Cooper main procedure*) 
   
@@ -678,6 +767,29 @@
   | _ => error "cooper: not an existential formula";
 
 
+(* A Version of cooper that returns a withness *)
+fun cooper_w vars1 fm =
+  case fm of
+   Const ("Ex",_) $ Abs(x0,T,p0) => let 
+    val (xn,p1) = variant_abs (x0,T,p0)
+    val x = Free (xn,T)
+    val vars = (xn::vars1)
+(*     val p = unitycoeff x  (posineq (simpl p1)) *)
+    val p = unitycoeff x  p1 
+    val ast = aset x p
+    val bst = bset x p
+    val d = divlcm x p
+    val (p_inf,S ) = 
+    if (length bst) <= (length ast) 
+     then (true,bst)
+     else (false,ast)
+    in withness d p_inf S vars x p 
+(*    fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
+    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+   in (list_disj (map stage js))
+*)
+   end
+  | _ => error "cooper: not an existential formula";
 
  
 (*Function itlist applys a double parametred function f : 'a->'b->b iteratively to a List l : 'a 
@@ -811,8 +923,8 @@
 fun mk_presburger_oracle (sg,COOPER_ORACLE t) = 
     if (!quick_and_dirty) 
     then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t))
-    else raise COOPER_ORACLE t;
-
+    else raise COOPER_ORACLE t
+    |mk_presburger_oracle (sg,_) = error "Oops";
 end;
 
 
diff -r e8cef6993701 -r f233706d9fce src/HOL/Integ/cooper_proof.ML
--- a/src/HOL/Integ/cooper_proof.ML	Wed Aug 04 11:25:08 2004 +0200
+++ b/src/HOL/Integ/cooper_proof.ML	Wed Aug 04 17:43:55 2004 +0200
@@ -219,7 +219,8 @@
         [zdvd_iff_zmod_eq_0,unity_coeff_ex]
       val ct =  cert_Trueprop sg fm2
     in 
-      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] 
+
     end
 
   (*"bl" like blast tactic*)
@@ -251,7 +252,8 @@
 
   | "fa" =>
     let val ct = cert_Trueprop sg fm2
-    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
+    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]  
+
     end
 
   | "sa" =>
@@ -259,7 +261,8 @@
       val ss = presburger_ss addsimps zadd_ac
       val ct = cert_Trueprop sg fm2
     in 
-      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
+
     end
   (* like Existance Conjunction *)
   | "ec" =>
@@ -283,7 +286,8 @@
       val ss = presburger_ss addsimps zadd_ac
       val ct = cert_Trueprop sg fm2
     in 
-      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
+
     end;
 
 (*=============================================================*)
@@ -917,6 +921,71 @@
 |cooper_prv _ _ _ =  error "Parameters format";
 
 
+(* **************************************** *)
+(*    An Other Version of cooper proving    *)
+(*     by giving a withness for EX          *)
+(* **************************************** *)
+
+
+
+fun cooper_prv_w sg (x as Free(xn,xT)) efm = let 
+   (* lfm_thm : efm = linearized form of efm*)
+   val lfm_thm = proof_of_linform sg [xn] efm
+   (*efm2 is the linearized form of efm *) 
+   val efm2 = snd(qe_get_terms lfm_thm)
+   (* l is the lcm of all coefficients of x *)
+   val l = formlcm x efm2
+   (*ac_thm: efm = efm2 with adjusted coefficients of x *)
+   val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
+   (* fm is efm2 with adjusted coefficients of x *)
+   val fm = snd (qe_get_terms ac_thm)
+  (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
+   val  cfm = unitycoeff x fm
+   (*afm is fm where c*x is replaced by 1*x or -1*x *)
+   val afm = adjustcoeff x l fm
+   (* P = %x.afm*)
+   val P = absfree(xn,xT,afm)
+   (* This simpset allows the elimination of the sets in bex {1..d} *)
+   val ss = presburger_ss addsimps
+     [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
+   (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
+   val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+   (* e_ac_thm : Ex x. efm = EX x. fm*)
+   val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
+   (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
+   val (lsuth,rsuth) = qe_get_terms (uth)
+   (* lseacth = EX x. efm; rseacth = EX x. fm*)
+   val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
+
+   val (w,rs) = cooper_w [] cfm
+   val exp_cp_thm =  case w of 
+     (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*)
+    Some n =>  e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*)
+   |_ => let 
+    (* A and B set of the formula*)
+    val A = aset x cfm
+    val B = bset x cfm
+    (* the divlcm (delta) of the formula*)
+    val dlcm = mk_numeral (divlcm x cfm)
+    (* Which set is smaller to generate the (hoepfully) shorter proof*)
+    val cms = if ((length A) < (length B )) then "pi" else "mi"
+    (* synthesize the proof of cooper's theorem*)
+     (* cp_thm: EX x. cfm = Q*)
+    val cp_thm = cooper_thm sg cms x cfm dlcm A B
+     (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
+    (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
+    in refl RS (simplify ss (cp_thm RSN (2,trans)))
+    end
+   (* lscth = EX x. cfm; rscth = Q' *)
+   val (lscth,rscth) = qe_get_terms (exp_cp_thm)
+   (* u_c_thm: EX x. P(l*x) = Q'*)
+   val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
+   (* result: EX x. efm = Q'*)
+ in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
+   end
+|cooper_prv_w _ _ _ =  error "Parameters format";
+
+
 
 fun decomp_cnnf sg lfnp P = case P of 
      Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )
diff -r e8cef6993701 -r f233706d9fce src/HOL/Tools/Presburger/cooper_dec.ML
--- a/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Aug 04 11:25:08 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Wed Aug 04 17:43:55 2004 +0200
@@ -42,6 +42,7 @@
   val plusinf : term -> term -> term
   val onatoms : (term -> term) -> term -> term
   val evalc : term -> term
+  val cooper_w : string list -> term -> (term option * term)
   val integer_qelim : Term.term -> Term.term
   val mk_presburger_oracle : (Sign.sg * exn) -> term
 end;
@@ -197,7 +198,7 @@
  
          else (warning "lint: apparent nonlinearity"; raise COOPER)
          end 
-  |_ =>   (error "COOPER:lint: unknown term  ")
+  |_ =>  error ("COOPER:lint: unknown term  \n");
    
  
  
@@ -414,7 +415,31 @@
 (* ------------------------------------------------------------------------- *) 
 (* Evaluation of constant expressions.                                       *) 
 (* ------------------------------------------------------------------------- *) 
- 
+
+(* An other implementation of divides, that covers more cases*) 
+
+exception DVD_UNKNOWN
+
+fun dvd_op (d, t) = 
+ if not(is_numeral d) then raise DVD_UNKNOWN
+ else let 
+   val dn = dest_numeral d
+   fun coeffs_of x = case x of 
+     Const(p,_) $ tl $ tr => 
+       if p = "op +" then (coeffs_of tl) union (coeffs_of tr)
+          else if p = "op *" 
+	        then if (is_numeral tr) 
+		 then [(dest_numeral tr) * (dest_numeral tl)] 
+		 else [dest_numeral tl]
+	        else []
+    |_ => if (is_numeral t) then [dest_numeral t]  else []
+   val ts = coeffs_of t
+   in case ts of
+     [] => raise DVD_UNKNOWN
+    |_  => foldr (fn(k,r) => r andalso (k mod dn = 0)) (ts,true)
+   end;
+
+
 val operations = 
   [("op =",op=), ("op <",op<), ("op >",op>), ("op <=",op<=) , ("op >=",op>=), 
    ("Divides.op dvd",fn (x,y) =>((y mod x) = 0))]; 
@@ -423,22 +448,44 @@
     |applyoperation _ (_, _) = false; 
  
 (*Evaluation of constant atomic formulas*) 
- 
+ (*FIXME : This is an optimation but still incorrect !! *)
+(*
 fun evalc_atom at = case at of  
-      (Const (p,_) $ s $ t) =>(  
-         case assoc (operations,p) of 
-             Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
-              handle _ => at) 
-             | _ =>  at) 
-     |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
-         case assoc (operations,p) of 
-             Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
-	     HOLogic.false_const else HOLogic.true_const)  
-              handle _ => at) 
-             | _ =>  at) 
-     | _ =>  at; 
- 
-(*Function onatoms apllys function f on the atomic formulas involved in a.*) 
+  (Const (p,_) $ s $ t) =>
+   (if p="Divides.op dvd" then 
+     ((if dvd_op(s,t) then HOLogic.true_const
+     else HOLogic.false_const)
+      handle _ => at)
+    else
+  case assoc (operations,p) of 
+    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
+    handle _ => at) 
+      | _ =>  at) 
+      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
+  case assoc (operations,p) of 
+    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
+    HOLogic.false_const else HOLogic.true_const)  
+    handle _ => at) 
+      | _ =>  at) 
+      | _ =>  at; 
+
+*)
+
+fun evalc_atom at = case at of  
+  (Const (p,_) $ s $ t) =>
+   ( case assoc (operations,p) of 
+    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then HOLogic.true_const else HOLogic.false_const)  
+    handle _ => at) 
+      | _ =>  at) 
+      |Const("Not",_)$(Const (p,_) $ s $ t) =>(  
+  case assoc (operations,p) of 
+    Some f => ((if (f ((dest_numeral s),(dest_numeral t))) then 
+    HOLogic.false_const else HOLogic.true_const)  
+    handle _ => at) 
+      | _ =>  at) 
+      | _ =>  at; 
+
+ (*Function onatoms apllys function f on the atomic formulas involved in a.*) 
  
 fun onatoms f a = if (is_arith_rel a) then f a else case a of 
  
@@ -653,6 +700,48 @@
   | _ => error "cooper: not an existential formula";
   
 
+(* Try to find a withness for the formula *)
+
+fun inf_w mi d vars x p = 
+  let val f = if mi then minusinf else plusinf in
+   case (simpl (minusinf x p)) of
+   Const("True",_)  => (Some (mk_numeral 1), HOLogic.true_const)
+  |Const("False",_) => (None,HOLogic.false_const)
+  |F => 
+      let 
+      fun h n =
+       case ((simpl o evalc) (linrep vars x (mk_numeral n) F)) of 
+	Const("True",_) => (Some (mk_numeral n),HOLogic.true_const)
+       |F' => if n=1 then (None,F')
+	     else let val (rw,rf) = h (n-1) in 
+	       (rw,HOLogic.mk_disj(F',rf))
+	     end
+
+      in (h d)
+      end
+  end;
+
+fun set_w d b st vars x p = let 
+    fun h ns = case ns of 
+    [] => (None,HOLogic.false_const)
+   |n::nl => ( case ((simpl o evalc) (linrep vars x n p)) of
+      Const("True",_) => (Some n,HOLogic.true_const)
+      |F' => let val (rw,rf) = h nl 
+             in (rw,HOLogic.mk_disj(F',rf)) 
+	     end)
+    val f = if b then linear_add else linear_sub
+    val p_elements = foldr (fn (i,l) => l union (map (fn e => f [] e (mk_numeral i)) st)) (1 upto d,[])
+    in h p_elements
+    end;
+
+fun withness d b st vars x p = case (inf_w b d vars x p) of 
+   (Some n,_) => (Some n,HOLogic.true_const)
+  |(None,Pinf) => (case (set_w d b st vars x p) of 
+    (Some n,_) => (Some n,HOLogic.true_const)
+    |(_,Pst) => (None,HOLogic.mk_disj(Pinf,Pst)));
+
+
+
 
 (*Cooper main procedure*) 
   
@@ -678,6 +767,29 @@
   | _ => error "cooper: not an existential formula";
 
 
+(* A Version of cooper that returns a withness *)
+fun cooper_w vars1 fm =
+  case fm of
+   Const ("Ex",_) $ Abs(x0,T,p0) => let 
+    val (xn,p1) = variant_abs (x0,T,p0)
+    val x = Free (xn,T)
+    val vars = (xn::vars1)
+(*     val p = unitycoeff x  (posineq (simpl p1)) *)
+    val p = unitycoeff x  p1 
+    val ast = aset x p
+    val bst = bset x p
+    val d = divlcm x p
+    val (p_inf,S ) = 
+    if (length bst) <= (length ast) 
+     then (true,bst)
+     else (false,ast)
+    in withness d p_inf S vars x p 
+(*    fun p_element j a = linrep vars x (f vars a (mk_numeral j)) p
+    fun stage j = list_disj (linrep vars x (mk_numeral j) p_inf :: map (p_element j) S)
+   in (list_disj (map stage js))
+*)
+   end
+  | _ => error "cooper: not an existential formula";
 
  
 (*Function itlist applys a double parametred function f : 'a->'b->b iteratively to a List l : 'a 
@@ -811,8 +923,8 @@
 fun mk_presburger_oracle (sg,COOPER_ORACLE t) = 
     if (!quick_and_dirty) 
     then HOLogic.mk_Trueprop (HOLogic.mk_eq(t,integer_qelim t))
-    else raise COOPER_ORACLE t;
-
+    else raise COOPER_ORACLE t
+    |mk_presburger_oracle (sg,_) = error "Oops";
 end;
 
 
diff -r e8cef6993701 -r f233706d9fce src/HOL/Tools/Presburger/cooper_proof.ML
--- a/src/HOL/Tools/Presburger/cooper_proof.ML	Wed Aug 04 11:25:08 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Wed Aug 04 17:43:55 2004 +0200
@@ -219,7 +219,8 @@
         [zdvd_iff_zmod_eq_0,unity_coeff_ex]
       val ct =  cert_Trueprop sg fm2
     in 
-      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] 
+
     end
 
   (*"bl" like blast tactic*)
@@ -251,7 +252,8 @@
 
   | "fa" =>
     let val ct = cert_Trueprop sg fm2
-    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]
+    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]  
+
     end
 
   | "sa" =>
@@ -259,7 +261,8 @@
       val ss = presburger_ss addsimps zadd_ac
       val ct = cert_Trueprop sg fm2
     in 
-      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
+
     end
   (* like Existance Conjunction *)
   | "ec" =>
@@ -283,7 +286,8 @@
       val ss = presburger_ss addsimps zadd_ac
       val ct = cert_Trueprop sg fm2
     in 
-      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]
+      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
+
     end;
 
 (*=============================================================*)
@@ -917,6 +921,71 @@
 |cooper_prv _ _ _ =  error "Parameters format";
 
 
+(* **************************************** *)
+(*    An Other Version of cooper proving    *)
+(*     by giving a withness for EX          *)
+(* **************************************** *)
+
+
+
+fun cooper_prv_w sg (x as Free(xn,xT)) efm = let 
+   (* lfm_thm : efm = linearized form of efm*)
+   val lfm_thm = proof_of_linform sg [xn] efm
+   (*efm2 is the linearized form of efm *) 
+   val efm2 = snd(qe_get_terms lfm_thm)
+   (* l is the lcm of all coefficients of x *)
+   val l = formlcm x efm2
+   (*ac_thm: efm = efm2 with adjusted coefficients of x *)
+   val ac_thm = [lfm_thm , (proof_of_adjustcoeffeq sg x l efm2)] MRS trans
+   (* fm is efm2 with adjusted coefficients of x *)
+   val fm = snd (qe_get_terms ac_thm)
+  (* cfm is l dvd x & fm' where fm' is fm where l*x is replaced by x*)
+   val  cfm = unitycoeff x fm
+   (*afm is fm where c*x is replaced by 1*x or -1*x *)
+   val afm = adjustcoeff x l fm
+   (* P = %x.afm*)
+   val P = absfree(xn,xT,afm)
+   (* This simpset allows the elimination of the sets in bex {1..d} *)
+   val ss = presburger_ss addsimps
+     [simp_from_to] delsimps [P_eqtrue, P_eqfalse, bex_triv, insert_iff]
+   (* uth : EX x.P(l*x) = EX x. l dvd x & P x*)
+   val uth = instantiate' [] [Some (cterm_of sg P) , Some (cterm_of sg (mk_numeral l))] (unity_coeff_ex)
+   (* e_ac_thm : Ex x. efm = EX x. fm*)
+   val e_ac_thm = (forall_intr (cterm_of sg x) ac_thm) COMP (qe_exI)
+   (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
+   val (lsuth,rsuth) = qe_get_terms (uth)
+   (* lseacth = EX x. efm; rseacth = EX x. fm*)
+   val (lseacth,rseacth) = qe_get_terms(e_ac_thm)
+
+   val (w,rs) = cooper_w [] cfm
+   val exp_cp_thm =  case w of 
+     (* FIXME - e_ac_thm just tipped to test syntactical correctness of the program!!!!*)
+    Some n =>  e_ac_thm (* Prove cfm (n) and use exI and then Eq_TrueI*)
+   |_ => let 
+    (* A and B set of the formula*)
+    val A = aset x cfm
+    val B = bset x cfm
+    (* the divlcm (delta) of the formula*)
+    val dlcm = mk_numeral (divlcm x cfm)
+    (* Which set is smaller to generate the (hoepfully) shorter proof*)
+    val cms = if ((length A) < (length B )) then "pi" else "mi"
+    (* synthesize the proof of cooper's theorem*)
+     (* cp_thm: EX x. cfm = Q*)
+    val cp_thm = cooper_thm sg cms x cfm dlcm A B
+     (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
+    (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
+    in refl RS (simplify ss (cp_thm RSN (2,trans)))
+    end
+   (* lscth = EX x. cfm; rscth = Q' *)
+   val (lscth,rscth) = qe_get_terms (exp_cp_thm)
+   (* u_c_thm: EX x. P(l*x) = Q'*)
+   val  u_c_thm = [([uth,prove_elementar sg "ss" (HOLogic.mk_eq (rsuth,lscth))] MRS trans),exp_cp_thm] MRS trans
+   (* result: EX x. efm = Q'*)
+ in  ([e_ac_thm,[(prove_elementar sg "ss" (HOLogic.mk_eq (rseacth,lsuth))),u_c_thm] MRS trans] MRS trans)
+   end
+|cooper_prv_w _ _ _ =  error "Parameters format";
+
+
 
 fun decomp_cnnf sg lfnp P = case P of 
      Const ("op &",_) $ p $q => ([p,q] , fn [th1,th2] => [th1,th2] MRS qe_conjI )