src/HOL/Library/positivstellensatz.ML
changeset 46497 89ccf66aa73d
parent 45654 cf10bde35973
child 46594 f11f332b964f
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Feb 15 22:44:31 2012 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Feb 15 23:19:30 2012 +0100
     1.3 @@ -285,7 +285,7 @@
     1.4  let val (a, b) = Rat.quotient_of_rat x
     1.5  in 
     1.6   if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
     1.7 -  else Thm.capply (Thm.capply @{cterm "op / :: real => _"} 
     1.8 +  else Thm.apply (Thm.apply @{cterm "op / :: real => _"} 
     1.9                     (Numeral.mk_cnumber @{ctyp "real"} a))
    1.10          (Numeral.mk_cnumber @{ctyp "real"} b)
    1.11  end;
    1.12 @@ -319,7 +319,7 @@
    1.13  
    1.14  (* Map back polynomials to HOL.                         *)
    1.15  
    1.16 -fun cterm_of_varpow x k = if k = 1 then x else Thm.capply (Thm.capply @{cterm "op ^ :: real => _"} x) 
    1.17 +fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply @{cterm "op ^ :: real => _"} x) 
    1.18    (Numeral.mk_cnumber @{ctyp nat} k)
    1.19  
    1.20  fun cterm_of_monomial m = 
    1.21 @@ -328,12 +328,12 @@
    1.22    let 
    1.23     val m' = FuncUtil.dest_monomial m
    1.24     val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' [] 
    1.25 -  in foldr1 (fn (s, t) => Thm.capply (Thm.capply @{cterm "op * :: real => _"} s) t) vps
    1.26 +  in foldr1 (fn (s, t) => Thm.apply (Thm.apply @{cterm "op * :: real => _"} s) t) vps
    1.27    end
    1.28  
    1.29  fun cterm_of_cmonomial (m,c) = if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
    1.30      else if c = Rat.one then cterm_of_monomial m
    1.31 -    else Thm.capply (Thm.capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
    1.32 +    else Thm.apply (Thm.apply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
    1.33  
    1.34  fun cterm_of_poly p = 
    1.35   if FuncUtil.Monomialfunc.is_empty p then @{cterm "0::real"} 
    1.36 @@ -341,7 +341,7 @@
    1.37    let 
    1.38     val cms = map cterm_of_cmonomial
    1.39       (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
    1.40 -  in foldr1 (fn (t1, t2) => Thm.capply(Thm.capply @{cterm "op + :: real => _"} t1) t2) cms
    1.41 +  in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply @{cterm "op + :: real => _"} t1) t2) cms
    1.42    end;
    1.43  
    1.44      (* A general real arithmetic prover *)
    1.45 @@ -397,14 +397,14 @@
    1.46          Axiom_eq n => nth eqs n
    1.47        | Axiom_le n => nth les n
    1.48        | Axiom_lt n => nth lts n
    1.49 -      | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.capply @{cterm Trueprop} 
    1.50 -                          (Thm.capply (Thm.capply @{cterm "op =::real => _"} (mk_numeric x)) 
    1.51 +      | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply @{cterm Trueprop} 
    1.52 +                          (Thm.apply (Thm.apply @{cterm "op =::real => _"} (mk_numeric x)) 
    1.53                                 @{cterm "0::real"})))
    1.54 -      | Rational_le x => eqT_elim(numeric_ge_conv(Thm.capply @{cterm Trueprop} 
    1.55 -                          (Thm.capply (Thm.capply @{cterm "op <=::real => _"} 
    1.56 +      | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply @{cterm Trueprop} 
    1.57 +                          (Thm.apply (Thm.apply @{cterm "op <=::real => _"} 
    1.58                                       @{cterm "0::real"}) (mk_numeric x))))
    1.59 -      | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.capply @{cterm Trueprop} 
    1.60 -                      (Thm.capply (Thm.capply @{cterm "op <::real => _"} @{cterm "0::real"})
    1.61 +      | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply @{cterm Trueprop} 
    1.62 +                      (Thm.apply (Thm.apply @{cterm "op <::real => _"} @{cterm "0::real"})
    1.63                          (mk_numeric x))))
    1.64        | Square pt => square_rule (cterm_of_poly pt)
    1.65        | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
    1.66 @@ -432,8 +432,8 @@
    1.67         val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
    1.68     in Thm.implies_elim (Thm.implies_elim
    1.69            (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
    1.70 -          (Thm.implies_intr (Thm.capply @{cterm Trueprop} p) th1))
    1.71 -        (Thm.implies_intr (Thm.capply @{cterm Trueprop} q) th2)
    1.72 +          (Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
    1.73 +        (Thm.implies_intr (Thm.apply @{cterm Trueprop} q) th2)
    1.74     end
    1.75   fun overall cert_choice dun ths = case ths of
    1.76    [] =>
    1.77 @@ -452,8 +452,8 @@
    1.78        overall cert_choice dun (th1::th2::oths) end
    1.79      else if is_disj ct then
    1.80        let 
    1.81 -       val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
    1.82 -       val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
    1.83 +       val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
    1.84 +       val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
    1.85        in (disj_cases th th1 th2, Branch (cert1, cert2)) end
    1.86     else overall cert_choice (th::dun) oths
    1.87    end
    1.88 @@ -469,8 +469,8 @@
    1.89      val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
    1.90      val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
    1.91      val th' = Drule.binop_cong_rule @{cterm HOL.disj} 
    1.92 -     (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
    1.93 -     (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
    1.94 +     (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
    1.95 +     (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
    1.96      in Thm.transitive th th' 
    1.97    end
    1.98   fun equal_implies_1_rule PQ = 
    1.99 @@ -496,7 +496,7 @@
   1.100    val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   1.101  
   1.102   fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   1.103 - fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
   1.104 + fun mk_ex v t = Thm.apply (ext (ctyp_of_term v)) (Thm.lambda v t)
   1.105  
   1.106   fun choose v th th' = case concl_of th of 
   1.107     @{term Trueprop} $ (Const(@{const_name Ex},_)$_) => 
   1.108 @@ -506,13 +506,13 @@
   1.109       val th0 = fconv_rule (Thm.beta_conversion true)
   1.110           (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
   1.111       val pv = (Thm.rhs_of o Thm.beta_conversion true) 
   1.112 -           (Thm.capply @{cterm Trueprop} (Thm.capply p v))
   1.113 +           (Thm.apply @{cterm Trueprop} (Thm.apply p v))
   1.114       val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
   1.115      in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
   1.116   | _ => raise THM ("choose",0,[th, th'])
   1.117  
   1.118    fun simple_choose v th = 
   1.119 -     choose v (Thm.assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
   1.120 +     choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
   1.121  
   1.122   val strip_forall =
   1.123    let fun h (acc, t) =
   1.124 @@ -534,7 +534,7 @@
   1.125    fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
   1.126                    (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv 
   1.127          try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
   1.128 -  val nct = Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} ct)
   1.129 +  val nct = Thm.apply @{cterm Trueprop} (Thm.apply @{cterm "Not"} ct)
   1.130    val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
   1.131    val tm0 = Thm.dest_arg (Thm.rhs_of th0)
   1.132    val (th, certificates) = if tm0 aconvc @{cterm False} then (equal_implies_1_rule th0, Trivial) else
   1.133 @@ -543,7 +543,7 @@
   1.134      val (avs,ibod) = strip_forall bod
   1.135      val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
   1.136      val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
   1.137 -    val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.capply @{cterm Trueprop} bod))) th2)
   1.138 +    val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
   1.139     in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
   1.140     end
   1.141    in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
   1.142 @@ -699,7 +699,7 @@
   1.143     fun eliminate_construct p c tm =
   1.144      let 
   1.145       val t = find_cterm p tm
   1.146 -     val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
   1.147 +     val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.apply (Thm.lambda t tm) t)
   1.148       val (p,ax) = (Thm.dest_comb o Thm.rhs_of) th0
   1.149      in fconv_rule(arg_conv(binop_conv (arg_conv (Thm.beta_conversion false))))
   1.150                 (Thm.transitive th0 (c p ax))