170 apply(simp_all add:permute_bv) |
170 apply(simp_all add:permute_bv) |
171 apply(simp add: perm_bv1[symmetric]) |
171 apply(simp add: perm_bv1[symmetric]) |
172 apply(simp add: eqvts) |
172 apply(simp add: eqvts) |
173 done |
173 done |
174 |
174 |
|
175 lemma alpha_perm_bn1: |
|
176 " alpha_bv_tvtk tvtk_lst (permute_bv_tvtk q tvtk_lst)" |
|
177 "alpha_bv_tvck tvck_lst (permute_bv_tvck q tvck_lst)" |
|
178 "alpha_bv_vt vt_lst (permute_bv_vt q vt_lst)" |
|
179 apply(induct tvtk_lst rule: inducts(11)) |
|
180 apply(simp_all add:permute_bv eqvts eq_iff) |
|
181 apply(induct tvck_lst rule: inducts(12)) |
|
182 apply(simp_all add:permute_bv eqvts eq_iff) |
|
183 apply(induct vt_lst rule: inducts(10)) |
|
184 apply(simp_all add:permute_bv eqvts eq_iff) |
|
185 done |
|
186 |
|
187 lemma alpha_perm_bn: |
|
188 "alpha_bv pat (permute_bv q pat)" |
|
189 apply(induct pat rule: inducts(9)) |
|
190 apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1) |
|
191 done |
|
192 |
175 lemma ACons_subst: |
193 lemma ACons_subst: |
176 "supp (Abs (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al" |
194 "supp (Abs (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al" |
177 sorry |
195 apply (simp only: eq_iff) |
|
196 apply (rule_tac x="q" in exI) |
|
197 apply (simp add: alphas) |
|
198 apply (simp add: perm_bv2[symmetric]) |
|
199 apply (simp add: eqvts[symmetric]) |
|
200 apply (simp add: supp_Abs) |
|
201 apply (simp add: fv_supp) |
|
202 apply (simp add: alpha_perm_bn) |
|
203 apply (rule supp_perm_eq[symmetric]) |
|
204 apply (subst supp_finite_atom_set) |
|
205 apply (rule finite_Diff) |
|
206 apply (simp add: finite_supp) |
|
207 apply (assumption) |
|
208 done |
178 |
209 |
179 lemma permute_bv_zero1: |
210 lemma permute_bv_zero1: |
180 "permute_bv_tvck 0 b = b" |
211 "permute_bv_tvck 0 b = b" |
181 "permute_bv_tvtk 0 c = c" |
212 "permute_bv_tvtk 0 c = c" |
182 "permute_bv_vt 0 d = d" |
213 "permute_bv_vt 0 d = d" |