src/HOL/Library/positivstellensatz.ML
changeset 63198 c583ca33076a
parent 62177 3a578ee55bff
child 63201 f151704c08e4
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue May 31 19:51:01 2016 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Tue May 31 21:54:10 2016 +0200
     1.3 @@ -585,27 +585,27 @@
     1.4  
     1.5  (* A linear arithmetic prover *)
     1.6  local
     1.7 -  val linear_add = FuncUtil.Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero)
     1.8 -  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c */ x)
     1.9 +  val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = Rat.zero)
    1.10 +  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c * x)
    1.11    val one_tm = @{cterm "1::real"}
    1.12    fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
    1.13       ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
    1.14         not(p(FuncUtil.Ctermfunc.apply e one_tm)))
    1.15  
    1.16    fun linear_ineqs vars (les,lts) =
    1.17 -    case find_first (contradictory (fn x => x >/ Rat.zero)) lts of
    1.18 +    case find_first (contradictory (fn x => x > Rat.zero)) lts of
    1.19        SOME r => r
    1.20      | NONE =>
    1.21 -      (case find_first (contradictory (fn x => x >/ Rat.zero)) les of
    1.22 +      (case find_first (contradictory (fn x => x > Rat.zero)) les of
    1.23           SOME r => r
    1.24         | NONE =>
    1.25           if null vars then error "linear_ineqs: no contradiction" else
    1.26           let
    1.27             val ineqs = les @ lts
    1.28             fun blowup v =
    1.29 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) ineqs) +
    1.30 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) ineqs) *
    1.31 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero </ Rat.zero) ineqs)
    1.32 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) ineqs) +
    1.33 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) ineqs) *
    1.34 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero < Rat.zero) ineqs)
    1.35             val v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j))
    1.36               (map (fn v => (v,blowup v)) vars)))
    1.37             fun addup (e1,p1) (e2,p2) acc =
    1.38 @@ -613,7 +613,7 @@
    1.39                 val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v Rat.zero
    1.40                 val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v Rat.zero
    1.41               in
    1.42 -               if c1 */ c2 >=/ Rat.zero then acc else
    1.43 +               if c1 * c2 >= Rat.zero then acc else
    1.44                 let
    1.45                   val e1' = linear_cmul (Rat.abs c2) e1
    1.46                   val e2' = linear_cmul (Rat.abs c1) e2
    1.47 @@ -623,13 +623,13 @@
    1.48                 end
    1.49               end
    1.50             val (les0,les1) =
    1.51 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) les
    1.52 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) les
    1.53             val (lts0,lts1) =
    1.54 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) lts
    1.55 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) lts
    1.56             val (lesp,lesn) =
    1.57 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) les1
    1.58 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) les1
    1.59             val (ltsp,ltsn) =
    1.60 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) lts1
    1.61 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) lts1
    1.62             val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0
    1.63             val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn
    1.64                        (fold_rev (fn ep1 => fold_rev (addup ep1) (lesn@ltsn)) ltsp lts0)
    1.65 @@ -637,7 +637,7 @@
    1.66           end)
    1.67  
    1.68    fun linear_eqs(eqs,les,lts) =
    1.69 -    case find_first (contradictory (fn x => x =/ Rat.zero)) eqs of
    1.70 +    case find_first (contradictory (fn x => x = Rat.zero)) eqs of
    1.71        SOME r => r
    1.72      | NONE =>
    1.73        (case eqs of
    1.74 @@ -651,9 +651,9 @@
    1.75             val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.delete_safe one_tm e)
    1.76             fun xform (inp as (t,q)) =
    1.77               let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
    1.78 -               if d =/ Rat.zero then inp else
    1.79 +               if d = Rat.zero then inp else
    1.80                 let
    1.81 -                 val k = (Rat.neg d) */ Rat.abs c // c
    1.82 +                 val k = (Rat.neg d) * Rat.abs c / c
    1.83                   val e' = linear_cmul k e
    1.84                   val t' = linear_cmul (Rat.abs c) t
    1.85                   val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)