48 shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2" |
48 shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2" |
49 and "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2" |
49 and "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2" |
50 and "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2" |
50 and "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2" |
51 by (case_tac [!] bs, case_tac [!] cs) |
51 by (case_tac [!] bs, case_tac [!] cs) |
52 (auto simp add: le_fun_def le_bool_def alphas) |
52 (auto simp add: le_fun_def le_bool_def alphas) |
|
53 |
|
54 (* equivariance *) |
|
55 lemma alpha_gen_eqvt[eqvt]: |
|
56 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)" |
|
57 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)" |
|
58 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)" |
|
59 unfolding alphas |
|
60 unfolding permute_eqvt[symmetric] |
|
61 unfolding set_eqvt[symmetric] |
|
62 unfolding permute_fun_app_eq[symmetric] |
|
63 unfolding Diff_eqvt[symmetric] |
|
64 by (auto simp add: permute_bool_def fresh_star_permute_iff) |
|
65 |
|
66 (* equivalence *) |
|
67 lemma alpha_gen_refl: |
|
68 assumes a: "R x x" |
|
69 shows "(bs, x) \<approx>gen R f 0 (bs, x)" |
|
70 and "(bs, x) \<approx>res R f 0 (bs, x)" |
|
71 and "(cs, x) \<approx>lst R f 0 (cs, x)" |
|
72 using a |
|
73 unfolding alphas |
|
74 unfolding fresh_star_def |
|
75 by (simp_all add: fresh_zero_perm) |
|
76 |
|
77 lemma alpha_gen_sym: |
|
78 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
|
79 shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" |
|
80 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
|
81 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
|
82 unfolding alphas fresh_star_def |
|
83 using a |
|
84 by (auto simp add: fresh_minus_perm) |
|
85 |
|
86 lemma alpha_gen_sym_eqvt: |
|
87 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" |
|
88 and b: "p \<bullet> R = R" |
|
89 shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" |
|
90 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
|
91 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
|
92 proof - |
|
93 { assume "R (p \<bullet> x) y" |
|
94 then have "R y (p \<bullet> x)" using a by simp |
|
95 then have "R (- p \<bullet> y) x" |
|
96 apply(rule_tac p="p" in permute_boolE) |
|
97 apply(perm_simp add: permute_minus_cancel b) |
|
98 apply(assumption) |
|
99 done |
|
100 } |
|
101 then show "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" |
|
102 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
|
103 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
|
104 unfolding alphas fresh_star_def |
|
105 by (auto simp add: fresh_minus_perm) |
|
106 qed |
|
107 |
|
108 lemma alpha_gen_trans: |
|
109 assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z" |
|
110 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)" |
|
111 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)" |
|
112 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)" |
|
113 using a |
|
114 unfolding alphas fresh_star_def |
|
115 by (simp_all add: fresh_plus_perm) |
|
116 |
|
117 |
|
118 |
|
119 section {* General Abstractions *} |
53 |
120 |
54 fun |
121 fun |
55 alpha_abs |
122 alpha_abs |
56 where |
123 where |
57 [simp del]: |
124 [simp del]: |
729 apply(simp) |
796 apply(simp) |
730 done |
797 done |
731 |
798 |
732 lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2 |
799 lemmas alphas_compose_trans2 = alpha_gen_compose_trans2 alpha_res_compose_trans2 alpha_lst_compose_trans2 |
733 |
800 |
734 lemma alpha_gen_refl: |
801 |
735 assumes a: "R x x" |
|
736 shows "(bs, x) \<approx>gen R f 0 (bs, x)" |
|
737 and "(bs, x) \<approx>res R f 0 (bs, x)" |
|
738 and "(cs, x) \<approx>lst R f 0 (cs, x)" |
|
739 using a |
|
740 unfolding alphas |
|
741 unfolding fresh_star_def |
|
742 by (simp_all add: fresh_zero_perm) |
|
743 |
|
744 lemma alpha_gen_sym: |
|
745 assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
|
746 shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" |
|
747 and "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" |
|
748 and "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)" |
|
749 unfolding alphas fresh_star_def |
|
750 using a |
|
751 by (auto simp add: fresh_minus_perm) |
|
752 |
|
753 lemma alpha_gen_trans: |
|
754 assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z" |
|
755 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)" |
|
756 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)" |
|
757 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)" |
|
758 using a |
|
759 unfolding alphas fresh_star_def |
|
760 by (simp_all add: fresh_plus_perm) |
|
761 |
|
762 |
|
763 lemma alpha_gen_eqvt[eqvt]: |
|
764 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)" |
|
765 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)" |
|
766 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)" |
|
767 unfolding alphas |
|
768 unfolding permute_eqvt[symmetric] |
|
769 unfolding set_eqvt[symmetric] |
|
770 unfolding permute_fun_app_eq[symmetric] |
|
771 unfolding Diff_eqvt[symmetric] |
|
772 by (auto simp add: permute_bool_def fresh_star_permute_iff) |
|
773 |
802 |
774 lemma alpha_gen_simpler: |
803 lemma alpha_gen_simpler: |
775 assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y" |
804 assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y" |
776 and fin_fv: "finite (f x)" |
805 and fin_fv: "finite (f x)" |
777 and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)" |
806 and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)" |