Quelle  Letrec.thy

(*  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"         (‹(‹indent=2 notation=‹mixfix Letrec binding›\›_ =/ _)› 10)
  ""          :: "recbind ==> recbindt"               (‹_›)
  "_recbindt" :: "[recbind, recbindt] ==> recbindt"   (‹_,/ _›)
  ""          :: "recbindt ==> recbinds"              (‹_›)
  "_recbinds" :: "[recbindt, recbinds] ==> recbinds"  (‹_;/ _›)
  "_Letrec"   :: "[recbinds, logic] ==> logic"        (‹(‹notation=‹mixfix Letrec expression›\›Letrec (_)/ in (_))› 10)

syntax_consts
  "_Letrec" ⇌ CLetrec

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