src/HOL/Integ/cooper_proof.ML
changeset 15164 5d7c96e0f9dc
parent 15123 4c49281dc9a8
child 15165 a1e84e86c583
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Sun Aug 29 17:42:11 2004 +0200
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Mon Aug 30 12:01:52 2004 +0200
     1.3 @@ -24,6 +24,12 @@
     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 @@ -827,7 +833,10 @@
    1.17     |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
    1.18     |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
    1.19     |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
    1.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)))
    1.21 +   |(Const("Divides.op dvd",_)$d$r) => 
    1.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)))
    1.23 +     else (warning "Nonlinear Term --- Non numeral leftside at dvd";
    1.24 +       raise COOPER)
    1.25     |_ => ([], fn [] => prove_elementar sg "lf" (HOLogic.mk_eq (t, linform vars t)));
    1.26  
    1.27  fun proof_of_linform sg vars f = thm_of sg (decomp_linform sg vars) f;
    1.28 @@ -870,6 +879,9 @@
    1.29  (* It shoud be plugged in the qfnp argument of the quantifier elimination proof function*)
    1.30  (* ------------------------------------------------------------------------- *)
    1.31  
    1.32 +val (timef:(unit->thm) -> thm,prtime,time_reset) = gen_timer();
    1.33 +val (timef2:(unit->thm) -> thm,prtime2,time_reset2) = gen_timer();
    1.34 +
    1.35  fun cooper_prv sg (x as Free(xn,xT)) efm = let 
    1.36     (* lfm_thm : efm = linearized form of efm*)
    1.37     val lfm_thm = proof_of_linform sg [xn] efm
    1.38 @@ -901,12 +913,16 @@
    1.39     val dlcm = mk_numeral (divlcm x cfm)
    1.40     (* Which set is smaller to generate the (hoepfully) shorter proof*)
    1.41     val cms = if ((length A) < (length B )) then "pi" else "mi"
    1.42 +   val _ = if cms = "pi" then writeln "Plusinfinity" else writeln "Minusinfinity"
    1.43     (* synthesize the proof of cooper's theorem*)
    1.44      (* cp_thm: EX x. cfm = Q*)
    1.45 -   val cp_thm = cooper_thm sg cms x cfm dlcm A B
    1.46 +   val cp_thm = timef ( fn () => cooper_thm sg cms x cfm dlcm A B)
    1.47     (* Exxpand the right hand side to get rid of EX j : {1..d} to get a huge disjunction*)
    1.48     (* exp_cp_thm: EX x.cfm = Q' , where Q' is a simplified version of Q*)
    1.49 -   val exp_cp_thm = refl RS (simplify ss (cp_thm RSN (2,trans)))
    1.50 +   val _ = prth cp_thm
    1.51 +   val _ = writeln "Expanding the bounded EX..."
    1.52 +   val exp_cp_thm = timef2 (fn () => refl RS (simplify ss (cp_thm RSN (2,trans))))
    1.53 +   val _ = writeln "Expanded"
    1.54     (* lsuth = EX.P(l*x) ; rsuth = EX x. l dvd x & P x*)
    1.55     val (lsuth,rsuth) = qe_get_terms (uth)
    1.56     (* lseacth = EX x. efm; rseacth = EX x. fm*)