author wenzelm Thu, 01 Feb 2018 17:15:07 +0100 changeset 67562 2427d3e72b6e parent 67561 f0b11413f1c9 child 67563 6e5316a43079
clarified signature; eliminated aliases of Thm.term_ord;
```--- 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```
```--- 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```
```--- 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```
```--- 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,```
```--- 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) ->
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) ->
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})

-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;```