author | huffman |
Mon, 27 Apr 2009 19:44:30 -0700 | |
changeset 31008 | b8f4e351b5bf |
parent 30158 | 83c50c62cf23 |
child 33401 | fc43fa403a69 |
permissions | -rw-r--r-- |
16554 | 1 |
(* Title: HOLCF/ex/Fixrec_ex.thy |
2 |
Author: Brian Huffman |
|
3 |
*) |
|
4 |
||
5 |
header {* Fixrec package examples *} |
|
6 |
||
7 |
theory Fixrec_ex |
|
8 |
imports HOLCF |
|
9 |
begin |
|
10 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
11 |
subsection {* Basic @{text fixrec} examples *} |
16554 | 12 |
|
13 |
text {* |
|
14 |
Fixrec patterns can mention any constructor defined by the domain |
|
15 |
package, as well as any of the following built-in constructors: |
|
16 |
cpair, spair, sinl, sinr, up, ONE, TT, FF. |
|
17 |
*} |
|
18 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
19 |
text {* Typical usage is with lazy constructors. *} |
16554 | 20 |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
21 |
fixrec down :: "'a u \<rightarrow> 'a" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
22 |
where "down\<cdot>(up\<cdot>x) = x" |
16554 | 23 |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
24 |
text {* With strict constructors, rewrite rules may require side conditions. *} |
16554 | 25 |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
26 |
fixrec from_sinl :: "'a \<oplus> 'b \<rightarrow> 'a" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
27 |
where "x \<noteq> \<bottom> \<Longrightarrow> from_sinl\<cdot>(sinl\<cdot>x) = x" |
16554 | 28 |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
29 |
text {* Lifting can turn a strict constructor into a lazy one. *} |
16554 | 30 |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
31 |
fixrec from_sinl_up :: "'a u \<oplus> 'b \<rightarrow> 'a" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
32 |
where "from_sinl_up\<cdot>(sinl\<cdot>(up\<cdot>x)) = x" |
16554 | 33 |
|
34 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
35 |
subsection {* Examples using @{text fixpat} *} |
16554 | 36 |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
37 |
text {* A type of lazy lists. *} |
16554 | 38 |
|
39 |
domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist") |
|
40 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
41 |
text {* A zip function for lazy lists. *} |
16554 | 42 |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
43 |
text {* Notice that the patterns are not exhaustive. *} |
16554 | 44 |
|
45 |
fixrec |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
46 |
lzip :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
47 |
where |
16554 | 48 |
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)" |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
49 |
| "lzip\<cdot>lNil\<cdot>lNil = lNil" |
16554 | 50 |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
51 |
text {* @{text fixpat} is useful for producing strictness theorems. *} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
52 |
text {* Note that pattern matching is done in left-to-right order. *} |
16554 | 53 |
|
54 |
fixpat lzip_stricts [simp]: |
|
55 |
"lzip\<cdot>\<bottom>\<cdot>ys" |
|
56 |
"lzip\<cdot>lNil\<cdot>\<bottom>" |
|
57 |
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>" |
|
58 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
59 |
text {* @{text fixpat} can also produce rules for missing cases. *} |
16554 | 60 |
|
61 |
fixpat lzip_undefs [simp]: |
|
62 |
"lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)" |
|
63 |
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil" |
|
64 |
||
65 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
66 |
subsection {* Pattern matching with bottoms *} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
67 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
68 |
text {* |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
69 |
As an alternative to using @{text fixpat}, it is also possible to |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
70 |
use bottom as a constructor pattern. When using a bottom pattern, |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
71 |
the right-hand-side must also be bottom; otherwise, @{text fixrec} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
72 |
will not be able to prove the equation. |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
73 |
*} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
74 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
75 |
fixrec |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
76 |
from_sinr_up :: "'a \<oplus> 'b\<^sub>\<bottom> \<rightarrow> 'b" |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
77 |
where |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
78 |
"from_sinr_up\<cdot>\<bottom> = \<bottom>" |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
79 |
| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x" |
16554 | 80 |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
81 |
text {* |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
82 |
If the function is already strict in that argument, then the bottom |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
83 |
pattern does not change the meaning of the function. For example, |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
84 |
in the definition of @{term from_sinr_up}, the first equation is |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
85 |
actually redundant, and could have been proven separately by |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
86 |
@{text fixpat}. |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
87 |
*} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
88 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
89 |
text {* |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
90 |
A bottom pattern can also be used to make a function strict in a |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
91 |
certain argument, similar to a bang-pattern in Haskell. |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
92 |
*} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
93 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
94 |
fixrec |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
95 |
seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
96 |
where |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
97 |
"seq\<cdot>\<bottom>\<cdot>y = \<bottom>" |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
98 |
| "x \<noteq> \<bottom> \<Longrightarrow> seq\<cdot>x\<cdot>y = y" |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
99 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
100 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
101 |
subsection {* Skipping proofs of rewrite rules *} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
102 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
103 |
text {* Another zip function for lazy lists. *} |
16554 | 104 |
|
105 |
text {* |
|
106 |
Notice that this version has overlapping patterns. |
|
107 |
The second equation cannot be proved as a theorem |
|
108 |
because it only applies when the first pattern fails. |
|
109 |
*} |
|
110 |
||
111 |
fixrec (permissive) |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
112 |
lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
113 |
where |
16554 | 114 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)" |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
115 |
| "lzip2\<cdot>xs\<cdot>ys = lNil" |
16554 | 116 |
|
117 |
text {* |
|
118 |
Usually fixrec tries to prove all equations as theorems. |
|
119 |
The "permissive" option overrides this behavior, so fixrec |
|
120 |
does not produce any simp rules. |
|
121 |
*} |
|
122 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
123 |
text {* Simp rules can be generated later using @{text fixpat}. *} |
16554 | 124 |
|
125 |
fixpat lzip2_simps [simp]: |
|
126 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys)" |
|
127 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil" |
|
128 |
"lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys)" |
|
129 |
"lzip2\<cdot>lNil\<cdot>lNil" |
|
130 |
||
131 |
fixpat lzip2_stricts [simp]: |
|
132 |
"lzip2\<cdot>\<bottom>\<cdot>ys" |
|
133 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom>" |
|
134 |
||
135 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
136 |
subsection {* Mutual recursion with @{text fixrec} *} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
137 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
138 |
text {* Tree and forest types. *} |
16554 | 139 |
|
140 |
domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest") |
|
141 |
and 'a forest = Empty | Trees (lazy "'a tree") "'a forest" |
|
142 |
||
143 |
text {* |
|
144 |
To define mutually recursive functions, separate the equations |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
145 |
for each function using the keyword @{text "and"}. |
16554 | 146 |
*} |
147 |
||
148 |
fixrec |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
149 |
map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)" |
16554 | 150 |
and |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
151 |
map_forest :: "('a \<rightarrow> 'b) \<rightarrow> ('a forest \<rightarrow> 'b forest)" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
152 |
where |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
153 |
"map_tree\<cdot>f\<cdot>(Leaf\<cdot>x) = Leaf\<cdot>(f\<cdot>x)" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
154 |
| "map_tree\<cdot>f\<cdot>(Branch\<cdot>ts) = Branch\<cdot>(map_forest\<cdot>f\<cdot>ts)" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
155 |
| "map_forest\<cdot>f\<cdot>Empty = Empty" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
156 |
| "ts \<noteq> \<bottom> \<Longrightarrow> |
16554 | 157 |
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)" |
158 |
||
159 |
fixpat map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom>" |
|
160 |
fixpat map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom>" |
|
161 |
||
162 |
text {* |
|
163 |
Theorems generated: |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
164 |
@{text map_tree_def} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
165 |
@{text map_forest_def} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
166 |
@{text map_tree_unfold} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
167 |
@{text map_forest_unfold} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
168 |
@{text map_tree_simps} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
169 |
@{text map_forest_simps} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
170 |
@{text map_tree_map_forest_induct} |
16554 | 171 |
*} |
172 |
||
173 |
end |