(* Title: HOL/HOLCF/ex/Letrec.thy Author: Brian Huffman \<open>Recursive let bindings\<close> theory Letrecimports HOLCFbegin definition "('a::pcpo \ 'a \ 'b::pcpo) \ 'b" where "CLetrec = (\ F. snd (F\(\ x. fst (F\x))))" and recbindt and recbindsyntax "_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) "_Letrec" \<rightleftharpoons> CLetrec translations "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)" "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 quality 80%
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
