760 using a |
760 using a |
761 unfolding alphas fresh_star_def |
761 unfolding alphas fresh_star_def |
762 by (simp_all add: fresh_plus_perm) |
762 by (simp_all add: fresh_plus_perm) |
763 |
763 |
764 |
764 |
765 (* PROBLEM: this should be the real eqvt lemma for the alphas *) |
765 lemma alpha_gen_eqvt[eqvt]: |
766 lemma alpha_gen_real_eqvt: |
|
767 shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)" |
766 shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)" |
768 and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)" |
767 and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)" |
769 and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" |
768 and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" |
770 unfolding alphas |
769 unfolding alphas |
771 unfolding permute_eqvt[symmetric] |
770 unfolding permute_eqvt[symmetric] |
772 unfolding set_eqvt[symmetric] |
771 unfolding set_eqvt[symmetric] |
773 unfolding permute_fun_app_eq[symmetric] |
772 unfolding permute_fun_app_eq[symmetric] |
774 unfolding Diff_eqvt[symmetric] |
773 unfolding Diff_eqvt[symmetric] |
775 by (auto simp add: permute_bool_def fresh_star_permute_iff) |
774 by (auto simp add: permute_bool_def fresh_star_permute_iff) |
776 |
|
777 |
|
778 lemma alpha_gen_eqvt: |
|
779 assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
|
780 and b: "p \<bullet> (f x) = f (p \<bullet> x)" |
|
781 and c: "p \<bullet> (f y) = f (p \<bullet> y)" |
|
782 shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)" |
|
783 and "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)" |
|
784 and "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst R f (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" |
|
785 unfolding alphas |
|
786 unfolding set_eqvt[symmetric] |
|
787 unfolding b[symmetric] c[symmetric] |
|
788 unfolding Diff_eqvt[symmetric] |
|
789 unfolding permute_eqvt[symmetric] |
|
790 using a |
|
791 by (auto simp add: fresh_star_permute_iff) |
|
792 |
|
793 |
775 |
794 lemma alpha_gen_simpler: |
776 lemma alpha_gen_simpler: |
795 assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y" |
777 assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y" |
796 and fin_fv: "finite (f x)" |
778 and fin_fv: "finite (f x)" |
797 and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)" |
779 and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)" |