153 | "der c (NMTIMES r 0 (Suc m)) = ALT (der c (NTIMES r (Suc m))) (der c (NMTIMES r 0 m))" |
153 | "der c (NMTIMES r 0 (Suc m)) = ALT (der c (NTIMES r (Suc m))) (der c (NMTIMES r 0 m))" |
154 | "der c (NMTIMES r (Suc n) m) = der c (SEQ r (NMTIMES r n m))" |
154 | "der c (NMTIMES r (Suc n) m) = der c (SEQ r (NMTIMES r n m))" |
155 by pat_completeness auto |
155 by pat_completeness auto |
156 |
156 |
157 termination der |
157 termination der |
158 apply(relation "measure (\<lambda>(c, r). M r)") |
158 by (relation "measure (\<lambda>(c, r). M r)") (simp_all) |
159 apply(simp_all) |
159 |
160 done |
|
161 |
160 |
162 fun |
161 fun |
163 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
162 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
164 where |
163 where |
165 "ders [] r = r" |
164 "ders [] r = r" |
238 lemma Der_pow [simp]: |
237 lemma Der_pow [simp]: |
239 shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})" |
238 shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})" |
240 unfolding Der_def |
239 unfolding Der_def |
241 by(auto simp add: Cons_eq_append_conv Seq_def) |
240 by(auto simp add: Cons_eq_append_conv Seq_def) |
242 |
241 |
243 |
|
244 lemma Der_UNION [simp]: |
242 lemma Der_UNION [simp]: |
245 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
243 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
246 by (auto simp add: Der_def) |
244 by (auto simp add: Der_def) |
247 |
245 |
248 lemma test: |
246 lemma Suc_Union: |
249 "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))" |
247 "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))" |
250 by (metis UN_insert atMost_Suc) |
248 by (metis UN_insert atMost_Suc) |
251 |
249 |
252 lemma yy: |
250 lemma Suc_reduce_Union: |
253 "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))" |
251 "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))" |
254 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost) |
252 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost) |
255 |
253 |
256 lemma uu: |
|
257 "(Suc n) + m = Suc (n + m)" |
|
258 by simp |
|
259 |
254 |
260 lemma der_correctness: |
255 lemma der_correctness: |
261 shows "L (der c r) = Der c (L r)" |
256 shows "L (der c r) = Der c (L r)" |
262 apply(induct rule: der.induct) |
257 by (induct rule: der.induct) |
263 apply(simp_all add: nullable_correctness)[12] |
258 (simp_all add: nullable_correctness |
264 apply(simp only: L.simps der.simps) |
259 Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost) |
265 apply(simp only: Der_UNION) |
260 |
266 apply(simp del: pow.simps Der_pow) |
|
267 apply(simp only: atLeast0AtMost) |
|
268 apply(simp only: test) |
|
269 apply(simp only: L.simps der.simps) |
|
270 apply(simp only: Der_UNION) |
|
271 apply(simp only: yy add_Suc) |
|
272 apply(simp only: seq_Union) |
|
273 apply(simp only: Der_UNION) |
|
274 apply(simp only: pow.simps) |
|
275 done |
|
276 |
261 |
277 lemma matcher_correctness: |
262 lemma matcher_correctness: |
278 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
263 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
279 by (induct s arbitrary: r) |
264 by (induct s arbitrary: r) |
280 (simp_all add: nullable_correctness der_correctness Der_def) |
265 (simp_all add: nullable_correctness der_correctness Der_def) |