# HG changeset patch
# User huffman
# Date 1269362361 25200
# Node ID 86559356502de5f7004c8c6affd666b8418ab0db
# Parent  90f38c8831e2b65f9ddbaa334d492a591882911d
move letrec stuff to new file HOLCF/ex/Letrec.thy

diff -r 90f38c8831e2 -r 86559356502d src/HOLCF/Fix.thy
--- 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
diff -r 90f38c8831e2 -r 86559356502d src/HOLCF/IsaMakefile
--- 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 \
diff -r 90f38c8831e2 -r 86559356502d src/HOLCF/ex/Letrec.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
diff -r 90f38c8831e2 -r 86559356502d src/HOLCF/ex/ROOT.ML
--- 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"];