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))
```