480 apply(simp) |
488 apply(simp) |
481 apply (metis nullable_correctness) |
489 apply (metis nullable_correctness) |
482 apply(metis PMatch.intros(7)) |
490 apply(metis PMatch.intros(7)) |
483 done |
491 done |
484 |
492 |
485 find_theorems Stars |
|
486 thm compat_val_list.induct compat_val.induct |
|
487 |
|
488 |
|
489 lemma PMatch_determ: |
493 lemma PMatch_determ: |
490 shows "\<lbrakk>s \<in> r \<rightarrow> v1; s \<in> r \<rightarrow> v2\<rbrakk> \<Longrightarrow> v1 = v2" |
494 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
491 and "\<lbrakk>s \<in> (STAR r) \<rightarrow> Stars vs1; s \<in> (STAR r) \<rightarrow> Stars vs2\<rbrakk> \<Longrightarrow> vs1 = vs2" |
495 shows "v1 = v2" |
492 apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: compat_val.induct compat_val_list.induct) |
496 using assms |
493 apply(erule PMatch.cases) |
497 apply(induct s r v1 arbitrary: v2 rule: PMatch.induct) |
494 apply(simp_all)[7] |
498 apply(erule PMatch.cases) |
495 apply(erule PMatch.cases) |
499 apply(simp_all)[7] |
496 apply(simp_all)[7] |
500 apply(erule PMatch.cases) |
497 apply(erule PMatch.cases) |
501 apply(simp_all)[7] |
498 apply(simp_all)[7] |
502 apply(rotate_tac 2) |
499 apply(erule PMatch.cases) |
503 apply(erule PMatch.cases) |
500 apply(simp_all)[7] |
504 apply(simp_all (no_asm_use))[7] |
501 apply(erule PMatch.cases) |
505 apply(clarify) |
502 apply(simp_all)[7] |
506 apply(force) |
503 apply(erule PMatch.cases) |
507 apply(clarify) |
504 apply(simp_all)[7] |
508 apply(drule PMatch1a) |
505 apply(clarify) |
509 apply(simp) |
506 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a") |
510 apply(rotate_tac 3) |
507 apply metis |
511 apply(erule PMatch.cases) |
508 apply(rule conjI) |
512 apply(simp_all (no_asm_use))[7] |
|
513 apply(drule PMatch1a)+ |
|
514 apply(simp) |
|
515 apply(simp) |
|
516 apply(rotate_tac 5) |
|
517 apply(erule PMatch.cases) |
|
518 apply(simp_all (no_asm_use))[7] |
|
519 apply(clarify) |
|
520 apply(subgoal_tac "s1 = s1a") |
|
521 apply(blast) |
509 apply(simp add: append_eq_append_conv2) |
522 apply(simp add: append_eq_append_conv2) |
510 apply(auto)[1] |
523 apply(clarify) |
511 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) |
524 apply (metis PMatch1a append_self_conv) |
512 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) |
525 apply(rotate_tac 6) |
513 apply(simp add: append_eq_append_conv2) |
526 apply(erule PMatch.cases) |
514 apply(auto)[1] |
527 apply(simp_all (no_asm_use))[7] |
515 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) |
528 apply(clarify) |
516 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) |
529 apply(subgoal_tac "s1 = s1a") |
517 apply(erule PMatch.cases) |
530 apply(simp) |
518 apply(simp_all)[7] |
531 apply(blast) |
519 apply(clarify) |
532 apply(simp (no_asm_use) add: append_eq_append_conv2) |
520 apply(erule PMatch.cases) |
533 apply(clarify) |
521 apply(simp_all)[7] |
534 apply (metis L.simps(6) PMatch1a append_self_conv) |
522 apply(clarify) |
535 apply(clarify) |
523 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) |
536 apply(rotate_tac 2) |
524 apply(erule PMatch.cases) |
537 apply(erule PMatch.cases) |
525 apply(simp_all)[7] |
538 apply(simp_all (no_asm_use))[7] |
526 apply(clarify) |
539 using PMatch1(2) apply auto[1] |
527 apply(erule PMatch.cases) |
540 using PMatch1(2) apply blast |
528 apply(simp_all)[7] |
541 apply(erule PMatch.cases) |
529 apply(clarify) |
542 apply(simp_all (no_asm_use))[7] |
530 apply (metis PMatch1(1) PMatch1(2) Prf_flat_L) |
543 apply(clarify) |
531 (* star case *) |
544 apply (simp add: PMatch1(2)) |
532 defer |
545 apply(simp) |
533 apply(erule PMatch.cases) |
546 done |
534 apply(simp_all)[7] |
|
535 apply(clarify) |
|
536 apply(erule PMatch.cases) |
|
537 apply(simp_all)[7] |
|
538 apply(clarify) |
|
539 apply (metis PMatch1(2)) |
|
540 apply(rotate_tac 3) |
|
541 apply(erule PMatch.cases) |
|
542 apply(simp_all)[7] |
|
543 apply(clarify) |
|
544 apply(erule PMatch.cases) |
|
545 apply(simp_all)[7] |
|
546 apply(clarify) |
|
547 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a") |
|
548 apply metis |
|
549 apply(simp add: append_eq_append_conv2) |
|
550 apply(auto)[1] |
|
551 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
552 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
553 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
554 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
555 apply(erule PMatch.cases) |
|
556 apply(simp_all)[7] |
|
557 apply(clarify) |
|
558 apply (metis PMatch1(2)) |
|
559 apply(erule PMatch.cases) |
|
560 apply(simp_all)[7] |
|
561 apply(clarify) |
|
562 apply(erule PMatch.cases) |
|
563 apply(simp_all)[7] |
|
564 apply(clarify) |
|
565 apply(subgoal_tac "s1 = s1a \<and> s2 = s2a") |
|
566 apply(drule_tac x="s1 @ s2" in meta_spec) |
|
567 apply(drule_tac x="rb" in meta_spec) |
|
568 apply(drule_tac x="(va#vsa)" in meta_spec) |
|
569 apply(simp) |
|
570 apply(drule meta_mp) |
|
571 apply (metis L.simps(6) PMatch.intros(6)) |
|
572 apply (metis L.simps(6) PMatch.intros(6)) |
|
573 apply(simp add: append_eq_append_conv2) |
|
574 apply(auto)[1] |
|
575 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
576 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
577 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
578 apply (metis L.simps(6) PMatch1(1) PMatch1(2) Prf_flat_L) |
|
579 apply (metis PMatch1(2)) |
|
580 apply(erule PMatch.cases) |
|
581 apply(simp_all)[7] |
|
582 apply(clarify) |
|
583 by (metis PMatch1(2)) |
|
584 |
547 |
585 (* a proof that does not need proj *) |
548 (* a proof that does not need proj *) |
586 lemma PMatch2_roy_version: |
549 lemma PMatch2_roy_version: |
587 assumes "s \<in> (der c r) \<rightarrow> v" |
550 assumes "s \<in> (der c r) \<rightarrow> v" |
588 shows "(c#s) \<in> r \<rightarrow> (injval r c v)" |
551 shows "(c#s) \<in> r \<rightarrow> (injval r c v)" |