src/ZF/Resid/Redex.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2874 b1e7e2179597
permissions -rw-r--r--
expanded tabs
clasohm@1478
     1
(*  Title:      Redex.thy
lcp@1048
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Ole Rasmussen
lcp@1048
     4
    Copyright   1995  University of Cambridge
lcp@1048
     5
    Logic Image: ZF
lcp@1048
     6
*)
lcp@1048
     7
lcp@1048
     8
Redex = Univ +
lcp@1048
     9
consts
clasohm@1401
    10
  redexes     :: i
lcp@1048
    11
lcp@1048
    12
datatype
clasohm@1478
    13
  "redexes" = Var ("n: nat")            
lcp@1048
    14
            | Fun ("t: redexes")
lcp@1048
    15
            | App ("b:bool" ,"f:redexes" , "a:redexes")
lcp@1048
    16
  type_intrs "[bool_into_univ]"
lcp@1048
    17
  
lcp@1048
    18
lcp@1048
    19
consts
clasohm@1478
    20
  redex_rec     :: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
lcp@1048
    21
 
lcp@1048
    22
defs
lcp@1048
    23
  redex_rec_def
clasohm@1155
    24
   "redex_rec(p,b,c,d) == 
clasohm@1155
    25
   Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),   
clasohm@1155
    26
                             %n x y.d(n, x, y, g`x, g`y), p))"
lcp@1048
    27
end
lcp@1048
    28