# HG changeset patch # User wenzelm # Date 1517494377 -3600 # Node ID 0fa87bd865661dea89b042fa9eb7e2a860298713 # Parent 833d154ab189e1d07f8cdbbc22cc1b9ba937804e tuned signature: more operations; diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Algebra/ringsimp.ML --- 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 = diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Analysis/normarith.ML --- 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 diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Library/Sum_of_Squares/sum_of_squares.ML --- 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))" diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Library/positivstellensatz.ML --- 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>$0::real) + 1$) diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Tools/ATP/atp_systems.ML --- 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 diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Tools/Nitpick/kodkod.ML --- 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 **) diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Tools/Nitpick/kodkod_sat.ML --- 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 diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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 diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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 diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- 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 = diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Tools/numeral_simprocs.ML --- 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]; diff -r 833d154ab189 -r 0fa87bd86566 src/HOL/Tools/semiring_normalizer.ML --- 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 *) diff -r 833d154ab189 -r 0fa87bd86566 src/Pure/library.ML --- 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 diff -r 833d154ab189 -r 0fa87bd86566 src/Tools/Argo/argo_heap.ML --- 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 diff -r 833d154ab189 -r 0fa87bd86566 src/Tools/Argo/argo_simplex.ML --- 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 *) diff -r 833d154ab189 -r 0fa87bd86566 src/Tools/float.ML --- 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;