src/HOL/Library/positivstellensatz.ML
changeset 67399 eab6ce8368fa
parent 67271 48ef58c6cf4c
child 67559 833d154ab189
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -290,7 +290,7 @@
     1.4      val (a, b) = Rat.dest x
     1.5    in
     1.6      if b = 1 then Numeral.mk_cnumber \<^ctyp>\<open>real\<close> a
     1.7 -    else Thm.apply (Thm.apply \<^cterm>\<open>op / :: real \<Rightarrow> _\<close>
     1.8 +    else Thm.apply (Thm.apply \<^cterm>\<open>(/) :: real \<Rightarrow> _\<close>
     1.9        (Numeral.mk_cnumber \<^ctyp>\<open>real\<close> a))
    1.10        (Numeral.mk_cnumber \<^ctyp>\<open>real\<close> b)
    1.11    end;
    1.12 @@ -324,7 +324,7 @@
    1.13  
    1.14  (* Map back polynomials to HOL.                         *)
    1.15  
    1.16 -fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply \<^cterm>\<open>op ^ :: real \<Rightarrow> _\<close> x)
    1.17 +fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply \<^cterm>\<open>(^) :: real \<Rightarrow> _\<close> x)
    1.18    (Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> k)
    1.19  
    1.20  fun cterm_of_monomial m =
    1.21 @@ -333,13 +333,13 @@
    1.22      let
    1.23        val m' = FuncUtil.dest_monomial m
    1.24        val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' []
    1.25 -    in foldr1 (fn (s, t) => Thm.apply (Thm.apply \<^cterm>\<open>op * :: real \<Rightarrow> _\<close> s) t) vps
    1.26 +    in foldr1 (fn (s, t) => Thm.apply (Thm.apply \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close> s) t) vps
    1.27      end
    1.28  
    1.29  fun cterm_of_cmonomial (m,c) =
    1.30    if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
    1.31    else if c = @1 then cterm_of_monomial m
    1.32 -  else Thm.apply (Thm.apply \<^cterm>\<open>op *::real \<Rightarrow> _\<close> (cterm_of_rat c)) (cterm_of_monomial m);
    1.33 +  else Thm.apply (Thm.apply \<^cterm>\<open>( * )::real \<Rightarrow> _\<close> (cterm_of_rat c)) (cterm_of_monomial m);
    1.34  
    1.35  fun cterm_of_poly p =
    1.36    if FuncUtil.Monomialfunc.is_empty p then \<^cterm>\<open>0::real\<close>
    1.37 @@ -347,7 +347,7 @@
    1.38      let
    1.39        val cms = map cterm_of_cmonomial
    1.40          (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
    1.41 -    in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply \<^cterm>\<open>op + :: real \<Rightarrow> _\<close> t1) t2) cms
    1.42 +    in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close> t1) t2) cms
    1.43      end;
    1.44  
    1.45  (* A general real arithmetic prover *)
    1.46 @@ -370,8 +370,8 @@
    1.47      fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
    1.48      fun oprconv cv ct =
    1.49        let val g = Thm.dest_fun2 ct
    1.50 -      in if g aconvc \<^cterm>\<open>(op \<le>) :: real \<Rightarrow> _\<close>
    1.51 -            orelse g aconvc \<^cterm>\<open>(op <) :: real \<Rightarrow> _\<close>
    1.52 +      in if g aconvc \<^cterm>\<open>((\<le>)) :: real \<Rightarrow> _\<close>
    1.53 +            orelse g aconvc \<^cterm>\<open>((<)) :: real \<Rightarrow> _\<close>
    1.54           then arg_conv cv ct else arg1_conv cv ct
    1.55        end
    1.56  
    1.57 @@ -406,13 +406,13 @@
    1.58            | Axiom_le n => nth les n
    1.59            | Axiom_lt n => nth lts n
    1.60            | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
    1.61 -                          (Thm.apply (Thm.apply \<^cterm>\<open>(op =)::real \<Rightarrow> _\<close> (mk_numeric x))
    1.62 +                          (Thm.apply (Thm.apply \<^cterm>\<open>((=))::real \<Rightarrow> _\<close> (mk_numeric x))
    1.63                                 \<^cterm>\<open>0::real\<close>)))
    1.64            | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
    1.65 -                          (Thm.apply (Thm.apply \<^cterm>\<open>(op \<le>)::real \<Rightarrow> _\<close>
    1.66 +                          (Thm.apply (Thm.apply \<^cterm>\<open>((\<le>))::real \<Rightarrow> _\<close>
    1.67                                       \<^cterm>\<open>0::real\<close>) (mk_numeric x))))
    1.68            | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
    1.69 -                      (Thm.apply (Thm.apply \<^cterm>\<open>(op <)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>)
    1.70 +                      (Thm.apply (Thm.apply \<^cterm>\<open>((<))::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>)
    1.71                          (mk_numeric x))))
    1.72            | Square pt => square_rule (cterm_of_poly pt)
    1.73            | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
    1.74 @@ -428,9 +428,9 @@
    1.75  
    1.76      val concl = Thm.dest_arg o Thm.cprop_of
    1.77      fun is_binop opr ct = (Thm.dest_fun2 ct aconvc opr handle CTERM _ => false)
    1.78 -    val is_req = is_binop \<^cterm>\<open>(op =):: real \<Rightarrow> _\<close>
    1.79 -    val is_ge = is_binop \<^cterm>\<open>(op \<le>):: real \<Rightarrow> _\<close>
    1.80 -    val is_gt = is_binop \<^cterm>\<open>(op <):: real \<Rightarrow> _\<close>
    1.81 +    val is_req = is_binop \<^cterm>\<open>((=)):: real \<Rightarrow> _\<close>
    1.82 +    val is_ge = is_binop \<^cterm>\<open>((\<le>)):: real \<Rightarrow> _\<close>
    1.83 +    val is_gt = is_binop \<^cterm>\<open>((<)):: real \<Rightarrow> _\<close>
    1.84      val is_conj = is_binop \<^cterm>\<open>HOL.conj\<close>
    1.85      val is_disj = is_binop \<^cterm>\<open>HOL.disj\<close>
    1.86      fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
    1.87 @@ -476,7 +476,7 @@
    1.88      fun dest_binary b ct =
    1.89          if is_binop b ct then Thm.dest_binop ct
    1.90          else raise CTERM ("dest_binary",[b,ct])
    1.91 -    val dest_eq = dest_binary \<^cterm>\<open>(op =) :: real \<Rightarrow> _\<close>
    1.92 +    val dest_eq = dest_binary \<^cterm>\<open>((=)) :: real \<Rightarrow> _\<close>
    1.93      val neq_th = nth pth 5
    1.94      fun real_not_eq_conv ct =
    1.95        let
    1.96 @@ -486,8 +486,8 @@
    1.97          val th_x = Drule.arg_cong_rule \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close> th_p
    1.98          val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
    1.99          val th' = Drule.binop_cong_rule \<^cterm>\<open>HOL.disj\<close>
   1.100 -          (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>(op <)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_p)
   1.101 -          (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>(op <)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_n)
   1.102 +          (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>((<))::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_p)
   1.103 +          (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>((<))::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_n)
   1.104        in Thm.transitive th th'
   1.105        end
   1.106      fun equal_implies_1_rule PQ =
   1.107 @@ -683,9 +683,9 @@
   1.108          else
   1.109            let val (opr,l) = Thm.dest_comb lop
   1.110            in
   1.111 -            if opr aconvc \<^cterm>\<open>op + :: real \<Rightarrow> _\<close>
   1.112 +            if opr aconvc \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
   1.113              then linear_add (lin_of_hol l) (lin_of_hol r)
   1.114 -            else if opr aconvc \<^cterm>\<open>op * :: real \<Rightarrow> _\<close>
   1.115 +            else if opr aconvc \<^cterm>\<open>( * ) :: real \<Rightarrow> _\<close>
   1.116                      andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
   1.117              else FuncUtil.Ctermfunc.onefunc (ct, @1)
   1.118            end