src/HOLCF/ex/Fixrec_ex.thy

--- a/src/HOLCF/ex/Fixrec_ex.thy	Fri Feb 27 18:34:20 2009 -0800
+++ b/src/HOLCF/ex/Fixrec_ex.thy	Fri Feb 27 19:05:46 2009 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/ex/Fixrec_ex.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -19,18 +18,18 @@
 
 text {* typical usage is with lazy constructors *}
 
-consts down :: "'a u \<rightarrow> 'a"
-fixrec "down\<cdot>(up\<cdot>x) = x"
+fixrec down :: "'a u \<rightarrow> 'a"
+where "down\<cdot>(up\<cdot>x) = x"
 
 text {* with strict constructors, rewrite rules may require side conditions *}
 
-consts from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
-fixrec "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
+fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"
+where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"
 
 text {* lifting can turn a strict constructor into a lazy one *}
 
-consts from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
-fixrec "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
+fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"
+where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"
 
 
 subsection {* fixpat examples *}
@@ -41,13 +40,13 @@
 
 text {* zip function for lazy lists *}
 
-consts lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
-
 text {* notice that the patterns are not exhaustive *}
 
 fixrec
+  lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
+where
   "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
-  "lzip\<cdot>lNil\<cdot>lNil = lNil"
+| "lzip\<cdot>lNil\<cdot>lNil = lNil"
 
 text {* fixpat is useful for producing strictness theorems *}
 text {* note that pattern matching is done in left-to-right order *}
@@ -68,8 +67,6 @@
 
 text {* another zip function for lazy lists *}
 
-consts lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
-
 text {*
   Notice that this version has overlapping patterns.
   The second equation cannot be proved as a theorem
@@ -77,8 +74,10 @@
 *}
 
 fixrec (permissive)
+  lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"
+where
   "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"
-  "lzip2\<cdot>xs\<cdot>ys = lNil"
+| "lzip2\<cdot>xs\<cdot>ys = lNil"
 
 text {*
   Usually fixrec tries to prove all equations as theorems.
@@ -105,21 +104,20 @@
 domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest")
 and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
 
-consts
-  map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
-  map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
-
 text {*
   To define mutually recursive functions, separate the equations
   for each function using the keyword "and".
 *}
 
 fixrec
-  "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
-  "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
+  map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"
 and
-  "map_forest\<cdot>f\<cdot>Empty = Empty"
-  "ts \<noteq> \<bottom> \<Longrightarrow>
+  map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"
+where
+  "map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"
+| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"
+| "map_forest\<cdot>f\<cdot>Empty = Empty"
+| "ts \<noteq> \<bottom> \<Longrightarrow>
     map_forest\<cdot>f\<cdot>(Trees\<cdot>t\<cdot>ts) = Trees\<cdot>(map_tree\<cdot>f\<cdot>t)\<cdot>(map_forest\<cdot>f\<cdot>ts)"
 
 fixpat map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom>"