35932
|
1 |
(* Title: HOLCF/ex/Letrec.thy
|
|
2 |
Author: Brian Huffman
|
|
3 |
*)
|
|
4 |
|
|
5 |
header {* Recursive let bindings *}
|
|
6 |
|
|
7 |
theory Letrec
|
|
8 |
imports HOLCF
|
|
9 |
begin
|
|
10 |
|
|
11 |
defaultsort pcpo
|
|
12 |
|
|
13 |
definition
|
|
14 |
CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
|
|
15 |
"CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
|
|
16 |
|
|
17 |
nonterminals
|
|
18 |
recbinds recbindt recbind
|
|
19 |
|
|
20 |
syntax
|
|
21 |
"_recbind" :: "['a, 'a] \<Rightarrow> recbind" ("(2_ =/ _)" 10)
|
|
22 |
"" :: "recbind \<Rightarrow> recbindt" ("_")
|
|
23 |
"_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" ("_,/ _")
|
|
24 |
"" :: "recbindt \<Rightarrow> recbinds" ("_")
|
|
25 |
"_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" ("_;/ _")
|
|
26 |
"_Letrec" :: "[recbinds, 'a] \<Rightarrow> 'a" ("(Letrec (_)/ in (_))" 10)
|
|
27 |
|
|
28 |
translations
|
|
29 |
(recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
|
|
30 |
(recbindt) "x = a, y = b" == (recbindt) "(x,y) = (a,b)"
|
|
31 |
|
|
32 |
translations
|
|
33 |
"_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)"
|
|
34 |
"Letrec xs = a in (e,es)" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e,es))"
|
|
35 |
"Letrec xs = a in e" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e))"
|
|
36 |
|
|
37 |
end
|