author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45788  9049b24959de 
child 58880  0baae4311a9f 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/ex/Letrec.thy 
35932  2 
Author: Brian Huffman 
3 
*) 

4 

5 
header {* Recursive let bindings *} 

6 

7 
theory Letrec 

8 
imports HOLCF 

9 
begin 

10 

11 
definition 

45788
9049b24959de
HOLCF/ex/Letrec.thy: keep class 'domain' as default sort
huffman
parents:
42151
diff
changeset

12 
CLetrec :: "('a::pcpo \<rightarrow> 'a \<times> 'b::pcpo) \<rightarrow> 'b" where 
35932  13 
"CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))" 
14 

41229
d797baa3d57c
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
wenzelm
parents:
40774
diff
changeset

15 
nonterminal recbinds and recbindt and recbind 
35932  16 

17 
syntax 

41479  18 
"_recbind" :: "[logic, logic] \<Rightarrow> recbind" ("(2_ =/ _)" 10) 
35932  19 
"" :: "recbind \<Rightarrow> recbindt" ("_") 
20 
"_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" ("_,/ _") 

21 
"" :: "recbindt \<Rightarrow> recbinds" ("_") 

22 
"_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" ("_;/ _") 

41479  23 
"_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" ("(Letrec (_)/ in (_))" 10) 
35932  24 

25 
translations 

26 
(recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)" 

27 
(recbindt) "x = a, y = b" == (recbindt) "(x,y) = (a,b)" 

28 

29 
translations 

30 
"_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)" 

31 
"Letrec xs = a in (e,es)" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e,es))" 

32 
"Letrec xs = a in e" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e))" 

33 

34 
end 