src/HOL/Library/positivstellensatz.ML
changeset 63211 0bec0d1d9998
parent 63205 97b721666890
child 63648 f9f3006a5579
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 17:46:12 2016 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 19:23:18 2016 +0200
     1.3 @@ -615,10 +615,10 @@
     1.4               in
     1.5                 if c1 * c2 >= @0 then acc else
     1.6                 let
     1.7 -                 val e1' = linear_cmul (Rat.abs c2) e1
     1.8 -                 val e2' = linear_cmul (Rat.abs c1) e2
     1.9 -                 val p1' = Product(Rational_lt(Rat.abs c2),p1)
    1.10 -                 val p2' = Product(Rational_lt(Rat.abs c1),p2)
    1.11 +                 val e1' = linear_cmul (abs c2) e1
    1.12 +                 val e2' = linear_cmul (abs c1) e2
    1.13 +                 val p1' = Product(Rational_lt (abs c2), p1)
    1.14 +                 val p2' = Product(Rational_lt (abs c1), p2)
    1.15                 in (linear_add e1' e2',Sum(p1',p2'))::acc
    1.16                 end
    1.17               end
    1.18 @@ -653,11 +653,11 @@
    1.19               let val d = FuncUtil.Ctermfunc.tryapplyd t x @0 in
    1.20                 if d = @0 then inp else
    1.21                 let
    1.22 -                 val k = (Rat.neg d) * Rat.abs c / c
    1.23 +                 val k = ~ d * abs c / c
    1.24                   val e' = linear_cmul k e
    1.25 -                 val t' = linear_cmul (Rat.abs c) t
    1.26 +                 val t' = linear_cmul (abs c) t
    1.27                   val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
    1.28 -                 val q' = Product(Rational_lt(Rat.abs c),q)
    1.29 +                 val q' = Product(Rational_lt (abs c), q)
    1.30                 in (linear_add e' t',Sum(p',q'))
    1.31                 end
    1.32               end