equal
deleted
inserted
replaced
181 alpha_lam_raw' |
181 alpha_lam_raw' |
182 where |
182 where |
183 a1: "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)" |
183 a1: "name = namea \<Longrightarrow> alpha_lam_raw' (Var_raw name) (Var_raw namea)" |
184 | a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow> |
184 | a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow> |
185 alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)" |
185 alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)" |
186 | a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow> |
186 | a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow> |
187 alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)" |
187 alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)" |
188 |
188 |
189 declare permute_lam_raw.simps[eqvt] |
189 declare permute_lam_raw.simps[eqvt] |
190 declare alpha_gen_eqvt[eqvt] |
190 declare alpha_gen_eqvt[eqvt] |
191 (*equivariance alpha_lam_raw'*) |
191 (*equivariance alpha_lam_raw'*) |
201 apply(simp) |
201 apply(simp) |
202 apply(perm_simp) |
202 apply(perm_simp) |
203 apply(rule a2) |
203 apply(rule a2) |
204 apply(simp) |
204 apply(simp) |
205 apply(simp) |
205 apply(simp) |
206 apply(perm_simp) |
206 |
207 apply(rule a3) |
207 apply simp |
208 apply(unfold alpha_gen) |
208 apply (rule a3) |
209 oops |
209 apply (erule exi[of _ _ "p"]) |
|
210 apply (simp add: alphas) |
|
211 apply (erule conjE)+ |
|
212 apply (rule conjI) |
|
213 apply (rule permute_eq_iff[of "- p", THEN iffD1]) |
|
214 apply (simp add: eqvts) |
|
215 apply (rule conjI) |
|
216 apply (rule fresh_star_permute_iff[of "- p", THEN iffD1]) |
|
217 apply (simp add: eqvts) |
|
218 apply (rule conjI) |
|
219 apply (simp add: permute_eqvt[symmetric]) |
|
220 apply (rule permute_eq_iff[of "- p", THEN iffD1]) |
|
221 apply (subst permute_eqvt) |
|
222 apply (simp add: eqvts) |
|
223 done |
210 |
224 |
211 lemma |
225 lemma |
212 assumes a: "alpha_lam_raw' t1 t2" |
226 assumes a: "alpha_lam_raw' t1 t2" |
213 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
227 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
214 using a |
228 using a |