author | huffman |
Tue, 03 Nov 2009 18:32:56 -0800 | |
changeset 33428 | 70ed971a79d1 |
parent 33401 | fc43fa403a69 |
child 35770 | a57ab2c01369 |
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 |
|
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
31008
diff
changeset
|
34 |
text {* Fixrec also works with the HOL pair constructor. *} |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
31008
diff
changeset
|
35 |
|
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
31008
diff
changeset
|
36 |
fixrec down2 :: "'a u \<times> 'b u \<rightarrow> 'a \<times> 'b" |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
31008
diff
changeset
|
37 |
where "down2\<cdot>(up\<cdot>x, up\<cdot>y) = (x, y)" |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
31008
diff
changeset
|
38 |
|
16554 | 39 |
|
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
40 |
subsection {* Examples using @{text fixrec_simp} *} |
16554 | 41 |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
42 |
text {* A type of lazy lists. *} |
16554 | 43 |
|
44 |
domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist") |
|
45 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
46 |
text {* A zip function for lazy lists. *} |
16554 | 47 |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
48 |
text {* Notice that the patterns are not exhaustive. *} |
16554 | 49 |
|
50 |
fixrec |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
51 |
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
|
52 |
where |
16554 | 53 |
"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
|
54 |
| "lzip\<cdot>lNil\<cdot>lNil = lNil" |
16554 | 55 |
|
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
56 |
text {* @{text fixrec_simp} is useful for producing strictness theorems. *} |
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
57 |
text {* Note that pattern matching is done in left-to-right order. *} |
16554 | 58 |
|
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
59 |
lemma lzip_stricts [simp]: |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
60 |
"lzip\<cdot>\<bottom>\<cdot>ys = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
61 |
"lzip\<cdot>lNil\<cdot>\<bottom> = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
62 |
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
63 |
by fixrec_simp+ |
16554 | 64 |
|
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
65 |
text {* @{text fixrec_simp} can also produce rules for missing cases. *} |
16554 | 66 |
|
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
67 |
lemma lzip_undefs [simp]: |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
68 |
"lzip\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
69 |
"lzip\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
70 |
by fixrec_simp+ |
16554 | 71 |
|
72 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
73 |
subsection {* Pattern matching with bottoms *} |
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 |
text {* |
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
76 |
As an alternative to using @{text fixrec_simp}, it is also possible |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
77 |
to use bottom as a constructor pattern. When using a bottom |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
78 |
pattern, the right-hand-side must also be bottom; otherwise, @{text |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
79 |
fixrec} will not be able to prove the equation. |
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
80 |
*} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
81 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
82 |
fixrec |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
83 |
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
|
84 |
where |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
85 |
"from_sinr_up\<cdot>\<bottom> = \<bottom>" |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
86 |
| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x" |
16554 | 87 |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
88 |
text {* |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
89 |
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
|
90 |
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
|
91 |
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
|
92 |
actually redundant, and could have been proven separately by |
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
93 |
@{text fixrec_simp}. |
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
94 |
*} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
95 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
96 |
text {* |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
97 |
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
|
98 |
certain argument, similar to a bang-pattern in Haskell. |
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 |
fixrec |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
102 |
seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
103 |
where |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
104 |
"seq\<cdot>\<bottom>\<cdot>y = \<bottom>" |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
105 |
| "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
|
106 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
107 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
108 |
subsection {* Skipping proofs of rewrite rules *} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
109 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
110 |
text {* Another zip function for lazy lists. *} |
16554 | 111 |
|
112 |
text {* |
|
113 |
Notice that this version has overlapping patterns. |
|
114 |
The second equation cannot be proved as a theorem |
|
115 |
because it only applies when the first pattern fails. |
|
116 |
*} |
|
117 |
||
118 |
fixrec (permissive) |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
119 |
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
|
120 |
where |
16554 | 121 |
"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
|
122 |
| "lzip2\<cdot>xs\<cdot>ys = lNil" |
16554 | 123 |
|
124 |
text {* |
|
125 |
Usually fixrec tries to prove all equations as theorems. |
|
126 |
The "permissive" option overrides this behavior, so fixrec |
|
127 |
does not produce any simp rules. |
|
128 |
*} |
|
129 |
||
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
130 |
text {* Simp rules can be generated later using @{text fixrec_simp}. *} |
16554 | 131 |
|
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
132 |
lemma lzip2_simps [simp]: |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
133 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot><x,y>\<cdot>(lzip\<cdot>xs\<cdot>ys)" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
134 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
135 |
"lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
136 |
"lzip2\<cdot>lNil\<cdot>lNil = lNil" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
137 |
by fixrec_simp+ |
16554 | 138 |
|
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
139 |
lemma lzip2_stricts [simp]: |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
140 |
"lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
141 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
142 |
by fixrec_simp+ |
16554 | 143 |
|
144 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
145 |
subsection {* Mutual recursion with @{text fixrec} *} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
146 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
147 |
text {* Tree and forest types. *} |
16554 | 148 |
|
149 |
domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest") |
|
150 |
and 'a forest = Empty | Trees (lazy "'a tree") "'a forest" |
|
151 |
||
152 |
text {* |
|
153 |
To define mutually recursive functions, separate the equations |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
154 |
for each function using the keyword @{text "and"}. |
16554 | 155 |
*} |
156 |
||
157 |
fixrec |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
158 |
map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)" |
16554 | 159 |
and |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
160 |
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
|
161 |
where |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
162 |
"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
|
163 |
| "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
|
164 |
| "map_forest\<cdot>f\<cdot>Empty = Empty" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
165 |
| "ts \<noteq> \<bottom> \<Longrightarrow> |
16554 | 166 |
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)" |
167 |
||
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
168 |
lemma map_tree_strict [simp]: "map_tree\<cdot>f\<cdot>\<bottom> = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
169 |
by fixrec_simp |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
170 |
|
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
171 |
lemma map_forest_strict [simp]: "map_forest\<cdot>f\<cdot>\<bottom> = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
172 |
by fixrec_simp |
16554 | 173 |
|
174 |
text {* |
|
175 |
Theorems generated: |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
176 |
@{text map_tree_def} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
177 |
@{text map_forest_def} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
178 |
@{text map_tree_unfold} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
179 |
@{text map_forest_unfold} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
180 |
@{text map_tree_simps} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
181 |
@{text map_forest_simps} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
182 |
@{text map_tree_map_forest_induct} |
16554 | 183 |
*} |
184 |
||
185 |
end |