term order stuff moved to term.ML;
authorwenzelm
Fri Dec 19 10:15:51 1997 +0100 (1997-12-19)
changeset 4443d55e85d7f0c2
parent 4442 8ed9e689a15e
child 4444 fa05a79b3e97
term order stuff moved to term.ML;
src/Pure/logic.ML
     1.1 --- a/src/Pure/logic.ML	Fri Dec 19 10:15:26 1997 +0100
     1.2 +++ b/src/Pure/logic.ML	Fri Dec 19 10:15:51 1997 +0100
     1.3 @@ -10,12 +10,6 @@
     1.4  
     1.5  signature LOGIC = 
     1.6  sig
     1.7 -  val indexname_ord	: indexname * indexname -> order
     1.8 -  val typ_ord		: typ * typ -> order
     1.9 -  val typs_ord		: typ list * typ list -> order
    1.10 -  val term_ord		: term * term -> order
    1.11 -  val terms_ord		: term list * term list -> order
    1.12 -  val termless		: term * term -> bool
    1.13    val assum_pairs	: term -> (term*term)list
    1.14    val auto_rename	: bool ref   
    1.15    val close_form	: term -> term   
    1.16 @@ -60,58 +54,6 @@
    1.17  struct
    1.18  
    1.19  
    1.20 -(** type and term orders **)
    1.21 -
    1.22 -fun indexname_ord ((x, i), (y, j)) =
    1.23 -  (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
    1.24 -
    1.25 -
    1.26 -(* typ_ord *)
    1.27 -
    1.28 -(*assumes that TFrees / TVars with the same name have same sorts*)
    1.29 -fun typ_ord (Type (a, Ts), Type (b, Us)) =
    1.30 -      (case string_ord (a, b) of EQUAL => typs_ord (Ts, Us) | ord => ord)
    1.31 -  | typ_ord (Type _, _) = GREATER
    1.32 -  | typ_ord (TFree _, Type _) = LESS
    1.33 -  | typ_ord (TFree (a, _), TFree (b, _)) = string_ord (a, b)
    1.34 -  | typ_ord (TFree _, TVar _) = GREATER
    1.35 -  | typ_ord (TVar _, Type _) = LESS
    1.36 -  | typ_ord (TVar _, TFree _) = LESS
    1.37 -  | typ_ord (TVar (xi, _), TVar (yj, _)) = indexname_ord (xi, yj)
    1.38 -and typs_ord Ts_Us = list_ord typ_ord Ts_Us;
    1.39 -
    1.40 -
    1.41 -(* term_ord *)
    1.42 -
    1.43 -(*a linear well-founded AC-compatible ordering 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 -            3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
    1.47 -               (s1..sn) < (t1..tn) (lexicographically)*)
    1.48 -
    1.49 -fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
    1.50 -  | dest_hd (Free (a, T)) = (((a, 0), T), 1)
    1.51 -  | dest_hd (Var v) = (v, 2)
    1.52 -  | dest_hd (Bound i) = ((("", i), dummyT), 3)
    1.53 -  | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
    1.54 -
    1.55 -fun term_ord (Abs (_, T, t), Abs(_, U, u)) =
    1.56 -      (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
    1.57 -  | term_ord (t, u) =
    1.58 -      (case int_ord (size_of_term t, size_of_term u) of
    1.59 -        EQUAL =>
    1.60 -          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    1.61 -            (case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord)
    1.62 -          end
    1.63 -      | ord => ord)
    1.64 -and hd_ord (f, g) =
    1.65 -  prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
    1.66 -and terms_ord (ts, us) = list_ord term_ord (ts, us);
    1.67 -
    1.68 -fun termless tu = (term_ord tu = LESS);
    1.69 -
    1.70 -
    1.71 -
    1.72  (*** Abstract syntax operations on the meta-connectives ***)
    1.73  
    1.74  (** equality **)
    1.75 @@ -227,8 +169,7 @@
    1.76  
    1.77  (*Close up a formula over all free variables by quantification*)
    1.78  fun close_form A =
    1.79 -    list_all_free (map dest_Free (sort atless (term_frees A)),   
    1.80 -		   A);
    1.81 +  list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A);
    1.82  
    1.83  
    1.84  (*** Specialized operations for resolution... ***)