tuned whitespace
authorhuffman
Wed Feb 22 17:34:31 2012 +0100 (2012-02-22)
changeset 46594f11f332b964f
parent 46593 c96bd702d1dd
child 46595 9517cc2883eb
tuned whitespace
src/HOL/Library/positivstellensatz.ML
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Feb 22 17:33:53 2012 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Feb 22 17:34:31 2012 +0100
     1.3 @@ -8,20 +8,20 @@
     1.4  
     1.5  (* A functor for finite mappings based on Tables *)
     1.6  
     1.7 -signature FUNC = 
     1.8 +signature FUNC =
     1.9  sig
    1.10 - include TABLE
    1.11 - val apply : 'a table -> key -> 'a
    1.12 - val applyd :'a table -> (key -> 'a) -> key -> 'a
    1.13 - val combine : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a table -> 'a table -> 'a table
    1.14 - val dom : 'a table -> key list
    1.15 - val tryapplyd : 'a table -> key -> 'a -> 'a
    1.16 - val updatep : (key * 'a -> bool) -> key * 'a -> 'a table -> 'a table
    1.17 - val choose : 'a table -> key * 'a
    1.18 - val onefunc : key * 'a -> 'a table
    1.19 +  include TABLE
    1.20 +  val apply : 'a table -> key -> 'a
    1.21 +  val applyd :'a table -> (key -> 'a) -> key -> 'a
    1.22 +  val combine : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a table -> 'a table -> 'a table
    1.23 +  val dom : 'a table -> key list
    1.24 +  val tryapplyd : 'a table -> key -> 'a -> 'a
    1.25 +  val updatep : (key * 'a -> bool) -> key * 'a -> 'a table -> 'a table
    1.26 +  val choose : 'a table -> key * 'a
    1.27 +  val onefunc : key * 'a -> 'a table
    1.28  end;
    1.29  
    1.30 -functor FuncFun(Key: KEY) : FUNC=
    1.31 +functor FuncFun(Key: KEY) : FUNC =
    1.32  struct
    1.33  
    1.34  structure Tab = Table(Key);
    1.35 @@ -29,24 +29,24 @@
    1.36  open Tab;
    1.37  
    1.38  fun dom a = sort Key.ord (Tab.keys a);
    1.39 -fun applyd f d x = case Tab.lookup f x of 
    1.40 +fun applyd f d x = case Tab.lookup f x of
    1.41     SOME y => y
    1.42   | NONE => d x;
    1.43  
    1.44  fun apply f x = applyd f (fn _ => raise Tab.UNDEF x) x;
    1.45  fun tryapplyd f a d = applyd f (K d) a;
    1.46  fun updatep p (k,v) t = if p (k, v) then t else update (k,v) t
    1.47 -fun combine f z a b = 
    1.48 - let
    1.49 -  fun h (k,v) t = case Tab.lookup t k of
    1.50 -     NONE => Tab.update (k,v) t
    1.51 -   | SOME v' => let val w = f v v'
    1.52 -     in if z w then Tab.delete k t else Tab.update (k,w) t end;
    1.53 +fun combine f z a b =
    1.54 +  let
    1.55 +    fun h (k,v) t = case Tab.lookup t k of
    1.56 +        NONE => Tab.update (k,v) t
    1.57 +      | SOME v' => let val w = f v v'
    1.58 +        in if z w then Tab.delete k t else Tab.update (k,w) t end;
    1.59    in Tab.fold h a b end;
    1.60  
    1.61 -fun choose f = case Tab.min_key f of 
    1.62 -   SOME k => (k, the (Tab.lookup f k))
    1.63 - | NONE => error "FuncFun.choose : Completely empty function"
    1.64 +fun choose f = case Tab.min_key f of
    1.65 +    SOME k => (k, the (Tab.lookup f k))
    1.66 +  | NONE => error "FuncFun.choose : Completely empty function"
    1.67  
    1.68  fun onefunc kv = update kv empty
    1.69  
    1.70 @@ -80,94 +80,96 @@
    1.71  fun dest_monomial mon = sort (cterm_ord o pairself fst) (Ctermfunc.dest mon);
    1.72  
    1.73  fun monomial_order (m1,m2) =
    1.74 - if Ctermfunc.is_empty m2 then LESS 
    1.75 - else if Ctermfunc.is_empty m1 then GREATER 
    1.76 - else
    1.77 -  let val mon1 = dest_monomial m1 
    1.78 +  if Ctermfunc.is_empty m2 then LESS
    1.79 +  else if Ctermfunc.is_empty m1 then GREATER
    1.80 +  else
    1.81 +    let
    1.82 +      val mon1 = dest_monomial m1
    1.83        val mon2 = dest_monomial m2
    1.84        val deg1 = fold (Integer.add o snd) mon1 0
    1.85 -      val deg2 = fold (Integer.add o snd) mon2 0 
    1.86 -  in if deg1 < deg2 then GREATER else if deg1 > deg2 then LESS
    1.87 -     else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
    1.88 -  end;
    1.89 +      val deg2 = fold (Integer.add o snd) mon2 0
    1.90 +    in if deg1 < deg2 then GREATER
    1.91 +       else if deg1 > deg2 then LESS
    1.92 +       else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
    1.93 +    end;
    1.94  
    1.95  end
    1.96  
    1.97  (* positivstellensatz datatype and prover generation *)
    1.98  
    1.99 -signature REAL_ARITH = 
   1.100 +signature REAL_ARITH =
   1.101  sig
   1.102 -  
   1.103 +
   1.104    datatype positivstellensatz =
   1.105 -   Axiom_eq of int
   1.106 - | Axiom_le of int
   1.107 - | Axiom_lt of int
   1.108 - | Rational_eq of Rat.rat
   1.109 - | Rational_le of Rat.rat
   1.110 - | Rational_lt of Rat.rat
   1.111 - | Square of FuncUtil.poly
   1.112 - | Eqmul of FuncUtil.poly * positivstellensatz
   1.113 - | Sum of positivstellensatz * positivstellensatz
   1.114 - | Product of positivstellensatz * positivstellensatz;
   1.115 +    Axiom_eq of int
   1.116 +  | Axiom_le of int
   1.117 +  | Axiom_lt of int
   1.118 +  | Rational_eq of Rat.rat
   1.119 +  | Rational_le of Rat.rat
   1.120 +  | Rational_lt of Rat.rat
   1.121 +  | Square of FuncUtil.poly
   1.122 +  | Eqmul of FuncUtil.poly * positivstellensatz
   1.123 +  | Sum of positivstellensatz * positivstellensatz
   1.124 +  | Product of positivstellensatz * positivstellensatz;
   1.125  
   1.126 -datatype pss_tree = Trivial | Cert of positivstellensatz | Branch of pss_tree * pss_tree
   1.127 +  datatype pss_tree = Trivial | Cert of positivstellensatz | Branch of pss_tree * pss_tree
   1.128  
   1.129 -datatype tree_choice = Left | Right
   1.130 +  datatype tree_choice = Left | Right
   1.131  
   1.132 -type prover = tree_choice list -> 
   1.133 -  (thm list * thm list * thm list -> positivstellensatz -> thm) ->
   1.134 -  thm list * thm list * thm list -> thm * pss_tree
   1.135 -type cert_conv = cterm -> thm * pss_tree
   1.136 +  type prover = tree_choice list ->
   1.137 +    (thm list * thm list * thm list -> positivstellensatz -> thm) ->
   1.138 +      thm list * thm list * thm list -> thm * pss_tree
   1.139 +  type cert_conv = cterm -> thm * pss_tree
   1.140  
   1.141 -val gen_gen_real_arith :
   1.142 -  Proof.context -> (Rat.rat -> cterm) * conv * conv * conv *
   1.143 -   conv * conv * conv * conv * conv * conv * prover -> cert_conv
   1.144 -val real_linear_prover : (thm list * thm list * thm list -> positivstellensatz -> thm) ->
   1.145 -  thm list * thm list * thm list -> thm * pss_tree
   1.146 +  val gen_gen_real_arith :
   1.147 +    Proof.context -> (Rat.rat -> cterm) * conv * conv * conv *
   1.148 +     conv * conv * conv * conv * conv * conv * prover -> cert_conv
   1.149 +  val real_linear_prover : (thm list * thm list * thm list -> positivstellensatz -> thm) ->
   1.150 +    thm list * thm list * thm list -> thm * pss_tree
   1.151  
   1.152 -val gen_real_arith : Proof.context ->
   1.153 -  (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv
   1.154 +  val gen_real_arith : Proof.context ->
   1.155 +    (Rat.rat -> cterm) * conv * conv * conv * conv * conv * conv * conv * prover -> cert_conv
   1.156  
   1.157 -val gen_prover_real_arith : Proof.context -> prover -> cert_conv
   1.158 +  val gen_prover_real_arith : Proof.context -> prover -> cert_conv
   1.159  
   1.160 -val is_ratconst : cterm -> bool
   1.161 -val dest_ratconst : cterm -> Rat.rat
   1.162 -val cterm_of_rat : Rat.rat -> cterm
   1.163 +  val is_ratconst : cterm -> bool
   1.164 +  val dest_ratconst : cterm -> Rat.rat
   1.165 +  val cterm_of_rat : Rat.rat -> cterm
   1.166  
   1.167  end
   1.168  
   1.169  structure RealArith : REAL_ARITH =
   1.170  struct
   1.171  
   1.172 - open Conv
   1.173 +open Conv
   1.174  (* ------------------------------------------------------------------------- *)
   1.175  (* Data structure for Positivstellensatz refutations.                        *)
   1.176  (* ------------------------------------------------------------------------- *)
   1.177  
   1.178  datatype positivstellensatz =
   1.179 -   Axiom_eq of int
   1.180 - | Axiom_le of int
   1.181 - | Axiom_lt of int
   1.182 - | Rational_eq of Rat.rat
   1.183 - | Rational_le of Rat.rat
   1.184 - | Rational_lt of Rat.rat
   1.185 - | Square of FuncUtil.poly
   1.186 - | Eqmul of FuncUtil.poly * positivstellensatz
   1.187 - | Sum of positivstellensatz * positivstellensatz
   1.188 - | Product of positivstellensatz * positivstellensatz;
   1.189 +    Axiom_eq of int
   1.190 +  | Axiom_le of int
   1.191 +  | Axiom_lt of int
   1.192 +  | Rational_eq of Rat.rat
   1.193 +  | Rational_le of Rat.rat
   1.194 +  | Rational_lt of Rat.rat
   1.195 +  | Square of FuncUtil.poly
   1.196 +  | Eqmul of FuncUtil.poly * positivstellensatz
   1.197 +  | Sum of positivstellensatz * positivstellensatz
   1.198 +  | Product of positivstellensatz * positivstellensatz;
   1.199           (* Theorems used in the procedure *)
   1.200  
   1.201  datatype pss_tree = Trivial | Cert of positivstellensatz | Branch of pss_tree * pss_tree
   1.202  datatype tree_choice = Left | Right
   1.203 -type prover = tree_choice list -> 
   1.204 +type prover = tree_choice list ->
   1.205    (thm list * thm list * thm list -> positivstellensatz -> thm) ->
   1.206 -  thm list * thm list * thm list -> thm * pss_tree
   1.207 +    thm list * thm list * thm list -> thm * pss_tree
   1.208  type cert_conv = cterm -> thm * pss_tree
   1.209  
   1.210  
   1.211      (* Some useful derived rules *)
   1.212 -fun deduct_antisym_rule tha thb = 
   1.213 -    Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha) 
   1.214 +fun deduct_antisym_rule tha thb =
   1.215 +    Thm.equal_intr (Thm.implies_intr (cprop_of thb) tha)
   1.216       (Thm.implies_intr (cprop_of tha) thb);
   1.217  
   1.218  fun prove_hyp tha thb =
   1.219 @@ -180,14 +182,14 @@
   1.220    by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)};
   1.221  
   1.222  val pth_final = @{lemma "(~p ==> False) ==> p" by blast}
   1.223 -val pth_add = 
   1.224 +val pth_add =
   1.225    @{lemma "(x = (0::real) ==> y = 0 ==> x + y = 0 )" and "( x = 0 ==> y >= 0 ==> x + y >= 0)" and
   1.226      "(x = 0 ==> y > 0 ==> x + y > 0)" and "(x >= 0 ==> y = 0 ==> x + y >= 0)" and
   1.227      "(x >= 0 ==> y >= 0 ==> x + y >= 0)" and "(x >= 0 ==> y > 0 ==> x + y > 0)" and
   1.228      "(x > 0 ==> y = 0 ==> x + y > 0)" and "(x > 0 ==> y >= 0 ==> x + y > 0)" and
   1.229      "(x > 0 ==> y > 0 ==> x + y > 0)" by simp_all};
   1.230  
   1.231 -val pth_mul = 
   1.232 +val pth_mul =
   1.233    @{lemma "(x = (0::real) ==> y = 0 ==> x * y = 0)" and "(x = 0 ==> y >= 0 ==> x * y = 0)" and
   1.234      "(x = 0 ==> y > 0 ==> x * y = 0)" and "(x >= 0 ==> y = 0 ==> x * y = 0)" and
   1.235      "(x >= 0 ==> y >= 0 ==> x * y >= 0)" and "(x >= 0 ==> y > 0 ==> x * y >= 0)" and
   1.236 @@ -273,41 +275,45 @@
   1.237  
   1.238  
   1.239           (* Miscellaneous *)
   1.240 -fun literals_conv bops uops cv = 
   1.241 - let fun h t =
   1.242 -  case (term_of t) of 
   1.243 -   b$_$_ => if member (op aconv) bops b then binop_conv h t else cv t
   1.244 - | u$_ => if member (op aconv) uops u then arg_conv h t else cv t
   1.245 - | _ => cv t
   1.246 - in h end;
   1.247 +fun literals_conv bops uops cv =
   1.248 +  let
   1.249 +    fun h t =
   1.250 +      case (term_of t) of
   1.251 +        b$_$_ => if member (op aconv) bops b then binop_conv h t else cv t
   1.252 +      | u$_ => if member (op aconv) uops u then arg_conv h t else cv t
   1.253 +      | _ => cv t
   1.254 +  in h end;
   1.255  
   1.256 -fun cterm_of_rat x = 
   1.257 -let val (a, b) = Rat.quotient_of_rat x
   1.258 -in 
   1.259 - if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
   1.260 -  else Thm.apply (Thm.apply @{cterm "op / :: real => _"} 
   1.261 -                   (Numeral.mk_cnumber @{ctyp "real"} a))
   1.262 -        (Numeral.mk_cnumber @{ctyp "real"} b)
   1.263 -end;
   1.264 +fun cterm_of_rat x =
   1.265 +  let
   1.266 +    val (a, b) = Rat.quotient_of_rat x
   1.267 +  in
   1.268 +    if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
   1.269 +    else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
   1.270 +      (Numeral.mk_cnumber @{ctyp "real"} a))
   1.271 +      (Numeral.mk_cnumber @{ctyp "real"} b)
   1.272 +  end;
   1.273  
   1.274 -  fun dest_ratconst t = case term_of t of
   1.275 -   Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
   1.276 - | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
   1.277 - fun is_ratconst t = can dest_ratconst t
   1.278 +fun dest_ratconst t =
   1.279 +  case term_of t of
   1.280 +    Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
   1.281 +  | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
   1.282 +fun is_ratconst t = can dest_ratconst t
   1.283  
   1.284  (*
   1.285 -fun find_term p t = if p t then t else 
   1.286 +fun find_term p t = if p t then t else
   1.287   case t of
   1.288    a$b => (find_term p a handle TERM _ => find_term p b)
   1.289   | Abs (_,_,t') => find_term p t'
   1.290   | _ => raise TERM ("find_term",[t]);
   1.291  *)
   1.292  
   1.293 -fun find_cterm p t = if p t then t else 
   1.294 - case term_of t of
   1.295 -  _$_ => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
   1.296 - | Abs (_,_,_) => find_cterm p (Thm.dest_abs NONE t |> snd)
   1.297 - | _ => raise CTERM ("find_cterm",[t]);
   1.298 +fun find_cterm p t =
   1.299 +  if p t then t else
   1.300 +  case term_of t of
   1.301 +    _$_ => (find_cterm p (Thm.dest_fun t) handle CTERM _ => find_cterm p (Thm.dest_arg t))
   1.302 +  | Abs (_,_,_) => find_cterm p (Thm.dest_abs NONE t |> snd)
   1.303 +  | _ => raise CTERM ("find_cterm",[t]);
   1.304  
   1.305      (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
   1.306  fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
   1.307 @@ -319,237 +325,247 @@
   1.308  
   1.309  (* Map back polynomials to HOL.                         *)
   1.310  
   1.311 -fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply @{cterm "op ^ :: real => _"} x) 
   1.312 +fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply @{cterm "op ^ :: real => _"} x)
   1.313    (Numeral.mk_cnumber @{ctyp nat} k)
   1.314  
   1.315 -fun cterm_of_monomial m = 
   1.316 - if FuncUtil.Ctermfunc.is_empty m then @{cterm "1::real"} 
   1.317 - else 
   1.318 -  let 
   1.319 -   val m' = FuncUtil.dest_monomial m
   1.320 -   val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' [] 
   1.321 -  in foldr1 (fn (s, t) => Thm.apply (Thm.apply @{cterm "op * :: real => _"} s) t) vps
   1.322 -  end
   1.323 +fun cterm_of_monomial m =
   1.324 +  if FuncUtil.Ctermfunc.is_empty m then @{cterm "1::real"}
   1.325 +  else
   1.326 +    let
   1.327 +      val m' = FuncUtil.dest_monomial m
   1.328 +      val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' []
   1.329 +    in foldr1 (fn (s, t) => Thm.apply (Thm.apply @{cterm "op * :: real => _"} s) t) vps
   1.330 +    end
   1.331  
   1.332 -fun cterm_of_cmonomial (m,c) = if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
   1.333 -    else if c = Rat.one then cterm_of_monomial m
   1.334 -    else Thm.apply (Thm.apply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
   1.335 +fun cterm_of_cmonomial (m,c) =
   1.336 +  if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
   1.337 +  else if c = Rat.one then cterm_of_monomial m
   1.338 +  else Thm.apply (Thm.apply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
   1.339  
   1.340 -fun cterm_of_poly p = 
   1.341 - if FuncUtil.Monomialfunc.is_empty p then @{cterm "0::real"} 
   1.342 - else
   1.343 -  let 
   1.344 -   val cms = map cterm_of_cmonomial
   1.345 -     (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
   1.346 -  in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply @{cterm "op + :: real => _"} t1) t2) cms
   1.347 -  end;
   1.348 +fun cterm_of_poly p =
   1.349 +  if FuncUtil.Monomialfunc.is_empty p then @{cterm "0::real"}
   1.350 +  else
   1.351 +    let
   1.352 +      val cms = map cterm_of_cmonomial
   1.353 +        (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
   1.354 +    in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply @{cterm "op + :: real => _"} t1) t2) cms
   1.355 +    end;
   1.356  
   1.357 -    (* A general real arithmetic prover *)
   1.358 +(* A general real arithmetic prover *)
   1.359  
   1.360  fun gen_gen_real_arith ctxt (mk_numeric,
   1.361         numeric_eq_conv,numeric_ge_conv,numeric_gt_conv,
   1.362         poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv,
   1.363 -       absconv1,absconv2,prover) = 
   1.364 -let
   1.365 - val pre_ss = HOL_basic_ss addsimps
   1.366 -  @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib all_conj_distrib if_bool_eq_disj}
   1.367 - val prenex_ss = HOL_basic_ss addsimps prenex_simps
   1.368 - val skolemize_ss = HOL_basic_ss addsimps [choice_iff]
   1.369 - val presimp_conv = Simplifier.rewrite (Simplifier.context ctxt pre_ss)
   1.370 - val prenex_conv = Simplifier.rewrite (Simplifier.context ctxt prenex_ss)
   1.371 - val skolemize_conv = Simplifier.rewrite (Simplifier.context ctxt skolemize_ss)
   1.372 - val weak_dnf_ss = HOL_basic_ss addsimps weak_dnf_simps
   1.373 - val weak_dnf_conv = Simplifier.rewrite (Simplifier.context ctxt weak_dnf_ss)
   1.374 - fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
   1.375 - fun oprconv cv ct = 
   1.376 -  let val g = Thm.dest_fun2 ct
   1.377 -  in if g aconvc @{cterm "op <= :: real => _"} 
   1.378 -       orelse g aconvc @{cterm "op < :: real => _"} 
   1.379 -     then arg_conv cv ct else arg1_conv cv ct
   1.380 -  end
   1.381 +       absconv1,absconv2,prover) =
   1.382 +  let
   1.383 +    val pre_ss = HOL_basic_ss addsimps
   1.384 +      @{thms simp_thms ex_simps all_simps not_all not_ex ex_disj_distrib all_conj_distrib if_bool_eq_disj}
   1.385 +    val prenex_ss = HOL_basic_ss addsimps prenex_simps
   1.386 +    val skolemize_ss = HOL_basic_ss addsimps [choice_iff]
   1.387 +    val presimp_conv = Simplifier.rewrite (Simplifier.context ctxt pre_ss)
   1.388 +    val prenex_conv = Simplifier.rewrite (Simplifier.context ctxt prenex_ss)
   1.389 +    val skolemize_conv = Simplifier.rewrite (Simplifier.context ctxt skolemize_ss)
   1.390 +    val weak_dnf_ss = HOL_basic_ss addsimps weak_dnf_simps
   1.391 +    val weak_dnf_conv = Simplifier.rewrite (Simplifier.context ctxt weak_dnf_ss)
   1.392 +    fun eqT_elim th = Thm.equal_elim (Thm.symmetric th) @{thm TrueI}
   1.393 +    fun oprconv cv ct =
   1.394 +      let val g = Thm.dest_fun2 ct
   1.395 +      in if g aconvc @{cterm "op <= :: real => _"}
   1.396 +            orelse g aconvc @{cterm "op < :: real => _"}
   1.397 +         then arg_conv cv ct else arg1_conv cv ct
   1.398 +      end
   1.399  
   1.400 - fun real_ineq_conv th ct =
   1.401 -  let
   1.402 -   val th' = (Thm.instantiate (Thm.match (Thm.lhs_of th, ct)) th 
   1.403 -      handle Pattern.MATCH => raise CTERM ("real_ineq_conv", [ct]))
   1.404 -  in Thm.transitive th' (oprconv poly_conv (Thm.rhs_of th'))
   1.405 -  end 
   1.406 -  val [real_lt_conv, real_le_conv, real_eq_conv,
   1.407 -       real_not_lt_conv, real_not_le_conv, _] =
   1.408 -       map real_ineq_conv pth
   1.409 -  fun match_mp_rule ths ths' = 
   1.410 -   let
   1.411 -     fun f ths ths' = case ths of [] => raise THM("match_mp_rule",0,ths)
   1.412 -      | th::ths => (ths' MRS th handle THM _ => f ths ths')
   1.413 -   in f ths ths' end
   1.414 -  fun mul_rule th th' = fconv_rule (arg_conv (oprconv poly_mul_conv))
   1.415 +    fun real_ineq_conv th ct =
   1.416 +      let
   1.417 +        val th' = (Thm.instantiate (Thm.match (Thm.lhs_of th, ct)) th
   1.418 +          handle Pattern.MATCH => raise CTERM ("real_ineq_conv", [ct]))
   1.419 +      in Thm.transitive th' (oprconv poly_conv (Thm.rhs_of th'))
   1.420 +      end
   1.421 +    val [real_lt_conv, real_le_conv, real_eq_conv,
   1.422 +         real_not_lt_conv, real_not_le_conv, _] =
   1.423 +         map real_ineq_conv pth
   1.424 +    fun match_mp_rule ths ths' =
   1.425 +      let
   1.426 +        fun f ths ths' = case ths of [] => raise THM("match_mp_rule",0,ths)
   1.427 +          | th::ths => (ths' MRS th handle THM _ => f ths ths')
   1.428 +      in f ths ths' end
   1.429 +    fun mul_rule th th' = fconv_rule (arg_conv (oprconv poly_mul_conv))
   1.430           (match_mp_rule pth_mul [th, th'])
   1.431 -  fun add_rule th th' = fconv_rule (arg_conv (oprconv poly_add_conv))
   1.432 +    fun add_rule th th' = fconv_rule (arg_conv (oprconv poly_add_conv))
   1.433           (match_mp_rule pth_add [th, th'])
   1.434 -  fun emul_rule ct th = fconv_rule (arg_conv (oprconv poly_mul_conv)) 
   1.435 -       (instantiate' [] [SOME ct] (th RS pth_emul)) 
   1.436 -  fun square_rule t = fconv_rule (arg_conv (oprconv poly_conv))
   1.437 +    fun emul_rule ct th = fconv_rule (arg_conv (oprconv poly_mul_conv))
   1.438 +       (instantiate' [] [SOME ct] (th RS pth_emul))
   1.439 +    fun square_rule t = fconv_rule (arg_conv (oprconv poly_conv))
   1.440         (instantiate' [] [SOME t] pth_square)
   1.441  
   1.442 -  fun hol_of_positivstellensatz(eqs,les,lts) proof =
   1.443 -   let 
   1.444 -    fun translate prf = case prf of
   1.445 -        Axiom_eq n => nth eqs n
   1.446 -      | Axiom_le n => nth les n
   1.447 -      | Axiom_lt n => nth lts n
   1.448 -      | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply @{cterm Trueprop} 
   1.449 -                          (Thm.apply (Thm.apply @{cterm "op =::real => _"} (mk_numeric x)) 
   1.450 +    fun hol_of_positivstellensatz(eqs,les,lts) proof =
   1.451 +      let
   1.452 +        fun translate prf =
   1.453 +          case prf of
   1.454 +            Axiom_eq n => nth eqs n
   1.455 +          | Axiom_le n => nth les n
   1.456 +          | Axiom_lt n => nth lts n
   1.457 +          | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply @{cterm Trueprop}
   1.458 +                          (Thm.apply (Thm.apply @{cterm "op =::real => _"} (mk_numeric x))
   1.459                                 @{cterm "0::real"})))
   1.460 -      | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply @{cterm Trueprop} 
   1.461 -                          (Thm.apply (Thm.apply @{cterm "op <=::real => _"} 
   1.462 +          | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply @{cterm Trueprop}
   1.463 +                          (Thm.apply (Thm.apply @{cterm "op <=::real => _"}
   1.464                                       @{cterm "0::real"}) (mk_numeric x))))
   1.465 -      | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply @{cterm Trueprop} 
   1.466 +          | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply @{cterm Trueprop}
   1.467                        (Thm.apply (Thm.apply @{cterm "op <::real => _"} @{cterm "0::real"})
   1.468                          (mk_numeric x))))
   1.469 -      | Square pt => square_rule (cterm_of_poly pt)
   1.470 -      | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
   1.471 -      | Sum(p1,p2) => add_rule (translate p1) (translate p2)
   1.472 -      | Product(p1,p2) => mul_rule (translate p1) (translate p2)
   1.473 -   in fconv_rule (first_conv [numeric_ge_conv, numeric_gt_conv, numeric_eq_conv, all_conv]) 
   1.474 +          | Square pt => square_rule (cterm_of_poly pt)
   1.475 +          | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
   1.476 +          | Sum(p1,p2) => add_rule (translate p1) (translate p2)
   1.477 +          | Product(p1,p2) => mul_rule (translate p1) (translate p2)
   1.478 +      in fconv_rule (first_conv [numeric_ge_conv, numeric_gt_conv, numeric_eq_conv, all_conv])
   1.479            (translate proof)
   1.480 -   end
   1.481 -  
   1.482 -  val init_conv = presimp_conv then_conv
   1.483 -      nnf_conv then_conv skolemize_conv then_conv prenex_conv then_conv
   1.484 -      weak_dnf_conv
   1.485 +      end
   1.486 +
   1.487 +    val init_conv = presimp_conv then_conv
   1.488 +        nnf_conv then_conv skolemize_conv then_conv prenex_conv then_conv
   1.489 +        weak_dnf_conv
   1.490  
   1.491 -  val concl = Thm.dest_arg o cprop_of
   1.492 -  fun is_binop opr ct = (Thm.dest_fun2 ct aconvc opr handle CTERM _ => false)
   1.493 -  val is_req = is_binop @{cterm "op =:: real => _"}
   1.494 -  val is_ge = is_binop @{cterm "op <=:: real => _"}
   1.495 -  val is_gt = is_binop @{cterm "op <:: real => _"}
   1.496 -  val is_conj = is_binop @{cterm HOL.conj}
   1.497 -  val is_disj = is_binop @{cterm HOL.disj}
   1.498 -  fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
   1.499 -  fun disj_cases th th1 th2 = 
   1.500 -   let val (p,q) = Thm.dest_binop (concl th)
   1.501 -       val c = concl th1
   1.502 -       val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
   1.503 -   in Thm.implies_elim (Thm.implies_elim
   1.504 +    val concl = Thm.dest_arg o cprop_of
   1.505 +    fun is_binop opr ct = (Thm.dest_fun2 ct aconvc opr handle CTERM _ => false)
   1.506 +    val is_req = is_binop @{cterm "op =:: real => _"}
   1.507 +    val is_ge = is_binop @{cterm "op <=:: real => _"}
   1.508 +    val is_gt = is_binop @{cterm "op <:: real => _"}
   1.509 +    val is_conj = is_binop @{cterm HOL.conj}
   1.510 +    val is_disj = is_binop @{cterm HOL.disj}
   1.511 +    fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
   1.512 +    fun disj_cases th th1 th2 =
   1.513 +      let
   1.514 +        val (p,q) = Thm.dest_binop (concl th)
   1.515 +        val c = concl th1
   1.516 +        val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
   1.517 +      in Thm.implies_elim (Thm.implies_elim
   1.518            (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
   1.519            (Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
   1.520          (Thm.implies_intr (Thm.apply @{cterm Trueprop} q) th2)
   1.521 -   end
   1.522 - fun overall cert_choice dun ths = case ths of
   1.523 -  [] =>
   1.524 -   let 
   1.525 -    val (eq,ne) = List.partition (is_req o concl) dun
   1.526 -     val (le,nl) = List.partition (is_ge o concl) ne
   1.527 -     val lt = filter (is_gt o concl) nl 
   1.528 -    in prover (rev cert_choice) hol_of_positivstellensatz (eq,le,lt) end
   1.529 - | th::oths =>
   1.530 -   let 
   1.531 -    val ct = concl th 
   1.532 -   in 
   1.533 -    if is_conj ct  then
   1.534 -     let 
   1.535 -      val (th1,th2) = conj_pair th in
   1.536 -      overall cert_choice dun (th1::th2::oths) end
   1.537 -    else if is_disj ct then
   1.538 -      let 
   1.539 -       val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
   1.540 -       val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
   1.541 -      in (disj_cases th th1 th2, Branch (cert1, cert2)) end
   1.542 -   else overall cert_choice (th::dun) oths
   1.543 -  end
   1.544 -  fun dest_binary b ct = if is_binop b ct then Thm.dest_binop ct 
   1.545 -                         else raise CTERM ("dest_binary",[b,ct])
   1.546 -  val dest_eq = dest_binary @{cterm "op = :: real => _"}
   1.547 -  val neq_th = nth pth 5
   1.548 -  fun real_not_eq_conv ct = 
   1.549 -   let 
   1.550 -    val (l,r) = dest_eq (Thm.dest_arg ct)
   1.551 -    val th = Thm.instantiate ([],[(@{cpat "?x::real"},l),(@{cpat "?y::real"},r)]) neq_th
   1.552 -    val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
   1.553 -    val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
   1.554 -    val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
   1.555 -    val th' = Drule.binop_cong_rule @{cterm HOL.disj} 
   1.556 -     (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
   1.557 -     (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
   1.558 -    in Thm.transitive th th' 
   1.559 -  end
   1.560 - fun equal_implies_1_rule PQ = 
   1.561 -  let 
   1.562 -   val P = Thm.lhs_of PQ
   1.563 -  in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P))
   1.564 -  end
   1.565 - (* FIXME!!! Copied from groebner.ml *)
   1.566 - val strip_exists =
   1.567 -  let fun h (acc, t) =
   1.568 -   case (term_of t) of
   1.569 -    Const(@{const_name Ex},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   1.570 -  | _ => (acc,t)
   1.571 -  in fn t => h ([],t)
   1.572 -  end
   1.573 -  fun name_of x = case term_of x of
   1.574 -   Free(s,_) => s
   1.575 - | Var ((s,_),_) => s
   1.576 - | _ => "x"
   1.577 +      end
   1.578 +    fun overall cert_choice dun ths =
   1.579 +      case ths of
   1.580 +        [] =>
   1.581 +        let
   1.582 +          val (eq,ne) = List.partition (is_req o concl) dun
   1.583 +          val (le,nl) = List.partition (is_ge o concl) ne
   1.584 +          val lt = filter (is_gt o concl) nl
   1.585 +        in prover (rev cert_choice) hol_of_positivstellensatz (eq,le,lt) end
   1.586 +      | th::oths =>
   1.587 +        let
   1.588 +          val ct = concl th
   1.589 +        in
   1.590 +          if is_conj ct then
   1.591 +            let
   1.592 +              val (th1,th2) = conj_pair th
   1.593 +            in overall cert_choice dun (th1::th2::oths) end
   1.594 +          else if is_disj ct then
   1.595 +            let
   1.596 +              val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
   1.597 +              val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
   1.598 +            in (disj_cases th th1 th2, Branch (cert1, cert2)) end
   1.599 +          else overall cert_choice (th::dun) oths
   1.600 +        end
   1.601 +    fun dest_binary b ct =
   1.602 +        if is_binop b ct then Thm.dest_binop ct
   1.603 +        else raise CTERM ("dest_binary",[b,ct])
   1.604 +    val dest_eq = dest_binary @{cterm "op = :: real => _"}
   1.605 +    val neq_th = nth pth 5
   1.606 +    fun real_not_eq_conv ct =
   1.607 +      let
   1.608 +        val (l,r) = dest_eq (Thm.dest_arg ct)
   1.609 +        val th = Thm.instantiate ([],[(@{cpat "?x::real"},l),(@{cpat "?y::real"},r)]) neq_th
   1.610 +        val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
   1.611 +        val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
   1.612 +        val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
   1.613 +        val th' = Drule.binop_cong_rule @{cterm HOL.disj}
   1.614 +          (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
   1.615 +          (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
   1.616 +      in Thm.transitive th th'
   1.617 +      end
   1.618 +    fun equal_implies_1_rule PQ =
   1.619 +      let
   1.620 +        val P = Thm.lhs_of PQ
   1.621 +      in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P))
   1.622 +      end
   1.623 +    (* FIXME!!! Copied from groebner.ml *)
   1.624 +    val strip_exists =
   1.625 +      let
   1.626 +        fun h (acc, t) =
   1.627 +          case (term_of t) of
   1.628 +            Const(@{const_name Ex},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   1.629 +          | _ => (acc,t)
   1.630 +      in fn t => h ([],t)
   1.631 +      end
   1.632 +    fun name_of x =
   1.633 +      case term_of x of
   1.634 +        Free(s,_) => s
   1.635 +      | Var ((s,_),_) => s
   1.636 +      | _ => "x"
   1.637  
   1.638 -  fun mk_forall x th = Drule.arg_cong_rule (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) (Thm.abstract_rule (name_of x) x th)
   1.639 +    fun mk_forall x th = Drule.arg_cong_rule (instantiate_cterm' [SOME (ctyp_of_term x)] [] @{cpat "All :: (?'a => bool) => _" }) (Thm.abstract_rule (name_of x) x th)
   1.640  
   1.641 -  val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   1.642 +    val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
   1.643  
   1.644 - fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   1.645 - fun mk_ex v t = Thm.apply (ext (ctyp_of_term v)) (Thm.lambda v t)
   1.646 +    fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   1.647 +    fun mk_ex v t = Thm.apply (ext (ctyp_of_term v)) (Thm.lambda v t)
   1.648  
   1.649 - fun choose v th th' = case concl_of th of 
   1.650 -   @{term Trueprop} $ (Const(@{const_name Ex},_)$_) => 
   1.651 -    let
   1.652 -     val p = (funpow 2 Thm.dest_arg o cprop_of) th
   1.653 -     val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
   1.654 -     val th0 = fconv_rule (Thm.beta_conversion true)
   1.655 -         (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
   1.656 -     val pv = (Thm.rhs_of o Thm.beta_conversion true) 
   1.657 -           (Thm.apply @{cterm Trueprop} (Thm.apply p v))
   1.658 -     val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
   1.659 -    in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
   1.660 - | _ => raise THM ("choose",0,[th, th'])
   1.661 +    fun choose v th th' =
   1.662 +      case concl_of th of
   1.663 +        @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
   1.664 +        let
   1.665 +          val p = (funpow 2 Thm.dest_arg o cprop_of) th
   1.666 +          val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
   1.667 +          val th0 = fconv_rule (Thm.beta_conversion true)
   1.668 +            (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
   1.669 +          val pv = (Thm.rhs_of o Thm.beta_conversion true)
   1.670 +            (Thm.apply @{cterm Trueprop} (Thm.apply p v))
   1.671 +          val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
   1.672 +        in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
   1.673 +      | _ => raise THM ("choose",0,[th, th'])
   1.674  
   1.675 -  fun simple_choose v th = 
   1.676 -     choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
   1.677 +    fun simple_choose v th =
   1.678 +      choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
   1.679  
   1.680 - val strip_forall =
   1.681 -  let fun h (acc, t) =
   1.682 -   case (term_of t) of
   1.683 -    Const(@{const_name All},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   1.684 -  | _ => (acc,t)
   1.685 -  in fn t => h ([],t)
   1.686 -  end
   1.687 +    val strip_forall =
   1.688 +      let
   1.689 +        fun h (acc, t) =
   1.690 +          case (term_of t) of
   1.691 +            Const(@{const_name All},_)$Abs(_,_,_) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   1.692 +          | _ => (acc,t)
   1.693 +      in fn t => h ([],t)
   1.694 +      end
   1.695  
   1.696 - fun f ct =
   1.697 -  let 
   1.698 -   val nnf_norm_conv' = 
   1.699 -     nnf_conv then_conv 
   1.700 -     literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
   1.701 -     (Conv.cache_conv 
   1.702 -       (first_conv [real_lt_conv, real_le_conv, 
   1.703 -                    real_eq_conv, real_not_lt_conv, 
   1.704 -                    real_not_le_conv, real_not_eq_conv, all_conv]))
   1.705 -  fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
   1.706 -                  (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv 
   1.707 -        try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
   1.708 -  val nct = Thm.apply @{cterm Trueprop} (Thm.apply @{cterm "Not"} ct)
   1.709 -  val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
   1.710 -  val tm0 = Thm.dest_arg (Thm.rhs_of th0)
   1.711 -  val (th, certificates) = if tm0 aconvc @{cterm False} then (equal_implies_1_rule th0, Trivial) else
   1.712 -   let 
   1.713 -    val (evs,bod) = strip_exists tm0
   1.714 -    val (avs,ibod) = strip_forall bod
   1.715 -    val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
   1.716 -    val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
   1.717 -    val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
   1.718 -   in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
   1.719 -   end
   1.720 -  in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
   1.721 - end
   1.722 -in f
   1.723 -end;
   1.724 +    fun f ct =
   1.725 +      let
   1.726 +        val nnf_norm_conv' =
   1.727 +          nnf_conv then_conv
   1.728 +          literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
   1.729 +          (Conv.cache_conv
   1.730 +            (first_conv [real_lt_conv, real_le_conv,
   1.731 +                         real_eq_conv, real_not_lt_conv,
   1.732 +                         real_not_le_conv, real_not_eq_conv, all_conv]))
   1.733 +        fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] []
   1.734 +                  (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv
   1.735 +                  try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
   1.736 +        val nct = Thm.apply @{cterm Trueprop} (Thm.apply @{cterm "Not"} ct)
   1.737 +        val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
   1.738 +        val tm0 = Thm.dest_arg (Thm.rhs_of th0)
   1.739 +        val (th, certificates) =
   1.740 +          if tm0 aconvc @{cterm False} then (equal_implies_1_rule th0, Trivial) else
   1.741 +          let
   1.742 +            val (evs,bod) = strip_exists tm0
   1.743 +            val (avs,ibod) = strip_forall bod
   1.744 +            val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
   1.745 +            val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
   1.746 +            val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
   1.747 +          in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
   1.748 +          end
   1.749 +      in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
   1.750 +      end
   1.751 +  in f
   1.752 +  end;
   1.753  
   1.754  (* A linear arithmetic prover *)
   1.755  local
   1.756 @@ -560,183 +576,190 @@
   1.757       ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso
   1.758         not(p(FuncUtil.Ctermfunc.apply e one_tm)))
   1.759  
   1.760 -  fun linear_ineqs vars (les,lts) = 
   1.761 -   case find_first (contradictory (fn x => x >/ Rat.zero)) lts of
   1.762 -    SOME r => r
   1.763 -  | NONE => 
   1.764 -   (case find_first (contradictory (fn x => x >/ Rat.zero)) les of
   1.765 -     SOME r => r
   1.766 -   | NONE => 
   1.767 -     if null vars then error "linear_ineqs: no contradiction" else
   1.768 -     let 
   1.769 -      val ineqs = les @ lts
   1.770 -      fun blowup v =
   1.771 -       length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) ineqs) +
   1.772 -       length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) ineqs) *
   1.773 -       length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero </ Rat.zero) ineqs)
   1.774 -      val  v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j))
   1.775 -                 (map (fn v => (v,blowup v)) vars)))
   1.776 -      fun addup (e1,p1) (e2,p2) acc =
   1.777 -       let 
   1.778 -        val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v Rat.zero 
   1.779 -        val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v Rat.zero
   1.780 -       in if c1 */ c2 >=/ Rat.zero then acc else
   1.781 -        let 
   1.782 -         val e1' = linear_cmul (Rat.abs c2) e1
   1.783 -         val e2' = linear_cmul (Rat.abs c1) e2
   1.784 -         val p1' = Product(Rational_lt(Rat.abs c2),p1)
   1.785 -         val p2' = Product(Rational_lt(Rat.abs c1),p2)
   1.786 -        in (linear_add e1' e2',Sum(p1',p2'))::acc
   1.787 -        end
   1.788 -       end
   1.789 -      val (les0,les1) = 
   1.790 -         List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) les
   1.791 -      val (lts0,lts1) = 
   1.792 -         List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) lts
   1.793 -      val (lesp,lesn) = 
   1.794 -         List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) les1
   1.795 -      val (ltsp,ltsn) = 
   1.796 -         List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) lts1
   1.797 -      val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0
   1.798 -      val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn
   1.799 +  fun linear_ineqs vars (les,lts) =
   1.800 +    case find_first (contradictory (fn x => x >/ Rat.zero)) lts of
   1.801 +      SOME r => r
   1.802 +    | NONE =>
   1.803 +      (case find_first (contradictory (fn x => x >/ Rat.zero)) les of
   1.804 +         SOME r => r
   1.805 +       | NONE =>
   1.806 +         if null vars then error "linear_ineqs: no contradiction" else
   1.807 +         let
   1.808 +           val ineqs = les @ lts
   1.809 +           fun blowup v =
   1.810 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) ineqs) +
   1.811 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) ineqs) *
   1.812 +             length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero </ Rat.zero) ineqs)
   1.813 +           val v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j))
   1.814 +             (map (fn v => (v,blowup v)) vars)))
   1.815 +           fun addup (e1,p1) (e2,p2) acc =
   1.816 +             let
   1.817 +               val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v Rat.zero
   1.818 +               val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v Rat.zero
   1.819 +             in
   1.820 +               if c1 */ c2 >=/ Rat.zero then acc else
   1.821 +               let
   1.822 +                 val e1' = linear_cmul (Rat.abs c2) e1
   1.823 +                 val e2' = linear_cmul (Rat.abs c1) e2
   1.824 +                 val p1' = Product(Rational_lt(Rat.abs c2),p1)
   1.825 +                 val p2' = Product(Rational_lt(Rat.abs c1),p2)
   1.826 +               in (linear_add e1' e2',Sum(p1',p2'))::acc
   1.827 +               end
   1.828 +             end
   1.829 +           val (les0,les1) =
   1.830 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) les
   1.831 +           val (lts0,lts1) =
   1.832 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) lts
   1.833 +           val (lesp,lesn) =
   1.834 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) les1
   1.835 +           val (ltsp,ltsn) =
   1.836 +             List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) lts1
   1.837 +           val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0
   1.838 +           val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn
   1.839                        (fold_rev (fn ep1 => fold_rev (addup ep1) (lesn@ltsn)) ltsp lts0)
   1.840 -     in linear_ineqs (remove (op aconvc) v vars) (les',lts')
   1.841 -     end)
   1.842 +         in linear_ineqs (remove (op aconvc) v vars) (les',lts')
   1.843 +         end)
   1.844  
   1.845 -  fun linear_eqs(eqs,les,lts) = 
   1.846 -   case find_first (contradictory (fn x => x =/ Rat.zero)) eqs of
   1.847 -    SOME r => r
   1.848 -  | NONE => (case eqs of 
   1.849 -    [] => 
   1.850 -     let val vars = remove (op aconvc) one_tm 
   1.851 -           (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
   1.852 -     in linear_ineqs vars (les,lts) end
   1.853 -   | (e,p)::es => 
   1.854 -     if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
   1.855 -     let 
   1.856 -      val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.delete_safe one_tm e)
   1.857 -      fun xform (inp as (t,q)) =
   1.858 -       let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
   1.859 -        if d =/ Rat.zero then inp else
   1.860 -        let 
   1.861 -         val k = (Rat.neg d) */ Rat.abs c // c
   1.862 -         val e' = linear_cmul k e
   1.863 -         val t' = linear_cmul (Rat.abs c) t
   1.864 -         val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
   1.865 -         val q' = Product(Rational_lt(Rat.abs c),q) 
   1.866 -        in (linear_add e' t',Sum(p',q')) 
   1.867 -        end 
   1.868 -      end
   1.869 -     in linear_eqs(map xform es,map xform les,map xform lts)
   1.870 -     end)
   1.871 +  fun linear_eqs(eqs,les,lts) =
   1.872 +    case find_first (contradictory (fn x => x =/ Rat.zero)) eqs of
   1.873 +      SOME r => r
   1.874 +    | NONE =>
   1.875 +      (case eqs of
   1.876 +         [] =>
   1.877 +         let val vars = remove (op aconvc) one_tm
   1.878 +             (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom o fst) (les@lts) [])
   1.879 +         in linear_ineqs vars (les,lts) end
   1.880 +       | (e,p)::es =>
   1.881 +         if FuncUtil.Ctermfunc.is_empty e then linear_eqs (es,les,lts) else
   1.882 +         let
   1.883 +           val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.delete_safe one_tm e)
   1.884 +           fun xform (inp as (t,q)) =
   1.885 +             let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
   1.886 +               if d =/ Rat.zero then inp else
   1.887 +               let
   1.888 +                 val k = (Rat.neg d) */ Rat.abs c // c
   1.889 +                 val e' = linear_cmul k e
   1.890 +                 val t' = linear_cmul (Rat.abs c) t
   1.891 +                 val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
   1.892 +                 val q' = Product(Rational_lt(Rat.abs c),q)
   1.893 +               in (linear_add e' t',Sum(p',q'))
   1.894 +               end
   1.895 +             end
   1.896 +         in linear_eqs(map xform es,map xform les,map xform lts)
   1.897 +         end)
   1.898  
   1.899 -  fun linear_prover (eq,le,lt) = 
   1.900 -   let 
   1.901 -    val eqs = map_index (fn (n, p) => (p,Axiom_eq n)) eq
   1.902 -    val les = map_index (fn (n, p) => (p,Axiom_le n)) le
   1.903 -    val lts = map_index (fn (n, p) => (p,Axiom_lt n)) lt
   1.904 -   in linear_eqs(eqs,les,lts)
   1.905 -   end 
   1.906 -  
   1.907 -  fun lin_of_hol ct = 
   1.908 -   if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.empty
   1.909 -   else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   1.910 -   else if is_ratconst ct then FuncUtil.Ctermfunc.onefunc (one_tm, dest_ratconst ct)
   1.911 -   else
   1.912 -    let val (lop,r) = Thm.dest_comb ct 
   1.913 -    in if not (is_comb lop) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   1.914 -       else
   1.915 -        let val (opr,l) = Thm.dest_comb lop 
   1.916 -        in if opr aconvc @{cterm "op + :: real =>_"} 
   1.917 -           then linear_add (lin_of_hol l) (lin_of_hol r)
   1.918 -           else if opr aconvc @{cterm "op * :: real =>_"} 
   1.919 -                   andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
   1.920 -           else FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   1.921 -        end
   1.922 +  fun linear_prover (eq,le,lt) =
   1.923 +    let
   1.924 +      val eqs = map_index (fn (n, p) => (p,Axiom_eq n)) eq
   1.925 +      val les = map_index (fn (n, p) => (p,Axiom_le n)) le
   1.926 +      val lts = map_index (fn (n, p) => (p,Axiom_lt n)) lt
   1.927 +    in linear_eqs(eqs,les,lts)
   1.928      end
   1.929  
   1.930 -  fun is_alien ct = case term_of ct of 
   1.931 -   Const(@{const_name "real"}, _)$ n => 
   1.932 -     if can HOLogic.dest_number n then false else true
   1.933 -  | _ => false
   1.934 -in 
   1.935 -fun real_linear_prover translator (eq,le,lt) = 
   1.936 - let 
   1.937 -  val lhs = lin_of_hol o Thm.dest_arg1 o Thm.dest_arg o cprop_of
   1.938 -  val rhs = lin_of_hol o Thm.dest_arg o Thm.dest_arg o cprop_of
   1.939 -  val eq_pols = map lhs eq
   1.940 -  val le_pols = map rhs le
   1.941 -  val lt_pols = map rhs lt 
   1.942 -  val aliens =  filter is_alien
   1.943 -      (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) 
   1.944 -          (eq_pols @ le_pols @ lt_pols) [])
   1.945 -  val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
   1.946 -  val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
   1.947 -  val le' = le @ map (fn a => instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens 
   1.948 - in ((translator (eq,le',lt) proof), Trivial)
   1.949 - end
   1.950 +  fun lin_of_hol ct =
   1.951 +    if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.empty
   1.952 +    else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   1.953 +    else if is_ratconst ct then FuncUtil.Ctermfunc.onefunc (one_tm, dest_ratconst ct)
   1.954 +    else
   1.955 +      let val (lop,r) = Thm.dest_comb ct
   1.956 +      in
   1.957 +        if not (is_comb lop) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   1.958 +        else
   1.959 +          let val (opr,l) = Thm.dest_comb lop
   1.960 +          in
   1.961 +            if opr aconvc @{cterm "op + :: real =>_"}
   1.962 +            then linear_add (lin_of_hol l) (lin_of_hol r)
   1.963 +            else if opr aconvc @{cterm "op * :: real =>_"}
   1.964 +                    andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
   1.965 +            else FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   1.966 +          end
   1.967 +      end
   1.968 +
   1.969 +  fun is_alien ct =
   1.970 +      case term_of ct of
   1.971 +        Const(@{const_name "real"}, _)$ n =>
   1.972 +        if can HOLogic.dest_number n then false else true
   1.973 +      | _ => false
   1.974 +in
   1.975 +fun real_linear_prover translator (eq,le,lt) =
   1.976 +  let
   1.977 +    val lhs = lin_of_hol o Thm.dest_arg1 o Thm.dest_arg o cprop_of
   1.978 +    val rhs = lin_of_hol o Thm.dest_arg o Thm.dest_arg o cprop_of
   1.979 +    val eq_pols = map lhs eq
   1.980 +    val le_pols = map rhs le
   1.981 +    val lt_pols = map rhs lt
   1.982 +    val aliens = filter is_alien
   1.983 +      (fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom)
   1.984 +                (eq_pols @ le_pols @ lt_pols) [])
   1.985 +    val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
   1.986 +    val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
   1.987 +    val le' = le @ map (fn a => instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens
   1.988 +  in ((translator (eq,le',lt) proof), Trivial)
   1.989 +  end
   1.990  end;
   1.991  
   1.992  (* A less general generic arithmetic prover dealing with abs,max and min*)
   1.993  
   1.994  local
   1.995 - val absmaxmin_elim_ss1 = HOL_basic_ss addsimps real_abs_thms1
   1.996 - fun absmaxmin_elim_conv1 ctxt = 
   1.997 +  val absmaxmin_elim_ss1 = HOL_basic_ss addsimps real_abs_thms1
   1.998 +  fun absmaxmin_elim_conv1 ctxt =
   1.999      Simplifier.rewrite (Simplifier.context ctxt absmaxmin_elim_ss1)
  1.1000  
  1.1001 - val absmaxmin_elim_conv2 =
  1.1002 -  let 
  1.1003 -   val pth_abs = instantiate' [SOME @{ctyp real}] [] abs_split'
  1.1004 -   val pth_max = instantiate' [SOME @{ctyp real}] [] max_split
  1.1005 -   val pth_min = instantiate' [SOME @{ctyp real}] [] min_split
  1.1006 -   val abs_tm = @{cterm "abs :: real => _"}
  1.1007 -   val p_tm = @{cpat "?P :: real => bool"}
  1.1008 -   val x_tm = @{cpat "?x :: real"}
  1.1009 -   val y_tm = @{cpat "?y::real"}
  1.1010 -   val is_max = is_binop @{cterm "max :: real => _"}
  1.1011 -   val is_min = is_binop @{cterm "min :: real => _"} 
  1.1012 -   fun is_abs t = is_comb t andalso Thm.dest_fun t aconvc abs_tm
  1.1013 -   fun eliminate_construct p c tm =
  1.1014 -    let 
  1.1015 -     val t = find_cterm p tm
  1.1016 -     val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.apply (Thm.lambda t tm) t)
  1.1017 -     val (p,ax) = (Thm.dest_comb o Thm.rhs_of) th0
  1.1018 -    in fconv_rule(arg_conv(binop_conv (arg_conv (Thm.beta_conversion false))))
  1.1019 -               (Thm.transitive th0 (c p ax))
  1.1020 -   end
  1.1021 +  val absmaxmin_elim_conv2 =
  1.1022 +    let
  1.1023 +      val pth_abs = instantiate' [SOME @{ctyp real}] [] abs_split'
  1.1024 +      val pth_max = instantiate' [SOME @{ctyp real}] [] max_split
  1.1025 +      val pth_min = instantiate' [SOME @{ctyp real}] [] min_split
  1.1026 +      val abs_tm = @{cterm "abs :: real => _"}
  1.1027 +      val p_tm = @{cpat "?P :: real => bool"}
  1.1028 +      val x_tm = @{cpat "?x :: real"}
  1.1029 +      val y_tm = @{cpat "?y::real"}
  1.1030 +      val is_max = is_binop @{cterm "max :: real => _"}
  1.1031 +      val is_min = is_binop @{cterm "min :: real => _"}
  1.1032 +      fun is_abs t = is_comb t andalso Thm.dest_fun t aconvc abs_tm
  1.1033 +      fun eliminate_construct p c tm =
  1.1034 +        let
  1.1035 +          val t = find_cterm p tm
  1.1036 +          val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.apply (Thm.lambda t tm) t)
  1.1037 +          val (p,ax) = (Thm.dest_comb o Thm.rhs_of) th0
  1.1038 +        in fconv_rule(arg_conv(binop_conv (arg_conv (Thm.beta_conversion false))))
  1.1039 +                     (Thm.transitive th0 (c p ax))
  1.1040 +        end
  1.1041  
  1.1042 -   val elim_abs = eliminate_construct is_abs
  1.1043 -    (fn p => fn ax => 
  1.1044 -       Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax)]) pth_abs)
  1.1045 -   val elim_max = eliminate_construct is_max
  1.1046 -    (fn p => fn ax => 
  1.1047 -      let val (ax,y) = Thm.dest_comb ax 
  1.1048 -      in  Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)]) 
  1.1049 -      pth_max end)
  1.1050 -   val elim_min = eliminate_construct is_min
  1.1051 -    (fn p => fn ax => 
  1.1052 -      let val (ax,y) = Thm.dest_comb ax 
  1.1053 -      in  Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)]) 
  1.1054 -      pth_min end)
  1.1055 -   in first_conv [elim_abs, elim_max, elim_min, all_conv]
  1.1056 -  end;
  1.1057 -in fun gen_real_arith ctxt (mkconst,eq,ge,gt,norm,neg,add,mul,prover) =
  1.1058 -        gen_gen_real_arith ctxt (mkconst,eq,ge,gt,norm,neg,add,mul,
  1.1059 -                       absmaxmin_elim_conv1 ctxt,absmaxmin_elim_conv2,prover)
  1.1060 +      val elim_abs = eliminate_construct is_abs
  1.1061 +        (fn p => fn ax =>
  1.1062 +          Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax)]) pth_abs)
  1.1063 +      val elim_max = eliminate_construct is_max
  1.1064 +        (fn p => fn ax =>
  1.1065 +          let val (ax,y) = Thm.dest_comb ax
  1.1066 +          in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)])
  1.1067 +                             pth_max end)
  1.1068 +      val elim_min = eliminate_construct is_min
  1.1069 +        (fn p => fn ax =>
  1.1070 +          let val (ax,y) = Thm.dest_comb ax
  1.1071 +          in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)])
  1.1072 +                             pth_min end)
  1.1073 +    in first_conv [elim_abs, elim_max, elim_min, all_conv]
  1.1074 +    end;
  1.1075 +in
  1.1076 +fun gen_real_arith ctxt (mkconst,eq,ge,gt,norm,neg,add,mul,prover) =
  1.1077 +  gen_gen_real_arith ctxt
  1.1078 +    (mkconst,eq,ge,gt,norm,neg,add,mul,
  1.1079 +     absmaxmin_elim_conv1 ctxt,absmaxmin_elim_conv2,prover)
  1.1080  end;
  1.1081  
  1.1082 -(* An instance for reals*) 
  1.1083 +(* An instance for reals*)
  1.1084  
  1.1085 -fun gen_prover_real_arith ctxt prover = 
  1.1086 - let
  1.1087 -  fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
  1.1088 -  val {add, mul, neg, pow = _, sub = _, main} = 
  1.1089 -     Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
  1.1090 -      (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
  1.1091 -     simple_cterm_ord
  1.1092 -in gen_real_arith ctxt
  1.1093 -   (cterm_of_rat, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv,
  1.1094 -    main,neg,add,mul, prover)
  1.1095 -end;
  1.1096 +fun gen_prover_real_arith ctxt prover =
  1.1097 +  let
  1.1098 +    fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS
  1.1099 +    val {add, mul, neg, pow = _, sub = _, main} =
  1.1100 +        Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
  1.1101 +        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
  1.1102 +        simple_cterm_ord
  1.1103 +  in gen_real_arith ctxt
  1.1104 +     (cterm_of_rat, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv, Numeral_Simprocs.field_comp_conv,
  1.1105 +      main,neg,add,mul, prover)
  1.1106 +  end;
  1.1107  
  1.1108  end