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 built-in 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 left-to-right 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
|