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