--- a/src/HOL/Integ/cooper_proof.ML Mon Aug 30 12:01:52 2004 +0200
+++ b/src/HOL/Integ/cooper_proof.ML Mon Aug 30 14:40:18 2004 +0200
@@ -24,12 +24,6 @@
val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
val prove_elementar : Sign.sg -> string -> term -> thm
val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
- val timef : (unit->thm) -> thm
- val prtime : unit -> unit
- val time_reset : unit -> unit
- val timef2 : (unit->thm) -> thm
- val prtime2 : unit -> unit
- val time_reset2 : unit -> unit
end;
structure CooperProof : COOPER_PROOF =
@@ -879,8 +873,8 @@
(* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
(* ------------------------------------------------------------------------- *)
-val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();
-val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer();
+(* val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();*)
+(* val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer(); *)
fun cooper_prv sg (x as Free(xn,xT)) efm = let
(* lfm_thm : efm = linearized form of efm*)
@@ -913,16 +907,19 @@
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"
- val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"
+(* val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*)
(* synthesize the proof of cooper's theorem*)
(* cp_thm: EX x. cfm = Q*)
- val cp_thm = timef ( fn () => cooper_thm sg cms x cfm dlcm A B)
+ 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*)
+(*
val _ = prth cp_thm
val _ = writeln "Expanding the bounded EX..."
- val exp_cp_thm = timef2 (fn () => refl RS (simplify ss (cp_thm RSN (2,trans))))
- val _ = writeln "Expanded"
+*)
+ val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
+(*
+ val _ = writeln "Expanded" *)
(* 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*)
--- a/src/HOL/Tools/Presburger/cooper_proof.ML Mon Aug 30 12:01:52 2004 +0200
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML Mon Aug 30 14:40:18 2004 +0200
@@ -24,12 +24,6 @@
val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
val prove_elementar : Sign.sg -> string -> term -> thm
val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
- val timef : (unit->thm) -> thm
- val prtime : unit -> unit
- val time_reset : unit -> unit
- val timef2 : (unit->thm) -> thm
- val prtime2 : unit -> unit
- val time_reset2 : unit -> unit
end;
structure CooperProof : COOPER_PROOF =
@@ -879,8 +873,8 @@
(* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
(* ------------------------------------------------------------------------- *)
-val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();
-val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer();
+(* val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();*)
+(* val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer(); *)
fun cooper_prv sg (x as Free(xn,xT)) efm = let
(* lfm_thm : efm = linearized form of efm*)
@@ -913,16 +907,19 @@
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"
- val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"
+(* val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*)
(* synthesize the proof of cooper's theorem*)
(* cp_thm: EX x. cfm = Q*)
- val cp_thm = timef ( fn () => cooper_thm sg cms x cfm dlcm A B)
+ 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*)
+(*
val _ = prth cp_thm
val _ = writeln "Expanding the bounded EX..."
- val exp_cp_thm = timef2 (fn () => refl RS (simplify ss (cp_thm RSN (2,trans))))
- val _ = writeln "Expanded"
+*)
+ val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
+(*
+ val _ = writeln "Expanded" *)
(* 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*)