author | wenzelm |
Sat, 24 Mar 2018 20:51:42 +0100 | |
changeset 67945 | 984c3dc46cc0 |
parent 62175 | 8ffc4d0e652d |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tutorial/Fixrec_ex.thy |
16554 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
62175 | 5 |
section \<open>Fixrec package examples\<close> |
16554 | 6 |
|
7 |
theory Fixrec_ex |
|
8 |
imports HOLCF |
|
9 |
begin |
|
10 |
||
62175 | 11 |
subsection \<open>Basic \<open>fixrec\<close> examples\<close> |
16554 | 12 |
|
62175 | 13 |
text \<open> |
16554 | 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. |
62175 | 17 |
\<close> |
16554 | 18 |
|
62175 | 19 |
text \<open>Typical usage is with lazy constructors.\<close> |
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 |
|
62175 | 24 |
text \<open>With strict constructors, rewrite rules may require side conditions.\<close> |
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 |
|
62175 | 29 |
text \<open>Lifting can turn a strict constructor into a lazy one.\<close> |
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 |
|
62175 | 34 |
text \<open>Fixrec also works with the HOL pair constructor.\<close> |
33401
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 |
|
62175 | 40 |
subsection \<open>Examples using \<open>fixrec_simp\<close>\<close> |
16554 | 41 |
|
62175 | 42 |
text \<open>A type of lazy lists.\<close> |
16554 | 43 |
|
44 |
domain 'a llist = lNil | lCons (lazy 'a) (lazy "'a llist") |
|
45 |
||
62175 | 46 |
text \<open>A zip function for lazy lists.\<close> |
16554 | 47 |
|
62175 | 48 |
text \<open>Notice that the patterns are not exhaustive.\<close> |
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 |
|
62175 | 56 |
text \<open>\<open>fixrec_simp\<close> is useful for producing strictness theorems.\<close> |
57 |
text \<open>Note that pattern matching is done in left-to-right order.\<close> |
|
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 |
|
62175 | 65 |
text \<open>\<open>fixrec_simp\<close> can also produce rules for missing cases.\<close> |
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 |
||
62175 | 73 |
subsection \<open>Pattern matching with bottoms\<close> |
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
74 |
|
62175 | 75 |
text \<open> |
76 |
As an alternative to using \<open>fixrec_simp\<close>, it is also possible |
|
33428
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 |
62175 | 78 |
pattern, the right-hand-side must also be bottom; otherwise, \<open>fixrec\<close> will not be able to prove the equation. |
79 |
\<close> |
|
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 |
fixrec |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
82 |
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
|
83 |
where |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
84 |
"from_sinr_up\<cdot>\<bottom> = \<bottom>" |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
85 |
| "from_sinr_up\<cdot>(sinr\<cdot>(up\<cdot>x)) = x" |
16554 | 86 |
|
62175 | 87 |
text \<open> |
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
88 |
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
|
89 |
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
|
90 |
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
|
91 |
actually redundant, and could have been proven separately by |
62175 | 92 |
\<open>fixrec_simp\<close>. |
93 |
\<close> |
|
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
94 |
|
62175 | 95 |
text \<open> |
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
96 |
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
|
97 |
certain argument, similar to a bang-pattern in Haskell. |
62175 | 98 |
\<close> |
31008
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 |
fixrec |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
101 |
seq :: "'a \<rightarrow> 'b \<rightarrow> 'b" |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
102 |
where |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
103 |
"seq\<cdot>\<bottom>\<cdot>y = \<bottom>" |
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
104 |
| "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
|
105 |
|
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
106 |
|
62175 | 107 |
subsection \<open>Skipping proofs of rewrite rules\<close> |
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
108 |
|
62175 | 109 |
text \<open>Another zip function for lazy lists.\<close> |
16554 | 110 |
|
62175 | 111 |
text \<open> |
16554 | 112 |
Notice that this version has overlapping patterns. |
113 |
The second equation cannot be proved as a theorem |
|
114 |
because it only applies when the first pattern fails. |
|
62175 | 115 |
\<close> |
16554 | 116 |
|
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
37000
diff
changeset
|
117 |
fixrec |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
118 |
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
|
119 |
where |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
37000
diff
changeset
|
120 |
"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
|
121 |
| (unchecked) "lzip2\<cdot>xs\<cdot>ys = lNil" |
16554 | 122 |
|
62175 | 123 |
text \<open> |
16554 | 124 |
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
|
125 |
The "unchecked" option overrides this behavior, so fixrec |
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
37000
diff
changeset
|
126 |
does not attempt to prove that particular equation. |
62175 | 127 |
\<close> |
16554 | 128 |
|
62175 | 129 |
text \<open>Simp rules can be generated later using \<open>fixrec_simp\<close>.\<close> |
16554 | 130 |
|
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
131 |
lemma lzip2_simps [simp]: |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
132 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
133 |
"lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
134 |
"lzip2\<cdot>lNil\<cdot>lNil = lNil" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
135 |
by fixrec_simp+ |
16554 | 136 |
|
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
137 |
lemma lzip2_stricts [simp]: |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
138 |
"lzip2\<cdot>\<bottom>\<cdot>ys = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
139 |
"lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>\<bottom> = \<bottom>" |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
140 |
by fixrec_simp+ |
16554 | 141 |
|
142 |
||
62175 | 143 |
subsection \<open>Mutual recursion with \<open>fixrec\<close>\<close> |
31008
b8f4e351b5bf
add proper support for bottom-patterns in fixrec package
huffman
parents:
30158
diff
changeset
|
144 |
|
62175 | 145 |
text \<open>Tree and forest types.\<close> |
16554 | 146 |
|
147 |
domain 'a tree = Leaf (lazy 'a) | Branch (lazy "'a forest") |
|
148 |
and 'a forest = Empty | Trees (lazy "'a tree") "'a forest" |
|
149 |
||
62175 | 150 |
text \<open> |
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
151 |
To define mutually recursive functions, give multiple type signatures |
62175 | 152 |
separated by the keyword \<open>and\<close>. |
153 |
\<close> |
|
16554 | 154 |
|
155 |
fixrec |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
156 |
map_tree :: "('a \<rightarrow> 'b) \<rightarrow> ('a tree \<rightarrow> 'b tree)" |
16554 | 157 |
and |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
158 |
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
|
159 |
where |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
160 |
"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
|
161 |
| "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
|
162 |
| "map_forest\<cdot>f\<cdot>Empty = Empty" |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
16554
diff
changeset
|
163 |
| "ts \<noteq> \<bottom> \<Longrightarrow> |
16554 | 164 |
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)" |
165 |
||
33428
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
166 |
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
|
167 |
by fixrec_simp |
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
168 |
|
70ed971a79d1
fixrec examples use fixrec_simp instead of fixpat
huffman
parents:
33401
diff
changeset
|
169 |
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
|
170 |
by fixrec_simp |
16554 | 171 |
|
37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
36997
diff
changeset
|
172 |
(* |
16554 | 173 |
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
|
174 |
@{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
|
175 |
@{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
|
176 |
@{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
|
177 |
@{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
|
178 |
@{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
|
179 |
@{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
|
180 |
@{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
|
181 |
*) |
16554 | 182 |
|
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
183 |
|
62175 | 184 |
subsection \<open>Looping simp rules\<close> |
36997
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
185 |
|
62175 | 186 |
text \<open> |
36997
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
187 |
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
|
188 |
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
|
189 |
arguments or functions with variable patterns, the defining |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
190 |
equations may cause the simplifier to loop. In these cases it will |
62175 | 191 |
be necessary to use a \<open>[simp del]\<close> declaration. |
192 |
\<close> |
|
36997
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 |
fixrec |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
195 |
repeat :: "'a \<rightarrow> 'a llist" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
196 |
where |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
197 |
[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
|
198 |
|
62175 | 199 |
text \<open> |
36997
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
200 |
We can derive other non-looping simp rules for @{const repeat} by |
62175 | 201 |
using the \<open>subst\<close> method with the \<open>repeat.simps\<close> rule. |
202 |
\<close> |
|
36997
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 |
lemma repeat_simps [simp]: |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
205 |
"repeat\<cdot>x \<noteq> \<bottom>" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
206 |
"repeat\<cdot>x \<noteq> lNil" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
207 |
"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
|
208 |
by (subst repeat.simps, simp)+ |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
209 |
|
40213
b63e966564da
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents:
40041
diff
changeset
|
210 |
lemma llist_case_repeat [simp]: |
b63e966564da
rename case combinators generated by domain package to 'foo_case' instead of 'foo_when'
huffman
parents:
40041
diff
changeset
|
211 |
"llist_case\<cdot>z\<cdot>f\<cdot>(repeat\<cdot>x) = f\<cdot>x\<cdot>(repeat\<cdot>x)" |
36997
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
212 |
by (subst repeat.simps, simp) |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
213 |
|
62175 | 214 |
text \<open> |
36997
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
215 |
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
|
216 |
equations are in the simpset at the same time. In such cases it may |
62175 | 217 |
only be necessary to declare \<open>[simp del]\<close> on one equation. |
218 |
\<close> |
|
36997
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 |
fixrec |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
221 |
inf_tree :: "'a tree" and inf_forest :: "'a forest" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
222 |
where |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
223 |
[simp del]: "inf_tree = Branch\<cdot>inf_forest" |
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
224 |
| "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
|
225 |
|
ca3172dbde8b
add section about fixrec definitions with looping simp rules
huffman
parents:
35925
diff
changeset
|
226 |
|
62175 | 227 |
subsection \<open>Using \<open>fixrec\<close> inside locales\<close> |
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
228 |
|
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
229 |
locale test = |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
230 |
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
|
231 |
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
|
232 |
begin |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
233 |
|
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
234 |
fixrec |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
235 |
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
|
236 |
where |
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
237 |
"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
|
238 |
|
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
239 |
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
|
240 |
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
|
241 |
|
16554 | 242 |
end |
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
243 |
|
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
33428
diff
changeset
|
244 |
end |