tuned signature: more operations;
authorwenzelm
Thu Feb 01 15:12:57 2018 +0100 (16 months ago)
changeset 675600fa87bd86566
parent 67559 833d154ab189
child 67561 f0b11413f1c9
tuned signature: more operations;
src/HOL/Algebra/ringsimp.ML
src/HOL/Analysis/normarith.ML
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/kodkod_sat.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/semiring_normalizer.ML
src/Pure/library.ML
src/Tools/Argo/argo_heap.ML
src/Tools/Argo/argo_simplex.ML
src/Tools/float.ML
     1.1 --- a/src/HOL/Algebra/ringsimp.ML	Thu Feb 01 13:55:10 2018 +0100
     1.2 +++ b/src/HOL/Algebra/ringsimp.ML	Thu Feb 01 15:12:57 2018 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4      val ops = map (fst o Term.strip_comb) ts;
     1.5      fun ord (Const (a, _)) = find_index (fn (Const (b, _)) => a=b | _ => false) ops
     1.6        | ord (Free (a, _)) = find_index (fn (Free (b, _)) => a=b | _ => false) ops;
     1.7 -    fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS);
     1.8 +    val less = is_less o Term_Ord.term_lpo ord;
     1.9    in asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps simps |> Simplifier.set_termless less) end;
    1.10  
    1.11  fun algebra_tac ctxt =
     2.1 --- a/src/HOL/Analysis/normarith.ML	Thu Feb 01 13:55:10 2018 +0100
     2.2 +++ b/src/HOL/Analysis/normarith.ML	Thu Feb 01 15:12:57 2018 +0100
     2.3 @@ -375,7 +375,7 @@
     2.4  local
     2.5   val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0}))
     2.6   fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
     2.7 - fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS;
     2.8 + fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u));
     2.9    (* FIXME: Lookup in the context every time!!! Fix this !!!*)
    2.10   fun splitequation ctxt th acc =
    2.11    let
     3.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Feb 01 13:55:10 2018 +0100
     3.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Thu Feb 01 15:12:57 2018 +0100
     3.3 @@ -750,7 +750,7 @@
     3.4  local
     3.5    open Conv
     3.6    val concl = Thm.dest_arg o Thm.cprop_of
     3.7 -  fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
     3.8 +  fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
     3.9  in
    3.10  (* FIXME: Replace tryfind by get_first !! *)
    3.11  fun real_nonlinear_prover proof_method ctxt =
    3.12 @@ -851,7 +851,7 @@
    3.13  
    3.14  local
    3.15    open Conv
    3.16 -  fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
    3.17 +  fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
    3.18    val concl = Thm.dest_arg o Thm.cprop_of
    3.19    val shuffle1 =
    3.20      fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))"
     4.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 13:55:10 2018 +0100
     4.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Feb 01 15:12:57 2018 +0100
     4.3 @@ -764,7 +764,7 @@
     4.4  
     4.5  fun gen_prover_real_arith ctxt prover =
     4.6    let
     4.7 -    fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS
     4.8 +    fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u))
     4.9      val {add, mul, neg, pow = _, sub = _, main} =
    4.10          Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
    4.11          (the (Semiring_Normalizer.match ctxt \<^cterm>\<open>(0::real) + 1\<close>))
     5.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 01 13:55:10 2018 +0100
     5.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 01 15:12:57 2018 +0100
     5.3 @@ -514,8 +514,8 @@
     5.4  
     5.5  (* Vampire 1.8 has TFF0 support, but the support was buggy until revision
     5.6     1435 (or shortly before). *)
     5.7 -fun is_vampire_at_least_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") <> LESS
     5.8 -fun is_vampire_beyond_1_8 () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER
     5.9 +fun is_vampire_at_least_1_8 () = is_greater_equal (string_ord (getenv "VAMPIRE_VERSION", "1.8"))
    5.10 +fun is_vampire_beyond_1_8 () = is_greater (string_ord (getenv "VAMPIRE_VERSION", "1.8"))
    5.11  
    5.12  val vampire_tff0 = TFF Monomorphic
    5.13  
     6.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Thu Feb 01 13:55:10 2018 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Thu Feb 01 15:12:57 2018 +0100
     6.3 @@ -326,7 +326,7 @@
     6.4    |> map (the_default 0 o Int.fromString)
     6.5  
     6.6  fun is_kodkodi_too_old () =
     6.7 -  dict_ord int_ord (kodkodi_version (), [1, 2, 14]) = LESS
     6.8 +  is_less (dict_ord int_ord (kodkodi_version (), [1, 2, 14]))
     6.9  
    6.10  (** Auxiliary functions on Kodkod problems **)
    6.11  
     7.1 --- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Feb 01 13:55:10 2018 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Thu Feb 01 15:12:57 2018 +0100
     7.3 @@ -80,7 +80,7 @@
     7.4    | dynamic_entry_for_info incremental
     7.5          (name, Internal (JNI from_version, mode, ss)) =
     7.6      if (incremental andalso mode = Batch) orelse
     7.7 -       dict_ord int_ord (kodkodi_version (), from_version) = LESS then
     7.8 +       is_less (dict_ord int_ord (kodkodi_version (), from_version)) then
     7.9        NONE
    7.10      else
    7.11        let
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Feb 01 13:55:10 2018 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Feb 01 15:12:57 2018 +0100
     8.3 @@ -337,12 +337,12 @@
     8.4    end
     8.5  
     8.6  fun normalize_eq (@{const Trueprop} $ (t as (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2)) =
     8.7 -    if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else t0 $ t2 $ t1
     8.8 +    if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else t0 $ t2 $ t1
     8.9    | normalize_eq (@{const Trueprop} $ (t as @{const Not}
    8.10        $ ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2))) =
    8.11 -    if Term_Ord.fast_term_ord (t1, t2) <> GREATER then t else HOLogic.mk_not (t0 $ t2 $ t1)
    8.12 +    if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then t else HOLogic.mk_not (t0 $ t2 $ t1)
    8.13    | normalize_eq (Const (@{const_name Pure.eq}, Type (_, [T, _])) $ t1 $ t2) =
    8.14 -    (if Term_Ord.fast_term_ord (t1, t2) <> GREATER then (t1, t2) else (t2, t1))
    8.15 +    (if is_less_equal (Term_Ord.fast_term_ord (t1, t2)) then (t1, t2) else (t2, t1))
    8.16      |> (fn (t1, t2) => HOLogic.eq_const T $ t1 $ t2)
    8.17    | normalize_eq t = t
    8.18  
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Feb 01 13:55:10 2018 +0100
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Feb 01 15:12:57 2018 +0100
     9.3 @@ -420,7 +420,7 @@
     9.4              (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of
     9.5                (0, 1) =>
     9.6                one_line_proof_text ctxt 0
     9.7 -                (if play_outcome_ord (play_outcome, one_line_play) = LESS then
     9.8 +                (if is_less (play_outcome_ord (play_outcome, one_line_play)) then
     9.9                     (case isar_proof of
    9.10                       Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
    9.11                       let
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Thu Feb 01 13:55:10 2018 +0100
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Thu Feb 01 15:12:57 2018 +0100
    10.3 @@ -199,7 +199,7 @@
    10.4  
    10.5            fun pop_next_candidate [] = (NONE, [])
    10.6              | pop_next_candidate (cands as (cand :: cands')) =
    10.7 -              fold (fn x => fn y => if cand_ord (x, y) = LESS then x else y) cands' cand
    10.8 +              fold (fn x => fn y => if is_less (cand_ord (x, y)) then x else y) cands' cand
    10.9                |> (fn best => (SOME best, remove (op =) best cands))
   10.10  
   10.11            fun try_eliminate i l labels steps =
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 01 13:55:10 2018 +0100
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 01 15:12:57 2018 +0100
    11.3 @@ -208,18 +208,18 @@
    11.4        let val i31 = i + i + i + 1 in
    11.5          if i31 + 2 < l then
    11.6            let val x = Unsynchronized.ref i31 in
    11.7 -            if cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)) = LESS then x := i31 + 1 else ();
    11.8 -            if cmp (Array.sub (a, !x), Array.sub (a, i31 + 2)) = LESS then x := i31 + 2 else ();
    11.9 +            if is_less (cmp (Array.sub (a, i31), Array.sub (a, i31 + 1))) then x := i31 + 1 else ();
   11.10 +            if is_less (cmp (Array.sub (a, !x), Array.sub (a, i31 + 2))) then x := i31 + 2 else ();
   11.11              !x
   11.12            end
   11.13          else
   11.14 -          if i31 + 1 < l andalso cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)) = LESS
   11.15 +          if i31 + 1 < l andalso is_less (cmp (Array.sub (a, i31), Array.sub (a, i31 + 1)))
   11.16            then i31 + 1 else if i31 < l then i31 else raise BOTTOM i
   11.17        end
   11.18  
   11.19      fun trickledown l i e =
   11.20        let val j = maxson l i in
   11.21 -        if cmp (Array.sub (a, j), e) = GREATER then
   11.22 +        if is_greater (cmp (Array.sub (a, j), e)) then
   11.23            (Array.update (a, i, Array.sub (a, j)); trickledown l j e)
   11.24          else
   11.25            Array.update (a, i, e)
   11.26 @@ -237,7 +237,7 @@
   11.27  
   11.28      fun trickleup i e =
   11.29        let val father = (i - 1) div 3 in
   11.30 -        if cmp (Array.sub (a, father), e) = LESS then
   11.31 +        if is_less (cmp (Array.sub (a, father), e)) then
   11.32            (Array.update (a, i, Array.sub (a, father));
   11.33             if father > 0 then trickleup father e else Array.update (a, 0, e))
   11.34          else
    12.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Thu Feb 01 13:55:10 2018 +0100
    12.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Feb 01 15:12:57 2018 +0100
    12.3 @@ -162,11 +162,9 @@
    12.4  and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
    12.5  end;
    12.6  
    12.7 -fun numtermless tu = (numterm_ord tu = LESS);
    12.8 -
    12.9  val num_ss =
   12.10    simpset_of (put_simpset HOL_basic_ss @{context}
   12.11 -    |> Simplifier.set_termless numtermless);
   12.12 +    |> Simplifier.set_termless (is_less o numterm_ord));
   12.13  
   12.14  (*Maps 1 to Numeral1 so that arithmetic isn't complicated by the abstract 1.*)
   12.15  val numeral_syms = [@{thm numeral_One} RS sym];
    13.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Thu Feb 01 13:55:10 2018 +0100
    13.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Thu Feb 01 15:12:57 2018 +0100
    13.3 @@ -851,7 +851,7 @@
    13.4      addsimps (@{thms eval_nat_numeral} @ @{thms diff_nat_numeral} @ @{thms arith_simps} @ @{thms rel_simps})
    13.5      addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]);
    13.6  
    13.7 -fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS;
    13.8 +fun simple_cterm_ord t u = is_less (Thm.term_ord (t, u));
    13.9  
   13.10  
   13.11  (* various normalizing conversions *)
    14.1 --- a/src/Pure/library.ML	Thu Feb 01 13:55:10 2018 +0100
    14.2 +++ b/src/Pure/library.ML	Thu Feb 01 15:12:57 2018 +0100
    14.3 @@ -184,6 +184,10 @@
    14.4  
    14.5    (*orders*)
    14.6    val is_equal: order -> bool
    14.7 +  val is_less: order -> bool
    14.8 +  val is_less_equal: order -> bool
    14.9 +  val is_greater: order -> bool
   14.10 +  val is_greater_equal: order -> bool
   14.11    val rev_order: order -> order
   14.12    val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
   14.13    val bool_ord: bool * bool -> order
   14.14 @@ -883,8 +887,11 @@
   14.15  
   14.16  (** orders **)
   14.17  
   14.18 -fun is_equal EQUAL = true
   14.19 -  | is_equal _ = false;
   14.20 +fun is_equal ord = ord = EQUAL;
   14.21 +fun is_less ord = ord = LESS;
   14.22 +fun is_less_equal ord = ord = LESS orelse ord = EQUAL;
   14.23 +fun is_greater ord = ord = GREATER;
   14.24 +fun is_greater_equal ord = ord = GREATER orelse ord = EQUAL;
   14.25  
   14.26  fun rev_order LESS = GREATER
   14.27    | rev_order EQUAL = EQUAL
    15.1 --- a/src/Tools/Argo/argo_heap.ML	Thu Feb 01 13:55:10 2018 +0100
    15.2 +++ b/src/Tools/Argo/argo_heap.ML	Thu Feb 01 15:12:57 2018 +0100
    15.3 @@ -65,7 +65,7 @@
    15.4  
    15.5  fun weight_of vals t = fst (value_of vals t)
    15.6  
    15.7 -fun less_than vals t1 t2 = weight_ord (weight_of vals t1, weight_of vals t2) = LESS
    15.8 +fun less_than vals t1 t2 = is_less (weight_ord (weight_of vals t1, weight_of vals t2))
    15.9  
   15.10  fun rescale activity = activity div activity_rescale
   15.11  
   15.12 @@ -163,7 +163,7 @@
   15.13  *)
   15.14  
   15.15  fun fix t (w, Some parent) (incr, vals) tree =
   15.16 -      if weight_ord (weight_of vals parent, w) = LESS then
   15.17 +      if is_less (weight_ord (weight_of vals parent, w)) then
   15.18          let val (tree1, tree2) = cut t (path_to vals parent []) tree
   15.19          in mk_heap' incr (merge tree1 tree2 (root t vals)) end
   15.20        else mk_heap incr vals tree
    16.1 --- a/src/Tools/Argo/argo_simplex.ML	Thu Feb 01 13:55:10 2018 +0100
    16.2 +++ b/src/Tools/Argo/argo_simplex.ML	Thu Feb 01 15:12:57 2018 +0100
    16.3 @@ -59,8 +59,8 @@
    16.4  
    16.5  val erat_ord = prod_ord Rat.ord Rat.ord
    16.6  
    16.7 -fun less_eq n1 n2 = (erat_ord (n1, n2) <> GREATER)
    16.8 -fun less n1 n2 = (erat_ord (n1, n2) = LESS)
    16.9 +fun less_eq n1 n2 = is_less_equal (erat_ord (n1, n2))
   16.10 +fun less n1 n2 = is_less (erat_ord (n1, n2))
   16.11  
   16.12  
   16.13  (* term functions *)
    17.1 --- a/src/Tools/float.ML	Thu Feb 01 13:55:10 2018 +0100
    17.2 +++ b/src/Tools/float.ML	Thu Feb 01 15:12:57 2018 +0100
    17.3 @@ -48,7 +48,7 @@
    17.4  
    17.5  fun ord (r, s) = sign (sub r s);
    17.6  
    17.7 -fun eq (r, s) = ord (r, s) = EQUAL;
    17.8 +val eq = is_equal o ord;
    17.9  
   17.10  fun min r s = case ord (r, s) of LESS => r | _ => s;
   17.11  fun max r s = case ord (r, s) of LESS => s | _ => r;