# HG changeset patch # User huffman # Date 1131223933 -3600 # Node ID 587692219f69d47a31aa085dd127da0762a9eff8 # Parent 2c5d5da79a1eb823a08e2d4643ef9f25d98c732c put iterate and fix in separate sections; added Letrec diff -r 2c5d5da79a1e -r 587692219f69 src/HOLCF/Fix.thy --- a/src/HOLCF/Fix.thy Sat Nov 05 21:50:37 2005 +0100 +++ b/src/HOLCF/Fix.thy Sat Nov 05 21:52:13 2005 +0100 @@ -13,33 +13,16 @@ defaultsort pcpo -subsection {* Definitions *} +subsection {* Iteration *} consts - iterate :: "nat \ ('a \ 'a) \ 'a \ 'a" - "fix" :: "('a \ 'a) \ 'a" + iterate :: "nat \ ('a::cpo \ 'a) \ ('a \ 'a)" primrec "iterate 0 = (\ F x. x)" "iterate (Suc n) = (\ F x. F\(iterate n\F\x))" -defs - fix_def: "fix \ \ F. \i. iterate i\F\\" - -subsection {* Binder syntax for @{term fix} *} - -syntax - "_FIX" :: "['a, 'a] \ 'a" ("(3FIX _./ _)" [1000, 10] 10) - -syntax (xsymbols) - "_FIX" :: "['a, 'a] \ 'a" ("(3\_./ _)" [1000, 10] 10) - -translations - "\ x. t" == "fix\(\ x. t)" - -subsection {* Properties of @{term iterate} *} - -text {* derive inductive properties of iterate from primitive recursion *} +text {* Derive inductive properties of iterate from primitive recursion *} lemma iterate_0 [simp]: "iterate 0\F\x = x" by simp @@ -63,7 +46,25 @@ lemma chain_iterate [simp]: "chain (\i. iterate i\F\\)" by (rule chain_iterate2 [OF minimal]) -subsection {* Properties of @{term fix} *} + +subsection {* Least fixed point operator *} + +constdefs + "fix" :: "('a \ 'a) \ 'a" + "fix \ \ F. \i. iterate i\F\\" + +text {* Binder syntax for @{term fix} *} + +syntax + "_FIX" :: "['a, 'a] \ 'a" ("(3FIX _./ _)" [1000, 10] 10) + +syntax (xsymbols) + "_FIX" :: "['a, 'a] \ 'a" ("(3\_./ _)" [1000, 10] 10) + +translations + "\ x. t" == "fix\(\ x. t)" + +text {* Properties of @{term fix} *} text {* direct connection between @{term fix} and iteration *} @@ -163,6 +164,32 @@ "\f \ fix\F; adm P; P \; \x. P x \ P (F\x)\ \ P f" by (simp add: fix_ind) +subsection {* Recursive let bindings *} + +constdefs + CLetrec :: "('a \ 'a \ 'b) \ 'b" + "CLetrec \ \ F. csnd\(F\(\ x. cfst\(F\x)))" + +nonterminals + recbinds recbindt recbind + +syntax + "_recbind" :: "['a, 'a] \ recbind" ("(2_ =/ _)" 10) + "" :: "recbind \ recbindt" ("_") + "_recbindt" :: "[recbind, recbindt] \ recbindt" ("_,/ _") + "" :: "recbindt \ recbinds" ("_") + "_recbinds" :: "[recbindt, recbinds] \ recbinds" ("_;/ _") + "_Letrec" :: "[recbinds, 'a] \ 'a" ("(Letrec (_)/ in (_))" 10) + +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\" == "CLetrec\(\ xs. \a,e,es\)" + "Letrec xs = a in e" == "CLetrec\(\ xs. \a,e\)" + subsection {* Weak admissibility *} constdefs