src/CCL/Term.thy
changeset 1474 3f7d67927fe2
parent 1149 5750eba8820d
child 2709 241fffc25284
equal deleted inserted replaced
1473:e8d4606e6502 1474:3f7d67927fe2
     1 (*  Title: 	CCL/terms.thy
     1 (*  Title:      CCL/terms.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author: 	Martin Coen
     3     Author:     Martin Coen
     4     Copyright   1993  University of Cambridge
     4     Copyright   1993  University of Cambridge
     5 
     5 
     6 Definitions of usual program constructs in CCL.
     6 Definitions of usual program constructs in CCL.
     7 
     7 
     8 *)
     8 *)
    36   letrec     :: "[[i,i=>i]=>i,(i=>i)=>i]=>i"
    36   letrec     :: "[[i,i=>i]=>i,(i=>i)=>i]=>i"
    37   letrec2    :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
    37   letrec2    :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i"
    38   letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
    38   letrec3    :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i"  
    39 
    39 
    40   "@let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
    40   "@let"     :: "[idt,i,i]=>i"             ("(3let _ be _/ in _)"
    41   			[0,0,60] 60)
    41                         [0,0,60] 60)
    42 
    42 
    43   "@letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
    43   "@letrec"  :: "[idt,idt,i,i]=>i"         ("(3letrec _ _ be _/ in _)"
    44   			[0,0,0,60] 60)
    44                         [0,0,0,60] 60)
    45 
    45 
    46   "@letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
    46   "@letrec2" :: "[idt,idt,idt,i,i]=>i"     ("(3letrec _ _ _ be _/ in _)"
    47   			[0,0,0,0,60] 60)
    47                         [0,0,0,0,60] 60)
    48 
    48 
    49   "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
    49   "@letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)"
    50   			[0,0,0,0,0,60] 60)
    50                         [0,0,0,0,0,60] 60)
    51 
    51 
    52   napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
    52   napply     :: "[i=>i,i,i]=>i"            ("(_ ^ _ ` _)" [56,56,56] 56)
    53 
    53 
    54 rules
    54 rules
    55 
    55 
    64   thd_def                 "thd(t) == split(t,%x p.split(p,%y z.z))"
    64   thd_def                 "thd(t) == split(t,%x p.split(p,%y z.z))"
    65   zero_def                  "zero == inl(one)"
    65   zero_def                  "zero == inl(one)"
    66   succ_def               "succ(n) == inr(n)"
    66   succ_def               "succ(n) == inr(n)"
    67   ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
    67   ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
    68   nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
    68   nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
    69   nil_def	              "[] == inl(one)"
    69   nil_def                     "[] == inl(one)"
    70   cons_def                   "h$t == inr(<h,t>)"
    70   cons_def                   "h$t == inr(<h,t>)"
    71   lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
    71   lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
    72   lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
    72   lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
    73 
    73 
    74   let_def  "let x be t in f(x) == case(t,f(true),f(false),%x y.f(<x,y>),%u.f(lam x.u(x)))"
    74   let_def  "let x be t in f(x) == case(t,f(true),f(false),%x y.f(<x,y>),%u.f(lam x.u(x)))"