src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
changeset 67271 48ef58c6cf4c
parent 67091 1393c2340eec
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Fri Dec 22 23:38:54 2017 +0000
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Sat Dec 23 19:02:11 2017 +0100
     1.3 @@ -48,8 +48,8 @@
     1.4    in s (if x2 >= b then d + 1 else d) end
     1.5  
     1.6  
     1.7 -val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
     1.8 -val debug = Attrib.setup_config_bool @{binding sos_debug} (K false);
     1.9 +val trace = Attrib.setup_config_bool \<^binding>\<open>sos_trace\<close> (K false);
    1.10 +val debug = Attrib.setup_config_bool \<^binding>\<open>sos_debug\<close> (K false);
    1.11  
    1.12  fun trace_message ctxt msg =
    1.13    if Config.get ctxt trace orelse Config.get ctxt debug then tracing (msg ()) else ();
    1.14 @@ -218,14 +218,14 @@
    1.15  (* Conversion from HOL term.                                                 *)
    1.16  
    1.17  local
    1.18 -  val neg_tm = @{cterm "uminus :: real => _"}
    1.19 -  val add_tm = @{cterm "op + :: real => _"}
    1.20 -  val sub_tm = @{cterm "op - :: real => _"}
    1.21 -  val mul_tm = @{cterm "op * :: real => _"}
    1.22 -  val inv_tm = @{cterm "inverse :: real => _"}
    1.23 -  val div_tm = @{cterm "op / :: real => _"}
    1.24 -  val pow_tm = @{cterm "op ^ :: real => _"}
    1.25 -  val zero_tm = @{cterm "0:: real"}
    1.26 +  val neg_tm = \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close>
    1.27 +  val add_tm = \<^cterm>\<open>op + :: real \<Rightarrow> _\<close>
    1.28 +  val sub_tm = \<^cterm>\<open>op - :: real \<Rightarrow> _\<close>
    1.29 +  val mul_tm = \<^cterm>\<open>op * :: real \<Rightarrow> _\<close>
    1.30 +  val inv_tm = \<^cterm>\<open>inverse :: real \<Rightarrow> _\<close>
    1.31 +  val div_tm = \<^cterm>\<open>op / :: real \<Rightarrow> _\<close>
    1.32 +  val pow_tm = \<^cterm>\<open>op ^ :: real \<Rightarrow> _\<close>
    1.33 +  val zero_tm = \<^cterm>\<open>0:: real\<close>
    1.34    val is_numeral = can (HOLogic.dest_number o Thm.term_of)
    1.35    fun poly_of_term tm =
    1.36      if tm aconvc zero_tm then poly_0
    1.37 @@ -270,7 +270,7 @@
    1.38          end handle CTERM ("dest_comb",_) => poly_var tm)
    1.39  in
    1.40    val poly_of_term = fn tm =>
    1.41 -    if type_of (Thm.term_of tm) = @{typ real}
    1.42 +    if type_of (Thm.term_of tm) = \<^typ>\<open>real\<close>
    1.43      then poly_of_term tm
    1.44      else error "poly_of_term: term does not have real type"
    1.45  end;
    1.46 @@ -757,7 +757,7 @@
    1.47    let
    1.48      val {add = _, mul = _, neg = _, pow = _, sub = _, main = real_poly_conv} =
    1.49        Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    1.50 -        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    1.51 +        (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
    1.52          simple_cterm_ord
    1.53      fun mainf cert_choice translator (eqs, les, lts) =
    1.54        let
    1.55 @@ -861,15 +861,15 @@
    1.56        by (atomize (full)) (simp add: field_simps)})
    1.57    fun substitutable_monomial fvs tm =
    1.58      (case Thm.term_of tm of
    1.59 -      Free (_, @{typ real}) =>
    1.60 +      Free (_, \<^typ>\<open>real\<close>) =>
    1.61          if not (member (op aconvc) fvs tm) then (@1, tm)
    1.62          else raise Failure "substitutable_monomial"
    1.63 -    | @{term "op * :: real => _"} $ _ $ (Free _) =>
    1.64 +    | \<^term>\<open>op * :: real \<Rightarrow> _\<close> $ _ $ (Free _) =>
    1.65          if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso
    1.66            not (member (op aconvc) fvs (Thm.dest_arg tm))
    1.67          then (RealArith.dest_ratconst (Thm.dest_arg1 tm), Thm.dest_arg tm)
    1.68          else raise Failure "substitutable_monomial"
    1.69 -    | @{term "op + :: real => _"}$_$_ =>
    1.70 +    | \<^term>\<open>op + :: real \<Rightarrow> _\<close>$_$_ =>
    1.71           (substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
    1.72             handle Failure _ =>
    1.73              substitutable_monomial (Drule.cterm_add_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
    1.74 @@ -882,7 +882,7 @@
    1.75        if v aconvc w then th
    1.76        else
    1.77          (case Thm.term_of w of
    1.78 -          @{term "op + :: real => _"} $ _ $ _ =>
    1.79 +          \<^term>\<open>op + :: real \<Rightarrow> _\<close> $ _ $ _ =>
    1.80              if Thm.dest_arg1 w aconvc v then shuffle2 th
    1.81              else isolate_variable v (shuffle1 th)
    1.82          | _ => error "isolate variable : This should not happen?")
    1.83 @@ -893,7 +893,7 @@
    1.84    let
    1.85      val {add = _, mul = real_poly_mul_conv, neg = _, pow = _, sub = _, main = real_poly_conv} =
    1.86        Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    1.87 -        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
    1.88 +        (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
    1.89          simple_cterm_ord
    1.90  
    1.91      fun make_substitution th =
    1.92 @@ -901,14 +901,14 @@
    1.93          val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th))
    1.94          val th1 =
    1.95            Drule.arg_cong_rule
    1.96 -            (Thm.apply @{cterm "op * :: real => _"} (RealArith.cterm_of_rat (Rat.inv c)))
    1.97 +            (Thm.apply \<^cterm>\<open>op * :: real \<Rightarrow> _\<close> (RealArith.cterm_of_rat (Rat.inv c)))
    1.98              (mk_meta_eq th)
    1.99          val th2 = fconv_rule (binop_conv (real_poly_mul_conv ctxt)) th1
   1.100        in fconv_rule (arg_conv (real_poly_conv ctxt)) (isolate_variable v th2) end
   1.101  
   1.102      fun oprconv cv ct =
   1.103        let val g = Thm.dest_fun2 ct in
   1.104 -        if g aconvc @{cterm "op <= :: real => _"} orelse g aconvc @{cterm "op < :: real => _"}
   1.105 +        if g aconvc \<^cterm>\<open>op \<le> :: real \<Rightarrow> _\<close> orelse g aconvc \<^cterm>\<open>op < :: real \<Rightarrow> _\<close>
   1.106          then arg_conv cv ct else arg1_conv cv ct
   1.107        end
   1.108      fun mainf cert_choice translator =
   1.109 @@ -921,7 +921,7 @@
   1.110              in
   1.111                substfirst
   1.112                  (filter_out
   1.113 -                  (fn t => (Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of) t aconvc @{cterm "0::real"})
   1.114 +                  (fn t => (Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of) t aconvc \<^cterm>\<open>0::real\<close>)
   1.115                    (map modify eqs),
   1.116                    map modify les,
   1.117                    map modify lts)
   1.118 @@ -938,21 +938,21 @@
   1.119  end;
   1.120  
   1.121  val known_sos_constants =
   1.122 -  [@{term "op ==>"}, @{term "Trueprop"},
   1.123 -   @{term HOL.False}, @{term HOL.implies}, @{term HOL.conj}, @{term HOL.disj},
   1.124 -   @{term "Not"}, @{term "op = :: bool => _"},
   1.125 -   @{term "All :: (real => _) => _"}, @{term "Ex :: (real => _) => _"},
   1.126 -   @{term "op = :: real => _"}, @{term "op < :: real => _"},
   1.127 -   @{term "op <= :: real => _"},
   1.128 -   @{term "op + :: real => _"}, @{term "op - :: real => _"},
   1.129 -   @{term "op * :: real => _"}, @{term "uminus :: real => _"},
   1.130 -   @{term "op / :: real => _"}, @{term "inverse :: real => _"},
   1.131 -   @{term "op ^ :: real => _"}, @{term "abs :: real => _"},
   1.132 -   @{term "min :: real => _"}, @{term "max :: real => _"},
   1.133 -   @{term "0::real"}, @{term "1::real"},
   1.134 -   @{term "numeral :: num => nat"},
   1.135 -   @{term "numeral :: num => real"},
   1.136 -   @{term "Num.Bit0"}, @{term "Num.Bit1"}, @{term "Num.One"}];
   1.137 +  [\<^term>\<open>op \<Longrightarrow>\<close>, \<^term>\<open>Trueprop\<close>,
   1.138 +   \<^term>\<open>HOL.False\<close>, \<^term>\<open>HOL.implies\<close>, \<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>,
   1.139 +   \<^term>\<open>Not\<close>, \<^term>\<open>op = :: bool \<Rightarrow> _\<close>,
   1.140 +   \<^term>\<open>All :: (real \<Rightarrow> _) \<Rightarrow> _\<close>, \<^term>\<open>Ex :: (real \<Rightarrow> _) \<Rightarrow> _\<close>,
   1.141 +   \<^term>\<open>op = :: real \<Rightarrow> _\<close>, \<^term>\<open>op < :: real \<Rightarrow> _\<close>,
   1.142 +   \<^term>\<open>op \<le> :: real \<Rightarrow> _\<close>,
   1.143 +   \<^term>\<open>op + :: real \<Rightarrow> _\<close>, \<^term>\<open>op - :: real \<Rightarrow> _\<close>,
   1.144 +   \<^term>\<open>op * :: real \<Rightarrow> _\<close>, \<^term>\<open>uminus :: real \<Rightarrow> _\<close>,
   1.145 +   \<^term>\<open>op / :: real \<Rightarrow> _\<close>, \<^term>\<open>inverse :: real \<Rightarrow> _\<close>,
   1.146 +   \<^term>\<open>op ^ :: real \<Rightarrow> _\<close>, \<^term>\<open>abs :: real \<Rightarrow> _\<close>,
   1.147 +   \<^term>\<open>min :: real \<Rightarrow> _\<close>, \<^term>\<open>max :: real \<Rightarrow> _\<close>,
   1.148 +   \<^term>\<open>0::real\<close>, \<^term>\<open>1::real\<close>,
   1.149 +   \<^term>\<open>numeral :: num \<Rightarrow> nat\<close>,
   1.150 +   \<^term>\<open>numeral :: num \<Rightarrow> real\<close>,
   1.151 +   \<^term>\<open>Num.Bit0\<close>, \<^term>\<open>Num.Bit1\<close>, \<^term>\<open>Num.One\<close>];
   1.152  
   1.153  fun check_sos kcts ct =
   1.154    let
   1.155 @@ -963,12 +963,12 @@
   1.156        else ()
   1.157      val fs = Term.add_frees t []
   1.158      val _ =
   1.159 -      if exists (fn ((_,T)) => not (T = @{typ "real"})) fs
   1.160 +      if exists (fn ((_,T)) => not (T = \<^typ>\<open>real\<close>)) fs
   1.161        then error "SOS: not sos. Variables with type not real"
   1.162        else ()
   1.163      val vs = Term.add_vars t []
   1.164      val _ =
   1.165 -      if exists (fn ((_,T)) => not (T = @{typ "real"})) vs
   1.166 +      if exists (fn ((_,T)) => not (T = \<^typ>\<open>real\<close>)) vs
   1.167        then error "SOS: not sos. Variables with type not real"
   1.168        else ()
   1.169      val ukcs = subtract (fn (t,p) => Const p aconv t) kcts (Term.add_consts t [])
   1.170 @@ -996,13 +996,13 @@
   1.171  in
   1.172    fun get_denom b ct =
   1.173      (case Thm.term_of ct of
   1.174 -      @{term "op / :: real => _"} $ _ $ _ =>
   1.175 +      \<^term>\<open>op / :: real \<Rightarrow> _\<close> $ _ $ _ =>
   1.176          if is_numeral (Thm.dest_arg ct)
   1.177          then get_denom b (Thm.dest_arg1 ct)
   1.178          else default_SOME (get_denom b) (get_denom b (Thm.dest_arg ct)) (Thm.dest_arg ct, b)
   1.179 -    | @{term "op < :: real => _"} $ _ $ _ =>
   1.180 +    | \<^term>\<open>op < :: real \<Rightarrow> _\<close> $ _ $ _ =>
   1.181          lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
   1.182 -    | @{term "op <= :: real => _"} $ _ $ _ =>
   1.183 +    | \<^term>\<open>op \<le> :: real \<Rightarrow> _\<close> $ _ $ _ =>
   1.184          lift_SOME (get_denom true) (get_denom true (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
   1.185      | _ $ _ => lift_SOME (get_denom b) (get_denom b (Thm.dest_fun ct)) (Thm.dest_arg ct)
   1.186      | _ => NONE)