Theory Letrec

```(*  Title:      HOL/HOLCF/ex/Letrec.thy
Author:     Brian Huffman
*)

section ‹Recursive let bindings›

theory Letrec
imports HOLCF
begin

definition
CLetrec :: "('a::pcpo → 'a × 'b::pcpo) → 'b" where
"CLetrec = (Λ F. snd (F⋅(μ x. fst (F⋅x))))"

nonterminal recbinds and recbindt and recbind

syntax
"_recbind"  :: "[logic, logic] ⇒ recbind"         ("(2_ =/ _)" 10)
""          :: "recbind ⇒ recbindt"               ("_")
"_recbindt" :: "[recbind, recbindt] ⇒ recbindt"   ("_,/ _")
""          :: "recbindt ⇒ recbinds"              ("_")
"_recbinds" :: "[recbindt, recbinds] ⇒ recbinds"  ("_;/ _")
"_Letrec"   :: "[recbinds, logic] ⇒ logic"        ("(Letrec (_)/ in (_))" 10)

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

translations
"_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)"
"Letrec xs = a in (e,es)"    == "CONST CLetrec⋅(Λ xs. (a,e,es))"
"Letrec xs = a in e"         == "CONST CLetrec⋅(Λ xs. (a,e))"

end
```