src/HOL/Library/positivstellensatz.ML
changeset 67267 c5994f1fa0fa
parent 67232 a00f5a71e672
child 67271 48ef58c6cf4c
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Fri Dec 22 21:23:06 2017 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Fri Dec 22 22:39:31 2017 +0100
     1.3 @@ -184,23 +184,23 @@
     1.4  
     1.5  val pth_final = @{lemma "(\<not>p \<Longrightarrow> False) \<Longrightarrow> p" by blast}
     1.6  val pth_add =
     1.7 -  @{lemma "(x = (0::real) ==> y = 0 ==> x + y = 0 )" and "( x = 0 ==> y >= 0 ==> x + y >= 0)" and
     1.8 -    "(x = 0 ==> y > 0 ==> x + y > 0)" and "(x >= 0 ==> y = 0 ==> x + y >= 0)" and
     1.9 -    "(x >= 0 ==> y >= 0 ==> x + y >= 0)" and "(x >= 0 ==> y > 0 ==> x + y > 0)" and
    1.10 -    "(x > 0 ==> y = 0 ==> x + y > 0)" and "(x > 0 ==> y >= 0 ==> x + y > 0)" and
    1.11 -    "(x > 0 ==> y > 0 ==> x + y > 0)" by simp_all};
    1.12 +  @{lemma "(x = (0::real) \<Longrightarrow> y = 0 \<Longrightarrow> x + y = 0 )" and "( x = 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x + y \<ge> 0)" and
    1.13 +    "(x = 0 \<Longrightarrow> y > 0 \<Longrightarrow> x + y > 0)" and "(x \<ge> 0 \<Longrightarrow> y = 0 \<Longrightarrow> x + y \<ge> 0)" and
    1.14 +    "(x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x + y \<ge> 0)" and "(x \<ge> 0 \<Longrightarrow> y > 0 \<Longrightarrow> x + y > 0)" and
    1.15 +    "(x > 0 \<Longrightarrow> y = 0 \<Longrightarrow> x + y > 0)" and "(x > 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x + y > 0)" and
    1.16 +    "(x > 0 \<Longrightarrow> y > 0 \<Longrightarrow> x + y > 0)" by simp_all};
    1.17  
    1.18  val pth_mul =
    1.19 -  @{lemma "(x = (0::real) ==> y = 0 ==> x * y = 0)" and "(x = 0 ==> y >= 0 ==> x * y = 0)" and
    1.20 -    "(x = 0 ==> y > 0 ==> x * y = 0)" and "(x >= 0 ==> y = 0 ==> x * y = 0)" and
    1.21 -    "(x >= 0 ==> y >= 0 ==> x * y >= 0)" and "(x >= 0 ==> y > 0 ==> x * y >= 0)" and
    1.22 -    "(x > 0 ==>  y = 0 ==> x * y = 0)" and "(x > 0 ==> y >= 0 ==> x * y >= 0)" and
    1.23 -    "(x > 0 ==>  y > 0 ==> x * y > 0)"
    1.24 +  @{lemma "(x = (0::real) \<Longrightarrow> y = 0 \<Longrightarrow> x * y = 0)" and "(x = 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x * y = 0)" and
    1.25 +    "(x = 0 \<Longrightarrow> y > 0 \<Longrightarrow> x * y = 0)" and "(x \<ge> 0 \<Longrightarrow> y = 0 \<Longrightarrow> x * y = 0)" and
    1.26 +    "(x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x * y \<ge> 0)" and "(x \<ge> 0 \<Longrightarrow> y > 0 \<Longrightarrow> x * y \<ge> 0)" and
    1.27 +    "(x > 0 \<Longrightarrow>  y = 0 \<Longrightarrow> x * y = 0)" and "(x > 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x * y \<ge> 0)" and
    1.28 +    "(x > 0 \<Longrightarrow>  y > 0 \<Longrightarrow> x * y > 0)"
    1.29    by (auto intro: mult_mono[where a="0::real" and b="x" and d="y" and c="0", simplified]
    1.30      mult_strict_mono[where b="x" and d="y" and a="0" and c="0", simplified])};
    1.31  
    1.32 -val pth_emul = @{lemma "y = (0::real) ==> x * y = 0"  by simp};
    1.33 -val pth_square = @{lemma "x * x >= (0::real)"  by simp};
    1.34 +val pth_emul = @{lemma "y = (0::real) \<Longrightarrow> x * y = 0"  by simp};
    1.35 +val pth_square = @{lemma "x * x \<ge> (0::real)"  by simp};
    1.36  
    1.37  val weak_dnf_simps =
    1.38    List.take (@{thms simp_thms}, 34) @
    1.39 @@ -289,15 +289,15 @@
    1.40    let
    1.41      val (a, b) = Rat.dest x
    1.42    in
    1.43 -    if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
    1.44 -    else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
    1.45 -      (Numeral.mk_cnumber @{ctyp "real"} a))
    1.46 -      (Numeral.mk_cnumber @{ctyp "real"} b)
    1.47 +    if b = 1 then Numeral.mk_cnumber \<^ctyp>\<open>real\<close> a
    1.48 +    else Thm.apply (Thm.apply \<^cterm>\<open>op / :: real \<Rightarrow> _\<close>
    1.49 +      (Numeral.mk_cnumber \<^ctyp>\<open>real\<close> a))
    1.50 +      (Numeral.mk_cnumber \<^ctyp>\<open>real\<close> b)
    1.51    end;
    1.52  
    1.53  fun dest_ratconst t =
    1.54    case Thm.term_of t of
    1.55 -    Const(@{const_name divide}, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.56 +    Const(\<^const_name>\<open>divide\<close>, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.57    | _ => Rat.of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
    1.58  fun is_ratconst t = can dest_ratconst t
    1.59  
    1.60 @@ -324,30 +324,30 @@
    1.61  
    1.62  (* Map back polynomials to HOL.                         *)
    1.63  
    1.64 -fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply @{cterm "op ^ :: real => _"} x)
    1.65 -  (Numeral.mk_cnumber @{ctyp nat} k)
    1.66 +fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply \<^cterm>\<open>op ^ :: real \<Rightarrow> _\<close> x)
    1.67 +  (Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> k)
    1.68  
    1.69  fun cterm_of_monomial m =
    1.70 -  if FuncUtil.Ctermfunc.is_empty m then @{cterm "1::real"}
    1.71 +  if FuncUtil.Ctermfunc.is_empty m then \<^cterm>\<open>1::real\<close>
    1.72    else
    1.73      let
    1.74        val m' = FuncUtil.dest_monomial m
    1.75        val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' []
    1.76 -    in foldr1 (fn (s, t) => Thm.apply (Thm.apply @{cterm "op * :: real => _"} s) t) vps
    1.77 +    in foldr1 (fn (s, t) => Thm.apply (Thm.apply \<^cterm>\<open>op * :: real \<Rightarrow> _\<close> s) t) vps
    1.78      end
    1.79  
    1.80  fun cterm_of_cmonomial (m,c) =
    1.81    if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
    1.82    else if c = @1 then cterm_of_monomial m
    1.83 -  else Thm.apply (Thm.apply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
    1.84 +  else Thm.apply (Thm.apply \<^cterm>\<open>op *::real \<Rightarrow> _\<close> (cterm_of_rat c)) (cterm_of_monomial m);
    1.85  
    1.86  fun cterm_of_poly p =
    1.87 -  if FuncUtil.Monomialfunc.is_empty p then @{cterm "0::real"}
    1.88 +  if FuncUtil.Monomialfunc.is_empty p then \<^cterm>\<open>0::real\<close>
    1.89    else
    1.90      let
    1.91        val cms = map cterm_of_cmonomial
    1.92          (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
    1.93 -    in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply @{cterm "op + :: real => _"} t1) t2) cms
    1.94 +    in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply \<^cterm>\<open>op + :: real \<Rightarrow> _\<close> t1) t2) cms
    1.95      end;
    1.96  
    1.97  (* A general real arithmetic prover *)
    1.98 @@ -370,8 +370,8 @@
    1.99      fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
   1.100      fun oprconv cv ct =
   1.101        let val g = Thm.dest_fun2 ct
   1.102 -      in if g aconvc @{cterm "(op <=) :: real => _"}
   1.103 -            orelse g aconvc @{cterm "(op <) :: real => _"}
   1.104 +      in if g aconvc \<^cterm>\<open>(op <=) :: real \<Rightarrow> _\<close>
   1.105 +            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  
   1.109 @@ -405,14 +405,14 @@
   1.110              Axiom_eq n => nth eqs n
   1.111            | Axiom_le n => nth les n
   1.112            | Axiom_lt n => nth lts n
   1.113 -          | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply @{cterm Trueprop}
   1.114 -                          (Thm.apply (Thm.apply @{cterm "(op =)::real => _"} (mk_numeric x))
   1.115 -                               @{cterm "0::real"})))
   1.116 -          | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply @{cterm Trueprop}
   1.117 -                          (Thm.apply (Thm.apply @{cterm "(op <=)::real => _"}
   1.118 -                                     @{cterm "0::real"}) (mk_numeric x))))
   1.119 -          | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply @{cterm Trueprop}
   1.120 -                      (Thm.apply (Thm.apply @{cterm "(op <)::real => _"} @{cterm "0::real"})
   1.121 +          | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
   1.122 +                          (Thm.apply (Thm.apply \<^cterm>\<open>(op =)::real \<Rightarrow> _\<close> (mk_numeric x))
   1.123 +                               \<^cterm>\<open>0::real\<close>)))
   1.124 +          | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
   1.125 +                          (Thm.apply (Thm.apply \<^cterm>\<open>(op <=)::real \<Rightarrow> _\<close>
   1.126 +                                     \<^cterm>\<open>0::real\<close>) (mk_numeric x))))
   1.127 +          | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
   1.128 +                      (Thm.apply (Thm.apply \<^cterm>\<open>(op <)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>)
   1.129                          (mk_numeric x))))
   1.130            | Square pt => square_rule (cterm_of_poly pt)
   1.131            | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
   1.132 @@ -428,11 +428,11 @@
   1.133  
   1.134      val concl = Thm.dest_arg o Thm.cprop_of
   1.135      fun is_binop opr ct = (Thm.dest_fun2 ct aconvc opr handle CTERM _ => false)
   1.136 -    val is_req = is_binop @{cterm "(op =):: real => _"}
   1.137 -    val is_ge = is_binop @{cterm "(op <=):: real => _"}
   1.138 -    val is_gt = is_binop @{cterm "(op <):: real => _"}
   1.139 -    val is_conj = is_binop @{cterm HOL.conj}
   1.140 -    val is_disj = is_binop @{cterm HOL.disj}
   1.141 +    val is_req = is_binop \<^cterm>\<open>(op =):: real \<Rightarrow> _\<close>
   1.142 +    val is_ge = is_binop \<^cterm>\<open>(op <=):: real \<Rightarrow> _\<close>
   1.143 +    val is_gt = is_binop \<^cterm>\<open>(op <):: real \<Rightarrow> _\<close>
   1.144 +    val is_conj = is_binop \<^cterm>\<open>HOL.conj\<close>
   1.145 +    val is_disj = is_binop \<^cterm>\<open>HOL.disj\<close>
   1.146      fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
   1.147      fun disj_cases th th1 th2 =
   1.148        let
   1.149 @@ -443,8 +443,8 @@
   1.150            else error "disj_cases : conclusions not alpha convertible"
   1.151        in Thm.implies_elim (Thm.implies_elim
   1.152            (Thm.implies_elim (Thm.instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
   1.153 -          (Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
   1.154 -        (Thm.implies_intr (Thm.apply @{cterm Trueprop} q) th2)
   1.155 +          (Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> p) th1))
   1.156 +        (Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> q) th2)
   1.157        end
   1.158      fun overall cert_choice dun ths =
   1.159        case ths of
   1.160 @@ -466,28 +466,28 @@
   1.161              let
   1.162                val (th1, cert1) =
   1.163                  overall (Left::cert_choice) dun
   1.164 -                  (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
   1.165 +                  (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.dest_arg1 ct))::oths)
   1.166                val (th2, cert2) =
   1.167                  overall (Right::cert_choice) dun
   1.168 -                  (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
   1.169 +                  (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.dest_arg ct))::oths)
   1.170              in (disj_cases th th1 th2, Branch (cert1, cert2)) end
   1.171            else overall cert_choice (th::dun) oths
   1.172          end
   1.173      fun dest_binary b ct =
   1.174          if is_binop b ct then Thm.dest_binop ct
   1.175          else raise CTERM ("dest_binary",[b,ct])
   1.176 -    val dest_eq = dest_binary @{cterm "(op =) :: real => _"}
   1.177 +    val dest_eq = dest_binary \<^cterm>\<open>(op =) :: real \<Rightarrow> _\<close>
   1.178      val neq_th = nth pth 5
   1.179      fun real_not_eq_conv ct =
   1.180        let
   1.181          val (l,r) = dest_eq (Thm.dest_arg ct)
   1.182 -        val th = Thm.instantiate ([],[((("x", 0), @{typ real}),l),((("y", 0), @{typ real}),r)]) neq_th
   1.183 +        val th = Thm.instantiate ([],[((("x", 0), \<^typ>\<open>real\<close>),l),((("y", 0), \<^typ>\<open>real\<close>),r)]) neq_th
   1.184          val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
   1.185 -        val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
   1.186 +        val th_x = Drule.arg_cong_rule \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close> th_p
   1.187          val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
   1.188 -        val th' = Drule.binop_cong_rule @{cterm HOL.disj}
   1.189 -          (Drule.arg_cong_rule (Thm.apply @{cterm "(op <)::real=>_"} @{cterm "0::real"}) th_p)
   1.190 -          (Drule.arg_cong_rule (Thm.apply @{cterm "(op <)::real=>_"} @{cterm "0::real"}) th_n)
   1.191 +        val th' = Drule.binop_cong_rule \<^cterm>\<open>HOL.disj\<close>
   1.192 +          (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>(op <)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_p)
   1.193 +          (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>(op <)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_n)
   1.194        in Thm.transitive th th'
   1.195        end
   1.196      fun equal_implies_1_rule PQ =
   1.197 @@ -500,7 +500,7 @@
   1.198        let
   1.199          fun h (acc, t) =
   1.200            case Thm.term_of t of
   1.201 -            Const(@{const_name Ex},_)$Abs(_,_,_) =>
   1.202 +            Const(\<^const_name>\<open>Ex\<close>,_)$Abs(_,_,_) =>
   1.203                h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   1.204            | _ => (acc,t)
   1.205        in fn t => h ([],t)
   1.206 @@ -514,24 +514,24 @@
   1.207      fun mk_forall x th =
   1.208        let
   1.209          val T = Thm.typ_of_cterm x
   1.210 -        val all = Thm.cterm_of ctxt (Const (@{const_name All}, (T --> @{typ bool}) --> @{typ bool}))
   1.211 +        val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
   1.212        in Drule.arg_cong_rule all (Thm.abstract_rule (name_of x) x th) end
   1.213  
   1.214      val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
   1.215  
   1.216 -    fun ext T = Thm.cterm_of ctxt (Const (@{const_name Ex}, (T --> @{typ bool}) --> @{typ bool}))
   1.217 +    fun ext T = Thm.cterm_of ctxt (Const (\<^const_name>\<open>Ex\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
   1.218      fun mk_ex v t = Thm.apply (ext (Thm.typ_of_cterm v)) (Thm.lambda v t)
   1.219  
   1.220      fun choose v th th' =
   1.221        case Thm.concl_of th of
   1.222 -        @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
   1.223 +        \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>Ex\<close>,_)$_) =>
   1.224          let
   1.225            val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
   1.226            val T = (hd o Thm.dest_ctyp o Thm.ctyp_of_cterm) p
   1.227            val th0 = fconv_rule (Thm.beta_conversion true)
   1.228              (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
   1.229            val pv = (Thm.rhs_of o Thm.beta_conversion true)
   1.230 -            (Thm.apply @{cterm Trueprop} (Thm.apply p v))
   1.231 +            (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply p v))
   1.232            val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
   1.233          in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
   1.234        | _ => raise THM ("choose",0,[th, th'])
   1.235 @@ -539,13 +539,13 @@
   1.236      fun simple_choose v th =
   1.237        choose v
   1.238          (Thm.assume
   1.239 -          ((Thm.apply @{cterm Trueprop} o mk_ex v) (Thm.dest_arg (hd (Thm.chyps_of th))))) th
   1.240 +          ((Thm.apply \<^cterm>\<open>Trueprop\<close> o mk_ex v) (Thm.dest_arg (hd (Thm.chyps_of th))))) th
   1.241  
   1.242      val strip_forall =
   1.243        let
   1.244          fun h (acc, t) =
   1.245            case Thm.term_of t of
   1.246 -            Const(@{const_name All},_)$Abs(_,_,_) =>
   1.247 +            Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,_) =>
   1.248                h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   1.249            | _ => (acc,t)
   1.250        in fn t => h ([],t)
   1.251 @@ -555,27 +555,27 @@
   1.252        let
   1.253          val nnf_norm_conv' =
   1.254            nnf_conv ctxt then_conv
   1.255 -          literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
   1.256 +          literals_conv [\<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>] []
   1.257            (Conv.cache_conv
   1.258              (first_conv [real_lt_conv, real_le_conv,
   1.259                           real_eq_conv, real_not_lt_conv,
   1.260                           real_not_le_conv, real_not_eq_conv, all_conv]))
   1.261 -        fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
   1.262 +        fun absremover ct = (literals_conv [\<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>] []
   1.263                    (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv
   1.264                    try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
   1.265 -        val nct = Thm.apply @{cterm Trueprop} (Thm.apply @{cterm "Not"} ct)
   1.266 +        val nct = Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close> ct)
   1.267          val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
   1.268          val tm0 = Thm.dest_arg (Thm.rhs_of th0)
   1.269          val (th, certificates) =
   1.270 -          if tm0 aconvc @{cterm False} then (equal_implies_1_rule th0, Trivial) else
   1.271 +          if tm0 aconvc \<^cterm>\<open>False\<close> then (equal_implies_1_rule th0, Trivial) else
   1.272            let
   1.273              val (evs,bod) = strip_exists tm0
   1.274              val (avs,ibod) = strip_forall bod
   1.275 -            val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
   1.276 +            val th1 = Drule.arg_cong_rule \<^cterm>\<open>Trueprop\<close> (fold mk_forall avs (absremover ibod))
   1.277              val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
   1.278              val th3 =
   1.279                fold simple_choose evs
   1.280 -                (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
   1.281 +                (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply \<^cterm>\<open>Trueprop\<close> bod))) th2)
   1.282            in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
   1.283            end
   1.284        in (Thm.implies_elim (Thm.instantiate' [] [SOME ct] pth_final) th, certificates)
   1.285 @@ -587,7 +587,7 @@
   1.286  local
   1.287    val linear_add = FuncUtil.Ctermfunc.combine (curry op +) (fn z => z = @0)
   1.288    fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c * x)
   1.289 -  val one_tm = @{cterm "1::real"}
   1.290 +  val one_tm = \<^cterm>\<open>1::real\<close>
   1.291    fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p @0)) orelse
   1.292       ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
   1.293         not(p(FuncUtil.Ctermfunc.apply e one_tm)))
   1.294 @@ -673,7 +673,7 @@
   1.295      end
   1.296  
   1.297    fun lin_of_hol ct =
   1.298 -    if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.empty
   1.299 +    if ct aconvc \<^cterm>\<open>0::real\<close> then FuncUtil.Ctermfunc.empty
   1.300      else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, @1)
   1.301      else if is_ratconst ct then FuncUtil.Ctermfunc.onefunc (one_tm, dest_ratconst ct)
   1.302      else
   1.303 @@ -683,9 +683,9 @@
   1.304          else
   1.305            let val (opr,l) = Thm.dest_comb lop
   1.306            in
   1.307 -            if opr aconvc @{cterm "op + :: real =>_"}
   1.308 +            if opr aconvc \<^cterm>\<open>op + :: real \<Rightarrow> _\<close>
   1.309              then linear_add (lin_of_hol l) (lin_of_hol r)
   1.310 -            else if opr aconvc @{cterm "op * :: real =>_"}
   1.311 +            else if opr aconvc \<^cterm>\<open>op * :: real \<Rightarrow> _\<close>
   1.312                      andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
   1.313              else FuncUtil.Ctermfunc.onefunc (ct, @1)
   1.314            end
   1.315 @@ -693,8 +693,8 @@
   1.316  
   1.317    fun is_alien ct =
   1.318      case Thm.term_of ct of
   1.319 -      Const(@{const_name "of_nat"}, _)$ n => not (can HOLogic.dest_number n)
   1.320 -    | Const(@{const_name "of_int"}, _)$ n => not (can HOLogic.dest_number n)
   1.321 +      Const(\<^const_name>\<open>of_nat\<close>, _)$ n => not (can HOLogic.dest_number n)
   1.322 +    | Const(\<^const_name>\<open>of_int\<close>, _)$ n => not (can HOLogic.dest_number n)
   1.323      | _ => false
   1.324  in
   1.325  fun real_linear_prover translator (eq,le,lt) =
   1.326 @@ -724,15 +724,15 @@
   1.327  
   1.328    val absmaxmin_elim_conv2 =
   1.329      let
   1.330 -      val pth_abs = Thm.instantiate' [SOME @{ctyp real}] [] abs_split'
   1.331 -      val pth_max = Thm.instantiate' [SOME @{ctyp real}] [] max_split
   1.332 -      val pth_min = Thm.instantiate' [SOME @{ctyp real}] [] min_split
   1.333 -      val abs_tm = @{cterm "abs :: real => _"}
   1.334 -      val p_v = (("P", 0), @{typ "real \<Rightarrow> bool"})
   1.335 -      val x_v = (("x", 0), @{typ real})
   1.336 -      val y_v = (("y", 0), @{typ real})
   1.337 -      val is_max = is_binop @{cterm "max :: real => _"}
   1.338 -      val is_min = is_binop @{cterm "min :: real => _"}
   1.339 +      val pth_abs = Thm.instantiate' [SOME \<^ctyp>\<open>real\<close>] [] abs_split'
   1.340 +      val pth_max = Thm.instantiate' [SOME \<^ctyp>\<open>real\<close>] [] max_split
   1.341 +      val pth_min = Thm.instantiate' [SOME \<^ctyp>\<open>real\<close>] [] min_split
   1.342 +      val abs_tm = \<^cterm>\<open>abs :: real \<Rightarrow> _\<close>
   1.343 +      val p_v = (("P", 0), \<^typ>\<open>real \<Rightarrow> bool\<close>)
   1.344 +      val x_v = (("x", 0), \<^typ>\<open>real\<close>)
   1.345 +      val y_v = (("y", 0), \<^typ>\<open>real\<close>)
   1.346 +      val is_max = is_binop \<^cterm>\<open>max :: real \<Rightarrow> _\<close>
   1.347 +      val is_min = is_binop \<^cterm>\<open>min :: real \<Rightarrow> _\<close>
   1.348        fun is_abs t = is_comb t andalso Thm.dest_fun t aconvc abs_tm
   1.349        fun eliminate_construct p c tm =
   1.350          let
   1.351 @@ -772,7 +772,7 @@
   1.352      fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
   1.353      val {add, mul, neg, pow = _, sub = _, main} =
   1.354          Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
   1.355 -        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
   1.356 +        (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
   1.357          simple_cterm_ord
   1.358    in gen_real_arith ctxt
   1.359       (cterm_of_rat,