# HG changeset patch
# User huffman
# Date 1119557304 -7200
# Node ID 5841e7f9eef5ee1eabd21679d72358b1807ad68f
# Parent  aa36d41e4263fefb79427735d7ec27f44cc10c75
add new file to test fixrec package

diff -r aa36d41e4263 -r 5841e7f9eef5 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Thu Jun 23 22:07:30 2005 +0200
+++ b/src/HOLCF/IsaMakefile	Thu Jun 23 22:08:24 2005 +0200
@@ -58,7 +58,7 @@
 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Dagstuhl.ML ex/Dagstuhl.thy \
   ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \
   ex/Focus_ex.thy ex/Hoare.ML ex/Hoare.thy ex/Loop.ML ex/Loop.thy \
-  ex/ROOT.ML ex/loeckx.ML \
+  ex/ROOT.ML ex/loeckx.ML ex/Fixrec_ex.thy \
   ../HOL/Library/Nat_Infinity.thy 
 	@$(ISATOOL) usedir $(OUT)/HOLCF ex
 
diff -r aa36d41e4263 -r 5841e7f9eef5 src/HOLCF/ex/Fixrec_ex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Fixrec_ex.thy	Thu Jun 23 22:08:24 2005 +0200
@@ -0,0 +1,136 @@
+(*  Title:      HOLCF/ex/Fixrec_ex.thy
+    ID:         $Id$
+    Author:     Brian Huffman
+*)
+
+header {* Fixrec package examples *}
+
+theory Fixrec_ex
+imports HOLCF
+begin
+
+subsection {* basic fixrec examples *}
+
+text {*
+  Fixrec patterns can mention any constructor defined by the domain
+  package, as well as any of the following built-in constructors:
+  cpair, spair, sinl, sinr, up, ONE, TT, FF.
+*}
+
+text {* typical usage is with lazy constructors *}
+
+consts down :: "'a u \<rightarrow> 'a"
+fixrec "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"
+
+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"
+
+
+subsection {* fixpat examples *}
+
+text {* a type of lazy lists *}
+
+domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist")
+
+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\<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"
+
+text {* fixpat is useful for producing strictness theorems *}
+text {* note that pattern matching is done in left-to-right order *}
+
+fixpat lzip_stricts [simp]:
+  "lzip\<cdot>\<bottom>\<cdot>ys"
+  "lzip\<cdot>lNil\<cdot>\<bottom>"
+  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
+
+text {* fixpat can also produce rules for missing cases *}
+
+fixpat lzip_undefs [simp]:
+  "lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
+  "lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
+
+
+subsection {* skipping proofs of rewrite rules *}
+
+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
+  because it only applies when the first pattern fails.
+*}
+
+fixrec (permissive)
+  "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"
+
+text {*
+  Usually fixrec tries to prove all equations as theorems.
+  The "permissive" option overrides this behavior, so fixrec
+  does not produce any simp rules.
+*}
+
+text {* simp rules can be generated later using fixpat *}
+
+fixpat lzip2_simps [simp]:
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys)"
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"
+  "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"
+  "lzip2\<cdot>lNil\<cdot>lNil"
+
+fixpat lzip2_stricts [simp]:
+  "lzip2\<cdot>\<bottom>\<cdot>ys"
+  "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"
+
+subsection {* mutual recursion with fixrec *}
+
+text {* tree and forest types *}
+
+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)"
+and
+  "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>"
+fixpat map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom>"
+
+text {*
+  Theorems generated:
+  map_tree_def map_forest_def
+  map_tree_unfold map_forest_unfold
+  map_tree_simps map_forest_simps
+  map_tree_map_forest_induct
+*}
+
+end
diff -r aa36d41e4263 -r 5841e7f9eef5 src/HOLCF/ex/ROOT.ML
--- a/src/HOLCF/ex/ROOT.ML	Thu Jun 23 22:07:30 2005 +0200
+++ b/src/HOLCF/ex/ROOT.ML	Thu Jun 23 22:08:24 2005 +0200
@@ -12,3 +12,4 @@
 time_use_thy "Hoare";
 time_use_thy "Loop";
 time_use "loeckx.ML";
+time_use_thy "Fixrec_ex";