more symbols;
authorwenzelm
Sat Dec 23 19:02:11 2017 +0100 (23 months ago)
changeset 6727148ef58c6cf4c
parent 67270 f18c774acde4
child 67272 c41a032d8386
more symbols;
src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/ex/SOS.thy
     1.1 --- a/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Fri Dec 22 23:38:54 2017 +0000
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML	Sat Dec 23 19:02:11 2017 +0100
     1.3 @@ -105,7 +105,7 @@
     1.4  val parse_id = Scan.one Symbol.is_letter ::: Scan.many Symbol.is_letdig >> implode
     1.5  
     1.6  fun parse_varpow ctxt = parse_id -- Scan.optional (str "^" |-- nat) 1 >>
     1.7 -  (fn (x, k) => (Thm.cterm_of ctxt (Free (x, @{typ real})), k))
     1.8 +  (fn (x, k) => (Thm.cterm_of ctxt (Free (x, \<^typ>\<open>real\<close>)), k))
     1.9  
    1.10  fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
    1.11    (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)
     2.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Dec 22 23:38:54 2017 +0000
     2.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Dec 23 19:02:11 2017 +0100
     2.3 @@ -48,8 +48,8 @@
     2.4    in s (if x2 >= b then d + 1 else d) end
     2.5  
     2.6  
     2.7 -val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
     2.8 -val debug = Attrib.setup_config_bool @{binding sos_debug} (K false);
     2.9 +val trace = Attrib.setup_config_bool \<^binding>\<open>sos_trace\<close> (K false);
    2.10 +val debug = Attrib.setup_config_bool \<^binding>\<open>sos_debug\<close> (K false);
    2.11  
    2.12  fun trace_message ctxt msg =
    2.13    if Config.get ctxt trace orelse Config.get ctxt debug then tracing (msg ()) else ();
    2.14 @@ -218,14 +218,14 @@
    2.15  (* Conversion from HOL term.                                                 *)
    2.16  
    2.17  local
    2.18 -  val neg_tm = @{cterm "uminus :: real => _"}
    2.19 -  val add_tm = @{cterm "op + :: real => _"}
    2.20 -  val sub_tm = @{cterm "op - :: real => _"}
    2.21 -  val mul_tm = @{cterm "op * :: real => _"}
    2.22 -  val inv_tm = @{cterm "inverse :: real => _"}
    2.23 -  val div_tm = @{cterm "op / :: real => _"}
    2.24 -  val pow_tm = @{cterm "op ^ :: real => _"}
    2.25 -  val zero_tm = @{cterm "0:: real"}
    2.26 +  val neg_tm = \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close>
    2.27 +  val add_tm = \<^cterm>\<open>op + :: real \<Rightarrow> _\<close>
    2.28 +  val sub_tm = \<^cterm>\<open>op - :: real \<Rightarrow> _\<close>
    2.29 +  val mul_tm = \<^cterm>\<open>op * :: real \<Rightarrow> _\<close>
    2.30 +  val inv_tm = \<^cterm>\<open>inverse :: real \<Rightarrow> _\<close>
    2.31 +  val div_tm = \<^cterm>\<open>op / :: real \<Rightarrow> _\<close>
    2.32 +  val pow_tm = \<^cterm>\<open>op ^ :: real \<Rightarrow> _\<close>
    2.33 +  val zero_tm = \<^cterm>\<open>0:: real\<close>
    2.34    val is_numeral = can (HOLogic.dest_number o Thm.term_of)
    2.35    fun poly_of_term tm =
    2.36      if tm aconvc zero_tm then poly_0
    2.37 @@ -270,7 +270,7 @@
    2.38          end handle CTERM ("dest_comb",_) => poly_var tm)
    2.39  in
    2.40    val poly_of_term = fn tm =>
    2.41 -    if type_of (Thm.term_of tm) = @{typ real}
    2.42 +    if type_of (Thm.term_of tm) = \<^typ>\<open>real\<close>
    2.43      then poly_of_term tm
    2.44      else error "poly_of_term: term does not have real type"
    2.45  end;
    2.46 @@ -757,7 +757,7 @@
    2.47    let
    2.48      val {add = _, mul = _, neg = _, pow = _, sub = _, main = real_poly_conv} =
    2.49        Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    2.50 -        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    2.51 +        (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
    2.52          simple_cterm_ord
    2.53      fun mainf cert_choice translator (eqs, les, lts) =
    2.54        let
    2.55 @@ -861,15 +861,15 @@
    2.56        by (atomize (full)) (simp add: field_simps)})
    2.57    fun substitutable_monomial fvs tm =
    2.58      (case Thm.term_of tm of
    2.59 -      Free (_, @{typ real}) =>
    2.60 +      Free (_, \<^typ>\<open>real\<close>) =>
    2.61          if not (member (op aconvc) fvs tm) then (@1, tm)
    2.62          else raise Failure "substitutable_monomial"
    2.63 -    | @{term "op * :: real => _"} $ _ $ (Free _) =>
    2.64 +    | \<^term>\<open>op * :: real \<Rightarrow> _\<close> $ _ $ (Free _) =>
    2.65          if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso
    2.66            not (member (op aconvc) fvs (Thm.dest_arg tm))
    2.67          then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
    2.68          else raise Failure "substitutable_monomial"
    2.69 -    | @{term "op + :: real => _"}$_$_ =>
    2.70 +    | \<^term>\<open>op + :: real \<Rightarrow> _\<close>$_$_ =>
    2.71           (substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
    2.72             handle Failure _ =>
    2.73              substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
    2.74 @@ -882,7 +882,7 @@
    2.75        if v aconvc w then th
    2.76        else
    2.77          (case Thm.term_of w of
    2.78 -          @{term "op + :: real => _"} $ _ $ _ =>
    2.79 +          \<^term>\<open>op + :: real \<Rightarrow> _\<close> $ _ $ _ =>
    2.80              if Thm.dest_arg1 w aconvc v then shuffle2 th
    2.81              else isolate_variable v (shuffle1 th)
    2.82          | _ => error "isolate variable : This should not happen?")
    2.83 @@ -893,7 +893,7 @@
    2.84    let
    2.85      val {add = _, mul = real_poly_mul_conv, neg = _, pow = _, sub = _, main = real_poly_conv} =
    2.86        Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    2.87 -        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    2.88 +        (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
    2.89          simple_cterm_ord
    2.90  
    2.91      fun make_substitution th =
    2.92 @@ -901,14 +901,14 @@
    2.93          val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th))
    2.94          val th1 =
    2.95            Drule.arg_cong_rule
    2.96 -            (Thm.apply @{cterm "op * :: real => _"} (RealArith.cterm_of_rat (Rat.inv c)))
    2.97 +            (Thm.apply \<^cterm>\<open>op * :: real \<Rightarrow> _\<close> (RealArith.cterm_of_rat (Rat.inv c)))
    2.98              (mk_meta_eq th)
    2.99          val th2 = fconv_rule (binop_conv (real_poly_mul_conv ctxt)) th1
   2.100        in fconv_rule (arg_conv (real_poly_conv ctxt)) (isolate_variable v th2) end
   2.101  
   2.102      fun oprconv cv ct =
   2.103        let val g = Thm.dest_fun2 ct in
   2.104 -        if g aconvc @{cterm "op <= :: real => _"} orelse g aconvc @{cterm "op < :: real => _"}
   2.105 +        if g aconvc \<^cterm>\<open>op \<le> :: real \<Rightarrow> _\<close> orelse g aconvc \<^cterm>\<open>op < :: real \<Rightarrow> _\<close>
   2.106          then arg_conv cv ct else arg1_conv cv ct
   2.107        end
   2.108      fun mainf cert_choice translator =
   2.109 @@ -921,7 +921,7 @@
   2.110              in
   2.111                substfirst
   2.112                  (filter_out
   2.113 -                  (fn t => (Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of) t aconvc @{cterm "0::real"})
   2.114 +                  (fn t => (Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of) t aconvc \<^cterm>\<open>0::real\<close>)
   2.115                    (map modify eqs),
   2.116                    map modify les,
   2.117                    map modify lts)
   2.118 @@ -938,21 +938,21 @@
   2.119  end;
   2.120  
   2.121  val known_sos_constants =
   2.122 -  [@{term "op ==>"}, @{term "Trueprop"},
   2.123 -   @{term HOL.False}, @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
   2.124 -   @{term "Not"}, @{term "op = :: bool => _"},
   2.125 -   @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
   2.126 -   @{term "op = :: real => _"}, @{term "op < :: real => _"},
   2.127 -   @{term "op <= :: real => _"},
   2.128 -   @{term "op + :: real => _"}, @{term "op - :: real => _"},
   2.129 -   @{term "op * :: real => _"}, @{term "uminus :: real => _"},
   2.130 -   @{term "op / :: real => _"}, @{term "inverse :: real => _"},
   2.131 -   @{term "op ^ :: real => _"}, @{term "abs :: real => _"},
   2.132 -   @{term "min :: real => _"}, @{term "max :: real => _"},
   2.133 -   @{term "0::real"}, @{term "1::real"},
   2.134 -   @{term "numeral :: num => nat"},
   2.135 -   @{term "numeral :: num => real"},
   2.136 -   @{term "Num.Bit0"}, @{term "Num.Bit1"}, @{term "Num.One"}];
   2.137 +  [\<^term>\<open>op \<Longrightarrow>\<close>, \<^term>\<open>Trueprop\<close>,
   2.138 +   \<^term>\<open>HOL.False\<close>, \<^term>\<open>HOL.implies\<close>, \<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>,
   2.139 +   \<^term>\<open>Not\<close>, \<^term>\<open>op = :: bool \<Rightarrow> _\<close>,
   2.140 +   \<^term>\<open>All :: (real \<Rightarrow> _) \<Rightarrow> _\<close>, \<^term>\<open>Ex :: (real \<Rightarrow> _) \<Rightarrow> _\<close>,
   2.141 +   \<^term>\<open>op = :: real \<Rightarrow> _\<close>, \<^term>\<open>op < :: real \<Rightarrow> _\<close>,
   2.142 +   \<^term>\<open>op \<le> :: real \<Rightarrow> _\<close>,
   2.143 +   \<^term>\<open>op + :: real \<Rightarrow> _\<close>, \<^term>\<open>op - :: real \<Rightarrow> _\<close>,
   2.144 +   \<^term>\<open>op * :: real \<Rightarrow> _\<close>, \<^term>\<open>uminus :: real \<Rightarrow> _\<close>,
   2.145 +   \<^term>\<open>op / :: real \<Rightarrow> _\<close>, \<^term>\<open>inverse :: real \<Rightarrow> _\<close>,
   2.146 +   \<^term>\<open>op ^ :: real \<Rightarrow> _\<close>, \<^term>\<open>abs :: real \<Rightarrow> _\<close>,
   2.147 +   \<^term>\<open>min :: real \<Rightarrow> _\<close>, \<^term>\<open>max :: real \<Rightarrow> _\<close>,
   2.148 +   \<^term>\<open>0::real\<close>, \<^term>\<open>1::real\<close>,
   2.149 +   \<^term>\<open>numeral :: num \<Rightarrow> nat\<close>,
   2.150 +   \<^term>\<open>numeral :: num \<Rightarrow> real\<close>,
   2.151 +   \<^term>\<open>Num.Bit0\<close>, \<^term>\<open>Num.Bit1\<close>, \<^term>\<open>Num.One\<close>];
   2.152  
   2.153  fun check_sos kcts ct =
   2.154    let
   2.155 @@ -963,12 +963,12 @@
   2.156        else ()
   2.157      val fs = Term.add_frees t []
   2.158      val _ =
   2.159 -      if exists (fn ((_,T)) => not (T = @{typ "real"})) fs
   2.160 +      if exists (fn ((_,T)) => not (T = \<^typ>\<open>real\<close>)) fs
   2.161        then error "SOS: not sos. Variables with type not real"
   2.162        else ()
   2.163      val vs = Term.add_vars t []
   2.164      val _ =
   2.165 -      if exists (fn ((_,T)) => not (T = @{typ "real"})) vs
   2.166 +      if exists (fn ((_,T)) => not (T = \<^typ>\<open>real\<close>)) vs
   2.167        then error "SOS: not sos. Variables with type not real"
   2.168        else ()
   2.169      val ukcs = subtract (fn (t,p) => Const p aconv t) kcts (Term.add_consts t [])
   2.170 @@ -996,13 +996,13 @@
   2.171  in
   2.172    fun get_denom b ct =
   2.173      (case Thm.term_of ct of
   2.174 -      @{term "op / :: real => _"} $ _ $ _ =>
   2.175 +      \<^term>\<open>op / :: real \<Rightarrow> _\<close> $ _ $ _ =>
   2.176          if is_numeral (Thm.dest_arg ct)
   2.177          then get_denom b (Thm.dest_arg1 ct)
   2.178          else default_SOME (get_denom b) (get_denom b (Thm.dest_arg ct)) (Thm.dest_arg ct, b)
   2.179 -    | @{term "op < :: real => _"} $ _ $ _ =>
   2.180 +    | \<^term>\<open>op < :: real \<Rightarrow> _\<close> $ _ $ _ =>
   2.181          lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
   2.182 -    | @{term "op <= :: real => _"} $ _ $ _ =>
   2.183 +    | \<^term>\<open>op \<le> :: real \<Rightarrow> _\<close> $ _ $ _ =>
   2.184          lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
   2.185      | _ $ _ => lift_SOME (get_denom b) (get_denom b (Thm.dest_fun ct)) (Thm.dest_arg ct)
   2.186      | _ => NONE)
     3.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri Dec 22 23:38:54 2017 +0000
     3.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sat Dec 23 19:02:11 2017 +0100
     3.3 @@ -370,7 +370,7 @@
     3.4      fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
     3.5      fun oprconv cv ct =
     3.6        let val g = Thm.dest_fun2 ct
     3.7 -      in if g aconvc \<^cterm>\<open>(op <=) :: real \<Rightarrow> _\<close>
     3.8 +      in if g aconvc \<^cterm>\<open>(op \<le>) :: real \<Rightarrow> _\<close>
     3.9              orelse g aconvc \<^cterm>\<open>(op <) :: real \<Rightarrow> _\<close>
    3.10           then arg_conv cv ct else arg1_conv cv ct
    3.11        end
    3.12 @@ -409,7 +409,7 @@
    3.13                            (Thm.apply (Thm.apply \<^cterm>\<open>(op =)::real \<Rightarrow> _\<close> (mk_numeric x))
    3.14                                 \<^cterm>\<open>0::real\<close>)))
    3.15            | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
    3.16 -                          (Thm.apply (Thm.apply \<^cterm>\<open>(op <=)::real \<Rightarrow> _\<close>
    3.17 +                          (Thm.apply (Thm.apply \<^cterm>\<open>(op \<le>)::real \<Rightarrow> _\<close>
    3.18                                       \<^cterm>\<open>0::real\<close>) (mk_numeric x))))
    3.19            | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
    3.20                        (Thm.apply (Thm.apply \<^cterm>\<open>(op <)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>)
    3.21 @@ -429,7 +429,7 @@
    3.22      val concl = Thm.dest_arg o Thm.cprop_of
    3.23      fun is_binop opr ct = (Thm.dest_fun2 ct aconvc opr handle CTERM _ => false)
    3.24      val is_req = is_binop \<^cterm>\<open>(op =):: real \<Rightarrow> _\<close>
    3.25 -    val is_ge = is_binop \<^cterm>\<open>(op <=):: real \<Rightarrow> _\<close>
    3.26 +    val is_ge = is_binop \<^cterm>\<open>(op \<le>):: real \<Rightarrow> _\<close>
    3.27      val is_gt = is_binop \<^cterm>\<open>(op <):: real \<Rightarrow> _\<close>
    3.28      val is_conj = is_binop \<^cterm>\<open>HOL.conj\<close>
    3.29      val is_disj = is_binop \<^cterm>\<open>HOL.disj\<close>
     4.1 --- a/src/HOL/ex/SOS.thy	Fri Dec 22 23:38:54 2017 +0000
     4.2 +++ b/src/HOL/ex/SOS.thy	Sat Dec 23 19:02:11 2017 +0100
     4.3 @@ -9,14 +9,14 @@
     4.4  imports "HOL-Library.Sum_of_Squares"
     4.5  begin
     4.6  
     4.7 -lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0"
     4.8 +lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<Longrightarrow> a < 0"
     4.9    by sos
    4.10  
    4.11  lemma "a1 \<ge> 0 \<and> a2 \<ge> 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (a1 * b1 + a2 * b2 = 0) \<longrightarrow>
    4.12      a1 * a2 - b1 * b2 \<ge> (0::real)"
    4.13    by sos
    4.14  
    4.15 -lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<longrightarrow> a < 0"
    4.16 +lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<longrightarrow> a < 0"
    4.17    by sos
    4.18  
    4.19  lemma "(0::real) \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1 \<longrightarrow>
    4.20 @@ -120,7 +120,7 @@
    4.21  lemma "(0::real) \<le> b \<and> 0 \<le> c \<and> 0 \<le> x \<and> 0 \<le> y \<and> x\<^sup>2 = c \<and> y\<^sup>2 = a\<^sup>2 * c + b \<longrightarrow> a * c \<le> y * x"
    4.22    by sos
    4.23  
    4.24 -lemma "\<bar>x - z\<bar> \<le> e \<and> \<bar>y - z\<bar> \<le> e \<and> 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1 --> \<bar>(u * x + v * y) - z\<bar> \<le> (e::real)"
    4.25 +lemma "\<bar>x - z\<bar> \<le> e \<and> \<bar>y - z\<bar> \<le> e \<and> 0 \<le> u \<and> 0 \<le> v \<and> u + v = 1 \<longrightarrow> \<bar>(u * x + v * y) - z\<bar> \<le> (e::real)"
    4.26    by sos
    4.27  
    4.28  lemma "(x::real) - y - 2 * x^4 = 0 \<and> 0 \<le> x \<and> x \<le> 2 \<and> 0 \<le> y \<and> y \<le> 3 \<longrightarrow> y\<^sup>2 - 7 * y - 12 * x + 17 \<ge> 0"