--- a/src/HOL/Algebra/ringsimp.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Thu Feb 01 15:12:57 2018 +0100
@@ -47,7 +47,7 @@
val ops = map (fst o Term.strip_comb) ts;
fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
| ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
- fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS);
+ val less = is_less o Term_Ord.term_lpo ord;
in asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps simps |> Simplifier.set_termless less) end;
fun algebra_tac ctxt =
--- a/src/HOL/Analysis/normarith.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Analysis/normarith.ML Thu Feb 01 15:12:57 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 = Thm.term_ord (t, u) = LESS;
+ 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
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Thu Feb 01 15:12:57 2018 +0100
@@ -750,7 +750,7 @@
local
open Conv
val concl = Thm.dest_arg o Thm.cprop_of
- fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
+ 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 =
@@ -851,7 +851,7 @@
local
open Conv
- fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
+ 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))"
--- a/src/HOL/Library/positivstellensatz.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Library/positivstellensatz.ML Thu Feb 01 15:12:57 2018 +0100
@@ -764,7 +764,7 @@
fun gen_prover_real_arith ctxt prover =
let
- fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
+ 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>))
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 01 15:12:57 2018 +0100
@@ -514,8 +514,8 @@
(* Vampire 1.8 has TFF0 support, but the support was buggy until revision
1435 (or shortly before). *)
-fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
-fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
+fun is_vampire_at_least_1_8 () = is_greater_equal (string_ord (getenv "VAMPIRE_VERSION", "1.8"))
+fun is_vampire_beyond_1_8 () = is_greater (string_ord (getenv "VAMPIRE_VERSION", "1.8"))
val vampire_tff0 = TFF Monomorphic
--- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Feb 01 15:12:57 2018 +0100
@@ -326,7 +326,7 @@
|> map (the_default 0 o Int.fromString)
fun is_kodkodi_too_old () =
- dict_ord int_ord (kodkodi_version (), [1, 2, 14]) = LESS
+ is_less (dict_ord int_ord (kodkodi_version (), [1, 2, 14]))
(** Auxiliary functions on Kodkod problems **)
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Thu Feb 01 15:12:57 2018 +0100
@@ -80,7 +80,7 @@
| dynamic_entry_for_info incremental
(name, Internal (JNI from_version, mode, ss)) =
if (incremental andalso mode = Batch) orelse
- dict_ord int_ord (kodkodi_version (), from_version) = LESS then
+ is_less (dict_ord int_ord (kodkodi_version (), from_version)) then
NONE
else
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Feb 01 15:12:57 2018 +0100
@@ -337,12 +337,12 @@
end
fun normalize_eq (@{const Trueprop} $ (t as (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
- if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else t0 $ t2 $ t1
+ if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else t0 $ t2 $ t1
| normalize_eq (@{const Trueprop} $ (t as @{const Not}
$ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
- if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1)
+ if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else HOLogic.mk_not (t0 $ t2 $ t1)
| normalize_eq (Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2) =
- (if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1))
+ (if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then (t1, t2) else (t2, t1))
|> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2)
| normalize_eq t = t
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Feb 01 15:12:57 2018 +0100
@@ -420,7 +420,7 @@
(case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of
(0, 1) =>
one_line_proof_text ctxt 0
- (if play_outcome_ord (play_outcome, one_line_play) = LESS then
+ (if is_less (play_outcome_ord (play_outcome, one_line_play)) then
(case isar_proof of
Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu Feb 01 15:12:57 2018 +0100
@@ -199,7 +199,7 @@
fun pop_next_candidate [] = (NONE, [])
| pop_next_candidate (cands as (cand :: cands')) =
- fold (fn x => fn y => if cand_ord (x, y) = LESS then x else y) cands' cand
+ fold (fn x => fn y => if is_less (cand_ord (x, y)) then x else y) cands' cand
|> (fn best => (SOME best, remove (op =) best cands))
fun try_eliminate i l labels steps =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Feb 01 15:12:57 2018 +0100
@@ -208,18 +208,18 @@
let val i31 = i + i + i + 1 in
if i31 + 2 < l then
let val x = Unsynchronized.ref i31 in
- if cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)) = LESS then x := i31 + 1 else ();
- if cmp (Array.sub (a, !x), Array.sub (a, i31 + 2)) = LESS then x := i31 + 2 else ();
+ if is_less (cmp (Array.sub (a, i31), Array.sub (a, i31 + 1))) then x := i31 + 1 else ();
+ if is_less (cmp (Array.sub (a, !x), Array.sub (a, i31 + 2))) then x := i31 + 2 else ();
!x
end
else
- if i31 + 1 < l andalso cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)) = LESS
+ if i31 + 1 < l andalso is_less (cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)))
then i31 + 1 else if i31 < l then i31 else raise BOTTOM i
end
fun trickledown l i e =
let val j = maxson l i in
- if cmp (Array.sub (a, j), e) = GREATER then
+ if is_greater (cmp (Array.sub (a, j), e)) then
(Array.update (a, i, Array.sub (a, j)); trickledown l j e)
else
Array.update (a, i, e)
@@ -237,7 +237,7 @@
fun trickleup i e =
let val father = (i - 1) div 3 in
- if cmp (Array.sub (a, father), e) = LESS then
+ if is_less (cmp (Array.sub (a, father), e)) then
(Array.update (a, i, Array.sub (a, father));
if father > 0 then trickleup father e else Array.update (a, 0, e))
else
--- a/src/HOL/Tools/numeral_simprocs.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML Thu Feb 01 15:12:57 2018 +0100
@@ -162,11 +162,9 @@
and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
end;
-fun numtermless tu = (numterm_ord tu = LESS);
-
val num_ss =
simpset_of (put_simpset HOL_basic_ss @{context}
- |> Simplifier.set_termless numtermless);
+ |> Simplifier.set_termless (is_less o numterm_ord));
(*Maps 1 to Numeral1 so that arithmetic isn't complicated by the abstract 1.*)
val numeral_syms = [@{thm numeral_One} RS sym];
--- a/src/HOL/Tools/semiring_normalizer.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML Thu Feb 01 15:12:57 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 = Thm.term_ord (t, u) = LESS;
+fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u));
(* various normalizing conversions *)
--- a/src/Pure/library.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/Pure/library.ML Thu Feb 01 15:12:57 2018 +0100
@@ -184,6 +184,10 @@
(*orders*)
val is_equal: order -> bool
+ val is_less: order -> bool
+ val is_less_equal: order -> bool
+ val is_greater: order -> bool
+ val is_greater_equal: order -> bool
val rev_order: order -> order
val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
val bool_ord: bool * bool -> order
@@ -883,8 +887,11 @@
(** orders **)
-fun is_equal EQUAL = true
- | is_equal _ = false;
+fun is_equal ord = ord = EQUAL;
+fun is_less ord = ord = LESS;
+fun is_less_equal ord = ord = LESS orelse ord = EQUAL;
+fun is_greater ord = ord = GREATER;
+fun is_greater_equal ord = ord = GREATER orelse ord = EQUAL;
fun rev_order LESS = GREATER
| rev_order EQUAL = EQUAL
--- a/src/Tools/Argo/argo_heap.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/Tools/Argo/argo_heap.ML Thu Feb 01 15:12:57 2018 +0100
@@ -65,7 +65,7 @@
fun weight_of vals t = fst (value_of vals t)
-fun less_than vals t1 t2 = weight_ord (weight_of vals t1, weight_of vals t2) = LESS
+fun less_than vals t1 t2 = is_less (weight_ord (weight_of vals t1, weight_of vals t2))
fun rescale activity = activity div activity_rescale
@@ -163,7 +163,7 @@
*)
fun fix t (w, Some parent) (incr, vals) tree =
- if weight_ord (weight_of vals parent, w) = LESS then
+ if is_less (weight_ord (weight_of vals parent, w)) then
let val (tree1, tree2) = cut t (path_to vals parent []) tree
in mk_heap' incr (merge tree1 tree2 (root t vals)) end
else mk_heap incr vals tree
--- a/src/Tools/Argo/argo_simplex.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/Tools/Argo/argo_simplex.ML Thu Feb 01 15:12:57 2018 +0100
@@ -59,8 +59,8 @@
val erat_ord = prod_ord Rat.ord Rat.ord
-fun less_eq n1 n2 = (erat_ord (n1, n2) <> GREATER)
-fun less n1 n2 = (erat_ord (n1, n2) = LESS)
+fun less_eq n1 n2 = is_less_equal (erat_ord (n1, n2))
+fun less n1 n2 = is_less (erat_ord (n1, n2))
(* term functions *)
--- a/src/Tools/float.ML Thu Feb 01 13:55:10 2018 +0100
+++ b/src/Tools/float.ML Thu Feb 01 15:12:57 2018 +0100
@@ -48,7 +48,7 @@
fun ord (r, s) = sign (sub r s);
-fun eq (r, s) = ord (r, s) = EQUAL;
+val eq = is_equal o ord;
fun min r s = case ord (r, s) of LESS => r | _ => s;
fun max r s = case ord (r, s) of LESS => s | _ => r;