src/HOL/HOLCF/ex/Letrec.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 45788 9049b24959de
child 62175 8ffc4d0e652d
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/ex/Letrec.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section {* 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