640 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)" |
640 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)" |
641 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
641 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
642 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
642 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
643 shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)" |
643 shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)" |
644 using b c apply - |
644 using b c apply - |
645 apply(simp add: alpha_gen.simps) |
645 apply(simp add: alpha_gen) |
646 apply(erule conjE)+ |
646 apply(erule conjE)+ |
647 apply(simp add: fresh_star_plus) |
647 apply(simp add: fresh_star_plus) |
648 apply(drule_tac x="- pia \<bullet> sa" in spec) |
648 apply(drule_tac x="- pia \<bullet> sa" in spec) |
649 apply(drule mp) |
649 apply(drule mp) |
650 apply(rotate_tac 5) |
650 apply(rotate_tac 5) |
651 apply(drule_tac pi="- pia" in a) |
651 apply(drule_tac pi="- pia" in a) |
652 apply(simp) |
652 apply(simp) |
653 apply(rotate_tac 7) |
653 apply(rotate_tac 7) |
654 apply(drule_tac pi="pia" in a) |
654 apply(drule_tac pi="pia" in a) |
|
655 apply(simp) |
|
656 done |
|
657 |
|
658 lemma alpha_gen_compose_trans2: |
|
659 fixes pi pia |
|
660 assumes b: "(aa, (t1, t2)) \<approx>gen |
|
661 (\<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)) |
|
662 (\<lambda>(b, a). fv_a b \<union> fv_b a) pi (ab, (ta1, ta2))" |
|
663 and c: "(ab, (ta1, ta2)) \<approx>gen (\<lambda>(b, a) (d, c). R1 b d \<and> R2 a c) (\<lambda>(b, a). fv_a b \<union> fv_b a) |
|
664 pia (ac, (sa1, sa2))" |
|
665 and r1: "\<And>pi t s. R1 t s \<Longrightarrow> R1 (pi \<bullet> t) (pi \<bullet> s)" |
|
666 and r2: "\<And>pi t s. R2 t s \<Longrightarrow> R2 (pi \<bullet> t) (pi \<bullet> s)" |
|
667 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) |
|
668 (pia + pi) (ac, (sa1, sa2))" |
|
669 using b c apply - |
|
670 apply(simp add: alpha_gen2) |
|
671 apply(simp add: alpha_gen) |
|
672 apply(erule conjE)+ |
|
673 apply(simp add: fresh_star_plus) |
|
674 apply(drule_tac x="- pia \<bullet> sa1" in spec) |
|
675 apply(drule mp) |
|
676 apply(rotate_tac 5) |
|
677 apply(drule_tac pi="- pia" in r1) |
|
678 apply(simp) |
|
679 apply(rotate_tac -1) |
|
680 apply(drule_tac pi="pia" in r1) |
|
681 apply(simp) |
|
682 apply(drule_tac x="- pia \<bullet> sa2" in spec) |
|
683 apply(drule mp) |
|
684 apply(rotate_tac 6) |
|
685 apply(drule_tac pi="- pia" in r2) |
|
686 apply(simp) |
|
687 apply(rotate_tac -1) |
|
688 apply(drule_tac pi="pia" in r2) |
655 apply(simp) |
689 apply(simp) |
656 done |
690 done |
657 |
691 |
658 lemma alpha_gen_compose_eqvt: |
692 lemma alpha_gen_compose_eqvt: |
659 fixes pia |
693 fixes pia |