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' |
192 thm eqvts_raw |
192 thm eqvts_raw |
|
193 |
|
194 |
|
195 |
|
196 (* HERE *) |
193 |
197 |
194 lemma |
198 lemma |
195 assumes a: "alpha_lam_raw' t1 t2" |
199 assumes a: "alpha_lam_raw' t1 t2" |
196 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
200 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
197 using a |
201 using a |
198 apply(induct) |
202 apply(induct) |
199 apply(perm_simp) |
|
200 apply(rule a1) |
|
201 apply(simp) |
|
202 apply(perm_simp) |
|
203 apply(rule a2) |
|
204 apply(simp) |
|
205 apply(simp) |
|
206 |
|
207 apply simp |
|
208 apply (rule a3) |
|
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 |
|
224 |
|
225 lemma |
|
226 assumes a: "alpha_lam_raw' t1 t2" |
|
227 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
|
228 using a |
|
229 apply(induct) |
|
230 ML_prf {* |
|
231 val ({names, ...}, {raw_induct, intrs, ...}) = |
|
232 Inductive.the_inductive @{context} (Sign.intern_const @{theory} "alpha_lam_raw") |
|
233 *} |
|
234 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac |
203 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac |
235 @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a1} 1*}) |
204 @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a1} 1*}) |
236 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac |
205 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac |
237 @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a2} 1*}) |
206 @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a2} 1*}) |
|
207 (* |
|
208 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac |
|
209 @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a3} 1*}) |
|
210 *) |
238 oops |
211 oops |
239 |
|
240 |
212 |
241 section {* size function *} |
213 section {* size function *} |
242 |
214 |
243 lemma size_eqvt_raw: |
215 lemma size_eqvt_raw: |
244 fixes t::"lam_raw" |
216 fixes t::"lam_raw" |