# HG changeset patch
# User wenzelm
# Date 853418687 -3600
# Node ID ce48daa388a78b12a99e509b597ec6099176f38a
# Parent  d290b91e76b86cebaf848ca8630c4a3e834a9529
added term order;

diff -r d290b91e76b8 -r ce48daa388a7 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Jan 13 18:24:40 1997 +0100
+++ b/src/Pure/logic.ML	Thu Jan 16 13:44:47 1997 +0100
@@ -45,8 +45,11 @@
   val strip_params	: term -> (string * typ) list
   val strip_prems	: int * term list * term -> term list * term
   val thaw_vars		: term -> term
-  val unvarify		: term -> term  
-  val varify		: term -> term  
+  val unvarify		: term -> term
+  val varify		: term -> term
+  val termord		: term * term -> order
+  val lextermord	: term list * term list -> order
+  val termless		: term * term -> bool
   end;
 
 structure Logic : LOGIC =
@@ -330,4 +333,44 @@
   | unvarify (f$t) = unvarify f $ unvarify t
   | unvarify t = t;
 
+
+(*** term order ***)
+
+(* NB: non-linearity of the ordering is not a soundness problem *)
+
+(* FIXME: "***ABSTRACTION***" is a hack and makes the ordering non-linear *)
+fun string_of_hd(Const(a,_)) = a
+  | string_of_hd(Free(a,_))  = a
+  | string_of_hd(Var(v,_))   = Syntax.string_of_vname v
+  | string_of_hd(Bound i)    = string_of_int i
+  | string_of_hd(Abs _)      = "***ABSTRACTION***";
+
+(* a strict (not reflexive) 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)
+ *)
+
+(* FIXME: should really take types into account as well.
+ * Otherwise non-linear *)
+fun termord(Abs(_,_,t),Abs(_,_,u)) = termord(t,u)
+  | termord(t,u) =
+      (case intord(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 stringord(string_of_hd f, string_of_hd g) of
+                       EQUAL => lextermord(ts,us)
+                     | ord   => ord
+                  end
+       | ord => ord)
+and lextermord(t::ts,u::us) =
+      (case termord(t,u) of
+         EQUAL => lextermord(ts,us)
+       | ord   => ord)
+  | lextermord([],[]) = EQUAL
+  | lextermord _ = error("lextermord");
+
+fun termless tu = (termord tu = LESS);
+
 end;