src/Pure/logic.ML
changeset 4345 7e9436ffb813
parent 4318 9b672ea2dfe7
child 4443 d55e85d7f0c2
     1.1 --- a/src/Pure/logic.ML	Tue Dec 02 12:41:29 1997 +0100
     1.2 +++ b/src/Pure/logic.ML	Tue Dec 02 12:42:28 1997 +0100
     1.3 @@ -9,7 +9,13 @@
     1.4  infix occs;
     1.5  
     1.6  signature LOGIC = 
     1.7 -  sig
     1.8 +sig
     1.9 +  val indexname_ord	: indexname * indexname -> order
    1.10 +  val typ_ord		: typ * typ -> order
    1.11 +  val typs_ord		: typ list * typ list -> order
    1.12 +  val term_ord		: term * term -> order
    1.13 +  val terms_ord		: term list * term list -> order
    1.14 +  val termless		: term * term -> bool
    1.15    val assum_pairs	: term -> (term*term)list
    1.16    val auto_rename	: bool ref   
    1.17    val close_form	: term -> term   
    1.18 @@ -48,14 +54,64 @@
    1.19    val strip_prems	: int * term list * term -> term list * term
    1.20    val unvarify		: term -> term
    1.21    val varify		: term -> term
    1.22 -  val termord		: term * term -> order
    1.23 -  val lextermord	: term list * term list -> order
    1.24 -  val termless		: term * term -> bool
    1.25 -  end;
    1.26 +end;
    1.27  
    1.28  structure Logic : LOGIC =
    1.29  struct
    1.30  
    1.31 +
    1.32 +(** type and term orders **)
    1.33 +
    1.34 +fun indexname_ord ((x, i), (y, j)) =
    1.35 +  (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
    1.36 +
    1.37 +
    1.38 +(* typ_ord *)
    1.39 +
    1.40 +(*assumes that TFrees / TVars with the same name have same sorts*)
    1.41 +fun typ_ord (Type (a, Ts), Type (b, Us)) =
    1.42 +      (case string_ord (a, b) of EQUAL => typs_ord (Ts, Us) | ord => ord)
    1.43 +  | typ_ord (Type _, _) = GREATER
    1.44 +  | typ_ord (TFree _, Type _) = LESS
    1.45 +  | typ_ord (TFree (a, _), TFree (b, _)) = string_ord (a, b)
    1.46 +  | typ_ord (TFree _, TVar _) = GREATER
    1.47 +  | typ_ord (TVar _, Type _) = LESS
    1.48 +  | typ_ord (TVar _, TFree _) = LESS
    1.49 +  | typ_ord (TVar (xi, _), TVar (yj, _)) = indexname_ord (xi, yj)
    1.50 +and typs_ord Ts_Us = list_ord typ_ord Ts_Us;
    1.51 +
    1.52 +
    1.53 +(* term_ord *)
    1.54 +
    1.55 +(*a linear well-founded AC-compatible ordering for terms:
    1.56 +  s < t <=> 1. size(s) < size(t) or
    1.57 +            2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
    1.58 +            3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
    1.59 +               (s1..sn) < (t1..tn) (lexicographically)*)
    1.60 +
    1.61 +fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
    1.62 +  | dest_hd (Free (a, T)) = (((a, 0), T), 1)
    1.63 +  | dest_hd (Var v) = (v, 2)
    1.64 +  | dest_hd (Bound i) = ((("", i), dummyT), 3)
    1.65 +  | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
    1.66 +
    1.67 +fun term_ord (Abs (_, T, t), Abs(_, U, u)) =
    1.68 +      (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
    1.69 +  | term_ord (t, u) =
    1.70 +      (case int_ord (size_of_term t, size_of_term u) of
    1.71 +        EQUAL =>
    1.72 +          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
    1.73 +            (case hd_ord (f, g) of EQUAL => terms_ord (ts, us) | ord => ord)
    1.74 +          end
    1.75 +      | ord => ord)
    1.76 +and hd_ord (f, g) =
    1.77 +  prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
    1.78 +and terms_ord (ts, us) = list_ord term_ord (ts, us);
    1.79 +
    1.80 +fun termless tu = (term_ord tu = LESS);
    1.81 +
    1.82 +
    1.83 +
    1.84  (*** Abstract syntax operations on the meta-connectives ***)
    1.85  
    1.86  (** equality **)
    1.87 @@ -312,66 +368,6 @@
    1.88    | unvarify t = t;
    1.89  
    1.90  
    1.91 -(*** term order ***)
    1.92 -
    1.93 -fun dest_hd(Const(a,T)) = (a,T,0)
    1.94 -  | dest_hd(Free(a,T))  = (a,T,1)
    1.95 -  | dest_hd(Var(v,T))   = (Syntax.string_of_vname v, T, 2)
    1.96 -  | dest_hd(Bound i)    = (string_of_int i,dummyT,3)
    1.97 -  | dest_hd(Abs(x,T,_)) = (x,T,4);
    1.98 -
    1.99 -(* assumes that vars/frees with the same name have same classes *)
   1.100 -fun typord(T,U) = if T=U then EQUAL else
   1.101 - (case (T,U) of
   1.102 -    (Type(a,Ts),Type(b,Us)) =>
   1.103 -      (case stringord(a,b) of EQUAL => lextypord(Ts,Us) | ord => ord)
   1.104 -  | (Type _, _) => GREATER
   1.105 -  | (TFree _,Type _) => LESS
   1.106 -  | (TFree(a,_),TFree(b,_)) => stringord(a,b)
   1.107 -  | (TFree _, TVar _) => GREATER
   1.108 -  | (TVar _,Type _) => LESS
   1.109 -  | (TVar _,TFree _) => LESS
   1.110 -  | (TVar(va,_),TVar(vb,_)) =>
   1.111 -      stringord(Syntax.string_of_vname va,Syntax.string_of_vname vb))
   1.112 -and lextypord(T::Ts,U::Us) =
   1.113 -      (case typord(T,U) of
   1.114 -         EQUAL => lextypord(Ts,Us)
   1.115 -       | ord   => ord)
   1.116 -  | lextypord([],[]) = EQUAL
   1.117 -  | lextypord _ = error("lextypord");
   1.118 -
   1.119 -
   1.120 -(* a linear well-founded AC-compatible ordering
   1.121 - * for terms:
   1.122 - * s < t <=> 1. size(s) < size(t) or
   1.123 -             2. size(s) = size(t) and s=f(...) and t = g(...) and f<g or
   1.124 -             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
   1.125 -                (s1..sn) < (t1..tn) (lexicographically)
   1.126 - *)
   1.127 -
   1.128 -fun termord(Abs(x,T,t),Abs(y,U,u)) =
   1.129 -      (case termord(t,u) of EQUAL => typord(T,U) | ord => ord)
   1.130 -  | termord(t,u) =
   1.131 -      (case intord(size_of_term t,size_of_term u) of
   1.132 -         EQUAL => let val (f,ts) = strip_comb t and (g,us) = strip_comb u
   1.133 -                      val (a,T,i) = dest_hd f and (b,U,j) = dest_hd g
   1.134 -                  in case stringord(a,b) of
   1.135 -                       EQUAL => (case typord(T,U) of
   1.136 -                                   EQUAL => (case intord(i,j) of
   1.137 -                                               EQUAL => lextermord(ts,us)
   1.138 -                                             | ord => ord)
   1.139 -                                 | ord => ord)
   1.140 -                     | ord   => ord
   1.141 -                  end
   1.142 -       | ord => ord)
   1.143 -and lextermord(t::ts,u::us) =
   1.144 -      (case termord(t,u) of
   1.145 -         EQUAL => lextermord(ts,us)
   1.146 -       | ord   => ord)
   1.147 -  | lextermord([],[]) = EQUAL
   1.148 -  | lextermord _ = error("lextermord");
   1.149 -
   1.150 -fun termless tu = (termord tu = LESS);
   1.151  
   1.152  (** Test wellformedness of rewrite rules **)
   1.153