--- a/src/HOLCF/Cfun.thy Tue Mar 23 19:35:03 2010 +0100
+++ b/src/HOLCF/Cfun.thy Tue Mar 23 19:35:33 2010 +0100
@@ -547,17 +547,26 @@
lemma strictify2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strictify\<cdot>f\<cdot>x = f\<cdot>x"
by (simp add: strictify_conv_if)
-subsection {* Continuous let-bindings *}
+subsection {* Continuity of let-bindings *}
-definition
- CLet :: "'a \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'b" where
- "CLet = (\<Lambda> s f. f\<cdot>s)"
+lemma cont2cont_Let:
+ assumes f: "cont (\<lambda>x. f x)"
+ assumes g1: "\<And>y. cont (\<lambda>x. g x y)"
+ assumes g2: "\<And>x. cont (\<lambda>y. g x y)"
+ shows "cont (\<lambda>x. let y = f x in g x y)"
+unfolding Let_def using f g2 g1 by (rule cont_apply)
-syntax
- "_CLet" :: "[letbinds, 'a] => 'a" ("(Let (_)/ in (_))" 10)
-
-translations
- "_CLet (_binds b bs) e" == "_CLet b (_CLet bs e)"
- "Let x = a in e" == "CONST CLet\<cdot>a\<cdot>(\<Lambda> x. e)"
+lemma cont2cont_Let' [cont2cont]:
+ assumes f: "cont (\<lambda>x. f x)"
+ assumes g: "cont (\<lambda>p. g (fst p) (snd p))"
+ shows "cont (\<lambda>x. let y = f x in g x y)"
+using f
+proof (rule cont2cont_Let)
+ fix x show "cont (\<lambda>y. g x y)"
+ using g by (rule cont_fst_snd_D2)
+next
+ fix y show "cont (\<lambda>x. g x y)"
+ using g by (rule cont_fst_snd_D1)
+qed
end
--- a/src/HOLCF/Fix.thy Tue Mar 23 19:35:03 2010 +0100
+++ b/src/HOLCF/Fix.thy Tue Mar 23 19:35:33 2010 +0100
@@ -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 19:35:03 2010 +0100
+++ b/src/HOLCF/IsaMakefile Tue Mar 23 19:35:33 2010 +0100
@@ -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 19:35:33 2010 +0100
@@ -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 19:35:03 2010 +0100
+++ b/src/HOLCF/ex/ROOT.ML Tue Mar 23 19:35:33 2010 +0100
@@ -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"];