src/CCL/Term.thy
changeset 3837 d7f033c74b38
parent 2709 241fffc25284
child 14765 bafb24c150c1
     1.1 --- a/src/CCL/Term.thy	Fri Oct 10 16:29:41 1997 +0200
     1.2 +++ b/src/CCL/Term.thy	Fri Oct 10 17:10:12 1997 +0200
     1.3 @@ -54,36 +54,36 @@
     1.4  rules
     1.5  
     1.6    one_def                    "one == true"
     1.7 -  if_def     "if b then t else u  == case(b,t,u,% x y.bot,%v.bot)"
     1.8 +  if_def     "if b then t else u  == case(b,t,u,% x y. bot,%v. bot)"
     1.9    inl_def                 "inl(a) == <true,a>"
    1.10    inr_def                 "inr(b) == <false,b>"
    1.11 -  when_def           "when(t,f,g) == split(t,%b x.if b then f(x) else g(x))"
    1.12 -  split_def           "split(t,f) == case(t,bot,bot,f,%u.bot)"
    1.13 -  fst_def                 "fst(t) == split(t,%x y.x)"
    1.14 -  snd_def                 "snd(t) == split(t,%x y.y)"
    1.15 -  thd_def                 "thd(t) == split(t,%x p.split(p,%y z.z))"
    1.16 +  when_def           "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))"
    1.17 +  split_def           "split(t,f) == case(t,bot,bot,f,%u. bot)"
    1.18 +  fst_def                 "fst(t) == split(t,%x y. x)"
    1.19 +  snd_def                 "snd(t) == split(t,%x y. y)"
    1.20 +  thd_def                 "thd(t) == split(t,%x p. split(p,%y z. z))"
    1.21    zero_def                  "zero == inl(one)"
    1.22    succ_def               "succ(n) == inr(n)"
    1.23 -  ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
    1.24 -  nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
    1.25 +  ncase_def         "ncase(n,b,c) == when(n,%x. b,%y. c(y))"
    1.26 +  nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)"
    1.27    nil_def                     "[] == inl(one)"
    1.28    cons_def                   "h$t == inr(<h,t>)"
    1.29 -  lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
    1.30 -  lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
    1.31 +  lcase_def         "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))"
    1.32 +  lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)"
    1.33  
    1.34 -  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)))"
    1.35 +  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)))"
    1.36    letrec_def    
    1.37 -  "letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)"
    1.38 +  "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)"
    1.39  
    1.40    letrec2_def  "letrec g x y be h(x,y,g) in f(g)== 
    1.41 -               letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) 
    1.42 -                          in f(%x y.g'(<x,y>))"
    1.43 +               letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>))) 
    1.44 +                          in f(%x y. g'(<x,y>))"
    1.45  
    1.46    letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) == 
    1.47 -             letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) 
    1.48 -                          in f(%x y z.g'(<x,<y,z>>))"
    1.49 +             letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>)))) 
    1.50 +                          in f(%x y z. g'(<x,<y,z>>))"
    1.51  
    1.52 -  napply_def "f ^n` a == nrec(n,a,%x g.f(g))"
    1.53 +  napply_def "f ^n` a == nrec(n,a,%x g. f(g))"
    1.54  
    1.55  end
    1.56