# HG changeset patch
# User wenzelm
# Date 1517501707 -3600
# Node ID 2427d3e72b6eeb5c2c1f79d51861baa72550554b
# Parent  f0b11413f1c9a6d595825b93dcf1cd1a805fea96
clarified signature;
eliminated aliases of Thm.term_ord;

diff -r f0b11413f1c9 -r 2427d3e72b6e src/HOL/Analysis/normarith.ML
--- a/src/HOL/Analysis/normarith.ML	Thu Feb 01 15:31:25 2018 +0100
+++ b/src/HOL/Analysis/normarith.ML	Thu Feb 01 17:15:07 2018 +0100
@@ -375,13 +375,12 @@
 local
  val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0}))
  fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
- fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u));
   (* FIXME: Lookup in the context every time!!! Fix this !!!*)
  fun splitequation ctxt th acc =
   let
    val real_poly_neg_conv = #neg
        (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
-        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
+        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) Thm.term_ord)
    val (th1,th2) = conj_pair(rawrule th)
   in th1::fconv_rule (arg_conv (arg_conv (real_poly_neg_conv ctxt))) th2::acc
   end
diff -r f0b11413f1c9 -r 2427d3e72b6e src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 15:31:25 2018 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Feb 01 17:15:07 2018 +0100
@@ -890,9 +890,11 @@
 
 declaration \<open>
 let
-  fun earlier [] x y = false
-    | earlier (h::t) x y =
-        if h aconvc y then false else if h aconvc x then true else earlier t x y;
+  fun earlier [] _ = false
+    | earlier (h::t) (x, y) =
+        if h aconvc y then false else if h aconvc x then true else earlier t (x, y);
+
+  val earlier_ord = make_ord o earlier;
 
 fun dest_frac ct =
   case Thm.term_of ct of
@@ -932,14 +934,14 @@
         val th = Thm.implies_elim (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] (map SOME [c,x,t])
              (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
         val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
-                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
+                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
       in rth end
     | ("x+t",[t]) =>
        let
         val T = Thm.ctyp_of_cterm x
         val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"}
         val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
-              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
+              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
        in  rth end
     | ("c*x",[c]) =>
        let
@@ -977,14 +979,14 @@
         val th = Thm.implies_elim (Thm.instantiate' [SOME cT] (map SOME [c,x,t])
              (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
         val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
-                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
+                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
       in rth end
     | ("x+t",[t]) =>
        let
         val T = Thm.ctyp_of_cterm x
         val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"}
         val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
-              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
+              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
        in  rth end
     | ("c*x",[c]) =>
        let
@@ -1020,14 +1022,14 @@
         val th = Thm.implies_elim
                  (Thm.instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
         val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
-                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
+                   (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
       in rth end
     | ("x+t",[t]) =>
        let
         val T = Thm.ctyp_of_cterm x
         val th = Thm.instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"}
         val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv
-              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th
+              (Semiring_Normalizer.semiring_normalize_ord_conv ctxt (earlier_ord vs)))) th
        in  rth end
     | ("c*x",[c]) =>
        let
@@ -1057,7 +1059,7 @@
        val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
        val nth = Conv.fconv_rule
          (Conv.arg_conv (Conv.arg1_conv
-              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
+              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
        val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
 | Const(@{const_name Orderings.less_eq},_)$a$b =>
@@ -1066,7 +1068,7 @@
        val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
        val nth = Conv.fconv_rule
          (Conv.arg_conv (Conv.arg1_conv
-              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
+              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
        val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
 
@@ -1076,7 +1078,7 @@
        val th = Thm.instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0
        val nth = Conv.fconv_rule
          (Conv.arg_conv (Conv.arg1_conv
-              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier vs)))) th
+              (Semiring_Normalizer.semiring_normalize_ord_conv (put_simpset ss ctxt) (earlier_ord vs)))) th
        val rth = Thm.transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
 | @{term "Not"} $(Const(@{const_name HOL.eq},_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct
diff -r f0b11413f1c9 -r 2427d3e72b6e src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Feb 01 15:31:25 2018 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Feb 01 17:15:07 2018 +0100
@@ -750,7 +750,6 @@
 local
   open Conv
   val concl = Thm.dest_arg o Thm.cprop_of
-  fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
 in
 (* FIXME: Replace tryfind by get_first !! *)
 fun real_nonlinear_prover proof_method ctxt =
@@ -758,7 +757,7 @@
     val {add = _, mul = _, neg = _, pow = _, sub = _, main = real_poly_conv} =
       Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
         (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
-        simple_cterm_ord
+        Thm.term_ord
     fun mainf cert_choice translator (eqs, les, lts) =
       let
         val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs
@@ -851,7 +850,6 @@
 
 local
   open Conv
-  fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
   val concl = Thm.dest_arg o Thm.cprop_of
   val shuffle1 =
     fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))"
@@ -894,7 +892,7 @@
     val {add = _, mul = real_poly_mul_conv, neg = _, pow = _, sub = _, main = real_poly_conv} =
       Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
         (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
-        simple_cterm_ord
+        Thm.term_ord
 
     fun make_substitution th =
       let
diff -r f0b11413f1c9 -r 2427d3e72b6e src/HOL/Library/positivstellensatz.ML
--- a/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 15:31:25 2018 +0100
+++ b/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 17:15:07 2018 +0100
@@ -764,11 +764,10 @@
 
 fun gen_prover_real_arith ctxt prover =
   let
-    fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
     val {add, mul, neg, pow = _, sub = _, main} =
         Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
         (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
-        simple_cterm_ord
+        Thm.term_ord
   in gen_real_arith ctxt
      (cterm_of_rat,
       Numeral_Simprocs.field_comp_conv ctxt,
diff -r f0b11413f1c9 -r 2427d3e72b6e src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Thu Feb 01 15:31:25 2018 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML	Thu Feb 01 17:15:07 2018 +0100
@@ -18,13 +18,13 @@
     local_theory -> local_theory
 
   val semiring_normalize_conv: Proof.context -> conv
-  val semiring_normalize_ord_conv: Proof.context -> (cterm -> cterm -> bool) -> conv
+  val semiring_normalize_ord_conv: Proof.context -> (cterm * cterm -> order) -> conv
   val semiring_normalize_wrapper: Proof.context -> entry -> conv
   val semiring_normalize_ord_wrapper: Proof.context -> entry
-    -> (cterm -> cterm -> bool) -> conv
+    -> (cterm * cterm -> order) -> conv
   val semiring_normalizers_conv: cterm list -> cterm list * thm list
     -> cterm list * thm list -> cterm list * thm list ->
-      (cterm -> bool) * conv * conv * conv -> (cterm -> cterm -> bool) ->
+      (cterm -> bool) * conv * conv * conv -> (cterm * cterm -> order) ->
         {add: Proof.context -> conv,
          mul: Proof.context -> conv,
          neg: Proof.context -> conv,
@@ -32,7 +32,7 @@
          pow: Proof.context -> conv,
          sub: Proof.context -> conv}
   val semiring_normalizers_ord_wrapper:  Proof.context -> entry ->
-    (cterm -> cterm -> bool) ->
+    (cterm * cterm -> order) ->
       {add: Proof.context -> conv,
        mul: Proof.context -> conv,
        neg: Proof.context -> conv,
@@ -327,7 +327,7 @@
      end
    | _ => (TrueI, true_tm, true_tm));
 
-in fn variable_order =>
+in fn variable_ord =>
  let
 
 (* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible.  *)
@@ -438,7 +438,7 @@
     else
      if x aconvc one_tm then ~1
      else if y aconvc one_tm then 1
-      else if variable_order x y then ~1 else 1
+      else if is_less (variable_ord (x, y)) then ~1 else 1
    fun monomial_mul tm l r =
     ((let val (lx,ly) = dest_mul l val vl = powvar lx
       in
@@ -594,8 +594,8 @@
   | (_ ,[]) => ~1
   | ([], _) => 1
   | (((x1,n1)::vs1),((x2,n2)::vs2)) =>
-     if variable_order x1 x2 then 1
-     else if variable_order x2 x1 then ~1
+     if is_less (variable_ord (x1, x2)) then 1
+     else if is_less (variable_ord (x2, x1)) then ~1
      else if n1 < n2 then ~1
      else if n2 < n1 then 1
      else lexorder vs1 vs2
@@ -851,13 +851,11 @@
     addsimps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps})
     addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]);
 
-fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u));
-
 
 (* various normalizing conversions *)
 
 fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal},
-                                     {conv, dest_const, mk_const, is_const}) ord =
+                                     {conv, dest_const, mk_const, is_const}) term_ord =
   let
     val pow_conv =
       Conv.arg_conv (Simplifier.rewrite (put_simpset nat_exp_ss ctxt))
@@ -865,21 +863,22 @@
         (put_simpset HOL_basic_ss ctxt addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
       then_conv conv ctxt
     val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
-  in semiring_normalizers_conv vars semiring ring field dat ord end;
+  in semiring_normalizers_conv vars semiring ring field dat term_ord end;
 
-fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord =
+fun semiring_normalize_ord_wrapper ctxt
+  ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) term_ord =
  #main (semiring_normalizers_ord_wrapper ctxt
   ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal},
-   {conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord) ctxt;
+   {conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) term_ord) ctxt;
 
 fun semiring_normalize_wrapper ctxt data =
-  semiring_normalize_ord_wrapper ctxt data simple_cterm_ord;
+  semiring_normalize_ord_wrapper ctxt data Thm.term_ord;
 
 fun semiring_normalize_ord_conv ctxt ord tm =
   (case match ctxt tm of
     NONE => Thm.reflexive tm
   | SOME res => semiring_normalize_ord_wrapper ctxt res ord tm);
 
-fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord;
+fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt Thm.term_ord;
 
 end;