diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/UTerm.thy
--- a/src/HOL/Subst/UTerm.thy	Thu May 15 12:29:59 1997 +0200
+++ b/src/HOL/Subst/UTerm.thy	Thu May 15 12:40:01 1997 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Substitutions/UTerm.thy
+(*  Title:      Subst/UTerm.thy
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
@@ -6,60 +6,32 @@
 Binary trees with leaves that are constants or variables.
 *)
 
-UTerm = Sexp +
+UTerm = Finite + 
 
-types uterm 1
-
-arities 
-  uterm     :: (term)term
+datatype 'a uterm = Var ('a) 
+                  | Const ('a)
+                  | Comb ('a uterm) ('a uterm)
 
 consts
-  uterm     :: 'a item set => 'a item set
-  Rep_uterm :: 'a uterm => 'a item
-  Abs_uterm :: 'a item => 'a uterm
-  VAR       :: 'a item => 'a item
-  CONST     :: 'a item => 'a item
-  COMB      :: ['a item, 'a item] => 'a item
-  Var       :: 'a => 'a uterm
-  Const     :: 'a => 'a uterm
-  Comb      :: ['a uterm, 'a uterm] => 'a uterm
-  UTerm_rec :: ['a item, 'a item => 'b, 'a item => 'b, 
-                ['a item , 'a item, 'b, 'b]=>'b] => 'b
-  uterm_rec :: ['a uterm, 'a => 'b, 'a => 'b, 
-                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b
+  vars_of  ::  'a uterm => 'a set
+  "<:"     ::  'a uterm => 'a uterm => bool   (infixl 54) 
+uterm_size ::  'a uterm => nat
+
 
-defs
-     (*defining the concrete constructors*)
-  VAR_def       "VAR(v) == In0(v)"
-  CONST_def     "CONST(v) == In1(In0(v))"
-  COMB_def      "COMB t u == In1(In1(t $ u))"
+primrec vars_of   uterm
+vars_of_Var   "vars_of (Var v) = {v}"
+vars_of_Const "vars_of (Const c) = {}"
+vars_of_Comb  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
 
-inductive "uterm(A)"
-  intrs
-    VAR_I          "v:A ==> VAR(v) : uterm(A)"
-    CONST_I  "c:A ==> CONST(c) : uterm(A)"
-    COMB_I   "[| M:uterm(A);  N:uterm(A) |] ==> COMB M N : uterm(A)"
-
-rules
-    (*faking a type definition...*)
-  Rep_uterm             "Rep_uterm(xs): uterm(range(Leaf))"
-  Rep_uterm_inverse     "Abs_uterm(Rep_uterm(xs)) = xs"
-  Abs_uterm_inverse     "M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
 
-defs
-     (*defining the abstract constructors*)
-  Var_def       "Var(v) == Abs_uterm(VAR(Leaf(v)))"
-  Const_def     "Const(c) == Abs_uterm(CONST(Leaf(c)))"
-  Comb_def      "Comb t u == Abs_uterm (COMB (Rep_uterm t) (Rep_uterm u))"
+primrec "op <:"   uterm
+occs_Var   "u <: (Var v) = False"
+occs_Const "u <: (Const c) = False"
+occs_Comb  "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
 
-     (*uterm recursion*)
-  UTerm_rec_def 
-   "UTerm_rec M b c d == wfrec (trancl pred_sexp) 
-    (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y))))) M"
-
-  uterm_rec_def
-   "uterm_rec t b c d == 
-   UTerm_rec (Rep_uterm t) (%x.b(inv Leaf x)) (%x.c(inv Leaf x)) 
-                           (%x y q r.d (Abs_uterm x) (Abs_uterm y) q r)"
+primrec uterm_size  uterm
+uterm_size_Var   "uterm_size (Var v) = 0"
+uterm_size_Const "uterm_size (Const c) = 0"
+uterm_size_Comb  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
 
 end