1.1 --- a/src/Pure/thm.ML	Thu Mar 24 18:14:45 1994 +0100
     1.2 +++ b/src/Pure/thm.ML	Sun Mar 27 12:33:14 1994 +0200
     1.3 @@ -991,51 +991,47 @@
     1.4  type termrec = (Sign.sg * term list) * term;
     1.5  type conv = meta_simpset -> termrec -> termrec;
     1.6  
     1.7 -datatype comparison = LESS | EQUAL | GREATER;
     1.8 +datatype order = LESS | EQUAL | GREATER;
     1.9  
    1.10 -fun stringcomp(a,b:string) = if a<b then LESS  else
    1.11 -                             if a=b then EQUAL else GREATER;
    1.12 +fun stringord(a,b:string) = if a<b then LESS  else
    1.13 +                            if a=b then EQUAL else GREATER;
    1.14  
    1.15 -fun intcomp(i,j:int) = if i<j then LESS  else
    1.16 -                       if i=j then EQUAL else GREATER;
    1.17 +fun intord(i,j:int) = if i<j then LESS  else
    1.18 +                      if i=j then EQUAL else GREATER;
    1.19  
    1.20 -fun xcomp((a,i),(b,j)) =
    1.21 -  (case stringcomp(a,b) of EQUAL => intcomp(i,j) | c => c);
    1.22 +(* FIXME: "***ABSTRACTION***" is a hack and makes the ordering non-linear *)
    1.23 +fun string_of_hd(Const(a,_)) = a
    1.24 +  | string_of_hd(Free(a,_))  = a
    1.25 +  | string_of_hd(Var(v,_))   = Syntax.string_of_vname v
    1.26 +  | string_of_hd(Bound i)    = string_of_int i
    1.27 +  | string_of_hd(Abs _)      = "***ABSTRACTION***";
    1.28  
    1.29 -(*a strict (not reflexive) linear ordering for terms*)
    1.30 +(* a strict (not reflexive) linear well-founded AC-compatible ordering
    1.31 + * for terms:
    1.32 + * s < t <=> 1. size(s) < size(t) or
    1.33 +             2. size(s) = size(t) and s=f(...) and t = g(...) and f<g or
    1.34 +             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
    1.35 +                (s1..sn) < (t1..tn) (lexicographically)
    1.36 + *)
    1.37 +
    1.38  (* FIXME: should really take types into account as well.
    1.39 -   Otherwise not linear *)
    1.40 -fun termcomp (t,u) =
    1.41 -  (case t of
    1.42 -     Const(a,_) => (case u of
    1.43 -                      Const(b,_) => stringcomp(a,b)
    1.44 -                    | _          => GREATER)
    1.45 -   | Free(a,_) => (case u of
    1.46 -                     Const _   => LESS
    1.47 -                   | Free(b,_) => stringcomp(a,b)
    1.48 -                   | _         => GREATER)
    1.49 -   | Var(v,_) => (case u of
    1.50 -                    Const _  => LESS
    1.51 -                  | Free _   => LESS
    1.52 -                  | Var(w,_) => xcomp(v,w)
    1.53 -                  | _        => GREATER)
    1.54 -  | Bound i => (case u of
    1.55 -                  Const _  => LESS
    1.56 -                | Free _   => LESS
    1.57 -                | Var _    => LESS
    1.58 -                | Bound j  => intcomp(i,j)
    1.59 -                | _        => GREATER)
    1.60 -  | Abs(_,_,r) => (case u of
    1.61 -                     _ $ _  => GREATER
    1.62 -                   | Abs(_,_,s) => termcomp(r,s)
    1.63 -                   | _          => LESS)
    1.64 -  | t1$t2 => (case u of
    1.65 -                u1$u2 => (case termcomp(t1,u1) of
    1.66 -                            EQUAL => termcomp(t2,u2)
    1.67 -                          | c => c)
    1.68 -              |  _    => LESS));
    1.69 + * Otherwise not linear *)
    1.70 +fun termord(t,u) =
    1.71 +      (case intord(size_of_term t,size_of_term u) of
    1.72 +         EQUAL => let val (f,ts) = strip_comb t and (g,us) = strip_comb u
    1.73 +                  in case stringord(string_of_hd f, string_of_hd g) of
    1.74 +                       EQUAL => lextermord(ts,us)
    1.75 +                     | ord   => ord
    1.76 +                  end
    1.77 +       | ord => ord)
    1.78 +and lextermord(t::ts,u::us) =
    1.79 +      (case termord(t,u) of
    1.80 +         EQUAL => lextermord(ts,us)
    1.81 +       | ord   => ord)
    1.82 +  | lextermord([],[]) = EQUAL
    1.83 +  | lextermord _ = error("lextermord");
    1.84  
    1.85 -fun termless tu = (termcomp tu = LESS);
    1.86 +fun termless tu = (termord tu = LESS);
    1.87  
    1.88  fun check_conv(thm as Thm{hyps,prop,...}, prop0) =
    1.89    let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; None)