758 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)" |
758 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)" |
759 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)" |
759 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)" |
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 |
|
764 |
|
765 (* PROBLEM: this should be the real eqvt lemma for the alphas *) |
|
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)" |
|
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)" |
|
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)" |
|
770 unfolding alphas |
|
771 unfolding permute_eqvt[symmetric] |
|
772 unfolding set_eqvt[symmetric] |
|
773 unfolding permute_fun_app_eq[symmetric] |
|
774 unfolding Diff_eqvt[symmetric] |
|
775 by (auto simp add: permute_bool_def fresh_star_permute_iff) |
|
776 |
763 |
777 |
764 lemma alpha_gen_eqvt: |
778 lemma alpha_gen_eqvt: |
765 assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
779 assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
766 and b: "p \<bullet> (f x) = f (p \<bullet> x)" |
780 and b: "p \<bullet> (f x) = f (p \<bullet> x)" |
767 and c: "p \<bullet> (f y) = f (p \<bullet> y)" |
781 and c: "p \<bullet> (f y) = f (p \<bullet> y)" |