# HG changeset patch
# User nipkow
# Date 764764394 -7200
# Node ID 4c2bbb5de4718259bc6d4f658037e070befac193
# Parent  5edc4f5e5ebdeec4f7601a655bbd36fb64a9938d
Changed term ordering for permutative rewrites to be AC-compatible.

diff -r 5edc4f5e5ebd -r 4c2bbb5de471 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Mar 24 18:14:45 1994 +0100
+++ b/src/Pure/thm.ML	Sun Mar 27 12:33:14 1994 +0200
@@ -991,51 +991,47 @@
 type termrec = (Sign.sg * term list) * term;
 type conv = meta_simpset -> termrec -> termrec;
 
-datatype comparison = LESS | EQUAL | GREATER;
+datatype order = LESS | EQUAL | GREATER;
 
-fun stringcomp(a,b:string) = if a<b then LESS  else
-                             if a=b then EQUAL else GREATER;
+fun stringord(a,b:string) = if a<b then LESS  else
+                            if a=b then EQUAL else GREATER;
+
+fun intord(i,j:int) = if i<j then LESS  else
+                      if i=j then EQUAL else GREATER;
 
-fun intcomp(i,j:int) = if i<j then LESS  else
-                       if i=j then EQUAL else GREATER;
+(* 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***";
 
-fun xcomp((a,i),(b,j)) =
-  (case stringcomp(a,b) of EQUAL => intcomp(i,j) | c => c);
+(* 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)
+ *)
 
-(*a strict (not reflexive) linear ordering for terms*)
 (* FIXME: should really take types into account as well.
-   Otherwise not linear *)
-fun termcomp (t,u) =
-  (case t of
-     Const(a,_) => (case u of
-                      Const(b,_) => stringcomp(a,b)
-                    | _          => GREATER)
-   | Free(a,_) => (case u of
-                     Const _   => LESS
-                   | Free(b,_) => stringcomp(a,b)
-                   | _         => GREATER)
-   | Var(v,_) => (case u of
-                    Const _  => LESS
-                  | Free _   => LESS
-                  | Var(w,_) => xcomp(v,w)
-                  | _        => GREATER)
-  | Bound i => (case u of
-                  Const _  => LESS
-                | Free _   => LESS
-                | Var _    => LESS
-                | Bound j  => intcomp(i,j)
-                | _        => GREATER)
-  | Abs(_,_,r) => (case u of
-                     _ $ _  => GREATER
-                   | Abs(_,_,s) => termcomp(r,s)
-                   | _          => LESS)
-  | t1$t2 => (case u of
-                u1$u2 => (case termcomp(t1,u1) of
-                            EQUAL => termcomp(t2,u2)
-                          | c => c)
-              |  _    => LESS));
+ * Otherwise not linear *)
+fun 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 = (termcomp tu = LESS);
+fun termless tu = (termord tu = LESS);
 
 fun check_conv(thm as Thm{hyps,prop,...}, prop0) =
   let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; None)