src/HOL/HOLCF/ex/Letrec.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45788 9049b24959de
child 58880 0baae4311a9f
permissions -rw-r--r--
Quotient_Info stores only relation maps
     1 (*  Title:      HOL/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 definition
    12   CLetrec :: "('a::pcpo \<rightarrow> 'a \<times> 'b::pcpo) \<rightarrow> 'b" where
    13   "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
    14 
    15 nonterminal recbinds and recbindt and recbind
    16 
    17 syntax
    18   "_recbind"  :: "[logic, logic] \<Rightarrow> recbind"         ("(2_ =/ _)" 10)
    19   ""          :: "recbind \<Rightarrow> recbindt"               ("_")
    20   "_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt"   ("_,/ _")
    21   ""          :: "recbindt \<Rightarrow> recbinds"              ("_")
    22   "_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds"  ("_;/ _")
    23   "_Letrec"   :: "[recbinds, logic] \<Rightarrow> logic"        ("(Letrec (_)/ in (_))" 10)
    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