src/HOL/Subst/UTerm.thy
author clasohm
Mon Feb 05 21:29:06 1996 +0100 (1996-02-05)
changeset 1476 608483c2122a
parent 1381 57777949b2f8
child 2903 d1d5a0acbf72
permissions -rw-r--r--
expanded tabs; incorporated Konrad's changes
     1 (*  Title:      Substitutions/UTerm.thy
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     4 
     5 Simple term structure for unification.
     6 Binary trees with leaves that are constants or variables.
     7 *)
     8 
     9 UTerm = Sexp +
    10 
    11 types uterm 1
    12 
    13 arities 
    14   uterm     :: (term)term
    15 
    16 consts
    17   uterm     :: 'a item set => 'a item set
    18   Rep_uterm :: 'a uterm => 'a item
    19   Abs_uterm :: 'a item => 'a uterm
    20   VAR       :: 'a item => 'a item
    21   CONST     :: 'a item => 'a item
    22   COMB      :: ['a item, 'a item] => 'a item
    23   Var       :: 'a => 'a uterm
    24   Const     :: 'a => 'a uterm
    25   Comb      :: ['a uterm, 'a uterm] => 'a uterm
    26   UTerm_rec :: ['a item, 'a item => 'b, 'a item => 'b, 
    27                 ['a item , 'a item, 'b, 'b]=>'b] => 'b
    28   uterm_rec :: ['a uterm, 'a => 'b, 'a => 'b, 
    29                 ['a uterm, 'a uterm,'b,'b]=>'b] => 'b
    30 
    31 defs
    32      (*defining the concrete constructors*)
    33   VAR_def       "VAR(v) == In0(v)"
    34   CONST_def     "CONST(v) == In1(In0(v))"
    35   COMB_def      "COMB t u == In1(In1(t $ u))"
    36 
    37 inductive "uterm(A)"
    38   intrs
    39     VAR_I          "v:A ==> VAR(v) : uterm(A)"
    40     CONST_I  "c:A ==> CONST(c) : uterm(A)"
    41     COMB_I   "[| M:uterm(A);  N:uterm(A) |] ==> COMB M N : uterm(A)"
    42 
    43 rules
    44     (*faking a type definition...*)
    45   Rep_uterm             "Rep_uterm(xs): uterm(range(Leaf))"
    46   Rep_uterm_inverse     "Abs_uterm(Rep_uterm(xs)) = xs"
    47   Abs_uterm_inverse     "M: uterm(range(Leaf)) ==> Rep_uterm(Abs_uterm(M)) = M"
    48 
    49 defs
    50      (*defining the abstract constructors*)
    51   Var_def       "Var(v) == Abs_uterm(VAR(Leaf(v)))"
    52   Const_def     "Const(c) == Abs_uterm(CONST(Leaf(c)))"
    53   Comb_def      "Comb t u == Abs_uterm (COMB (Rep_uterm t) (Rep_uterm u))"
    54 
    55      (*uterm recursion*)
    56   UTerm_rec_def 
    57    "UTerm_rec M b c d == wfrec (trancl pred_sexp) 
    58     (%g. Case (%x.b(x)) (Case (%y. c(y)) (Split (%x y. d x y (g x) (g y))))) M"
    59 
    60   uterm_rec_def
    61    "uterm_rec t b c d == 
    62    UTerm_rec (Rep_uterm t) (%x.b(Inv Leaf x)) (%x.c(Inv Leaf x)) 
    63                            (%x y q r.d (Abs_uterm x) (Abs_uterm y) q r)"
    64 
    65 end