--- a/src/HOLCF/Fix.thy Tue Mar 23 16:18:44 2010 +0100
+++ b/src/HOLCF/Fix.thy Tue Mar 23 09:39:21 2010 -0700
@@ -203,31 +203,7 @@
by (simp add: fix_def2)
qed
-subsection {* Recursive let bindings *}
-
-definition
- CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
- "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
-
-nonterminals
- recbinds recbindt recbind
-
-syntax
- "_recbind" :: "['a, 'a] \<Rightarrow> recbind" ("(2_ =/ _)" 10)
- "" :: "recbind \<Rightarrow> recbindt" ("_")
- "_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" ("_,/ _")
- "" :: "recbindt \<Rightarrow> recbinds" ("_")
- "_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" ("_;/ _")
- "_Letrec" :: "[recbinds, 'a] \<Rightarrow> '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)" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e,es))"
- "Letrec xs = a in e" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e))"
+subsection {* Fixed-points on product types *}
text {*
Bekic's Theorem: Simultaneous fixed points over pairs
--- a/src/HOLCF/IsaMakefile Tue Mar 23 16:18:44 2010 +0100
+++ b/src/HOLCF/IsaMakefile Tue Mar 23 09:39:21 2010 -0700
@@ -101,6 +101,7 @@
ex/Fixrec_ex.thy \
ex/Focus_ex.thy \
ex/Hoare.thy \
+ ex/Letrec.thy \
ex/Loop.thy \
ex/New_Domain.thy \
ex/Powerdomain_ex.thy \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Letrec.thy Tue Mar 23 09:39:21 2010 -0700
@@ -0,0 +1,37 @@
+(* Title: HOLCF/ex/Letrec.thy
+ Author: Brian Huffman
+*)
+
+header {* Recursive let bindings *}
+
+theory Letrec
+imports HOLCF
+begin
+
+defaultsort pcpo
+
+definition
+ CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
+ "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
+
+nonterminals
+ recbinds recbindt recbind
+
+syntax
+ "_recbind" :: "['a, 'a] \<Rightarrow> recbind" ("(2_ =/ _)" 10)
+ "" :: "recbind \<Rightarrow> recbindt" ("_")
+ "_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" ("_,/ _")
+ "" :: "recbindt \<Rightarrow> recbinds" ("_")
+ "_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" ("_;/ _")
+ "_Letrec" :: "[recbinds, 'a] \<Rightarrow> '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)" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e,es))"
+ "Letrec xs = a in e" == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e))"
+
+end
--- a/src/HOLCF/ex/ROOT.ML Tue Mar 23 16:18:44 2010 +0100
+++ b/src/HOLCF/ex/ROOT.ML Tue Mar 23 09:39:21 2010 -0700
@@ -5,5 +5,6 @@
use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare",
"Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex", "Domain_Proofs",
+ "Letrec",
"Strict_Fun",
"New_Domain"];