author | huffman |
Tue, 19 Oct 2010 16:21:24 -0700 | |
changeset 40041 | 1f09b4c7b85e |
parent 37000 | 41a22e7c1145 |
child 40213 | b63e966564da |
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: |
|
35925 | 16 |
Pair, spair, sinl, sinr, up, ONE, TT, FF. |
16554 | 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 |
35925 | 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 |
||
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
37000
diff
changeset
|
118 |
fixrec |
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 |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
37000
diff
changeset
|
121 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip2\<cdot>xs\<cdot>ys)" |
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
37000
diff
changeset
|
122 |
| (unchecked) "lzip2\<cdot>xs\<cdot>ys = lNil" |
16554 | 123 |
|
124 |
text {* |
|
125 |
Usually fixrec tries to prove all equations as theorems. |
|
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
37000
diff
changeset
|
126 |
The "unchecked" option overrides this behavior, so fixrec |
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
37000
diff
changeset
|
127 |
does not attempt to prove that particular equation. |
16554 | 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>lNil = lNil" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
134 |
"lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
135 |
"lzip2\<cdot>lNil\<cdot>lNil = lNil" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
136 |
by fixrec_simp+ |
16554 | 137 |
|
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
138 |
lemma lzip2_stricts [simp]: |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
139 |
"lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
140 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
141 |
by fixrec_simp+ |
16554 | 142 |
|
143 |
||
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
144 |
subsection {* Mutual recursion with @{text fixrec} *} |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
145 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
146 |
text {* Tree and forest types. *} |
16554 | 147 |
|
148 |
domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest") |
|
149 |
and 'a forest = Empty | Trees (lazy "'a tree") "'a forest" |
|
150 |
||
151 |
text {* |
|
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
152 |
To define mutually recursive functions, give multiple type signatures |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
153 |
separated by the keyword @{text "and"}. |
16554 | 154 |
*} |
155 |
||
156 |
fixrec |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
157 |
map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)" |
16554 | 158 |
and |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
159 |
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
|
160 |
where |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
161 |
"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
|
162 |
| "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
|
163 |
| "map_forest\<cdot>f\<cdot>Empty = Empty" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
164 |
| "ts \<noteq> \<bottom> \<Longrightarrow> |
16554 | 165 |
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)" |
166 |
||
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
167 |
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
|
168 |
by fixrec_simp |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
169 |
|
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
170 |
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
|
171 |
by fixrec_simp |
16554 | 172 |
|
37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
36997
diff
changeset
|
173 |
(* |
16554 | 174 |
Theorems generated: |
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
175 |
@{text map_tree_def} @{thm map_tree_def} |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
176 |
@{text map_forest_def} @{thm map_forest_def} |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
177 |
@{text map_tree.unfold} @{thm map_tree.unfold} |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
178 |
@{text map_forest.unfold} @{thm map_forest.unfold} |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
179 |
@{text map_tree.simps} @{thm map_tree.simps} |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
180 |
@{text map_forest.simps} @{thm map_forest.simps} |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
181 |
@{text map_tree_map_forest.induct} @{thm map_tree_map_forest.induct} |
37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
36997
diff
changeset
|
182 |
*) |
16554 | 183 |
|
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
184 |
|
36997
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
185 |
subsection {* Looping simp rules *} |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
186 |
|
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
187 |
text {* |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
188 |
The defining equations of a fixrec definition are declared as simp |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
189 |
rules by default. In some cases, especially for constants with no |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
190 |
arguments or functions with variable patterns, the defining |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
191 |
equations may cause the simplifier to loop. In these cases it will |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
192 |
be necessary to use a @{text "[simp del]"} declaration. |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
193 |
*} |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
194 |
|
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
195 |
fixrec |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
196 |
repeat :: "'a \<rightarrow> 'a llist" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
197 |
where |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
198 |
[simp del]: "repeat\<cdot>x = lCons\<cdot>x\<cdot>(repeat\<cdot>x)" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
199 |
|
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
200 |
text {* |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
201 |
We can derive other non-looping simp rules for @{const repeat} by |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
202 |
using the @{text subst} method with the @{text repeat.simps} rule. |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
203 |
*} |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
204 |
|
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
205 |
lemma repeat_simps [simp]: |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
206 |
"repeat\<cdot>x \<noteq> \<bottom>" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
207 |
"repeat\<cdot>x \<noteq> lNil" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
208 |
"repeat\<cdot>x = lCons\<cdot>y\<cdot>ys \<longleftrightarrow> x = y \<and> repeat\<cdot>x = ys" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
209 |
by (subst repeat.simps, simp)+ |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
210 |
|
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
211 |
lemma llist_when_repeat [simp]: |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
212 |
"llist_when\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
213 |
by (subst repeat.simps, simp) |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
214 |
|
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
215 |
text {* |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
216 |
For mutually-recursive constants, looping might only occur if all |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
217 |
equations are in the simpset at the same time. In such cases it may |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
218 |
only be necessary to declare @{text "[simp del]"} on one equation. |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
219 |
*} |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
220 |
|
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
221 |
fixrec |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
222 |
inf_tree :: "'a tree" and inf_forest :: "'a forest" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
223 |
where |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
224 |
[simp del]: "inf_tree = Branch\<cdot>inf_forest" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
225 |
| "inf_forest = Trees\<cdot>inf_tree\<cdot>(Trees\<cdot>inf_tree\<cdot>Empty)" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
226 |
|
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
227 |
|
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
228 |
subsection {* Using @{text fixrec} inside locales *} |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
229 |
|
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
230 |
locale test = |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
231 |
fixes foo :: "'a \<rightarrow> 'a" |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
232 |
assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>" |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
233 |
begin |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
234 |
|
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
235 |
fixrec |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
236 |
bar :: "'a u \<rightarrow> 'a" |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
237 |
where |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
238 |
"bar\<cdot>(up\<cdot>x) = foo\<cdot>x" |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
239 |
|
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
240 |
lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>" |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
241 |
by fixrec_simp |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
242 |
|
16554 | 243 |
end |
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
244 |
|
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
245 |
end |