src/HOL/Library/positivstellensatz.ML
changeset 63205 97b721666890
parent 63201 f151704c08e4
child 63211 0bec0d1d9998
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 15:01:43 2016 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 15:10:27 2016 +0200
     1.3 @@ -338,7 +338,7 @@
     1.4  
     1.5  fun cterm_of_cmonomial (m,c) =
     1.6    if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
     1.7 -  else if c = Rat.one then cterm_of_monomial m
     1.8 +  else if c = @1 then cterm_of_monomial m
     1.9    else Thm.apply (Thm.apply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
    1.10  
    1.11  fun cterm_of_poly p =
    1.12 @@ -585,35 +585,35 @@
    1.13  
    1.14  (* A linear arithmetic prover *)
    1.15  local
    1.16 -  val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = Rat.zero)
    1.17 +  val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = @0)
    1.18    fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c * x)
    1.19    val one_tm = @{cterm "1::real"}
    1.20 -  fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
    1.21 +  fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p @0)) orelse
    1.22       ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
    1.23         not(p(FuncUtil.Ctermfunc.apply e one_tm)))
    1.24  
    1.25    fun linear_ineqs vars (les,lts) =
    1.26 -    case find_first (contradictory (fn x => x > Rat.zero)) lts of
    1.27 +    case find_first (contradictory (fn x => x > @0)) lts of
    1.28        SOME r => r
    1.29      | NONE =>
    1.30 -      (case find_first (contradictory (fn x => x > Rat.zero)) les of
    1.31 +      (case find_first (contradictory (fn x => x > @0)) les of
    1.32           SOME r => r
    1.33         | NONE =>
    1.34           if null vars then error "linear_ineqs: no contradiction" else
    1.35           let
    1.36             val ineqs = les @ lts
    1.37             fun blowup v =
    1.38 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) ineqs) +
    1.39 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) ineqs) *
    1.40 -             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero < Rat.zero) ineqs)
    1.41 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) ineqs) +
    1.42 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) ineqs) *
    1.43 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 < @0) ineqs)
    1.44             val v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j))
    1.45               (map (fn v => (v,blowup v)) vars)))
    1.46             fun addup (e1,p1) (e2,p2) acc =
    1.47               let
    1.48 -               val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v Rat.zero
    1.49 -               val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v Rat.zero
    1.50 +               val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v @0
    1.51 +               val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v @0
    1.52               in
    1.53 -               if c1 * c2 >= Rat.zero then acc else
    1.54 +               if c1 * c2 >= @0 then acc else
    1.55                 let
    1.56                   val e1' = linear_cmul (Rat.abs c2) e1
    1.57                   val e2' = linear_cmul (Rat.abs c1) e2
    1.58 @@ -623,13 +623,13 @@
    1.59                 end
    1.60               end
    1.61             val (les0,les1) =
    1.62 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) les
    1.63 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) les
    1.64             val (lts0,lts1) =
    1.65 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero = Rat.zero) lts
    1.66 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 = @0) lts
    1.67             val (lesp,lesn) =
    1.68 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) les1
    1.69 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) les1
    1.70             val (ltsp,ltsn) =
    1.71 -             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero > Rat.zero) lts1
    1.72 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v @0 > @0) lts1
    1.73             val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0
    1.74             val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn
    1.75                        (fold_rev (fn ep1 => fold_rev (addup ep1) (lesn@ltsn)) ltsp lts0)
    1.76 @@ -637,7 +637,7 @@
    1.77           end)
    1.78  
    1.79    fun linear_eqs(eqs,les,lts) =
    1.80 -    case find_first (contradictory (fn x => x = Rat.zero)) eqs of
    1.81 +    case find_first (contradictory (fn x => x = @0)) eqs of
    1.82        SOME r => r
    1.83      | NONE =>
    1.84        (case eqs of
    1.85 @@ -650,8 +650,8 @@
    1.86           let
    1.87             val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.delete_safe one_tm e)
    1.88             fun xform (inp as (t,q)) =
    1.89 -             let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
    1.90 -               if d = Rat.zero then inp else
    1.91 +             let val d = FuncUtil.Ctermfunc.tryapplyd t x @0 in
    1.92 +               if d = @0 then inp else
    1.93                 let
    1.94                   val k = (Rat.neg d) * Rat.abs c / c
    1.95                   val e' = linear_cmul k e
    1.96 @@ -674,12 +674,12 @@
    1.97  
    1.98    fun lin_of_hol ct =
    1.99      if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.empty
   1.100 -    else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   1.101 +    else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, @1)
   1.102      else if is_ratconst ct then FuncUtil.Ctermfunc.onefunc (one_tm, dest_ratconst ct)
   1.103      else
   1.104        let val (lop,r) = Thm.dest_comb ct
   1.105        in
   1.106 -        if not (is_comb lop) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   1.107 +        if not (is_comb lop) then FuncUtil.Ctermfunc.onefunc (ct, @1)
   1.108          else
   1.109            let val (opr,l) = Thm.dest_comb lop
   1.110            in
   1.111 @@ -687,7 +687,7 @@
   1.112              then linear_add (lin_of_hol l) (lin_of_hol r)
   1.113              else if opr aconvc @{cterm "op * :: real =>_"}
   1.114                      andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
   1.115 -            else FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   1.116 +            else FuncUtil.Ctermfunc.onefunc (ct, @1)
   1.117            end
   1.118        end
   1.119  
   1.120 @@ -707,7 +707,7 @@
   1.121      val aliens = filter is_alien
   1.122        (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom)
   1.123                  (eq_pols @ le_pols @ lt_pols) [])
   1.124 -    val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
   1.125 +    val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,@1)) aliens
   1.126      val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
   1.127      val le' = le @ map (fn a => Thm.instantiate' [] [SOME (Thm.dest_arg a)] @{thm of_nat_0_le_iff}) aliens
   1.128    in ((translator (eq,le',lt) proof), Trivial)