585 unfolding alphas |
585 unfolding alphas |
586 unfolding fresh_star_def |
586 unfolding fresh_star_def |
587 by (simp_all add: fresh_zero_perm) |
587 by (simp_all add: fresh_zero_perm) |
588 |
588 |
589 lemma alpha_gen_sym: |
589 lemma alpha_gen_sym: |
590 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
590 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" |
|
591 and b: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)" |
591 shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" |
592 shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" |
592 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
593 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
593 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
594 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
|
595 unfolding alphas fresh_star_def |
|
596 apply (erule_tac [1] conjE)+ |
|
597 apply (erule_tac [2] conjE)+ |
|
598 apply (erule_tac [3] conjE)+ |
594 using a |
599 using a |
595 unfolding alphas |
600 apply (simp_all add: fresh_minus_perm) |
596 unfolding fresh_star_def |
601 apply (rotate_tac [!] -1) |
597 by (auto simp add: fresh_minus_perm) |
602 apply (drule_tac [!] p="-p" in b) |
598 |
603 apply (simp_all) |
|
604 apply (metis permute_minus_cancel(2)) |
|
605 apply (metis permute_minus_cancel(2)) |
|
606 done |
599 lemma alpha_gen_trans: |
607 lemma alpha_gen_trans: |
600 assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z" |
608 assumes a: "(\<forall>c. R y c \<longrightarrow> R (p \<bullet> x) c)" |
|
609 and b: "R (p \<bullet> x) y" |
|
610 and c: "R (q \<bullet> y) z" |
|
611 and d: "\<And>x y p. R x y \<Longrightarrow> R (p \<bullet> x) (p \<bullet> y)" |
601 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)" |
612 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)" |
602 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)" |
613 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)" |
603 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)" |
614 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)" |
604 using a |
|
605 unfolding alphas |
615 unfolding alphas |
606 unfolding fresh_star_def |
616 unfolding fresh_star_def |
607 by (simp_all add: fresh_plus_perm) |
617 apply (simp_all add: fresh_plus_perm) |
|
618 apply (metis a c d permute_minus_cancel(2))+ |
|
619 done |
608 |
620 |
609 lemma alpha_gen_eqvt: |
621 lemma alpha_gen_eqvt: |
610 assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
622 assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
611 and b: "p \<bullet> (f x) = f (p \<bullet> x)" |
623 and b: "p \<bullet> (f x) = f (p \<bullet> x)" |
612 and c: "p \<bullet> (f y) = f (p \<bullet> y)" |
624 and c: "p \<bullet> (f y) = f (p \<bullet> y)" |