Fixed the definition of `termord': is now antisymmetric.
authornipkow
Fri Nov 28 07:35:10 1997 +0100 (1997-11-28)
changeset 43189b672ea2dfe7
parent 4317 7264fa2ff2ec
child 4319 afb60b8bf15e
Fixed the definition of `termord': is now antisymmetric.
src/Pure/logic.ML
     1.1 --- a/src/Pure/logic.ML	Thu Nov 27 19:39:02 1997 +0100
     1.2 +++ b/src/Pure/logic.ML	Fri Nov 28 07:35:10 1997 +0100
     1.3 @@ -314,16 +314,34 @@
     1.4  
     1.5  (*** term order ***)
     1.6  
     1.7 -(* NB: non-linearity of the ordering is not a soundness problem *)
     1.8 +fun dest_hd(Const(a,T)) = (a,T,0)
     1.9 +  | dest_hd(Free(a,T))  = (a,T,1)
    1.10 +  | dest_hd(Var(v,T))   = (Syntax.string_of_vname v, T, 2)
    1.11 +  | dest_hd(Bound i)    = (string_of_int i,dummyT,3)
    1.12 +  | dest_hd(Abs(x,T,_)) = (x,T,4);
    1.13  
    1.14 -(* FIXME: "***ABSTRACTION***" is a hack and makes the ordering non-linear *)
    1.15 -fun string_of_hd(Const(a,_)) = a
    1.16 -  | string_of_hd(Free(a,_))  = a
    1.17 -  | string_of_hd(Var(v,_))   = Syntax.string_of_vname v
    1.18 -  | string_of_hd(Bound i)    = string_of_int i
    1.19 -  | string_of_hd(Abs _)      = "***ABSTRACTION***";
    1.20 +(* assumes that vars/frees with the same name have same classes *)
    1.21 +fun typord(T,U) = if T=U then EQUAL else
    1.22 + (case (T,U) of
    1.23 +    (Type(a,Ts),Type(b,Us)) =>
    1.24 +      (case stringord(a,b) of EQUAL => lextypord(Ts,Us) | ord => ord)
    1.25 +  | (Type _, _) => GREATER
    1.26 +  | (TFree _,Type _) => LESS
    1.27 +  | (TFree(a,_),TFree(b,_)) => stringord(a,b)
    1.28 +  | (TFree _, TVar _) => GREATER
    1.29 +  | (TVar _,Type _) => LESS
    1.30 +  | (TVar _,TFree _) => LESS
    1.31 +  | (TVar(va,_),TVar(vb,_)) =>
    1.32 +      stringord(Syntax.string_of_vname va,Syntax.string_of_vname vb))
    1.33 +and lextypord(T::Ts,U::Us) =
    1.34 +      (case typord(T,U) of
    1.35 +         EQUAL => lextypord(Ts,Us)
    1.36 +       | ord   => ord)
    1.37 +  | lextypord([],[]) = EQUAL
    1.38 +  | lextypord _ = error("lextypord");
    1.39  
    1.40 -(* a strict (not reflexive) linear well-founded AC-compatible ordering
    1.41 +
    1.42 +(* a linear well-founded AC-compatible ordering
    1.43   * for terms:
    1.44   * s < t <=> 1. size(s) < size(t) or
    1.45               2. size(s) = size(t) and s=f(...) and t = g(...) and f<g or
    1.46 @@ -331,14 +349,18 @@
    1.47                  (s1..sn) < (t1..tn) (lexicographically)
    1.48   *)
    1.49  
    1.50 -(* FIXME: should really take types into account as well.
    1.51 - * Otherwise non-linear *)
    1.52 -fun termord(Abs(_,_,t),Abs(_,_,u)) = termord(t,u)
    1.53 +fun termord(Abs(x,T,t),Abs(y,U,u)) =
    1.54 +      (case termord(t,u) of EQUAL => typord(T,U) | ord => ord)
    1.55    | termord(t,u) =
    1.56        (case intord(size_of_term t,size_of_term u) of
    1.57           EQUAL => let val (f,ts) = strip_comb t and (g,us) = strip_comb u
    1.58 -                  in case stringord(string_of_hd f, string_of_hd g) of
    1.59 -                       EQUAL => lextermord(ts,us)
    1.60 +                      val (a,T,i) = dest_hd f and (b,U,j) = dest_hd g
    1.61 +                  in case stringord(a,b) of
    1.62 +                       EQUAL => (case typord(T,U) of
    1.63 +                                   EQUAL => (case intord(i,j) of
    1.64 +                                               EQUAL => lextermord(ts,us)
    1.65 +                                             | ord => ord)
    1.66 +                                 | ord => ord)
    1.67                       | ord   => ord
    1.68                    end
    1.69         | ord => ord)