47 |
47 |
48 definition "let1" :: "[i,i\<Rightarrow>i]\<Rightarrow>i" |
48 definition "let1" :: "[i,i\<Rightarrow>i]\<Rightarrow>i" |
49 where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))" |
49 where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))" |
50 |
50 |
51 syntax "_let1" :: "[idt,i,i]\<Rightarrow>i" ("(3let _ be _/ in _)" [0,0,60] 60) |
51 syntax "_let1" :: "[idt,i,i]\<Rightarrow>i" ("(3let _ be _/ in _)" [0,0,60] 60) |
|
52 syntax_consts "_let1" == let1 |
52 translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)" |
53 translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)" |
53 syntax_consts "_let1" == let1 |
|
54 |
54 |
55 definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i" |
55 definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i" |
56 where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)" |
56 where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)" |
57 |
57 |
58 definition letrec2 :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i" |
58 definition letrec2 :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i" |
66 |
66 |
67 syntax |
67 syntax |
68 "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60) |
68 "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60) |
69 "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60) |
69 "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60) |
70 "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60) |
70 "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i" ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60) |
|
71 syntax_consts |
|
72 "_letrec" == letrec and |
|
73 "_letrec2" == letrec2 and |
|
74 "_letrec3" == letrec3 |
71 parse_translation \<open> |
75 parse_translation \<open> |
72 let |
76 let |
73 fun abs_tr t u = Syntax_Trans.abs_tr [t, u]; |
77 fun abs_tr t u = Syntax_Trans.abs_tr [t, u]; |
74 fun letrec_tr [f, x, a, b] = |
78 fun letrec_tr [f, x, a, b] = |
75 Syntax.const \<^const_syntax>\<open>letrec\<close> $ abs_tr x (abs_tr f a) $ abs_tr f b; |
79 Syntax.const \<^const_syntax>\<open>letrec\<close> $ abs_tr x (abs_tr f a) $ abs_tr f b; |
121 [(\<^const_syntax>\<open>letrec\<close>, K letrec_tr'), |
125 [(\<^const_syntax>\<open>letrec\<close>, K letrec_tr'), |
122 (\<^const_syntax>\<open>letrec2\<close>, K letrec2_tr'), |
126 (\<^const_syntax>\<open>letrec2\<close>, K letrec2_tr'), |
123 (\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')] |
127 (\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')] |
124 end |
128 end |
125 \<close> |
129 \<close> |
126 syntax_consts |
|
127 "_letrec" == letrec and |
|
128 "_letrec2" == letrec2 and |
|
129 "_letrec3" == letrec3 |
|
130 |
130 |
131 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i" |
131 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i" |
132 where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)" |
132 where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)" |
133 |
133 |
134 definition nil :: "i" ("([])") |
134 definition nil :: "i" ("([])") |