--- 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) ->
{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;