113 Notice that this version has overlapping patterns. |
113 Notice that this version has overlapping patterns. |
114 The second equation cannot be proved as a theorem |
114 The second equation cannot be proved as a theorem |
115 because it only applies when the first pattern fails. |
115 because it only applies when the first pattern fails. |
116 *} |
116 *} |
117 |
117 |
118 fixrec (permissive) |
118 fixrec |
119 lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist" |
119 lzip2 :: "'a llist \<rightarrow> 'b llist \<rightarrow> ('a \<times> 'b) llist" |
120 where |
120 where |
121 "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)" |
121 "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip2\<cdot>xs\<cdot>ys)" |
122 | "lzip2\<cdot>xs\<cdot>ys = lNil" |
122 | (unchecked) "lzip2\<cdot>xs\<cdot>ys = lNil" |
123 |
123 |
124 text {* |
124 text {* |
125 Usually fixrec tries to prove all equations as theorems. |
125 Usually fixrec tries to prove all equations as theorems. |
126 The "permissive" option overrides this behavior, so fixrec |
126 The "unchecked" option overrides this behavior, so fixrec |
127 does not produce any simp rules. |
127 does not attempt to prove that particular equation. |
128 *} |
128 *} |
129 |
129 |
130 text {* Simp rules can be generated later using @{text fixrec_simp}. *} |
130 text {* Simp rules can be generated later using @{text fixrec_simp}. *} |
131 |
131 |
132 lemma lzip2_simps [simp]: |
132 lemma lzip2_simps [simp]: |
133 "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>(lCons\<cdot>y\<cdot>ys) = lCons\<cdot>(x, y)\<cdot>(lzip\<cdot>xs\<cdot>ys)" |
|
134 "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil" |
133 "lzip2\<cdot>(lCons\<cdot>x\<cdot>xs)\<cdot>lNil = lNil" |
135 "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil" |
134 "lzip2\<cdot>lNil\<cdot>(lCons\<cdot>y\<cdot>ys) = lNil" |
136 "lzip2\<cdot>lNil\<cdot>lNil = lNil" |
135 "lzip2\<cdot>lNil\<cdot>lNil = lNil" |
137 by fixrec_simp+ |
136 by fixrec_simp+ |
138 |
137 |