moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;
--- a/src/CCL/Wfd.thy Wed Dec 31 00:08:14 2008 +0100
+++ b/src/CCL/Wfd.thy Wed Dec 31 15:30:10 2008 +0100
@@ -434,9 +434,9 @@
| get_bno l n (Bound m) = (m-length(l),n)
(* Not a great way of identifying induction hypothesis! *)
-fun could_IH x = could_unify(x,hd (prems_of @{thm rcallT})) orelse
- could_unify(x,hd (prems_of @{thm rcall2T})) orelse
- could_unify(x,hd (prems_of @{thm rcall3T}))
+fun could_IH x = Term.could_unify(x,hd (prems_of @{thm rcallT})) orelse
+ Term.could_unify(x,hd (prems_of @{thm rcall2T})) orelse
+ Term.could_unify(x,hd (prems_of @{thm rcall3T}))
fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
let val bvs = bvars Bi []
--- a/src/FOLP/IFOLP.thy Wed Dec 31 00:08:14 2008 +0100
+++ b/src/FOLP/IFOLP.thy Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: FOLP/IFOLP.thy
- ID: $Id$
Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
@@ -247,7 +246,7 @@
and concl = discard_proof (Logic.strip_assums_concl prem)
in
if exists (fn hyp => hyp aconv concl) hyps
- then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
+ then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of
[_] => assume_tac i
| _ => no_tac
else no_tac
--- a/src/HOL/Algebra/abstract/Ring2.thy Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy Wed Dec 31 15:30:10 2008 +0100
@@ -1,8 +1,7 @@
-(*
- Title: The algebraic hierarchy of rings as axiomatic classes
- Id: $Id$
- Author: Clemens Ballarin, started 9 December 1996
- Copyright: Clemens Ballarin
+(* Title: HOL/Algebra/abstract/Ring2.thy
+ Author: Clemens Ballarin
+
+The algebraic hierarchy of rings as axiomatic classes.
*)
header {* The algebraic hierarchy of rings as type classes *}
@@ -211,7 +210,7 @@
@{const_name HOL.minus}, @{const_name HOL.one}, @{const_name HOL.times}]
| ring_ord _ = ~1;
-fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);
+fun termless_ring (a, b) = (TermOrd.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",
--- a/src/HOL/Algebra/ringsimp.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,6 +1,4 @@
-(*
- Id: $Id$
- Author: Clemens Ballarin
+(* Author: Clemens Ballarin
Normalisation method for locales ring and cring.
*)
@@ -48,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) = (Term.term_lpo ord (a, b) = LESS);
+ fun less (a, b) = (TermOrd.term_lpo ord (a, b) = LESS);
in asm_full_simp_tac (HOL_ss settermless less addsimps simps) end;
fun algebra_tac ctxt =
--- a/src/HOL/Import/shuffler.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Import/shuffler.ML Wed Dec 31 15:30:10 2008 +0100
@@ -353,7 +353,7 @@
fun equals_fun thy assume t =
case t of
- Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
+ Const("op ==",_) $ u $ v => if TermOrd.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
| _ => NONE
fun eta_expand thy assumes origt =
--- a/src/HOL/OrderedGroup.thy Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/OrderedGroup.thy Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/OrderedGroup.thy
- ID: $Id$
- Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
- with contributions by Jeremy Avigad
+ Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
*)
header {* Ordered Groups *}
@@ -1376,7 +1374,7 @@
@{const_name HOL.uminus}, @{const_name HOL.minus}]
| agrp_ord _ = ~1;
-fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
+fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
local
val ac1 = mk_meta_eq @{thm add_assoc};
--- a/src/HOL/Statespace/DistinctTreeProver.thy Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
-(* Title: DistinctTreeProver.thy
- ID: $Id$
+(* Title: HOL/Statespace/DistinctTreeProver.thy
Author: Norbert Schirmer, TU Muenchen
*)
@@ -646,9 +645,9 @@
val const_decls = map (fn i => Syntax.no_syn
("const" ^ string_of_int i,Type ("nat",[]))) nums
-val consts = sort Term.fast_term_ord
+val consts = sort TermOrd.fast_term_ord
(map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
-val consts' = sort Term.fast_term_ord
+val consts' = sort TermOrd.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
--- a/src/HOL/Statespace/distinct_tree_prover.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
-(* Title: distinct_tree_prover.thy
- ID: $Id$
+(* Title: HOL/Statespace/distinct_tree_prover.ML
Author: Norbert Schirmer, TU Muenchen
*)
@@ -83,7 +82,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 Term.fast_term_ord e t of
+ (case bin_find_tree TermOrd.fast_term_ord e t of
NONE => lin_find_tree e t
| x => x);
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/Groebner_Basis/groebner.ML
- ID: $Id$
Author: Amine Chaieb, TU Muenchen
*)
@@ -599,14 +598,14 @@
if length ideal = 2 then ideal else [eq_commute, eq_commute]
val ring_dest_neg =
fn t => let val (l,r) = dest_comb t in
- if could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
+ if Term.could_unify(term_of l,term_of ring_neg_tm) then r else raise CTERM ("ring_dest_neg", [t])
end
val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
(*
fun ring_dest_inv t =
let val (l,r) = dest_comb t in
- if could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
+ if Term.could_unify(term_of l, term_of ring_inv_tm) then r else raise CTERM "ring_dest_inv"
end
*)
val ring_dest_add = dest_binary ring_add_tm;
@@ -687,7 +686,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) => Term.term_ord(term_of x,term_of y))
+ val vars = sort (fn (x, y) => TermOrd.term_ord(term_of x,term_of y))
(distinct (op aconvc) rawvars)
in (vars,map (grobify_equation vars) cjs)
end;
@@ -896,7 +895,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) => Term.term_ord (term_of s, term_of t))
+ (fn (s,t) => TermOrd.term_ord (term_of s, term_of t))
in (eq,Library.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/Groebner_Basis/normalizer.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/Groebner_Basis/normalizer.ML
- ID: $Id$
Author: Amine Chaieb, TU Muenchen
*)
@@ -615,7 +614,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 add_0}, @{thm add_Suc}];
-fun simple_cterm_ord t u = Term.term_ord (term_of t, term_of u) = LESS;
+fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS;
fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, idom, ideal},
{conv, dest_const, mk_const, is_const}) ord =
--- a/src/HOL/Tools/Qelim/langford.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/Qelim/langford.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,3 +1,7 @@
+(* Title: HOL/Tools/Qelim/langford.ML
+ Author: Amine Chaieb, TU Muenchen
+*)
+
signature LANGFORD_QE =
sig
val dlo_tac : Proof.context -> int -> tactic
@@ -211,7 +215,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) => Term.fast_term_ord (term_of a, term_of b)) (f p)
+ val ts = sort (fn (a,b) => TermOrd.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));
--- a/src/HOL/Tools/Qelim/presburger.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Wed Dec 31 15:30:10 2008 +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) => Term.fast_term_ord (term_of a, term_of b)) (f p)
+ val ts = sort (fn (a,b) => TermOrd.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));
--- a/src/HOL/Tools/function_package/decompose.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/function_package/decompose.ML Wed Dec 31 15:30:10 2008 +0100
@@ -19,7 +19,7 @@
structure Decompose : DECOMPOSE =
struct
-structure TermGraph = GraphFun(type key = term val ord = Term.fast_term_ord);
+structure TermGraph = GraphFun(type key = term val ord = TermOrd.fast_term_ord);
fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>
--- a/src/HOL/Tools/function_package/termination.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/function_package/termination.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/function_package/termination_data.ML
+(* Title: HOL/Tools/function_package/termination.ML
Author: Alexander Krauss, TU Muenchen
Context data for termination proofs
@@ -50,9 +50,9 @@
open FundefLib
-val term2_ord = prod_ord Term.fast_term_ord Term.fast_term_ord
+val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
-structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord Term.fast_term_ord term2_ord);
+structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
(** Analyzing binary trees **)
--- a/src/HOL/Tools/int_arith.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/int_arith.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
-(* Title: HOL/int_arith1.ML
- ID: $Id$
+(* Title: HOL/Tools/int_arith1.ML
Authors: Larry Paulson and Tobias Nipkow
Simprocs and decision procedure for linear arithmetic.
@@ -66,12 +65,12 @@
EQUAL => int_ord (Int.sign i, Int.sign j)
| ord => ord);
-(*This resembles Term.term_ord, but it puts binary numerals before other
+(*This resembles TermOrd.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 => typ_ord (T, U) | ord => ord)
+ (case numterm_ord (t, u) of EQUAL => TermOrd.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)
@@ -81,7 +80,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 hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
+ (case TermOrd.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)
@@ -164,7 +163,7 @@
(*Express t as a product of (possibly) a numeral with other sorted terms*)
fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
| dest_coeff sign t =
- let val ts = sort Term.term_ord (dest_prod t)
+ let val ts = sort TermOrd.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;
--- a/src/HOL/Tools/nat_simprocs.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
-(* Title: HOL/nat_simprocs.ML
- ID: $Id$
+(* Title: HOL/Tools/nat_simprocs.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 2000 University of Cambridge
Simprocs for nat numerals.
*)
@@ -81,7 +79,7 @@
(*Express t as a product of (possibly) a numeral with other factors, sorted*)
fun dest_coeff t =
- let val ts = sort Term.term_ord (dest_prod t)
+ let val ts = sort TermOrd.term_ord (dest_prod t)
val (n, _, ts') = find_first_numeral [] ts
handle TERM _ => (1, one, ts)
in (n, mk_prod ts') end;
--- a/src/HOL/Tools/sat_funcs.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/sat_funcs.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,9 +1,6 @@
(* Title: HOL/Tools/sat_funcs.ML
- ID: $Id$
Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
- Author: Tjark Weber
- Copyright 2005-2006
-
+ Author: Tjark Weber, TU Muenchen
Proof reconstruction from SAT solvers.
@@ -323,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 (Term.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
+ val sorted_clauses = sort (TermOrd.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
val _ = if !trace_sat then
tracing ("Sorted non-trivial clauses:\n" ^ cat_lines (map Display.string_of_cterm sorted_clauses))
else ()
--- a/src/HOL/ex/reflection.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/ex/reflection.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,19 +1,18 @@
-(*
- ID: $Id$
- Author: Amine Chaieb, TU Muenchen
+(* Author: Amine Chaieb, TU Muenchen
A trial for automatical reification.
*)
-signature REFLECTION = sig
+signature REFLECTION =
+sig
val genreify_tac: Proof.context -> thm list -> term option -> int -> tactic
val reflection_tac: Proof.context -> thm list -> thm list -> term option -> int -> tactic
val gen_reflection_tac: Proof.context -> (cterm -> thm)
-> thm list -> thm list -> term option -> int -> tactic
end;
-structure Reflection : REFLECTION
-= struct
+structure Reflection : REFLECTION =
+struct
val ext2 = thm "ext2";
val nth_Cons_0 = thm "nth_Cons_0";
@@ -38,7 +37,7 @@
val (((_,_),[th']), ctxt') = Variable.import_thms true [th] ctxt
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th'))
fun add_fterms (t as t1 $ t2) =
- if exists (fn f => could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
+ if exists (fn f => Term.could_unify (t |> strip_comb |> fst, f)) fs then insert (op aconv) t
else add_fterms t1 #> add_fterms t2
| add_fterms (t as Abs(xn,xT,t')) =
if (fN mem (term_consts t)) then (fn _ => [t]) else (fn _ => [])
@@ -139,7 +138,7 @@
val (tyenv, tmenv) =
Pattern.match thy
((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
- (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
+ (Envir.type_env (Envir.empty 0), Vartab.empty)
val (fnvs,invs) = List.partition (fn ((vn,_),_) => vn mem vns) (Vartab.dest tmenv)
val (fts,its) =
(map (snd o snd) fnvs,
@@ -191,7 +190,7 @@
val rhs_P = subst_free subst rhs
val (tyenv, tmenv) = Pattern.match
thy (rhs_P, t)
- (Envir.type_env (Envir.empty 0),Term.Vartab.empty)
+ (Envir.type_env (Envir.empty 0), Vartab.empty)
val sbst = Envir.subst_vars (tyenv, tmenv)
val sbsT = Envir.typ_subst_TVars tyenv
val subst_ty = map (fn (n,(s,t)) => (certT (TVar (n, s)), certT t))
--- a/src/Provers/Arith/cancel_factor.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Provers/Arith/cancel_factor.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Provers/Arith/cancel_factor.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Cancel common constant factor from balanced exression (e.g. =, <=, < of sums).
@@ -36,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 Term.term_ord ts, []);
+fun count_terms ts = foldr ins_term (sort TermOrd.term_ord ts, []);
(* divide sum *)
--- a/src/Provers/Arith/cancel_sums.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Provers/Arith/cancel_sums.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Provers/Arith/cancel_sums.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
Cancel common summands of balanced expressions:
@@ -38,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. Logic.term_ord*)
+(*symmetric difference of multisets -- assumed to be sorted wrt. TermOrd.term_ord*)
fun cancel ts [] vs = (ts, [], vs)
| cancel [] us vs = ([], us, vs)
| cancel (t :: ts) (u :: us) vs =
- (case Term.term_ord (t, u) of
+ (case TermOrd.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));
@@ -64,7 +63,7 @@
| SOME bal =>
let
val thy = ProofContext.theory_of (Simplifier.the_context ss);
- val (ts, us) = pairself (sort Term.term_ord o Data.dest_sum) bal;
+ val (ts, us) = pairself (sort TermOrd.term_ord o Data.dest_sum) bal;
val (ts', us', vs) = cancel ts us [];
in
if null vs then NONE
--- a/src/Provers/eqsubst.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Provers/eqsubst.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,13 +1,12 @@
(* Title: Provers/eqsubst.ML
- ID: $Id$
- Author: Lucas Dixon, University of Edinburgh, lucas.dixon@ed.ac.uk
+ Author: Lucas Dixon, University of Edinburgh
A proof method to perform a substiution using an equation.
*)
signature EQSUBST =
sig
- (* a type abriviation for match information *)
+ (* a type abbreviation for match information *)
type match =
((indexname * (sort * typ)) list (* type instantiations *)
* (indexname * (typ * term)) list) (* term instantiations *)
@@ -224,7 +223,7 @@
(* is it OK to ignore the type instantiation info?
or should I be using it? *)
val typs_unify =
- SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
+ SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
handle Type.TUNIFY => NONE;
in
case typs_unify of
--- a/src/Pure/IsaMakefile Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/IsaMakefile Wed Dec 31 15:30:10 2008 +0100
@@ -82,8 +82,8 @@
logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML \
old_goals.ML old_term.ML pattern.ML primitive_defs.ML proofterm.ML \
pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML \
- subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML theory.ML \
- thm.ML type.ML type_infer.ML unify.ML variable.ML \
+ subgoal.ML tactic.ML tctical.ML term.ML term_ord.ML term_subst.ML \
+ theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML \
../Tools/quickcheck.ML
@./mk
--- a/src/Pure/Isar/find_theorems.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/Isar/find_theorems.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/find_theorems.ML
- ID: $Id$
Author: Rafal Kolanski and Gerwin Klein, NICTA
Retrieve theorems from proof context.
@@ -287,7 +286,7 @@
fun rem_thm_dups xs =
xs ~~ (1 upto length xs)
- |> sort (Term.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
+ |> sort (TermOrd.fast_term_ord o pairself (Thm.prop_of o #2 o #1))
|> rem_cdups
|> sort (int_ord o pairself #2)
|> map #1;
--- a/src/Pure/Isar/locale.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/Isar/locale.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,6 +1,6 @@
(* Title: Pure/Isar/locale.ML
- ID: $Id$
- Author: Clemens Ballarin, TU Muenchen; Markus Wenzel, LMU/TU Muenchen
+ Author: Clemens Ballarin, TU Muenchen
+ Author: Markus Wenzel, LMU/TU Muenchen
Locales -- Isar proof contexts as meta-level predicates, with local
syntax and implicit structures.
@@ -1297,7 +1297,7 @@
fun defs_ord (defs1, defs2) =
list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
- Term.fast_term_ord (d1, d2)) (defs1, defs2);
+ TermOrd.fast_term_ord (d1, d2)) (defs1, defs2);
structure Defstab =
TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
--- a/src/Pure/Isar/rule_cases.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/Isar/rule_cases.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/rule_cases.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Annotations and local contexts of rules.
@@ -319,7 +318,7 @@
local
fun equal_cterms ts us =
- is_equal (list_ord (Term.fast_term_ord o pairself Thm.term_of) (ts, us));
+ is_equal (list_ord (TermOrd.fast_term_ord o pairself Thm.term_of) (ts, us));
fun prep_rule n th =
let
--- a/src/Pure/ROOT.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/ROOT.ML Wed Dec 31 15:30:10 2008 +0100
@@ -25,6 +25,7 @@
(*fundamental structures*)
use "name.ML";
use "term.ML";
+use "term_ord.ML";
use "term_subst.ML";
use "old_term.ML";
use "logic.ML";
--- a/src/Pure/envir.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/envir.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
(* Title: Pure/envir.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1988 University of Cambridge
Environments. The type of a term variable / sort of a type variable is
part of its name. The lookup function must apply type substitutions,
@@ -118,7 +116,7 @@
fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of
Var (nT as (name', T)) =>
if a = name' then env (*cycle!*)
- else if Term.indexname_ord (a, name') = LESS then
+ else if TermOrd.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))
--- a/src/Pure/facts.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/facts.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/facts.ML
- ID: $Id$
Author: Makarius
Environment of named facts, optionally indexed by proposition.
@@ -166,7 +165,7 @@
(* indexed props *)
-val prop_ord = Term.term_ord o pairself Thm.full_prop_of;
+val prop_ord = TermOrd.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;
--- a/src/Pure/meta_simplifier.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/meta_simplifier.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,6 +1,5 @@
(* Title: Pure/meta_simplifier.ML
- ID: $Id$
- Author: Tobias Nipkow and Stefan Berghofer
+ Author: Tobias Nipkow and Stefan Berghofer, TU Muenchen
Meta-level Simplification.
*)
@@ -788,7 +787,7 @@
mk_eq_True = K NONE,
reorient = default_reorient};
-val empty_ss = init_ss basic_mk_rews Term.termless (K (K no_tac)) ([], []);
+val empty_ss = init_ss basic_mk_rews TermOrd.termless (K (K no_tac)) ([], []);
(* merge *) (*NOTE: ignores some fields of 2nd simpset*)
--- a/src/Pure/more_thm.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/more_thm.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/more_thm.ML
- ID: $Id$
Author: Makarius
Further operations on type ctyp/cterm/thm, outside the inference kernel.
@@ -128,12 +127,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 Term.fast_term_ord (prop1, prop2) of
+ (case TermOrd.fast_term_ord (prop1, prop2) of
EQUAL =>
- (case list_ord (prod_ord Term.fast_term_ord Term.fast_term_ord) (tpairs1, tpairs2) of
+ (case list_ord (prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord) (tpairs1, tpairs2) of
EQUAL =>
- (case list_ord Term.fast_term_ord (hyps1, hyps2) of
- EQUAL => list_ord Term.sort_ord (shyps1, shyps2)
+ (case list_ord TermOrd.fast_term_ord (hyps1, hyps2) of
+ EQUAL => list_ord TermOrd.sort_ord (shyps1, shyps2)
| ord => ord)
| ord => ord)
| ord => ord)
--- a/src/Pure/old_term.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/old_term.ML Wed Dec 31 15:30:10 2008 +0100
@@ -17,7 +17,7 @@
(*Accumulates the Vars in the term, suppressing duplicates*)
fun add_term_vars (t, vars: term list) = case t of
- Var _ => OrdList.insert Term.term_ord t vars
+ Var _ => OrdList.insert TermOrd.term_ord t vars
| Abs (_,_,body) => add_term_vars(body,vars)
| f$t => add_term_vars (f, add_term_vars(t, vars))
| _ => vars;
@@ -26,7 +26,7 @@
(*Accumulates the Frees in the term, suppressing duplicates*)
fun add_term_frees (t, frees: term list) = case t of
- Free _ => OrdList.insert Term.term_ord t frees
+ Free _ => OrdList.insert TermOrd.term_ord t frees
| Abs (_,_,body) => add_term_frees(body,frees)
| f$t => add_term_frees (f, add_term_frees(t, frees))
| _ => frees;
--- a/src/Pure/pattern.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/pattern.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,6 +1,5 @@
(* Title: Pure/pattern.ML
- ID: $Id$
- Author: Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer
+ Author: Tobias Nipkow, Christine Heinzelmann, and Stefan Berghofer, TU Muenchen
Unification of Higher-Order Patterns.
@@ -223,7 +222,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 Term.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) 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
fun unify_types thy (T,U) (env as Envir.Envir{asol,iTs,maxidx}) =
if T=U then env
--- a/src/Pure/proofterm.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/proofterm.ML Wed Dec 31 15:30:10 2008 +0100
@@ -188,7 +188,7 @@
(* proof body *)
-val oracle_ord = prod_ord fast_string_ord Term.fast_term_ord;
+val oracle_ord = prod_ord fast_string_ord TermOrd.fast_term_ord;
fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
fun make_body prf =
--- a/src/Pure/search.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/search.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/search.ML
- ID: $Id$
Author: Lawrence C Paulson and Norbert Voelker
Search tacticals.
@@ -42,10 +41,8 @@
(** Instantiation of heaps for best-first search **)
(*total ordering on theorems, allowing duplicates to be found*)
-structure ThmHeap =
- HeapFun (type elem = int * thm
- val ord = Library.prod_ord Library.int_ord
- (Term.term_ord o Library.pairself (#prop o Thm.rep_thm)));
+structure ThmHeap = HeapFun(type elem = int * thm
+ val ord = prod_ord int_ord (TermOrd.term_ord o pairself Thm.prop_of));
structure Search : SEARCH =
--- a/src/Pure/sorts.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/sorts.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/sorts.ML
- ID: $Id$
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
The order-sorted algebra of type classes.
@@ -74,13 +73,13 @@
(** ordered lists of sorts **)
-val make = OrdList.make Term.sort_ord;
-val op subset = OrdList.subset Term.sort_ord;
-val op union = OrdList.union Term.sort_ord;
-val subtract = OrdList.subtract Term.sort_ord;
+val make = OrdList.make TermOrd.sort_ord;
+val op subset = OrdList.subset TermOrd.sort_ord;
+val op union = OrdList.union TermOrd.sort_ord;
+val subtract = OrdList.subtract TermOrd.sort_ord;
-val remove_sort = OrdList.remove Term.sort_ord;
-val insert_sort = OrdList.insert Term.sort_ord;
+val remove_sort = OrdList.remove TermOrd.sort_ord;
+val insert_sort = OrdList.insert TermOrd.sort_ord;
fun insert_typ (TFree (_, S)) Ss = insert_sort S Ss
| insert_typ (TVar (_, S)) Ss = insert_sort S Ss
--- a/src/Pure/term.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/term.ML Wed Dec 31 15:30:10 2008 +0100
@@ -76,9 +76,6 @@
val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
val add_term_names: term * string list -> string list
val aconv: term * term -> bool
- structure Vartab: TABLE
- structure Typtab: TABLE
- structure Termtab: TABLE
val propT: typ
val strip_all_body: term -> term
val strip_all_vars: term -> (string * typ) list
@@ -92,8 +89,6 @@
val subst_bound: term * term -> term
val betapply: term * term -> term
val betapplys: term * term list -> term
- val eq_ix: indexname * indexname -> bool
- val could_unify: term * term -> bool
val subst_free: (term * term) list -> term -> term
val abstract_over: term * term -> term
val lambda: term -> term -> term
@@ -156,23 +151,14 @@
val add_free_names: term -> string list -> string list
val add_frees: term -> (string * typ) list -> (string * typ) list
val hidden_polymorphism: term -> (indexname * sort) list
+ val eq_ix: indexname * indexname -> bool
+ val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
+ val eq_var: (indexname * typ) * (indexname * typ) -> bool
+ val could_unify: term * term -> bool
val strip_abs_eta: int -> term -> (string * typ) list * term
- val fast_indexname_ord: indexname * indexname -> order
- val indexname_ord: indexname * indexname -> order
- val sort_ord: sort * sort -> order
- val typ_ord: typ * typ -> order
- val fast_term_ord: term * term -> order
- val term_ord: term * term -> order
- val hd_ord: term * term -> order
- val termless: term * term -> bool
- val term_lpo: (term -> int) -> term * term -> order
val match_bvars: (term * term) * (string * string) list -> (string * string) list
val map_abs_vars: (string -> string) -> term -> term
val rename_abs: term -> term -> term -> term option
- val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
- val eq_var: (indexname * typ) * (indexname * typ) -> bool
- val tvar_ord: (indexname * sort) * (indexname * sort) -> order
- val var_ord: (indexname * typ) * (indexname * typ) -> order
val close_schematic_term: term -> term
val maxidx_typ: typ -> int -> int
val maxidx_typs: typ list -> int -> int
@@ -514,9 +500,17 @@
-(** Comparing terms, types, sorts etc. **)
+(** Comparing terms **)
+
+(* variables *)
+
+fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
-(* alpha equivalence -- tuned for equalities *)
+fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
+fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
+
+
+(* alpha equivalence *)
fun tm1 aconv tm2 =
pointer_eq (tm1, tm2) orelse
@@ -526,184 +520,24 @@
| (a1, a2) => a1 = a2);
-(* fast syntactic ordering -- tuned for inequalities *)
-
-fun fast_indexname_ord ((x, i), (y, j)) =
- (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
-
-fun sort_ord SS =
- if pointer_eq SS then EQUAL
- else dict_ord fast_string_ord SS;
-
-local
-
-fun cons_nr (TVar _) = 0
- | cons_nr (TFree _) = 1
- | cons_nr (Type _) = 2;
-
-in
-
-fun typ_ord TU =
- if pointer_eq TU then EQUAL
- else
- (case TU of
- (Type (a, Ts), Type (b, Us)) =>
- (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
- | (TFree (a, S), TFree (b, S')) =>
- (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
- | (TVar (xi, S), TVar (yj, S')) =>
- (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
- | (T, U) => int_ord (cons_nr T, cons_nr U));
-
-end;
-
-local
-
-fun cons_nr (Const _) = 0
- | cons_nr (Free _) = 1
- | cons_nr (Var _) = 2
- | cons_nr (Bound _) = 3
- | cons_nr (Abs _) = 4
- | cons_nr (_ $ _) = 5;
-
-fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
- | struct_ord (t1 $ t2, u1 $ u2) =
- (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
- | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
-
-fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
- | atoms_ord (t1 $ t2, u1 $ u2) =
- (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
- | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
- | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
- | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
- | atoms_ord (Bound i, Bound j) = int_ord (i, j)
- | atoms_ord _ = sys_error "atoms_ord";
-
-fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
- (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
- | types_ord (t1 $ t2, u1 $ u2) =
- (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
- | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
- | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
- | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
- | types_ord (Bound _, Bound _) = EQUAL
- | types_ord _ = sys_error "types_ord";
-
-in
-
-fun fast_term_ord tu =
- if pointer_eq tu then EQUAL
- else
- (case struct_ord tu of
- EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
- | ord => ord);
-
-structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord);
-structure Typtab = TableFun(type key = typ val ord = typ_ord);
-structure Termtab = TableFun(type key = term val ord = fast_term_ord);
-
-end;
-
-
-(* term_ord *)
-
-(*a linear well-founded AC-compatible ordering for terms:
- s < t <=> 1. size(s) < size(t) or
- 2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
- 3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
- (s1..sn) < (t1..tn) (lexicographically)*)
+(*A fast unification filter: true unless the two terms cannot be unified.
+ Terms must be NORMAL. Treats all Vars as distinct. *)
+fun could_unify (t, u) =
+ let
+ fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
+ | matchrands _ _ = true;
+ in
+ case (head_of t, head_of u) of
+ (_, Var _) => true
+ | (Var _, _) => true
+ | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
+ | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
+ | (Bound i, Bound j) => i = j andalso matchrands t u
+ | (Abs _, _) => true (*because of possible eta equality*)
+ | (_, Abs _) => true
+ | _ => false
+ end;
-fun indexname_ord ((x, i), (y, j)) =
- (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
-
-local
-
-fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
- | hd_depth p = p;
-
-fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
- | dest_hd (Free (a, T)) = (((a, 0), T), 1)
- | dest_hd (Var v) = (v, 2)
- | dest_hd (Bound i) = ((("", i), dummyT), 3)
- | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
-
-in
-
-fun term_ord tu =
- if pointer_eq tu then EQUAL
- else
- (case tu of
- (Abs (_, T, t), Abs(_, U, u)) =>
- (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
- | (t, u) =>
- (case int_ord (size_of_term t, size_of_term u) of
- EQUAL =>
- (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
- EQUAL => args_ord (t, u) | ord => ord)
- | ord => ord))
-and hd_ord (f, g) =
- prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
-and args_ord (f $ t, g $ u) =
- (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
- | args_ord _ = EQUAL;
-
-fun termless tu = (term_ord tu = LESS);
-
-end;
-
-
-(** Lexicographic path order on terms **)
-
-(*
- See Baader & Nipkow, Term rewriting, CUP 1998.
- Without variables. Const, Var, Bound, Free and Abs are treated all as
- constants.
-
- f_ord maps terms to integers and serves two purposes:
- - Predicate on constant symbols. Those that are not recognised by f_ord
- must be mapped to ~1.
- - Order on the recognised symbols. These must be mapped to distinct
- integers >= 0.
- The argument of f_ord is never an application.
-*)
-
-local
-
-fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
- | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
- | unrecognized (Var v) = ((1, v), 1)
- | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
- | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
-
-fun dest_hd f_ord t =
- let val ord = f_ord t
- in if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) end;
-
-fun term_lpo f_ord (s, t) =
- let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
- if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
- then case hd_ord f_ord (f, g) of
- GREATER =>
- if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
- then GREATER else LESS
- | EQUAL =>
- if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
- then list_ord (term_lpo f_ord) (ss, ts)
- else LESS
- | LESS => LESS
- else GREATER
- end
-and hd_ord f_ord (f, g) = case (f, g) of
- (Abs (_, T, t), Abs (_, U, u)) =>
- (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
- | (_, _) => prod_ord (prod_ord int_ord
- (prod_ord indexname_ord typ_ord)) int_ord
- (dest_hd f_ord f, dest_hd f_ord g);
-
-in
-val term_lpo = term_lpo
-end;
(** Connectives of higher order logic **)
@@ -854,35 +688,6 @@
in (vs1 @ vs2, t'') end;
-(* comparing variables *)
-
-fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
-
-fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
-fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
-
-val tvar_ord = prod_ord indexname_ord sort_ord;
-val var_ord = prod_ord indexname_ord typ_ord;
-
-
-(*A fast unification filter: true unless the two terms cannot be unified.
- Terms must be NORMAL. Treats all Vars as distinct. *)
-fun could_unify (t, u) =
- let
- fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
- | matchrands _ _ = true;
- in
- case (head_of t, head_of u) of
- (_, Var _) => true
- | (Var _, _) => true
- | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
- | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
- | (Bound i, Bound j) => i = j andalso matchrands t u
- | (Abs _, _) => true (*because of possible eta equality*)
- | (_, Abs _) => true
- | _ => false
- end;
-
(*Substitute new for free occurrences of old in a term*)
fun subst_free [] = I
| subst_free pairs =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/term_ord.ML Wed Dec 31 15:30:10 2008 +0100
@@ -0,0 +1,209 @@
+(* Title: Pure/term_ord.ML
+ Author: Tobias Nipkow and Makarius, TU Muenchen
+
+Term orderings.
+*)
+
+signature TERM_ORD =
+sig
+ val fast_indexname_ord: indexname * indexname -> order
+ val sort_ord: sort * sort -> order
+ val typ_ord: typ * typ -> order
+ val fast_term_ord: term * term -> order
+ val indexname_ord: indexname * indexname -> order
+ val tvar_ord: (indexname * sort) * (indexname * sort) -> order
+ val var_ord: (indexname * typ) * (indexname * typ) -> order
+ val term_ord: term * term -> order
+ val hd_ord: term * term -> order
+ val termless: term * term -> bool
+ val term_lpo: (term -> int) -> term * term -> order
+end;
+
+structure TermOrd: TERM_ORD =
+struct
+
+(* fast syntactic ordering -- tuned for inequalities *)
+
+fun fast_indexname_ord ((x, i), (y, j)) =
+ (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
+
+fun sort_ord SS =
+ if pointer_eq SS then EQUAL
+ else dict_ord fast_string_ord SS;
+
+local
+
+fun cons_nr (TVar _) = 0
+ | cons_nr (TFree _) = 1
+ | cons_nr (Type _) = 2;
+
+in
+
+fun typ_ord TU =
+ if pointer_eq TU then EQUAL
+ else
+ (case TU of
+ (Type (a, Ts), Type (b, Us)) =>
+ (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
+ | (TFree (a, S), TFree (b, S')) =>
+ (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
+ | (TVar (xi, S), TVar (yj, S')) =>
+ (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
+ | (T, U) => int_ord (cons_nr T, cons_nr U));
+
+end;
+
+local
+
+fun cons_nr (Const _) = 0
+ | cons_nr (Free _) = 1
+ | cons_nr (Var _) = 2
+ | cons_nr (Bound _) = 3
+ | cons_nr (Abs _) = 4
+ | cons_nr (_ $ _) = 5;
+
+fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
+ | struct_ord (t1 $ t2, u1 $ u2) =
+ (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
+ | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
+
+fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
+ | atoms_ord (t1 $ t2, u1 $ u2) =
+ (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
+ | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
+ | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
+ | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
+ | atoms_ord (Bound i, Bound j) = int_ord (i, j)
+ | atoms_ord _ = sys_error "atoms_ord";
+
+fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
+ (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
+ | types_ord (t1 $ t2, u1 $ u2) =
+ (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
+ | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
+ | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
+ | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
+ | types_ord (Bound _, Bound _) = EQUAL
+ | types_ord _ = sys_error "types_ord";
+
+in
+
+fun fast_term_ord tu =
+ if pointer_eq tu then EQUAL
+ else
+ (case struct_ord tu of
+ EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
+ | ord => ord);
+
+end;
+
+
+(* term_ord *)
+
+(*a linear well-founded AC-compatible ordering for terms:
+ s < t <=> 1. size(s) < size(t) or
+ 2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
+ 3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
+ (s1..sn) < (t1..tn) (lexicographically)*)
+
+fun indexname_ord ((x, i), (y, j)) =
+ (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
+
+val tvar_ord = prod_ord indexname_ord sort_ord;
+val var_ord = prod_ord indexname_ord typ_ord;
+
+
+local
+
+fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
+ | hd_depth p = p;
+
+fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
+ | dest_hd (Free (a, T)) = (((a, 0), T), 1)
+ | dest_hd (Var v) = (v, 2)
+ | dest_hd (Bound i) = ((("", i), dummyT), 3)
+ | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
+
+in
+
+fun term_ord tu =
+ if pointer_eq tu then EQUAL
+ else
+ (case tu of
+ (Abs (_, T, t), Abs(_, U, u)) =>
+ (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
+ | (t, u) =>
+ (case int_ord (size_of_term t, size_of_term u) of
+ EQUAL =>
+ (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
+ EQUAL => args_ord (t, u) | ord => ord)
+ | ord => ord))
+and hd_ord (f, g) =
+ prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
+and args_ord (f $ t, g $ u) =
+ (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
+ | args_ord _ = EQUAL;
+
+fun termless tu = (term_ord tu = LESS);
+
+end;
+
+
+(* Lexicographic path order on terms *)
+
+(*
+ See Baader & Nipkow, Term rewriting, CUP 1998.
+ Without variables. Const, Var, Bound, Free and Abs are treated all as
+ constants.
+
+ f_ord maps terms to integers and serves two purposes:
+ - Predicate on constant symbols. Those that are not recognised by f_ord
+ must be mapped to ~1.
+ - Order on the recognised symbols. These must be mapped to distinct
+ integers >= 0.
+ The argument of f_ord is never an application.
+*)
+
+local
+
+fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
+ | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
+ | unrecognized (Var v) = ((1, v), 1)
+ | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
+ | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
+
+fun dest_hd f_ord t =
+ let val ord = f_ord t
+ in if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) end;
+
+fun term_lpo f_ord (s, t) =
+ let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
+ if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
+ then case hd_ord f_ord (f, g) of
+ GREATER =>
+ if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
+ then GREATER else LESS
+ | EQUAL =>
+ if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
+ then list_ord (term_lpo f_ord) (ss, ts)
+ else LESS
+ | LESS => LESS
+ else GREATER
+ end
+and hd_ord f_ord (f, g) = case (f, g) of
+ (Abs (_, T, t), Abs (_, U, u)) =>
+ (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
+ | (_, _) => prod_ord (prod_ord int_ord
+ (prod_ord indexname_ord typ_ord)) int_ord
+ (dest_hd f_ord f, dest_hd f_ord g);
+
+in
+val term_lpo = term_lpo
+end;
+
+
+end;
+
+structure Vartab = TableFun(type key = indexname val ord = TermOrd.fast_indexname_ord);
+structure Typtab = TableFun(type key = typ val ord = TermOrd.typ_ord);
+structure Termtab = TableFun(type key = term val ord = TermOrd.fast_term_ord);
--- a/src/Pure/term_subst.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/term_subst.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/term_subst.ML
- ID: $Id$
Author: Makarius
Efficient term substitution -- avoids copying.
@@ -163,9 +162,9 @@
fun zero_var_indexes_inst ts =
let
- val tvars = sort Term.tvar_ord (fold Term.add_tvars ts []);
+ val tvars = sort TermOrd.tvar_ord (fold Term.add_tvars ts []);
val instT = map (apsnd TVar) (zero_var_inst tvars);
- val vars = sort Term.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
+ val vars = sort TermOrd.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
val inst = map (apsnd Var) (zero_var_inst vars);
in (instT, inst) end;
--- a/src/Pure/thm.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/thm.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,6 @@
(* Title: Pure/thm.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
+ Author: Makarius
The very core of Isabelle's Meta Logic: certified types and terms,
derivations, theorems, framework rules (including lifting and
@@ -380,9 +379,9 @@
fun full_prop_of (Thm (_, {tpairs, prop, ...})) = attach_tpairs tpairs prop;
-val union_hyps = OrdList.union Term.fast_term_ord;
-val insert_hyps = OrdList.insert Term.fast_term_ord;
-val remove_hyps = OrdList.remove Term.fast_term_ord;
+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;
(* merge theories of cterms/thms -- trivial absorption only *)
@@ -1561,9 +1560,9 @@
(*Quick test whether rule is resolvable with the subgoal with hyps Hs
and conclusion B. If eres_flg then checks 1st premise of rule also*)
fun could_bires (Hs, B, eres_flg, rule) =
- let fun could_reshyp (A1::_) = exists (fn H => could_unify (A1, H)) Hs
+ let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs
| could_reshyp [] = false; (*no premise -- illegal*)
- in could_unify(concl_of rule, B) andalso
+ in Term.could_unify(concl_of rule, B) andalso
(not eres_flg orelse could_reshyp (prems_of rule))
end;
--- a/src/Pure/type.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/type.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/type.ML
- ID: $Id$
Author: Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel
Type signatures and certified types, special treatment of type vars,
@@ -401,7 +400,7 @@
fun occ (Type (_, Ts)) = exists occ Ts
| occ (TFree _) = false
| occ (TVar (w, S)) =
- eq_ix (v, w) orelse
+ Term.eq_ix (v, w) orelse
(case lookup tye (w, S) of
NONE => false
| SOME U => occ U);
@@ -438,7 +437,7 @@
fun unif (ty1, ty2) tye =
(case (devar tye ty1, devar tye ty2) of
(T as TVar (v, S1), U as TVar (w, S2)) =>
- if eq_ix (v, w) then
+ if Term.eq_ix (v, w) then
if S1 = S2 then tye else tvar_clash v S1 S2
else if Sorts.sort_le classes (S1, S2) then
Vartab.update_new (w, (S2, T)) tye
@@ -466,7 +465,7 @@
fun raw_unify (ty1, ty2) tye =
(case (devar tye ty1, devar tye ty2) of
(T as TVar (v, S1), U as TVar (w, S2)) =>
- if eq_ix (v, w) then
+ if Term.eq_ix (v, w) then
if S1 = S2 then tye else tvar_clash v S1 S2
else Vartab.update_new (w, (S2, T)) tye
| (TVar (v, S), T) =>
--- a/src/Pure/unify.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/unify.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/unify.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright Cambridge University 1992
@@ -104,7 +103,7 @@
| occur (Free _) = false
| occur (Var (w, T)) =
if member (op =) (!seen) w then false
- else if eq_ix(v,w) then true
+ else if Term.eq_ix (v, w) then true
(*no need to lookup: v has no assignment*)
else (seen := w:: !seen;
case Envir.lookup (env, (w, T)) of
@@ -167,7 +166,7 @@
| occur (Free _) = NoOcc
| occur (Var (w, T)) =
if member (op =) (!seen) w then NoOcc
- else if eq_ix(v,w) then Rigid
+ else if Term.eq_ix (v, w) then Rigid
else (seen := w:: !seen;
case Envir.lookup (env, (w, T)) of
NONE => NoOcc
@@ -176,7 +175,7 @@
| occur (t as f$_) = (*switch to nonrigid search?*)
(case head_of_in (env,f) of
Var (w,_) => (*w is not assigned*)
- if eq_ix(v,w) then Rigid
+ if Term.eq_ix (v, w) then Rigid
else nonrigid t
| Abs(_,_,body) => nonrigid t (*not in normal form*)
| _ => occomb t)
@@ -541,10 +540,10 @@
let val t = Envir.norm_term env t0 and u = Envir.norm_term env u0
in case (head_of t, head_of u) of
(Var(v,T), Var(w,U)) => (*Check for identical variables...*)
- if eq_ix(v,w) then (*...occur check would falsely return true!*)
+ 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 Term.indexname_ord (v, w) = LESS then (*prefer to update the LARGER variable*)
+ else if TermOrd.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])
--- a/src/Sequents/modal.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Sequents/modal.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,9 +1,8 @@
(* Title: Sequents/modal.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Simple modal reasoner
+Simple modal reasoner.
*)
@@ -39,7 +38,7 @@
Assumes each formula in seqc is surrounded by sequence variables
-- checks that each concl formula looks like some subgoal formula.*)
fun could_res (seqp,seqc) =
- forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc))
+ forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc))
(forms_of_seq seqp))
(forms_of_seq seqc);
--- a/src/Sequents/prover.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Sequents/prover.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,9 +1,8 @@
-(* Title: Sequents/prover
- ID: $Id$
+(* Title: Sequents/prover.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-Simple classical reasoner for the sequent calculus, based on "theorem packs"
+Simple classical reasoner for the sequent calculus, based on "theorem packs".
*)
@@ -65,7 +64,7 @@
-- checks that each concl formula looks like some subgoal formula.
It SHOULD check order as well, using recursion rather than forall/exists*)
fun could_res (seqp,seqc) =
- forall (fn Qc => exists (fn Qp => could_unify (Qp,Qc))
+ forall (fn Qc => exists (fn Qp => Term.could_unify (Qp,Qc))
(forms_of_seq seqp))
(forms_of_seq seqc);
@@ -78,7 +77,7 @@
could_res (leftp,leftc) andalso could_res (rightp,rightc)
| (_ $ Abs(_,_,leftp) $ rightp,
_ $ Abs(_,_,leftc) $ rightc) =>
- could_res (leftp,leftc) andalso could_unify (rightp,rightc)
+ could_res (leftp,leftc) andalso Term.could_unify (rightp,rightc)
| _ => false;
--- a/src/Tools/Compute_Oracle/compute.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Tools/Compute_Oracle/compute.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Tools/Compute_Oracle/compute.ML
- ID: $Id$
Author: Steven Obua
*)
@@ -168,7 +167,7 @@
| machine_of_prog (ProgHaskell _) = HASKELL
| machine_of_prog (ProgSML _) = SML
-structure Sorttab = TableFun(type key = sort val ord = Term.sort_ord)
+structure Sorttab = TableFun(type key = sort val ord = TermOrd.sort_ord)
type naming = int -> string
--- a/src/Tools/Compute_Oracle/linker.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Tools/Compute_Oracle/linker.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Tools/Compute_Oracle/linker.ML
- ID: $Id$
Author: Steven Obua
Linker.ML solves the problem that the computing oracle does not
@@ -51,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) Term.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) TermOrd.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))
@@ -71,7 +70,7 @@
handle Type.TYPE_MATCH => NONE
fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
- (list_ord (prod_ord Term.fast_indexname_ord (prod_ord Term.sort_ord Term.typ_ord))) (Vartab.dest A, Vartab.dest B)
+ (list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B)
structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord);
@@ -379,7 +378,7 @@
ComputeThm (hyps, shyps, prop)
end
-val cthm_ord' = prod_ord (prod_ord (list_ord Term.term_ord) (list_ord Term.sort_ord)) Term.term_ord
+val cthm_ord' = prod_ord (prod_ord (list_ord TermOrd.term_ord) (list_ord TermOrd.sort_ord)) TermOrd.term_ord
fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
--- a/src/ZF/arith_data.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/ZF/arith_data.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
(* Title: ZF/arith_data.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 2000 University of Cambridge
Arithmetic simplification: cancellation of common terms
*)
@@ -106,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 Term.term_ord (dest_prod t)));
+fun dest_coeff t = (1, mk_prod (sort TermOrd.term_ord (dest_prod t)));
(*Find first coefficient-term THAT MATCHES u*)
fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
--- a/src/ZF/int_arith.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/ZF/int_arith.ML Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
(* Title: ZF/int_arith.ML
- ID: $Id$
Author: Larry Paulson
- Copyright 2000 University of Cambridge
Simprocs for linear arithmetic.
*)
@@ -72,7 +70,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 Term.term_ord (dest_prod t)
+ let val ts = sort TermOrd.term_ord (dest_prod t)
val (n, ts') = find_first_numeral [] ts
handle TERM _ => (1, ts)
in (sign*n, mk_prod ts') end;