corrected
authorchaieb
Mon Aug 30 14:40:18 2004 +0200 (2004-08-30)
changeset 15165a1e84e86c583
parent 15164 5d7c96e0f9dc
child 15166 66f0584aa714
corrected
src/HOL/Integ/cooper_proof.ML
src/HOL/Tools/Presburger/cooper_proof.ML
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Mon Aug 30 12:01:52 2004 +0200
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Mon Aug 30 14:40:18 2004 +0200
     1.3 @@ -24,12 +24,6 @@
     1.4    val proof_of_adjustcoeffeq : Sign.sg -> term -> int -> term -> thm
     1.5    val prove_elementar : Sign.sg -> string -> term -> thm
     1.6    val thm_of : Sign.sg -> (term -> (term list * (thm list -> thm))) -> term -> thm
     1.7 -  val timef : (unit->thm) -> thm
     1.8 -  val prtime : unit -> unit
     1.9 -  val time_reset  : unit -> unit
    1.10 -  val timef2 : (unit->thm) -> thm
    1.11 -  val prtime2 : unit -> unit
    1.12 -  val time_reset2  : unit -> unit
    1.13  end;
    1.14  
    1.15  structure CooperProof : COOPER_PROOF =
    1.16 @@ -879,8 +873,8 @@
    1.17  (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
    1.18  (* ------------------------------------------------------------------------- *)
    1.19  
    1.20 -val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();
    1.21 -val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer();
    1.22 +(* val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();*)
    1.23 +(* val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer(); *)
    1.24  
    1.25  fun cooper_prv sg (x as Free(xn,xT)) efm = let 
    1.26     (* lfm_thm : efm = linearized form of efm*)
    1.27 @@ -913,16 +907,19 @@
    1.28     val dlcm = mk_numeral (divlcm x cfm)
    1.29     (* Which set is smaller to generate the (hoepfully) shorter proof*)
    1.30     val cms = if ((length A) < (length B )) then "pi" else "mi"
    1.31 -   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"
    1.32 +(*   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*)
    1.33     (* synthesize the proof of cooper's theorem*)
    1.34      (* cp_thm: EX x. cfm = Q*)
    1.35 -   val cp_thm = timef ( fn () => cooper_thm sg cms x cfm dlcm A B)
    1.36 +   val cp_thm =  cooper_thm sg cms x cfm dlcm A B
    1.37     (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    1.38     (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
    1.39 +(*
    1.40     val _ = prth cp_thm
    1.41     val _ = writeln "Expanding the bounded EX..."
    1.42 -   val exp_cp_thm = timef2 (fn () => refl RS (simplify ss (cp_thm RSN (2,trans))))
    1.43 -   val _ = writeln "Expanded"
    1.44 +*)
    1.45 +   val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
    1.46 +(*
    1.47 +   val _ = writeln "Expanded" *)
    1.48     (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    1.49     val (lsuth,rsuth) = qe_get_terms (uth)
    1.50     (* lseacth = EX x. efm; rseacth = EX x. fm*)
     2.1 --- a/src/HOL/Tools/Presburger/cooper_proof.ML	Mon Aug 30 12:01:52 2004 +0200
     2.2 +++ b/src/HOL/Tools/Presburger/cooper_proof.ML	Mon Aug 30 14:40:18 2004 +0200
     2.3 @@ -24,12 +24,6 @@
     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 @@ -879,8 +873,8 @@
    2.17  (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
    2.18  (* ------------------------------------------------------------------------- *)
    2.19  
    2.20 -val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();
    2.21 -val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer();
    2.22 +(* val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();*)
    2.23 +(* val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer(); *)
    2.24  
    2.25  fun cooper_prv sg (x as Free(xn,xT)) efm = let 
    2.26     (* lfm_thm : efm = linearized form of efm*)
    2.27 @@ -913,16 +907,19 @@
    2.28     val dlcm = mk_numeral (divlcm x cfm)
    2.29     (* Which set is smaller to generate the (hoepfully) shorter proof*)
    2.30     val cms = if ((length A) < (length B )) then "pi" else "mi"
    2.31 -   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"
    2.32 +(*   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"*)
    2.33     (* synthesize the proof of cooper's theorem*)
    2.34      (* cp_thm: EX x. cfm = Q*)
    2.35 -   val cp_thm = timef ( fn () => cooper_thm sg cms x cfm dlcm A B)
    2.36 +   val cp_thm =  cooper_thm sg cms x cfm dlcm A B
    2.37     (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    2.38     (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
    2.39 +(*
    2.40     val _ = prth cp_thm
    2.41     val _ = writeln "Expanding the bounded EX..."
    2.42 -   val exp_cp_thm = timef2 (fn () => refl RS (simplify ss (cp_thm RSN (2,trans))))
    2.43 -   val _ = writeln "Expanded"
    2.44 +*)
    2.45 +   val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
    2.46 +(*
    2.47 +   val _ = writeln "Expanded" *)
    2.48     (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    2.49     val (lsuth,rsuth) = qe_get_terms (uth)
    2.50     (* lseacth = EX x. efm; rseacth = EX x. fm*)