194 | "der c (NOT r) = NOT(der c r)" |
194 | "der c (NOT r) = NOT(der c r)" |
195 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
195 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
196 | "der c (OPT r) = der c r" |
196 | "der c (OPT r) = der c r" |
197 | "der c (NTIMES r 0) = NULL" |
197 | "der c (NTIMES r 0) = NULL" |
198 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))" |
198 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))" |
199 | "der c (NMTIMES r n m) = (if m < n then NULL else |
199 | "der c (NMTIMES r n m) = |
|
200 (if m < n then NULL else |
|
201 (if m = 0 then NULL else |
|
202 (der c (SEQ r (NMTIMES r (n - 1) (m - 1))))))" |
|
203 (* |
|
204 |
|
205 (if m < n then NULL else |
200 (if n = m then der c (NTIMES r n) else |
206 (if n = m then der c (NTIMES r n) else |
201 ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))" |
207 ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))" |
|
208 *) |
202 by pat_completeness auto |
209 by pat_completeness auto |
203 |
210 |
204 termination der |
211 termination der |
205 apply(relation "measure (\<lambda>(c, r). M r)") |
212 apply(relation "measure (\<lambda>(c, r). M r)") |
206 apply(simp_all) |
213 apply(simp_all) |
292 |
299 |
293 lemma Der_UNION [simp]: |
300 lemma Der_UNION [simp]: |
294 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
301 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
295 by (auto simp add: Der_def) |
302 by (auto simp add: Der_def) |
296 |
303 |
297 |
|
298 |
|
299 lemma der_correctness: |
304 lemma der_correctness: |
300 shows "L (der c r) = Der c (L r)" |
305 shows "L (der c r) = Der c (L r)" |
301 apply(induct rule: der.induct) |
306 apply(induct rule: der.induct) |
302 apply(simp_all add: nullable_correctness |
307 apply(simp_all add: nullable_correctness |
303 Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost) |
308 Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost) |
|
309 apply(case_tac "[] \<in> L r") |
|
310 apply(simp) |
|
311 apply(case_tac n) |
|
312 apply(auto)[1] |
|
313 apply(case_tac m) |
|
314 apply(simp) |
|
315 apply(auto simp add: )[1] |
|
316 apply (metis (full_types, hide_lams) Der_pow Der_seq Suc_le_mono UnCI atLeast0AtMost atMost_iff not_less_eq_eq) |
|
317 |
|
318 apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl) |
|
319 apply (metis Suc_leD atLeastAtMost_iff) |
|
320 by (metis atLeastAtMost_iff le_antisym not_less_eq_eq) |
|
321 |
|
322 (* |
|
323 lemma der_correctness: |
|
324 shows "L (der c r) = Der c (L r)" |
|
325 apply(induct rule: der.induct) |
|
326 apply(simp_all add: nullable_correctness |
|
327 Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost) |
304 apply(case_tac m) |
328 apply(case_tac m) |
305 apply(simp) |
329 apply(simp) |
306 apply(simp) |
330 apply(simp) |
307 apply(auto) |
331 apply(auto) |
308 apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl) |
332 apply (metis (poly_guards_query) atLeastAtMost_iff not_le order_refl) |
309 apply (metis Suc_leD atLeastAtMost_iff) |
333 apply (metis Suc_leD atLeastAtMost_iff) |
310 by (metis atLeastAtMost_iff le_antisym not_less_eq_eq) |
334 by (metis atLeastAtMost_iff le_antisym not_less_eq_eq) |
311 |
335 *) |
312 |
336 |
313 lemma matcher_correctness: |
337 lemma matcher_correctness: |
314 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
338 shows "matcher r s \<longleftrightarrow> s \<in> L r" |
315 by (induct s arbitrary: r) |
339 by (induct s arbitrary: r) |
316 (simp_all add: nullable_correctness der_correctness Der_def) |
340 (simp_all add: nullable_correctness der_correctness Der_def) |
317 |
341 |
318 |
342 |
|
343 lemma "L (der c (NMTIMES r n m)) = |
|
344 L ((if m < n then NULL else |
|
345 (if m = 0 then NULL else |
|
346 (der c (SEQ r (NMTIMES r (n - 1) (m - 1)))))))" |
|
347 apply(subst der.simps(12)) |
|
348 apply(auto simp del: der.simps) |
|
349 apply(simp) |
|
350 apply(auto)[1] |
|
351 apply(case_tac m) |
|
352 apply(simp) |
|
353 apply(simp) |
|
354 apply(case_tac m) |
|
355 apply(simp) |
|
356 apply(simp) |
|
357 apply(simp) |
|
358 apply(subst (asm) der.simps(12)) |
|
359 apply(auto)[1] |
|
360 apply(case_tac m) |
|
361 apply(simp) |
|
362 apply(simp) |
|
363 apply(case_tac m) |
|
364 apply(simp) |
|
365 apply(simp) |
|
366 apply(auto)[1] |
|
367 apply(auto simp del: der.simps(12))[1] |
|
368 apply(subst (asm) der.simps(12)) |
|
369 apply(case_tac n) |
|
370 apply(simp) |
|
371 apply(simp) |
|
372 apply(case_tac m) |
|
373 apply(simp) |
|
374 apply(simp) |
|
375 apply(case_tac "Suc nat = nata") |
|
376 apply(simp) |
|
377 apply(auto simp del: der.simps(12))[1] |
|
378 apply(auto)[1] |
|
379 apply(case_tac n) |
|
380 apply(simp) |
|
381 apply(simp) |
|
382 apply(case_tac m) |
|
383 apply(simp) |
|
384 apply(simp) |
|
385 apply(simp add: Seq_def) |
|
386 apply(auto)[1] |
|
387 apply (metis atLeastAtMost_iff le_eq_less_or_eq linorder_neqE_nat) |
|
388 apply(simp (no_asm) del: der.simps(12)) |
|
389 apply(auto simp del: der.simps(12))[1] |
|
390 apply(case_tac "m = Suc n") |
|
391 apply(simp) |
|
392 apply(case_tac n) |
|
393 apply(simp) |
|
394 apply(simp) |
|
395 apply(auto simp add: Seq_def del: der.simps(12))[1] |
|
396 |
|
397 apply(case_tac n) |
|
398 apply(simp) |
|
399 apply(case_tac m) |
|
400 apply(simp) |
|
401 apply(simp) |
|
402 apply(simp add: Seq_def) |
|
403 apply(auto)[1] |
|
404 apply(case_tac "nat = 0") |
|
405 apply(simp) |
|
406 apply(simp) |
|
407 apply(auto)[1] |
|
408 apply(case_tac "Suc 0 = nat") |
|
409 apply(simp) |
|
410 apply(auto simp del: der.simps(12))[1] |
|
411 apply(simp) |
|
412 apply(case_tac "Suc 0 = nat") |
|
413 apply(simp) |
|
414 apply(auto simp add: Seq_def del: der.simps(12))[1] |
|
415 apply(rule_tac x="s1" in exI) |
|
416 apply(rule_tac x="s2" in exI) |
|
417 apply(simp) |
|
418 apply(rule_tac x="1" in bexI) |
|
419 apply(simp) |
|
420 apply(simp) |
|
421 apply(simp) |
|
422 apply(auto simp add: Seq_def)[1] |
|
423 apply(case_tac m) |
|
424 apply(simp) |
|
425 apply(simp) |
|
426 |
319 end |
427 end |