src/HOL/Library/positivstellensatz.ML
changeset 67232 a00f5a71e672
parent 67091 1393c2340eec
child 67267 c5994f1fa0fa
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Dec 20 21:06:08 2017 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Dec 20 21:52:35 2017 +0100
     1.3 @@ -370,8 +370,8 @@
     1.4      fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
     1.5      fun oprconv cv ct =
     1.6        let val g = Thm.dest_fun2 ct
     1.7 -      in if g aconvc @{cterm "op <= :: real => _"}
     1.8 -            orelse g aconvc @{cterm "op < :: real => _"}
     1.9 +      in if g aconvc @{cterm "(op <=) :: real => _"}
    1.10 +            orelse g aconvc @{cterm "(op <) :: real => _"}
    1.11           then arg_conv cv ct else arg1_conv cv ct
    1.12        end
    1.13  
    1.14 @@ -406,13 +406,13 @@
    1.15            | Axiom_le n => nth les n
    1.16            | Axiom_lt n => nth lts n
    1.17            | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply @{cterm Trueprop}
    1.18 -                          (Thm.apply (Thm.apply @{cterm "op =::real => _"} (mk_numeric x))
    1.19 +                          (Thm.apply (Thm.apply @{cterm "(op =)::real => _"} (mk_numeric x))
    1.20                                 @{cterm "0::real"})))
    1.21            | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply @{cterm Trueprop}
    1.22 -                          (Thm.apply (Thm.apply @{cterm "op <=::real => _"}
    1.23 +                          (Thm.apply (Thm.apply @{cterm "(op <=)::real => _"}
    1.24                                       @{cterm "0::real"}) (mk_numeric x))))
    1.25            | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply @{cterm Trueprop}
    1.26 -                      (Thm.apply (Thm.apply @{cterm "op <::real => _"} @{cterm "0::real"})
    1.27 +                      (Thm.apply (Thm.apply @{cterm "(op <)::real => _"} @{cterm "0::real"})
    1.28                          (mk_numeric x))))
    1.29            | Square pt => square_rule (cterm_of_poly pt)
    1.30            | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
    1.31 @@ -428,9 +428,9 @@
    1.32  
    1.33      val concl = Thm.dest_arg o Thm.cprop_of
    1.34      fun is_binop opr ct = (Thm.dest_fun2 ct aconvc opr handle CTERM _ => false)
    1.35 -    val is_req = is_binop @{cterm "op =:: real => _"}
    1.36 -    val is_ge = is_binop @{cterm "op <=:: real => _"}
    1.37 -    val is_gt = is_binop @{cterm "op <:: real => _"}
    1.38 +    val is_req = is_binop @{cterm "(op =):: real => _"}
    1.39 +    val is_ge = is_binop @{cterm "(op <=):: real => _"}
    1.40 +    val is_gt = is_binop @{cterm "(op <):: real => _"}
    1.41      val is_conj = is_binop @{cterm HOL.conj}
    1.42      val is_disj = is_binop @{cterm HOL.disj}
    1.43      fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
    1.44 @@ -476,7 +476,7 @@
    1.45      fun dest_binary b ct =
    1.46          if is_binop b ct then Thm.dest_binop ct
    1.47          else raise CTERM ("dest_binary",[b,ct])
    1.48 -    val dest_eq = dest_binary @{cterm "op = :: real => _"}
    1.49 +    val dest_eq = dest_binary @{cterm "(op =) :: real => _"}
    1.50      val neq_th = nth pth 5
    1.51      fun real_not_eq_conv ct =
    1.52        let
    1.53 @@ -486,8 +486,8 @@
    1.54          val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
    1.55          val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
    1.56          val th' = Drule.binop_cong_rule @{cterm HOL.disj}
    1.57 -          (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
    1.58 -          (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
    1.59 +          (Drule.arg_cong_rule (Thm.apply @{cterm "(op <)::real=>_"} @{cterm "0::real"}) th_p)
    1.60 +          (Drule.arg_cong_rule (Thm.apply @{cterm "(op <)::real=>_"} @{cterm "0::real"}) th_n)
    1.61        in Thm.transitive th th'
    1.62        end
    1.63      fun equal_implies_1_rule PQ =