src/Pure/logic.ML
changeset 2508 ce48daa388a7
parent 2266 82aef6857c5b
child 3408 98a2d517cabe
     1.1 --- a/src/Pure/logic.ML	Mon Jan 13 18:24:40 1997 +0100
     1.2 +++ b/src/Pure/logic.ML	Thu Jan 16 13:44:47 1997 +0100
     1.3 @@ -45,8 +45,11 @@
     1.4    val strip_params	: term -> (string * typ) list
     1.5    val strip_prems	: int * term list * term -> term list * term
     1.6    val thaw_vars		: term -> term
     1.7 -  val unvarify		: term -> term  
     1.8 -  val varify		: term -> term  
     1.9 +  val unvarify		: term -> term
    1.10 +  val varify		: term -> term
    1.11 +  val termord		: term * term -> order
    1.12 +  val lextermord	: term list * term list -> order
    1.13 +  val termless		: term * term -> bool
    1.14    end;
    1.15  
    1.16  structure Logic : LOGIC =
    1.17 @@ -330,4 +333,44 @@
    1.18    | unvarify (f$t) = unvarify f $ unvarify t
    1.19    | unvarify t = t;
    1.20  
    1.21 +
    1.22 +(*** term order ***)
    1.23 +
    1.24 +(* NB: non-linearity of the ordering is not a soundness problem *)
    1.25 +
    1.26 +(* FIXME: "***ABSTRACTION***" is a hack and makes the ordering non-linear *)
    1.27 +fun string_of_hd(Const(a,_)) = a
    1.28 +  | string_of_hd(Free(a,_))  = a
    1.29 +  | string_of_hd(Var(v,_))   = Syntax.string_of_vname v
    1.30 +  | string_of_hd(Bound i)    = string_of_int i
    1.31 +  | string_of_hd(Abs _)      = "***ABSTRACTION***";
    1.32 +
    1.33 +(* a strict (not reflexive) linear well-founded AC-compatible ordering
    1.34 + * for terms:
    1.35 + * s < t <=> 1. size(s) < size(t) or
    1.36 +             2. size(s) = size(t) and s=f(...) and t = g(...) and f<g or
    1.37 +             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
    1.38 +                (s1..sn) < (t1..tn) (lexicographically)
    1.39 + *)
    1.40 +
    1.41 +(* FIXME: should really take types into account as well.
    1.42 + * Otherwise non-linear *)
    1.43 +fun termord(Abs(_,_,t),Abs(_,_,u)) = termord(t,u)
    1.44 +  | termord(t,u) =
    1.45 +      (case intord(size_of_term t,size_of_term u) of
    1.46 +         EQUAL => let val (f,ts) = strip_comb t and (g,us) = strip_comb u
    1.47 +                  in case stringord(string_of_hd f, string_of_hd g) of
    1.48 +                       EQUAL => lextermord(ts,us)
    1.49 +                     | ord   => ord
    1.50 +                  end
    1.51 +       | ord => ord)
    1.52 +and lextermord(t::ts,u::us) =
    1.53 +      (case termord(t,u) of
    1.54 +         EQUAL => lextermord(ts,us)
    1.55 +       | ord   => ord)
    1.56 +  | lextermord([],[]) = EQUAL
    1.57 +  | lextermord _ = error("lextermord");
    1.58 +
    1.59 +fun termless tu = (termord tu = LESS);
    1.60 +
    1.61  end;