458 assumes q1: "Quotient R1 Abs1 Rep1" |
458 assumes q1: "Quotient R1 Abs1 Rep1" |
459 and q2: "Quotient R2 Abs2 Rep2" |
459 and q2: "Quotient R2 Abs2 Rep2" |
460 shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split" |
460 shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split" |
461 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
461 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
462 |
462 |
463 lemma alpha_gen2: |
463 lemma alphas2: |
464 "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) = |
464 "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) = |
465 (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 |
465 (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 |
466 \<and> pi \<bullet> bs = cs)" |
466 \<and> pi \<bullet> bs = cs)" |
467 by (simp add: alpha_gen) |
467 "(bs, x1, x2) \<approx>res (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) = |
468 |
468 (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2)" |
|
469 "(bsl, x1, x2) \<approx>lst (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (csl, y1, y2) = |
|
470 (f1 x1 \<union> f2 x2 - set bsl = f1 y1 \<union> f2 y2 - set csl \<and> (f1 x1 \<union> f2 x2 - set bsl) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2 |
|
471 \<and> pi \<bullet> bsl = csl)" |
|
472 by (simp_all add: alphas) |
469 |
473 |
470 lemma alpha_gen_compose_sym: |
474 lemma alpha_gen_compose_sym: |
471 fixes pi |
475 fixes pi |
472 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
476 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
473 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
477 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
474 shows "(ab, s) \<approx>gen R f (- pi) (aa, t)" |
478 shows "(ab, s) \<approx>gen R f (- pi) (aa, t)" |
475 using b apply - |
479 using b apply - |
476 apply(simp add: alpha_gen) |
480 apply(simp add: alphas) |
477 apply(erule conjE)+ |
481 apply(erule conjE)+ |
478 apply(rule conjI) |
482 apply(rule conjI) |
479 apply(simp add: fresh_star_def fresh_minus_perm) |
483 apply(simp add: fresh_star_def fresh_minus_perm) |
480 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
484 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
481 apply simp |
485 apply simp |
482 apply(clarify) |
486 apply(clarify) |
483 apply(simp) |
487 apply(simp) |
484 apply(rule a) |
488 apply(rule a) |
485 apply assumption |
489 apply assumption |
486 done |
490 done |
|
491 |
|
492 lemma alpha_res_compose_sym: |
|
493 fixes pi |
|
494 assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
|
495 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
496 shows "(ab, s) \<approx>res R f (- pi) (aa, t)" |
|
497 using b apply - |
|
498 apply(simp add: alphas) |
|
499 apply(erule conjE)+ |
|
500 apply(rule conjI) |
|
501 apply(simp add: fresh_star_def fresh_minus_perm) |
|
502 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
503 apply simp |
|
504 apply(rule a) |
|
505 apply assumption |
|
506 done |
|
507 |
|
508 lemma alpha_lst_compose_sym: |
|
509 fixes pi |
|
510 assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
|
511 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
512 shows "(ab, s) \<approx>lst R f (- pi) (aa, t)" |
|
513 using b apply - |
|
514 apply(simp add: alphas) |
|
515 apply(erule conjE)+ |
|
516 apply(rule conjI) |
|
517 apply(simp add: fresh_star_def fresh_minus_perm) |
|
518 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
519 apply simp |
|
520 apply(clarify) |
|
521 apply(simp) |
|
522 apply(rule a) |
|
523 apply assumption |
|
524 done |
|
525 |
|
526 lemmas alphas_compose_sym = alpha_gen_compose_sym alpha_res_compose_sym alpha_lst_compose_sym |
487 |
527 |
488 lemma alpha_gen_compose_sym2: |
528 lemma alpha_gen_compose_sym2: |
489 assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22). |
529 assumes a: "(aa, t1, t2) \<approx>gen (\<lambda>(x11, x12) (x21, x22). |
490 (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)" |
530 (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)" |
491 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
531 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
492 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
532 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
493 shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)" |
533 shows "(ab, s1, s2) \<approx>gen (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)" |
494 using a |
534 using a |
495 apply(simp add: alpha_gen) |
535 apply(simp add: alphas) |
496 apply clarify |
536 apply clarify |
497 apply (rule conjI) |
537 apply (rule conjI) |
498 apply(simp add: fresh_star_def fresh_minus_perm) |
538 apply(simp add: fresh_star_def fresh_minus_perm) |
499 apply (rule conjI) |
539 apply (rule conjI) |
500 apply (rotate_tac 3) |
540 apply (rotate_tac 3) |
504 apply (rotate_tac -1) |
544 apply (rotate_tac -1) |
505 apply (drule_tac pi="- pi" in r2) |
545 apply (drule_tac pi="- pi" in r2) |
506 apply simp_all |
546 apply simp_all |
507 done |
547 done |
508 |
548 |
|
549 lemma alpha_res_compose_sym2: |
|
550 assumes a: "(aa, t1, t2) \<approx>res (\<lambda>(x11, x12) (x21, x22). |
|
551 (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)" |
|
552 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
553 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
554 shows "(ab, s1, s2) \<approx>res (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)" |
|
555 using a |
|
556 apply(simp add: alphas) |
|
557 apply clarify |
|
558 apply (rule conjI) |
|
559 apply(simp add: fresh_star_def fresh_minus_perm) |
|
560 apply (rule conjI) |
|
561 apply (rotate_tac 3) |
|
562 apply (drule_tac pi="- pi" in r1) |
|
563 apply simp |
|
564 apply (rotate_tac -1) |
|
565 apply (drule_tac pi="- pi" in r2) |
|
566 apply simp |
|
567 done |
|
568 |
|
569 lemma alpha_lst_compose_sym2: |
|
570 assumes a: "(aa, t1, t2) \<approx>lst (\<lambda>(x11, x12) (x21, x22). |
|
571 (R1 x11 x21 \<and> R1 x21 x11) \<and> R2 x12 x22 \<and> R2 x22 x12) (\<lambda>(b, a). fb b \<union> fa a) pi (ab, s1, s2)" |
|
572 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
573 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
574 shows "(ab, s1, s2) \<approx>lst (\<lambda>(a, b) (d, c). R1 a d \<and> R2 b c) (\<lambda>(b, a). fb b \<union> fa a) (- pi) (aa, t1, t2)" |
|
575 using a |
|
576 apply(simp add: alphas) |
|
577 apply clarify |
|
578 apply (rule conjI) |
|
579 apply(simp add: fresh_star_def fresh_minus_perm) |
|
580 apply (rule conjI) |
|
581 apply (rotate_tac 3) |
|
582 apply (drule_tac pi="- pi" in r1) |
|
583 apply simp |
|
584 apply (rule conjI) |
|
585 apply (rotate_tac -1) |
|
586 apply (drule_tac pi="- pi" in r2) |
|
587 apply simp_all |
|
588 done |
|
589 |
|
590 lemmas alphas_compose_sym2 = alpha_gen_compose_sym2 alpha_res_compose_sym2 alpha_lst_compose_sym2 |
|
591 |
509 lemma alpha_gen_compose_trans: |
592 lemma alpha_gen_compose_trans: |
510 fixes pi pia |
593 fixes pi pia |
511 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
594 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
512 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
595 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
513 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
596 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
514 shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)" |
597 shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)" |
515 using b c apply - |
598 using b c apply - |
516 apply(simp add: alpha_gen) |
599 apply(simp add: alphas) |
517 apply(erule conjE)+ |
600 apply(erule conjE)+ |
518 apply(simp add: fresh_star_plus) |
601 apply(simp add: fresh_star_plus) |
519 apply(drule_tac x="- pia \<bullet> sa" in spec) |
602 apply(drule_tac x="- pia \<bullet> sa" in spec) |
520 apply(drule mp) |
603 apply(drule mp) |
521 apply(rotate_tac 5) |
604 apply(rotate_tac 5) |
523 apply(simp) |
606 apply(simp) |
524 apply(rotate_tac 7) |
607 apply(rotate_tac 7) |
525 apply(drule_tac pi="pia" in a) |
608 apply(drule_tac pi="pia" in a) |
526 apply(simp) |
609 apply(simp) |
527 done |
610 done |
|
611 |
|
612 lemma alpha_res_compose_trans: |
|
613 fixes pi pia |
|
614 assumes b: "(aa, t) \<approx>res (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
|
615 and c: "(ab, ta) \<approx>res R f pia (ac, sa)" |
|
616 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
617 shows "(aa, t) \<approx>res R f (pia + pi) (ac, sa)" |
|
618 using b c apply - |
|
619 apply(simp add: alphas) |
|
620 apply(erule conjE)+ |
|
621 apply(simp add: fresh_star_plus) |
|
622 apply(drule_tac x="- pia \<bullet> sa" in spec) |
|
623 apply(drule mp) |
|
624 apply(drule_tac pi="- pia" in a) |
|
625 apply(simp) |
|
626 apply(rotate_tac 6) |
|
627 apply(drule_tac pi="pia" in a) |
|
628 apply(simp) |
|
629 done |
|
630 |
|
631 lemma alpha_lst_compose_trans: |
|
632 fixes pi pia |
|
633 assumes b: "(aa, t) \<approx>lst (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
|
634 and c: "(ab, ta) \<approx>lst R f pia (ac, sa)" |
|
635 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
636 shows "(aa, t) \<approx>lst R f (pia + pi) (ac, sa)" |
|
637 using b c apply - |
|
638 apply(simp add: alphas) |
|
639 apply(erule conjE)+ |
|
640 apply(simp add: fresh_star_plus) |
|
641 apply(drule_tac x="- pia \<bullet> sa" in spec) |
|
642 apply(drule mp) |
|
643 apply(rotate_tac 5) |
|
644 apply(drule_tac pi="- pia" in a) |
|
645 apply(simp) |
|
646 apply(rotate_tac 7) |
|
647 apply(drule_tac pi="pia" in a) |
|
648 apply(simp) |
|
649 done |
|
650 |
|
651 lemmas alphas_compose_trans = alpha_gen_compose_trans alpha_res_compose_trans alpha_lst_compose_trans |
528 |
652 |
529 lemma alpha_gen_compose_trans2: |
653 lemma alpha_gen_compose_trans2: |
530 fixes pi pia |
654 fixes pi pia |
531 assumes b: "(aa, (t1, t2)) \<approx>gen |
655 assumes b: "(aa, (t1, t2)) \<approx>gen |
532 (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z)) |
656 (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z)) |
536 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
660 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
537 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
661 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
538 shows "(aa, (t1, t2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
662 shows "(aa, (t1, t2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
539 (pia + pi) (ac, (sa1, sa2))" |
663 (pia + pi) (ac, (sa1, sa2))" |
540 using b c apply - |
664 using b c apply - |
541 apply(simp add: alpha_gen2) |
665 apply(simp add: alphas2) |
542 apply(simp add: alpha_gen) |
666 apply(simp add: alphas) |
543 apply(erule conjE)+ |
667 apply(erule conjE)+ |
544 apply(simp add: fresh_star_plus) |
668 apply(simp add: fresh_star_plus) |
545 apply(drule_tac x="- pia \<bullet> sa1" in spec) |
669 apply(drule_tac x="- pia \<bullet> sa1" in spec) |
546 apply(drule mp) |
670 apply(drule mp) |
547 apply(rotate_tac 5) |
671 apply(rotate_tac 5) |
557 apply(simp) |
681 apply(simp) |
558 apply(rotate_tac -1) |
682 apply(rotate_tac -1) |
559 apply(drule_tac pi="pia" in r2) |
683 apply(drule_tac pi="pia" in r2) |
560 apply(simp) |
684 apply(simp) |
561 done |
685 done |
|
686 |
|
687 lemma alpha_res_compose_trans2: |
|
688 fixes pi pia |
|
689 assumes b: "(aa, (t1, t2)) \<approx>res |
|
690 (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z)) |
|
691 (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))" |
|
692 and c: "(ab, (ta1, ta2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
|
693 pia (ac, (sa1, sa2))" |
|
694 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
695 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
696 shows "(aa, (t1, t2)) \<approx>res (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
|
697 (pia + pi) (ac, (sa1, sa2))" |
|
698 using b c apply - |
|
699 apply(simp add: alphas2) |
|
700 apply(simp add: alphas) |
|
701 apply(erule conjE)+ |
|
702 apply(simp add: fresh_star_plus) |
|
703 apply(drule_tac x="- pia \<bullet> sa1" in spec) |
|
704 apply(drule mp) |
|
705 apply(rotate_tac 5) |
|
706 apply(drule_tac pi="- pia" in r1) |
|
707 apply(simp) |
|
708 apply(rotate_tac -1) |
|
709 apply(drule_tac pi="pia" in r1) |
|
710 apply(simp) |
|
711 apply(drule_tac x="- pia \<bullet> sa2" in spec) |
|
712 apply(drule mp) |
|
713 apply(rotate_tac 6) |
|
714 apply(drule_tac pi="- pia" in r2) |
|
715 apply(simp) |
|
716 apply(rotate_tac -1) |
|
717 apply(drule_tac pi="pia" in r2) |
|
718 apply(simp) |
|
719 done |
|
720 |
|
721 lemma alpha_lst_compose_trans2: |
|
722 fixes pi pia |
|
723 assumes b: "(aa, (t1, t2)) \<approx>lst |
|
724 (\<lambda>(b, a) (d, c). R1 b d \<and> (\<forall>z. R1 d z \<longrightarrow> R1 b z) \<and> R2 a c \<and> (\<forall>z. R2 c z \<longrightarrow> R2 a z)) |
|
725 (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))" |
|
726 and c: "(ab, (ta1, ta2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
|
727 pia (ac, (sa1, sa2))" |
|
728 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
729 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
730 shows "(aa, (t1, t2)) \<approx>lst (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
|
731 (pia + pi) (ac, (sa1, sa2))" |
|
732 using b c apply - |
|
733 apply(simp add: alphas2) |
|
734 apply(simp add: alphas) |
|
735 apply(erule conjE)+ |
|
736 apply(simp add: fresh_star_plus) |
|
737 apply(drule_tac x="- pia \<bullet> sa1" in spec) |
|
738 apply(drule mp) |
|
739 apply(rotate_tac 5) |
|
740 apply(drule_tac pi="- pia" in r1) |
|
741 apply(simp) |
|
742 apply(rotate_tac -1) |
|
743 apply(drule_tac pi="pia" in r1) |
|
744 apply(simp) |
|
745 apply(drule_tac x="- pia \<bullet> sa2" in spec) |
|
746 apply(drule mp) |
|
747 apply(rotate_tac 6) |
|
748 apply(drule_tac pi="- pia" in r2) |
|
749 apply(simp) |
|
750 apply(rotate_tac -1) |
|
751 apply(drule_tac pi="pia" in r2) |
|
752 apply(simp) |
|
753 done |
|
754 |
|
755 lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2 |
562 |
756 |
563 lemma alpha_gen_refl: |
757 lemma alpha_gen_refl: |
564 assumes a: "R x x" |
758 assumes a: "R x x" |
565 shows "(bs, x) \<approx>gen R f 0 (bs, x)" |
759 shows "(bs, x) \<approx>gen R f 0 (bs, x)" |
566 and "(bs, x) \<approx>res R f 0 (bs, x)" |
760 and "(bs, x) \<approx>res R f 0 (bs, x)" |
569 unfolding alphas |
763 unfolding alphas |
570 unfolding fresh_star_def |
764 unfolding fresh_star_def |
571 by (simp_all add: fresh_zero_perm) |
765 by (simp_all add: fresh_zero_perm) |
572 |
766 |
573 lemma alpha_gen_sym: |
767 lemma alpha_gen_sym: |
574 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" |
768 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
575 and b: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)" |
|
576 shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" |
769 shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" |
577 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
770 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
578 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
771 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
579 unfolding alphas fresh_star_def |
772 unfolding alphas fresh_star_def |
580 apply (erule_tac [1] conjE)+ |
|
581 apply (erule_tac [2] conjE)+ |
|
582 apply (erule_tac [3] conjE)+ |
|
583 using a |
773 using a |
584 apply (simp_all add: fresh_minus_perm) |
774 by (auto simp add: fresh_minus_perm) |
585 apply (rotate_tac [!] -1) |
775 |
586 apply (drule_tac [!] p="-p" in b) |
|
587 apply (simp_all) |
|
588 apply (metis permute_minus_cancel(2)) |
|
589 apply (metis permute_minus_cancel(2)) |
|
590 done |
|
591 lemma alpha_gen_trans: |
776 lemma alpha_gen_trans: |
592 assumes a: "(\<forall>c. R y c \<longrightarrow> R (p \<bullet> x) c)" |
777 assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z" |
593 and b: "R (p \<bullet> x) y" |
|
594 and c: "R (q \<bullet> y) z" |
|
595 and d: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)" |
|
596 shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)" |
778 shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)" |
597 and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)" |
779 and "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)" |
598 and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)" |
780 and "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)" |
599 unfolding alphas |
781 using a |
600 unfolding fresh_star_def |
782 unfolding alphas fresh_star_def |
601 apply (simp_all add: fresh_plus_perm) |
783 by (simp_all add: fresh_plus_perm) |
602 apply (metis a c d permute_minus_cancel(2))+ |
|
603 done |
|
604 |
784 |
605 lemma alpha_gen_eqvt: |
785 lemma alpha_gen_eqvt: |
606 assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
786 assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
607 and b: "p \<bullet> (f x) = f (p \<bullet> x)" |
787 and b: "p \<bullet> (f x) = f (p \<bullet> x)" |
608 and c: "p \<bullet> (f y) = f (p \<bullet> y)" |
788 and c: "p \<bullet> (f y) = f (p \<bullet> y)" |