178 |
178 |
179 |
179 |
180 inductive |
180 inductive |
181 alpha_lam_raw' |
181 alpha_lam_raw' |
182 where |
182 where |
183 "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 | "\<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 | "\<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_real_eqvt[eqvt]*) |
190 declare alpha_gen_eqvt[eqvt] |
191 (*equivariance alpha_lam_raw'*) |
191 (*equivariance alpha_lam_raw'*) |
|
192 thm eqvts_raw |
|
193 |
|
194 lemma |
|
195 assumes a: "alpha_lam_raw' t1 t2" |
|
196 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
|
197 oops |
192 |
198 |
193 lemma |
199 lemma |
194 assumes a: "alpha_lam_raw' t1 t2" |
200 assumes a: "alpha_lam_raw' t1 t2" |
195 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
201 shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)" |
196 using a |
202 using a |
197 apply(induct) |
203 apply(induct) |
|
204 ML_prf {* |
|
205 val ({names, ...}, {raw_induct, intrs, ...}) = |
|
206 Inductive.the_inductive @{context} (Sign.intern_const @{theory} "alpha_lam_raw") |
|
207 *} |
|
208 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac |
|
209 @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a1} 1*}) |
|
210 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac |
|
211 @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a2} 1*}) |
198 oops |
212 oops |
199 |
213 |
200 |
214 |
201 section {* size function *} |
215 section {* size function *} |
202 |
216 |