equal
deleted
inserted
replaced
251 "a ^^^ n \<equiv> replicate n a" |
251 "a ^^^ n \<equiv> replicate n a" |
252 |
252 |
253 definition |
253 definition |
254 "length_test s a b \<equiv> length (filter (op= a) s) = length (filter (op= b) s)" |
254 "length_test s a b \<equiv> length (filter (op= a) s) = length (filter (op= b) s)" |
255 |
255 |
256 lemma [simp]: |
|
257 assumes "i \<noteq> j" "a \<noteq> b" |
|
258 shows "length_test ((a ^^^ i) @ (b ^^^ j)) a b \<noteq> length_test ((a ^^^ n) @ (b ^^^ n)) a b" |
|
259 using assms unfolding length_test_def by auto |
|
260 |
|
261 lemma [simp]: |
|
262 assumes "a \<noteq> b" |
|
263 shows "filter (op= a) ((a ^^^ i) @ (b ^^^ j)) = a ^^^ i" |
|
264 and "filter (op= b) ((a ^^^ i) @ (b ^^^ j)) = b ^^^ j" |
|
265 using assms by simp_all |
|
266 |
|
267 lemma length_test: |
256 lemma length_test: |
268 "x = y \<Longrightarrow> length_test x a b = length_test y a b" |
257 "x = y \<Longrightarrow> length_test x a b = length_test y a b" |
269 by simp |
258 by simp |
270 |
259 |
271 lemma an_bn_not_regular: |
260 lemma an_bn_not_regular: |