16554

1 
(* Title: HOLCF/ex/Fixrec_ex.thy


2 
ID: $Id$


3 
Author: Brian Huffman


4 
*)


5 


6 
header {* Fixrec package examples *}


7 


8 
theory Fixrec_ex


9 
imports HOLCF


10 
begin


11 


12 
subsection {* basic fixrec examples *}


13 


14 
text {*


15 
Fixrec patterns can mention any constructor defined by the domain


16 
package, as well as any of the following builtin constructors:


17 
cpair, spair, sinl, sinr, up, ONE, TT, FF.


18 
*}


19 


20 
text {* typical usage is with lazy constructors *}


21 


22 
consts down :: "'a u \<rightarrow> 'a"


23 
fixrec "down\<cdot>(up\<cdot>x) = x"


24 


25 
text {* with strict constructors, rewrite rules may require side conditions *}


26 


27 
consts from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a"


28 
fixrec "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x"


29 


30 
text {* lifting can turn a strict constructor into a lazy one *}


31 


32 
consts from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a"


33 
fixrec "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x"


34 


35 


36 
subsection {* fixpat examples *}


37 


38 
text {* a type of lazy lists *}


39 


40 
domain 'a llist = lNil  lCons (lazy 'a) (lazy "'a llist")


41 


42 
text {* zip function for lazy lists *}


43 


44 
consts lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"


45 


46 
text {* notice that the patterns are not exhaustive *}


47 


48 
fixrec


49 
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"


50 
"lzip\<cdot>lNil\<cdot>lNil = lNil"


51 


52 
text {* fixpat is useful for producing strictness theorems *}


53 
text {* note that pattern matching is done in lefttoright order *}


54 


55 
fixpat lzip_stricts [simp]:


56 
"lzip\<cdot>\<bottom>\<cdot>ys"


57 
"lzip\<cdot>lNil\<cdot>\<bottom>"


58 
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"


59 


60 
text {* fixpat can also produce rules for missing cases *}


61 


62 
fixpat lzip_undefs [simp]:


63 
"lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"


64 
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"


65 


66 


67 
subsection {* skipping proofs of rewrite rules *}


68 


69 
text {* another zip function for lazy lists *}


70 


71 
consts lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist"


72 


73 
text {*


74 
Notice that this version has overlapping patterns.


75 
The second equation cannot be proved as a theorem


76 
because it only applies when the first pattern fails.


77 
*}


78 


79 
fixrec (permissive)


80 
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)"


81 
"lzip2\<cdot>xs\<cdot>ys = lNil"


82 


83 
text {*


84 
Usually fixrec tries to prove all equations as theorems.


85 
The "permissive" option overrides this behavior, so fixrec


86 
does not produce any simp rules.


87 
*}


88 


89 
text {* simp rules can be generated later using fixpat *}


90 


91 
fixpat lzip2_simps [simp]:


92 
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys)"


93 
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil"


94 
"lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)"


95 
"lzip2\<cdot>lNil\<cdot>lNil"


96 


97 
fixpat lzip2_stricts [simp]:


98 
"lzip2\<cdot>\<bottom>\<cdot>ys"


99 
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>"


100 


101 
subsection {* mutual recursion with fixrec *}


102 


103 
text {* tree and forest types *}


104 


105 
domain 'a tree = Leaf (lazy 'a)  Branch (lazy "'a forest")


106 
and 'a forest = Empty  Trees (lazy "'a tree") "'a forest"


107 


108 
consts


109 
map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)"


110 
map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)"


111 


112 
text {*


113 
To define mutually recursive functions, separate the equations


114 
for each function using the keyword "and".


115 
*}


116 


117 
fixrec


118 
"map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)"


119 
"map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)"


120 
and


121 
"map_forest\<cdot>f\<cdot>Empty = Empty"


122 
"ts \<noteq> \<bottom> \<Longrightarrow>


123 
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)"


124 


125 
fixpat map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom>"


126 
fixpat map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom>"


127 


128 
text {*


129 
Theorems generated:


130 
map_tree_def map_forest_def


131 
map_tree_unfold map_forest_unfold


132 
map_tree_simps map_forest_simps


133 
map_tree_map_forest_induct


134 
*}


135 


136 
end
