--- a/src/HOL/Analysis/normarith.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Analysis/normarith.ML Thu Feb 01 13:55:10 2018 +0100
@@ -375,7 +375,7 @@
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 = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS;
+ fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS;
(* FIXME: Lookup in the context every time!!! Fix this !!!*)
fun splitequation ctxt th acc =
let
--- a/src/HOL/Decision_Procs/langford.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Thu Feb 01 13:55:10 2018 +0100
@@ -229,7 +229,7 @@
let
fun all x t =
Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t)
- val ts = sort (fn (a, b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
+ val ts = sort Thm.fast_term_ord (f p)
val p' = fold_rev all ts p
in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Thu Feb 01 13:55:10 2018 +0100
@@ -211,9 +211,9 @@
FuncUtil.Monomialfunc.fold (fn (m, _) => fn a => max (monomial_multidegree m) a) p 0;
fun poly_variables p =
- sort FuncUtil.cterm_ord
+ sort Thm.fast_term_ord
(FuncUtil.Monomialfunc.fold_rev
- (fn (m, _) => union (is_equal o FuncUtil.cterm_ord) (monomial_variables m)) p []);
+ (fn (m, _) => union (is_equal o Thm.fast_term_ord) (monomial_variables m)) p []);
(* Conversion from HOL term. *)
@@ -750,7 +750,7 @@
local
open Conv
val concl = Thm.dest_arg o Thm.cprop_of
- fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
+ fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
in
(* FIXME: Replace tryfind by get_first !! *)
fun real_nonlinear_prover proof_method ctxt =
@@ -851,7 +851,7 @@
local
open Conv
- fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
+ fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
val concl = Thm.dest_arg o Thm.cprop_of
val shuffle1 =
fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))"
--- a/src/HOL/Library/positivstellensatz.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Thu Feb 01 13:55:10 2018 +0100
@@ -63,22 +63,17 @@
structure Intpairfunc = FuncFun(type key = int*int val ord = prod_ord int_ord int_ord);
structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord);
-
-val cterm_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of
-
-structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
+structure Ctermfunc = FuncFun(type key = cterm val ord = Thm.fast_term_ord);
type monomial = int Ctermfunc.table;
-
-val monomial_ord = list_ord (prod_ord cterm_ord int_ord) o apply2 Ctermfunc.dest
-
+val monomial_ord = list_ord (prod_ord Thm.fast_term_ord int_ord) o apply2 Ctermfunc.dest
structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
type poly = Rat.rat Monomialfunc.table;
(* The ordering so we can create canonical HOL polynomials. *)
-fun dest_monomial mon = sort (cterm_ord o apply2 fst) (Ctermfunc.dest mon);
+fun dest_monomial mon = sort (Thm.fast_term_ord o apply2 fst) (Ctermfunc.dest mon);
fun monomial_order (m1,m2) =
if Ctermfunc.is_empty m2 then LESS
@@ -91,7 +86,7 @@
val deg2 = fold (Integer.add o snd) mon2 0
in if deg1 < deg2 then GREATER
else if deg1 > deg2 then LESS
- else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
+ else list_ord (prod_ord Thm.fast_term_ord int_ord) (mon1,mon2)
end;
end
@@ -769,7 +764,7 @@
fun gen_prover_real_arith ctxt prover =
let
- fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS
+ fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
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>))
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Feb 01 13:55:10 2018 +0100
@@ -803,7 +803,7 @@
let
fun all x t =
Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t)
- val ts = sort (fn (a, b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p)
+ val ts = sort Thm.fast_term_ord (f p)
val p' = fold_rev all ts p
in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
--- a/src/HOL/Tools/groebner.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Tools/groebner.ML Thu Feb 01 13:55:10 2018 +0100
@@ -646,8 +646,7 @@
val cjs = conjs tm
val rawvars =
fold_rev (fn eq => fn a => grobvars (Thm.dest_arg1 eq) (grobvars (Thm.dest_arg eq) a)) cjs []
- val vars = sort (fn (x, y) => Term_Ord.term_ord (Thm.term_of x, Thm.term_of y))
- (distinct (op aconvc) rawvars)
+ val vars = sort Thm.term_ord (distinct (op aconvc) rawvars)
in (vars,map (grobify_equation vars) cjs)
end;
@@ -866,8 +865,7 @@
let
val vars = filter (fn v => free_in v eq) evs
val (qs,p) = isolate_monomials vars eq
- val rs = ideal (qs @ ps) p
- (fn (s,t) => Term_Ord.term_ord (Thm.term_of s, Thm.term_of t))
+ val rs = ideal (qs @ ps) p Thm.term_ord
in (eq, take (length qs) rs ~~ vars)
end;
fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
--- a/src/HOL/Tools/sat.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Tools/sat.ML Thu Feb 01 13:55:10 2018 +0100
@@ -303,7 +303,7 @@
(* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
(* terms sorted in descending order, while only linear for terms *)
(* sorted in ascending order *)
- val sorted_clauses = sort (Term_Ord.fast_term_ord o apply2 Thm.term_of) nontrivial_clauses
+ val sorted_clauses = sort Thm.fast_term_ord nontrivial_clauses
val _ =
cond_tracing ctxt (fn () =>
"Sorted non-trivial clauses:\n" ^
--- a/src/HOL/Tools/semiring_normalizer.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML Thu Feb 01 13:55:10 2018 +0100
@@ -851,7 +851,7 @@
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 = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS;
+fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS;
(* various normalizing conversions *)
--- a/src/Pure/Isar/rule_cases.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/Pure/Isar/rule_cases.ML Thu Feb 01 13:55:10 2018 +0100
@@ -415,7 +415,7 @@
local
fun equal_cterms ts us =
- is_equal (list_ord (Term_Ord.fast_term_ord o apply2 Thm.term_of) (ts, us));
+ is_equal (list_ord Thm.fast_term_ord (ts, us));
fun prep_rule n th =
let
--- a/src/Pure/more_thm.ML Wed Jan 31 21:05:47 2018 +0100
+++ b/src/Pure/more_thm.ML Thu Feb 01 13:55:10 2018 +0100
@@ -38,6 +38,8 @@
val dest_equals_rhs: cterm -> cterm
val lhs_of: thm -> cterm
val rhs_of: thm -> cterm
+ val fast_term_ord: cterm * cterm -> order
+ val term_ord: cterm * cterm -> order
val thm_ord: thm * thm -> order
val cterm_cache: (cterm -> 'a) -> cterm -> 'a
val thm_cache: (thm -> 'a) -> thm -> 'a
@@ -179,6 +181,12 @@
val rhs_of = dest_equals_rhs o Thm.cprop_of;
+(* certified term order *)
+
+val fast_term_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of;
+val term_ord = Term_Ord.term_ord o apply2 Thm.term_of;
+
+
(* thm order: ignores theory context! *)
fun thm_ord ths =
@@ -198,7 +206,7 @@
(* tables and caches *)
-structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o apply2 Thm.term_of);
+structure Ctermtab = Table(type key = cterm val ord = fast_term_ord);
structure Thmtab = Table(type key = thm val ord = thm_ord);
fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f;