(* 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