src/HOL/HOLCF/ex/Letrec.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 36452 src/HOLCF/ex/Letrec.thy@d37c6eed8117
child 41229 d797baa3d57c
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
     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 default_sort 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