src/HOL/Library/positivstellensatz.ML
changeset 61609 77b453bd616f
parent 61075 f6b0d827240e
child 61945 1135b8de26c3
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Nov 03 11:20:21 2015 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Tue Nov 10 14:18:41 2015 +0000
     1.3 @@ -695,8 +695,8 @@
     1.4  
     1.5    fun is_alien ct =
     1.6      case Thm.term_of ct of
     1.7 -      Const(@{const_name "real"}, _)$ n =>
     1.8 -      if can HOLogic.dest_number n then false else true
     1.9 +      Const(@{const_name "of_nat"}, _)$ n => not (can HOLogic.dest_number n)
    1.10 +    | Const(@{const_name "of_int"}, _)$ n => not (can HOLogic.dest_number n)
    1.11      | _ => false
    1.12  in
    1.13  fun real_linear_prover translator (eq,le,lt) =
    1.14 @@ -711,7 +711,7 @@
    1.15                  (eq_pols @ le_pols @ lt_pols) [])
    1.16      val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
    1.17      val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
    1.18 -    val le' = le @ map (fn a => Thm.instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens
    1.19 +    val le' = le @ map (fn a => Thm.instantiate' [] [SOME (Thm.dest_arg a)] @{thm of_nat_0_le_iff}) aliens
    1.20    in ((translator (eq,le',lt) proof), Trivial)
    1.21    end
    1.22  end;