1.1 --- a/src/HOL/Integ/cooper_dec.ML	Sun Aug 29 17:42:11 2004 +0200
     1.2 +++ b/src/HOL/Integ/cooper_dec.ML	Mon Aug 30 12:01:52 2004 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4    val is_arith_rel : term -> bool
     1.5    val mk_numeral : int -> term
     1.6    val dest_numeral : term -> int
     1.7 +  val is_numeral : term -> bool
     1.8    val zero : term
     1.9    val one : term
    1.10    val linear_cmul : int -> term -> term
    1.11 @@ -208,10 +209,13 @@
    1.12   
    1.13  fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); 
    1.14   
    1.15 -fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =  
    1.16 +fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =
    1.17 +    if is_numeral c then   
    1.18        let val c' = (mk_numeral(abs(dest_numeral c)))  
    1.19        in (HOLogic.mk_binrel "Divides.op dvd" (c,lint vars t)) 
    1.20        end 
    1.21 +    else (warning "Nonlinear term --- Non numeral leftside at dvd"
    1.22 +      ;raise COOPER)
    1.23    |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
    1.24    |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
    1.25    |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 

     2.1 --- a/src/HOL/Integ/cooper_proof.ML	Sun Aug 29 17:42:11 2004 +0200
     2.2 +++ b/src/HOL/Integ/cooper_proof.ML	Mon Aug 30 12:01:52 2004 +0200
     2.3 @@ -24,6 +24,12 @@
     2.4    val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
     2.5    val prove_elementar : Sign.sg -> string -> term -> thm
     2.6    val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
     2.7 +  val timef : (unit->thm) -> thm
     2.8 +  val prtime : unit -> unit
     2.9 +  val time_reset  : unit -> unit
    2.10 +  val timef2 : (unit->thm) -> thm
    2.11 +  val prtime2 : unit -> unit
    2.12 +  val time_reset2  : unit -> unit
    2.13  end;
    2.14  
    2.15  structure CooperProof : COOPER_PROOF =
    2.16 @@ -827,7 +833,10 @@
    2.17     |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
    2.18     |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
    2.19     |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
    2.20 -   |(Const("Divides.op dvd",_)$d$r) => ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd)))
    2.21 +   |(Const("Divides.op dvd",_)$d$r) => 
    2.22 +     if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd)))
    2.23 +     else (warning "Nonlinear Term --- Non numeral leftside at dvd";
    2.24 +       raise COOPER)
    2.25     |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
    2.26  
    2.27  fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f;
    2.28 @@ -870,6 +879,9 @@
    2.29  (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
    2.30  (* ------------------------------------------------------------------------- *)
    2.31  
    2.32 +val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();
    2.33 +val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer();
    2.34 +
    2.35  fun cooper_prv sg (x as Free(xn,xT)) efm = let 
    2.36     (* lfm_thm : efm = linearized form of efm*)
    2.37     val lfm_thm = proof_of_linform sg [xn] efm
    2.38 @@ -901,12 +913,16 @@
    2.39     val dlcm = mk_numeral (divlcm x cfm)
    2.40     (* Which set is smaller to generate the (hoepfully) shorter proof*)
    2.41     val cms = if ((length A) < (length B )) then "pi" else "mi"
    2.42 +   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"
    2.43     (* synthesize the proof of cooper's theorem*)
    2.44      (* cp_thm: EX x. cfm = Q*)
    2.45 -   val cp_thm = cooper_thm sg cms x cfm dlcm A B
    2.46 +   val cp_thm = timef ( fn () => cooper_thm sg cms x cfm dlcm A B)
    2.47     (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    2.48     (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
    2.49 -   val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
    2.50 +   val _ = prth cp_thm
    2.51 +   val _ = writeln "Expanding the bounded EX..."
    2.52 +   val exp_cp_thm = timef2 (fn () => refl RS (simplify ss (cp_thm RSN (2,trans))))
    2.53 +   val _ = writeln "Expanded"
    2.54     (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    2.55     val (lsuth,rsuth) = qe_get_terms (uth)
    2.56     (* lseacth = EX x. efm; rseacth = EX x. fm*)

     3.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Sun Aug 29 17:42:11 2004 +0200
     3.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Mon Aug 30 12:01:52 2004 +0200
     3.3 @@ -14,6 +14,7 @@
     3.4    val is_arith_rel : term -> bool
     3.5    val mk_numeral : int -> term
     3.6    val dest_numeral : term -> int
     3.7 +  val is_numeral : term -> bool
     3.8    val zero : term
     3.9    val one : term
    3.10    val linear_cmul : int -> term -> term
    3.11 @@ -208,10 +209,13 @@
    3.12   
    3.13  fun mkatom vars p t = Const(p,HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ zero $ (lint vars t); 
    3.14   
    3.15 -fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =  
    3.16 +fun linform vars (Const ("Divides.op dvd",_) $ c $ t) =
    3.17 +    if is_numeral c then   
    3.18        let val c' = (mk_numeral(abs(dest_numeral c)))  
    3.19        in (HOLogic.mk_binrel "Divides.op dvd" (c,lint vars t)) 
    3.20        end 
    3.21 +    else (warning "Nonlinear term --- Non numeral leftside at dvd"
    3.22 +      ;raise COOPER)
    3.23    |linform vars  (Const("op =",Type ("fun",[Type ("IntDef.int", []),_])) $ s $ t ) = (mkatom vars "op =" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s) ) 
    3.24    |linform vars  (Const("op <",_)$ s $t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ t $ s))
    3.25    |linform vars  (Const("op >",_) $ s $ t ) = (mkatom vars "op <" (Const ("op -",HOLogic.intT --> HOLogic.intT --> HOLogic.intT) $ s $ t)) 

     4.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Sun Aug 29 17:42:11 2004 +0200
     4.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Mon Aug 30 12:01:52 2004 +0200
     4.3 @@ -24,6 +24,12 @@
     4.4    val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
     4.5    val prove_elementar : Sign.sg -> string -> term -> thm
     4.6    val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
     4.7 +  val timef : (unit->thm) -> thm
     4.8 +  val prtime : unit -> unit
     4.9 +  val time_reset  : unit -> unit
    4.10 +  val timef2 : (unit->thm) -> thm
    4.11 +  val prtime2 : unit -> unit
    4.12 +  val time_reset2  : unit -> unit
    4.13  end;
    4.14  
    4.15  structure CooperProof : COOPER_PROOF =
    4.16 @@ -827,7 +833,10 @@
    4.17     |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
    4.18     |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
    4.19     |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
    4.20 -   |(Const("Divides.op dvd",_)$d$r) => ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd)))
    4.21 +   |(Const("Divides.op dvd",_)$d$r) => 
    4.22 +     if is_numeral d then ([], fn [] => (prove_elementar sg "lf" (HOLogic.mk_eq (r, lint vars r))) RS (instantiate' [] [None , None, Some (cterm_of sg d)](linearize_dvd)))
    4.23 +     else (warning "Nonlinear Term --- Non numeral leftside at dvd";
    4.24 +       raise COOPER)
    4.25     |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
    4.26  
    4.27  fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f;
    4.28 @@ -870,6 +879,9 @@
    4.29  (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
    4.30  (* ------------------------------------------------------------------------- *)
    4.31  
    4.32 +val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();
    4.33 +val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer();
    4.34 +
    4.35  fun cooper_prv sg (x as Free(xn,xT)) efm = let 
    4.36     (* lfm_thm : efm = linearized form of efm*)
    4.37     val lfm_thm = proof_of_linform sg [xn] efm
    4.38 @@ -901,12 +913,16 @@
    4.39     val dlcm = mk_numeral (divlcm x cfm)
    4.40     (* Which set is smaller to generate the (hoepfully) shorter proof*)
    4.41     val cms = if ((length A) < (length B )) then "pi" else "mi"
    4.42 +   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"
    4.43     (* synthesize the proof of cooper's theorem*)
    4.44      (* cp_thm: EX x. cfm = Q*)
    4.45 -   val cp_thm = cooper_thm sg cms x cfm dlcm A B
    4.46 +   val cp_thm = timef ( fn () => cooper_thm sg cms x cfm dlcm A B)
    4.47     (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    4.48     (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
    4.49 -   val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
    4.50 +   val _ = prth cp_thm
    4.51 +   val _ = writeln "Expanding the bounded EX..."
    4.52 +   val exp_cp_thm = timef2 (fn () => refl RS (simplify ss (cp_thm RSN (2,trans))))
    4.53 +   val _ = writeln "Expanded"
    4.54     (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    4.55     val (lsuth,rsuth) = qe_get_terms (uth)
    4.56     (* lseacth = EX x. efm; rseacth = EX x. fm*)