# HG changeset patch # User wenzelm # Date 1267308781 -3600 # Node ID b48ab741683b129bdf8932147ffce0eb5232e4fb # Parent 980d4194a212a9ee50b5894a0fee88a4ccf5cd63 modernized structure Term_Ord; diff -r 980d4194a212 -r b48ab741683b doc-src/IsarImplementation/Thy/Prelim.thy --- a/doc-src/IsarImplementation/Thy/Prelim.thy Sat Feb 27 22:52:25 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy Sat Feb 27 23:13:01 2010 +0100 @@ -436,14 +436,14 @@ val empty = []; val extend = I; fun merge (ts1, ts2) = - OrdList.union TermOrd.fast_term_ord ts1 ts2; + OrdList.union Term_Ord.fast_term_ord ts1 ts2; ) val get = Terms.get; fun add raw_t thy = let val t = Sign.cert_term thy raw_t - in Terms.map (OrdList.insert TermOrd.fast_term_ord t) thy end; + in Terms.map (OrdList.insert Term_Ord.fast_term_ord t) thy end; end; *} diff -r 980d4194a212 -r b48ab741683b src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Algebra/abstract/Ring2.thy Sat Feb 27 23:13:01 2010 +0100 @@ -207,7 +207,7 @@ @{const_name Groups.minus}, @{const_name Groups.one}, @{const_name Groups.times}] | ring_ord _ = ~1; -fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS); +fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS); val ring_ss = HOL_basic_ss settermless termless_ring addsimps [thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc", diff -r 980d4194a212 -r b48ab741683b src/HOL/Algebra/ringsimp.ML --- a/src/HOL/Algebra/ringsimp.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Algebra/ringsimp.ML Sat Feb 27 23:13:01 2010 +0100 @@ -46,7 +46,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) = (TermOrd.term_lpo ord (a, b) = LESS); + fun less (a, b) = (Term_Ord.term_lpo ord (a, b) = LESS); in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end; fun algebra_tac ctxt = diff -r 980d4194a212 -r b48ab741683b src/HOL/Groups.thy --- a/src/HOL/Groups.thy Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Groups.thy Sat Feb 27 23:13:01 2010 +0100 @@ -1216,7 +1216,7 @@ @{const_name Groups.uminus}, @{const_name Groups.minus}] | agrp_ord _ = ~1; -fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS); +fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS); local val ac1 = mk_meta_eq @{thm add_assoc}; diff -r 980d4194a212 -r b48ab741683b src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Import/shuffler.ML Sat Feb 27 23:13:01 2010 +0100 @@ -351,7 +351,7 @@ fun equals_fun thy assume t = case t of - Const("op ==",_) $ u $ v => if TermOrd.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE + Const("op ==",_) $ u $ v => if Term_Ord.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE | _ => NONE fun eta_expand thy assumes origt = diff -r 980d4194a212 -r b48ab741683b src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sat Feb 27 23:13:01 2010 +0100 @@ -1189,7 +1189,7 @@ local open Conv val concl = Thm.dest_arg o cprop_of - fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS + fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS in (* FIXME: Replace tryfind by get_first !! *) fun real_nonlinear_prover proof_method ctxt = @@ -1279,7 +1279,7 @@ local open Conv - fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS + fun simple_cterm_ord t u = Term_Ord.fast_term_ord (term_of t, term_of u) = LESS val concl = Thm.dest_arg o cprop_of val shuffle1 = fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" by (atomize (full)) (simp add: ring_simps) }) diff -r 980d4194a212 -r b48ab741683b src/HOL/Library/normarith.ML --- a/src/HOL/Library/normarith.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Library/normarith.ML Sat Feb 27 23:13:01 2010 +0100 @@ -216,7 +216,7 @@ let val l = headvector lt val r = headvector rt - in (case TermOrd.fast_term_ord (l,r) of + in (case Term_Ord.fast_term_ord (l,r) of LESS => (apply_pthb then_conv arg_conv vector_add_conv then_conv apply_pthd) ct | GREATER => (apply_pthc then_conv arg_conv vector_add_conv @@ -378,7 +378,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 = TermOrd.term_ord (term_of t, term_of u) = LESS; + fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; (* FIXME: Lookup in the context every time!!! Fix this !!!*) fun splitequation ctxt th acc = let diff -r 980d4194a212 -r b48ab741683b src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Library/positivstellensatz.ML Sat Feb 27 23:13:01 2010 +0100 @@ -61,9 +61,9 @@ structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord); 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 = TermOrd.fast_term_ord); +structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord); -val cterm_ord = TermOrd.fast_term_ord o pairself term_of +val cterm_ord = Term_Ord.fast_term_ord o pairself term_of structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord); @@ -745,7 +745,7 @@ fun gen_prover_real_arith ctxt prover = let - fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS + fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) diff -r 980d4194a212 -r b48ab741683b src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Mutabelle/mutabelle.ML Sat Feb 27 23:13:01 2010 +0100 @@ -361,7 +361,7 @@ val t' = canonize_term t comms; val u' = canonize_term u comms; in - if s mem comms andalso TermOrd.termless (u', t') + if s mem comms andalso Term_Ord.termless (u', t') then Const (s, T) $ u' $ t' else Const (s, T) $ t' $ u' end diff -r 980d4194a212 -r b48ab741683b src/HOL/SMT/Tools/smt_translate.ML --- a/src/HOL/SMT/Tools/smt_translate.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/SMT/Tools/smt_translate.ML Sat Feb 27 23:13:01 2010 +0100 @@ -253,9 +253,9 @@ | atoms_ord (SNum (i, _), SNum (j, _)) = int_ord (i, j) | atoms_ord _ = sys_error "atoms_ord" - fun types_ord (SConst (_, T), SConst (_, U)) = TermOrd.typ_ord (T, U) - | types_ord (SFree (_, T), SFree (_, U)) = TermOrd.typ_ord (T, U) - | types_ord (SNum (_, T), SNum (_, U)) = TermOrd.typ_ord (T, U) + fun types_ord (SConst (_, T), SConst (_, U)) = Term_Ord.typ_ord (T, U) + | types_ord (SFree (_, T), SFree (_, U)) = Term_Ord.typ_ord (T, U) + | types_ord (SNum (_, T), SNum (_, U)) = Term_Ord.typ_ord (T, U) | types_ord _ = sys_error "types_ord" fun fast_sym_ord tu = diff -r 980d4194a212 -r b48ab741683b src/HOL/Statespace/DistinctTreeProver.thy --- a/src/HOL/Statespace/DistinctTreeProver.thy Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Statespace/DistinctTreeProver.thy Sat Feb 27 23:13:01 2010 +0100 @@ -645,9 +645,9 @@ val const_decls = map (fn i => Syntax.no_syn ("const" ^ string_of_int i,Type ("nat",[]))) nums -val consts = sort TermOrd.fast_term_ord +val consts = sort Term_Ord.fast_term_ord (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums) -val consts' = sort TermOrd.fast_term_ord +val consts' = sort Term_Ord.fast_term_ord (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums') val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts diff -r 980d4194a212 -r b48ab741683b src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Sat Feb 27 23:13:01 2010 +0100 @@ -79,7 +79,7 @@ | bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t]) fun find_tree e t = - (case bin_find_tree TermOrd.fast_term_ord e t of + (case bin_find_tree Term_Ord.fast_term_ord e t of NONE => lin_find_tree e t | x => x); diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/Function/termination.ML Sat Feb 27 23:13:01 2010 +0100 @@ -51,9 +51,10 @@ open Function_Lib -val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord +val term2_ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord structure Term2tab = Table(type key = term * term val ord = term2_ord); -structure Term3tab = Table(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord); +structure Term3tab = + Table(type key = term * (term * term) val ord = prod_ord Term_Ord.fast_term_ord term2_ord); (** Analyzing binary trees **) diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Sat Feb 27 23:13:01 2010 +0100 @@ -689,7 +689,7 @@ val cjs = conjs tm val rawvars = fold_rev (fn eq => fn a => grobvars (dest_arg1 eq) (grobvars (dest_arg eq) a)) cjs [] - val vars = sort (fn (x, y) => TermOrd.term_ord(term_of x,term_of y)) + val vars = sort (fn (x, y) => Term_Ord.term_ord(term_of x,term_of y)) (distinct (op aconvc) rawvars) in (vars,map (grobify_equation vars) cjs) end; @@ -898,7 +898,7 @@ 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) => TermOrd.term_ord (term_of s, term_of t)) + (fn (s,t) => Term_Ord.term_ord (term_of s, term_of t)) in (eq, take (length qs) rs ~~ vars) end; fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p)); diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/Groebner_Basis/normalizer.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Sat Feb 27 23:13:01 2010 +0100 @@ -636,7 +636,7 @@ val nat_exp_ss = HOL_basic_ss addsimps (@{thms nat_number} @ nat_arith @ @{thms arith_simps} @ @{thms rel_simps}) addsimps [Let_def, if_False, if_True, @{thm Nat.add_0}, @{thm add_Suc}]; -fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS; +fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Feb 27 23:13:01 2010 +0100 @@ -359,7 +359,7 @@ not standard orelse T = nat_T orelse is_word_type T orelse exists (curry (op =) T o domain_type o type_of) sel_names val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) - |> sort TermOrd.typ_ord + |> sort Term_Ord.typ_ord val _ = if verbose andalso binary_ints = SOME true andalso exists (member (op =) [nat_T, int_T]) all_Ts then print_v (K "The option \"binary_ints\" will be ignored because \ diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Feb 27 23:13:01 2010 +0100 @@ -1122,7 +1122,7 @@ (* term list -> (indexname * typ) list *) fun special_bounds ts = - fold Term.add_vars ts [] |> sort (TermOrd.fast_indexname_ord o pairself fst) + fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst) (* indexname * typ -> term -> term *) fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Feb 27 23:13:01 2010 +0100 @@ -103,7 +103,7 @@ (case nice_term_ord (t11, t21) of EQUAL => nice_term_ord (t12, t22) | ord => ord) - | _ => TermOrd.fast_term_ord tp + | _ => Term_Ord.fast_term_ord tp (* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *) fun tuple_list_for_name rel_table bounds name = diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Sat Feb 27 23:13:01 2010 +0100 @@ -400,13 +400,13 @@ | name_ord (_, BoundName _) = GREATER | name_ord (FreeName (s1, T1, _), FreeName (s2, T2, _)) = (case fast_string_ord (s1, s2) of - EQUAL => TermOrd.typ_ord (T1, T2) + EQUAL => Term_Ord.typ_ord (T1, T2) | ord => ord) | name_ord (FreeName _, _) = LESS | name_ord (_, FreeName _) = GREATER | name_ord (ConstName (s1, T1, _), ConstName (s2, T2, _)) = (case fast_string_ord (s1, s2) of - EQUAL => TermOrd.typ_ord (T1, T2) + EQUAL => Term_Ord.typ_ord (T1, T2) | ord => ord) | name_ord (u1, u2) = raise NUT ("Nitpick_Nut.name_ord", [u1, u2]) diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Feb 27 23:13:01 2010 +0100 @@ -247,7 +247,7 @@ let val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2) val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) - val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last + val T = [T1, T2] |> sort Term_Ord.typ_ord |> List.last in list_comb (Const (s0, T --> T --> body_type T0), map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2]) @@ -815,7 +815,7 @@ | call_sets [] uss vs = vs :: call_sets uss [] [] | call_sets ([] :: _) _ _ = [] | call_sets ((t :: ts) :: tss) uss vs = - OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss) + OrdList.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss) val sets = call_sets (fun_calls t [] []) [] [] val indexed_sets = sets ~~ (index_seq 0 (length sets)) in @@ -830,7 +830,7 @@ (* hol_context -> styp -> term list -> (int * term option) list *) fun static_args_in_terms hol_ctxt x = map (static_args_in_term hol_ctxt x) - #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord))) + #> fold1 (OrdList.inter (prod_ord int_ord (option_ord Term_Ord.term_ord))) (* (int * term option) list -> (int * term) list -> int list *) fun overlapping_indices [] _ = [] @@ -882,7 +882,7 @@ val _ = not (null fixed_js) orelse raise SAME () val fixed_args = filter_indices fixed_js args val vars = fold Term.add_vars fixed_args [] - |> sort (TermOrd.fast_indexname_ord o pairself fst) + |> sort (Term_Ord.fast_indexname_ord o pairself fst) val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js)) fixed_args [] |> sort int_ord @@ -972,7 +972,7 @@ fun generality (js, _, _) = ~(length js) (* special_triple -> special_triple -> bool *) fun is_more_specific (j1, t1, x1) (j2, t2, x2) = - x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord) + x1 <> x2 andalso OrdList.subset (prod_ord int_ord Term_Ord.term_ord) (j2 ~~ t2, j1 ~~ t1) (* typ -> special_triple list -> special_triple list -> special_triple list -> term list -> term list *) diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/Qelim/langford.ML --- a/src/HOL/Tools/Qelim/langford.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/Qelim/langford.ML Sat Feb 27 23:13:01 2010 +0100 @@ -210,7 +210,7 @@ let fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) - val ts = sort (fn (a,b) => TermOrd.fast_term_ord (term_of a, term_of b)) (f p) + val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p) val p' = fold_rev gen ts p in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end)); diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/Qelim/presburger.ML --- a/src/HOL/Tools/Qelim/presburger.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/Qelim/presburger.ML Sat Feb 27 23:13:01 2010 +0100 @@ -103,7 +103,7 @@ let fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) - val ts = sort (fn (a,b) => TermOrd.fast_term_ord (term_of a, term_of b)) (f p) + val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p) val p' = fold_rev gen ts p in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end)); diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/nat_numeral_simprocs.ML --- a/src/HOL/Tools/nat_numeral_simprocs.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sat Feb 27 23:13:01 2010 +0100 @@ -80,7 +80,7 @@ (*Express t as a product of (possibly) a numeral with other factors, sorted*) fun dest_coeff t = - let val ts = sort TermOrd.term_ord (dest_prod t) + let val ts = sort Term_Ord.term_ord (dest_prod t) val (n, _, ts') = find_first_numeral [] ts handle TERM _ => (1, one, ts) in (n, mk_prod ts') end; diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/numeral_simprocs.ML --- a/src/HOL/Tools/numeral_simprocs.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/numeral_simprocs.ML Sat Feb 27 23:13:01 2010 +0100 @@ -74,7 +74,7 @@ (*Express t as a product of (possibly) a numeral with other sorted terms*) fun dest_coeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_coeff (~sign) t | dest_coeff sign t = - let val ts = sort TermOrd.term_ord (dest_prod t) + let val ts = sort Term_Ord.term_ord (dest_prod t) val (n, ts') = find_first_numeral [] ts handle TERM _ => (1, ts) in (sign*n, mk_prod (Term.fastype_of t) ts') end; @@ -124,12 +124,12 @@ EQUAL => int_ord (Int.sign i, Int.sign j) | ord => ord); -(*This resembles TermOrd.term_ord, but it puts binary numerals before other +(*This resembles Term_Ord.term_ord, but it puts binary numerals before other non-atomic terms.*) local open Term in fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) = - (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord) + (case numterm_ord (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord) | numterm_ord (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) = num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w) @@ -139,7 +139,7 @@ (case int_ord (size_of_term t, size_of_term u) of EQUAL => let val (f, ts) = strip_comb t and (g, us) = strip_comb u in - (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord) + (case Term_Ord.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord) end | ord => ord) and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/record.ML Sat Feb 27 23:13:01 2010 +0100 @@ -1100,7 +1100,7 @@ fun get_accupd_simps thy term defset = let val (acc, [body]) = strip_comb term; - val upd_funs = sort_distinct TermOrd.fast_term_ord (get_upd_funs body); + val upd_funs = sort_distinct Term_Ord.fast_term_ord (get_upd_funs body); fun get_simp upd = let (* FIXME fresh "f" (!?) *) diff -r 980d4194a212 -r b48ab741683b src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/HOL/Tools/sat_funcs.ML Sat Feb 27 23:13:01 2010 +0100 @@ -320,7 +320,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 (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses + val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses val _ = if !trace_sat then tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) diff -r 980d4194a212 -r b48ab741683b src/Provers/Arith/cancel_factor.ML --- a/src/Provers/Arith/cancel_factor.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Provers/Arith/cancel_factor.ML Sat Feb 27 23:13:01 2010 +0100 @@ -35,7 +35,7 @@ if t aconv u then (u, k + 1) :: uks else (t, 1) :: (u, k) :: uks; -fun count_terms ts = foldr ins_term (sort TermOrd.term_ord ts, []); +fun count_terms ts = foldr ins_term (sort Term_Ord.term_ord ts, []); (* divide sum *) diff -r 980d4194a212 -r b48ab741683b src/Provers/Arith/cancel_sums.ML --- a/src/Provers/Arith/cancel_sums.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Provers/Arith/cancel_sums.ML Sat Feb 27 23:13:01 2010 +0100 @@ -37,11 +37,11 @@ fun cons2 y (x, ys, z) = (x, y :: ys, z); fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z); -(*symmetric difference of multisets -- assumed to be sorted wrt. TermOrd.term_ord*) +(*symmetric difference of multisets -- assumed to be sorted wrt. Term_Ord.term_ord*) fun cancel ts [] vs = (ts, [], vs) | cancel [] us vs = ([], us, vs) | cancel (t :: ts) (u :: us) vs = - (case TermOrd.term_ord (t, u) of + (case Term_Ord.term_ord (t, u) of EQUAL => cancel ts us (t :: vs) | LESS => cons1 t (cancel ts (u :: us) vs) | GREATER => cons2 u (cancel (t :: ts) us vs)); @@ -63,7 +63,7 @@ | SOME bal => let val thy = ProofContext.theory_of (Simplifier.the_context ss); - val (ts, us) = pairself (sort TermOrd.term_ord o Data.dest_sum) bal; + val (ts, us) = pairself (sort Term_Ord.term_ord o Data.dest_sum) bal; val (ts', us', vs) = cancel ts us []; in if null vs then NONE diff -r 980d4194a212 -r b48ab741683b src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/Isar/rule_cases.ML Sat Feb 27 23:13:01 2010 +0100 @@ -379,7 +379,7 @@ local fun equal_cterms ts us = - is_equal (list_ord (TermOrd.fast_term_ord o pairself Thm.term_of) (ts, us)); + is_equal (list_ord (Term_Ord.fast_term_ord o pairself Thm.term_of) (ts, us)); fun prep_rule n th = let diff -r 980d4194a212 -r b48ab741683b src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/Tools/find_theorems.ML Sat Feb 27 23:13:01 2010 +0100 @@ -364,7 +364,7 @@ fun rem_thm_dups nicer xs = xs ~~ (1 upto length xs) - |> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1)) + |> sort (Term_Ord.fast_term_ord o pairself (Thm.prop_of o #2 o #1)) |> rem_cdups nicer |> sort (int_ord o pairself #2) |> map #1; diff -r 980d4194a212 -r b48ab741683b src/Pure/envir.ML --- a/src/Pure/envir.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/envir.ML Sat Feb 27 23:13:01 2010 +0100 @@ -139,7 +139,7 @@ (case t of Var (nT as (name', T)) => if a = name' then env (*cycle!*) - else if TermOrd.indexname_ord (a, name') = LESS then + else if Term_Ord.indexname_ord (a, name') = LESS then (case lookup (env, nT) of (*if already assigned, chase*) NONE => update ((nT, Var (a, T)), env) | SOME u => vupdate ((aU, u), env)) diff -r 980d4194a212 -r b48ab741683b src/Pure/facts.ML --- a/src/Pure/facts.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/facts.ML Sat Feb 27 23:13:01 2010 +0100 @@ -171,7 +171,7 @@ (* indexed props *) -val prop_ord = TermOrd.term_ord o pairself Thm.full_prop_of; +val prop_ord = Term_Ord.term_ord o pairself Thm.full_prop_of; fun props (Facts {props, ...}) = sort_distinct prop_ord (Net.content props); fun could_unify (Facts {props, ...}) = Net.unify_term props; diff -r 980d4194a212 -r b48ab741683b src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/meta_simplifier.ML Sat Feb 27 23:13:01 2010 +0100 @@ -755,7 +755,7 @@ mk_eq_True = K NONE, reorient = default_reorient}; -val empty_ss = init_ss basic_mk_rews TermOrd.termless (K (K no_tac)) ([], []); +val empty_ss = init_ss basic_mk_rews Term_Ord.termless (K (K no_tac)) ([], []); (* merge *) (*NOTE: ignores some fields of 2nd simpset*) diff -r 980d4194a212 -r b48ab741683b src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/more_thm.ML Sat Feb 27 23:13:01 2010 +0100 @@ -151,12 +151,12 @@ val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1; val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2; in - (case TermOrd.fast_term_ord (prop1, prop2) of + (case Term_Ord.fast_term_ord (prop1, prop2) of EQUAL => - (case list_ord (prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord) (tpairs1, tpairs2) of + (case list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) (tpairs1, tpairs2) of EQUAL => - (case list_ord TermOrd.fast_term_ord (hyps1, hyps2) of - EQUAL => list_ord TermOrd.sort_ord (shyps1, shyps2) + (case list_ord Term_Ord.fast_term_ord (hyps1, hyps2) of + EQUAL => list_ord Term_Ord.sort_ord (shyps1, shyps2) | ord => ord) | ord => ord) | ord => ord) @@ -165,7 +165,7 @@ (* tables and caches *) -structure Ctermtab = Table(type key = cterm val ord = TermOrd.fast_term_ord o pairself Thm.term_of); +structure Ctermtab = Table(type key = cterm val ord = Term_Ord.fast_term_ord o pairself Thm.term_of); structure Thmtab = Table(type key = thm val ord = thm_ord); fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f; diff -r 980d4194a212 -r b48ab741683b src/Pure/old_term.ML --- a/src/Pure/old_term.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/old_term.ML Sat Feb 27 23:13:01 2010 +0100 @@ -75,7 +75,7 @@ (*Accumulates the Vars in the term, suppressing duplicates.*) fun add_term_vars (t, vars: term list) = case t of - Var _ => OrdList.insert TermOrd.term_ord t vars + Var _ => OrdList.insert Term_Ord.term_ord t vars | Abs (_,_,body) => add_term_vars(body,vars) | f$t => add_term_vars (f, add_term_vars(t, vars)) | _ => vars; @@ -84,7 +84,7 @@ (*Accumulates the Frees in the term, suppressing duplicates.*) fun add_term_frees (t, frees: term list) = case t of - Free _ => OrdList.insert TermOrd.term_ord t frees + Free _ => OrdList.insert Term_Ord.term_ord t frees | Abs (_,_,body) => add_term_frees(body,frees) | f$t => add_term_frees (f, add_term_frees(t, frees)) | _ => frees; diff -r 980d4194a212 -r b48ab741683b src/Pure/pattern.ML --- a/src/Pure/pattern.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/pattern.ML Sat Feb 27 23:13:01 2010 +0100 @@ -226,7 +226,7 @@ fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks)); in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env')) end; - in if TermOrd.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end + in if Term_Ord.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) = if T = U then env diff -r 980d4194a212 -r b48ab741683b src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/proofterm.ML Sat Feb 27 23:13:01 2010 +0100 @@ -214,7 +214,7 @@ (* proof body *) -val oracle_ord = prod_ord fast_string_ord TermOrd.fast_term_ord; +val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord; fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i); val merge_oracles = OrdList.union oracle_ord; diff -r 980d4194a212 -r b48ab741683b src/Pure/search.ML --- a/src/Pure/search.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/search.ML Sat Feb 27 23:13:01 2010 +0100 @@ -197,7 +197,7 @@ structure Thm_Heap = Heap ( type elem = int * thm; - val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of); + val ord = prod_ord int_ord (Term_Ord.term_ord o pairself Thm.prop_of); ); val trace_BEST_FIRST = Unsynchronized.ref false; diff -r 980d4194a212 -r b48ab741683b src/Pure/sorts.ML --- a/src/Pure/sorts.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/sorts.ML Sat Feb 27 23:13:01 2010 +0100 @@ -71,13 +71,13 @@ (** ordered lists of sorts **) -val make = OrdList.make TermOrd.sort_ord; -val subset = OrdList.subset TermOrd.sort_ord; -val union = OrdList.union TermOrd.sort_ord; -val subtract = OrdList.subtract TermOrd.sort_ord; +val make = OrdList.make Term_Ord.sort_ord; +val subset = OrdList.subset Term_Ord.sort_ord; +val union = OrdList.union Term_Ord.sort_ord; +val subtract = OrdList.subtract Term_Ord.sort_ord; -val remove_sort = OrdList.remove TermOrd.sort_ord; -val insert_sort = OrdList.insert TermOrd.sort_ord; +val remove_sort = OrdList.remove Term_Ord.sort_ord; +val insert_sort = OrdList.insert Term_Ord.sort_ord; fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss | insert_typ (TVar (_, S)) Ss = insert_sort S Ss diff -r 980d4194a212 -r b48ab741683b src/Pure/term_ord.ML --- a/src/Pure/term_ord.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/term_ord.ML Sat Feb 27 23:13:01 2010 +0100 @@ -29,7 +29,7 @@ val term_cache: (term -> 'a) -> term -> 'a end; -structure TermOrd: TERM_ORD = +structure Term_Ord: TERM_ORD = struct (* fast syntactic ordering -- tuned for inequalities *) @@ -223,11 +223,11 @@ end; -structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd; +structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord; open Basic_Term_Ord; -structure Var_Graph = Graph(type key = indexname val ord = TermOrd.fast_indexname_ord); -structure Sort_Graph = Graph(type key = sort val ord = TermOrd.sort_ord); -structure Typ_Graph = Graph(type key = typ val ord = TermOrd.typ_ord); -structure Term_Graph = Graph(type key = term val ord = TermOrd.fast_term_ord); +structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord); +structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord); +structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord); +structure Term_Graph = Graph(type key = term val ord = Term_Ord.fast_term_ord); diff -r 980d4194a212 -r b48ab741683b src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/term_subst.ML Sat Feb 27 23:13:01 2010 +0100 @@ -198,9 +198,9 @@ fun zero_var_indexes_inst ts = let - val tvars = sort TermOrd.tvar_ord (fold Term.add_tvars ts []); + val tvars = sort Term_Ord.tvar_ord (fold Term.add_tvars ts []); val instT = map (apsnd TVar) (zero_var_inst tvars); - val vars = sort TermOrd.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts [])); + val vars = sort Term_Ord.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts [])); val inst = map (apsnd Var) (zero_var_inst vars); in (instT, inst) end; diff -r 980d4194a212 -r b48ab741683b src/Pure/thm.ML --- a/src/Pure/thm.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/thm.ML Sat Feb 27 23:13:01 2010 +0100 @@ -384,9 +384,9 @@ fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop; -val union_hyps = OrdList.union TermOrd.fast_term_ord; -val insert_hyps = OrdList.insert TermOrd.fast_term_ord; -val remove_hyps = OrdList.remove TermOrd.fast_term_ord; +val union_hyps = OrdList.union Term_Ord.fast_term_ord; +val insert_hyps = OrdList.insert Term_Ord.fast_term_ord; +val remove_hyps = OrdList.remove Term_Ord.fast_term_ord; (* merge theories of cterms/thms -- trivial absorption only *) diff -r 980d4194a212 -r b48ab741683b src/Pure/unify.ML --- a/src/Pure/unify.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Pure/unify.ML Sat Feb 27 23:13:01 2010 +0100 @@ -558,7 +558,7 @@ if Term.eq_ix (v, w) then (*...occur check would falsely return true!*) if T=U then (env, add_tpair (rbinder, (t,u), tpairs)) else raise TERM ("add_ffpair: Var name confusion", [t,u]) - else if TermOrd.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*) + else if Term_Ord.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*) clean_ffpair thy ((rbinder, u, t), (env,tpairs)) else clean_ffpair thy ((rbinder, t, u), (env,tpairs)) | _ => raise TERM ("add_ffpair: Vars expected", [t,u]) diff -r 980d4194a212 -r b48ab741683b src/Tools/Compute_Oracle/linker.ML --- a/src/Tools/Compute_Oracle/linker.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/Tools/Compute_Oracle/linker.ML Sat Feb 27 23:13:01 2010 +0100 @@ -50,7 +50,7 @@ | constant_of _ = raise Link "constant_of" fun bool_ord (x,y) = if x then (if y then EQUAL else GREATER) else (if y then LESS else EQUAL) -fun constant_ord (Constant (x1,x2,x3), Constant (y1,y2,y3)) = (prod_ord (prod_ord bool_ord fast_string_ord) TermOrd.typ_ord) (((x1,x2),x3), ((y1,y2),y3)) +fun constant_ord (Constant (x1,x2,x3), Constant (y1,y2,y3)) = (prod_ord (prod_ord bool_ord fast_string_ord) Term_Ord.typ_ord) (((x1,x2),x3), ((y1,y2),y3)) fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2)) @@ -70,7 +70,7 @@ handle Type.TYPE_MATCH => NONE fun subst_ord (A:Type.tyenv, B:Type.tyenv) = - (list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B) + (list_ord (prod_ord Term_Ord.fast_indexname_ord (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))) (Vartab.dest A, Vartab.dest B) structure Substtab = Table(type key = Type.tyenv val ord = subst_ord); @@ -380,7 +380,7 @@ ComputeThm (hyps, shyps, prop) end -val cthm_ord' = prod_ord (prod_ord (list_ord TermOrd.term_ord) (list_ord TermOrd.sort_ord)) TermOrd.term_ord +val cthm_ord' = prod_ord (prod_ord (list_ord Term_Ord.term_ord) (list_ord Term_Ord.sort_ord)) Term_Ord.term_ord fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2)) diff -r 980d4194a212 -r b48ab741683b src/ZF/arith_data.ML --- a/src/ZF/arith_data.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/ZF/arith_data.ML Sat Feb 27 23:13:01 2010 +0100 @@ -104,7 +104,7 @@ (*Dummy version: the "coefficient" is always 1. In the result, the factors are sorted terms*) -fun dest_coeff t = (1, mk_prod (sort TermOrd.term_ord (dest_prod t))); +fun dest_coeff t = (1, mk_prod (sort Term_Ord.term_ord (dest_prod t))); (*Find first coefficient-term THAT MATCHES u*) fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) diff -r 980d4194a212 -r b48ab741683b src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/ZF/int_arith.ML Sat Feb 27 23:13:01 2010 +0100 @@ -95,7 +95,7 @@ (*Express t as a product of (possibly) a numeral with other sorted terms*) fun dest_coeff sign (Const (@{const_name "zminus"}, _) $ t) = dest_coeff (~sign) t | dest_coeff sign t = - let val ts = sort TermOrd.term_ord (dest_prod t) + let val ts = sort Term_Ord.term_ord (dest_prod t) val (n, ts') = find_first_numeral [] ts handle TERM _ => (1, ts) in (sign*n, mk_prod ts') end;