261 assumes a1: "\<And>name b. P b (Var name)" |
261 assumes a1: "\<And>name b. P b (Var name)" |
262 and a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)" |
262 and a2: "\<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2)" |
263 and a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> lam\<rbrakk> \<Longrightarrow> P b (Lam name lam)" |
263 and a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> lam\<rbrakk> \<Longrightarrow> P b (Lam name lam)" |
264 shows "P a lam" |
264 shows "P a lam" |
265 proof - |
265 proof - |
266 have "\<And>(pi::name prm). P a (pi \<bullet> lam)" |
266 have "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" |
267 proof (induct lam rule: lam_induct) |
267 proof (induct lam rule: lam_induct) |
268 case (1 name pi) |
268 case (1 name pi) |
269 show "P a (pi \<bullet> Var name)" |
269 show "P a (pi \<bullet> Var name)" |
270 apply (simp only: pi_var1) |
270 apply (simp only: pi_var1) |
271 apply (rule a1) |
271 apply (rule a1) |
272 done |
272 done |
273 next |
273 next |
274 case (2 lam1 lam2 pi) |
274 case (2 lam1 lam2 pi) |
275 have b1: "P a (pi \<bullet> lam1)" by fact |
275 have b1: "\<And>(pi::name prm) a. P a (pi \<bullet> lam1)" by fact |
276 have b2: "P a (pi \<bullet> lam2)" by fact |
276 have b2: "\<And>(pi::name prm) a. P a (pi \<bullet> lam2)" by fact |
277 show "P a (pi \<bullet> App lam1 lam2)" |
277 show "P a (pi \<bullet> App lam1 lam2)" |
278 apply (simp only: pi_app) |
278 apply (simp only: pi_app) |
279 apply (rule a2) |
279 apply (rule a2) |
280 using b1 b2 |
280 apply (rule b1) |
281 sorry |
281 apply (rule b2) |
|
282 done |
282 next |
283 next |
283 case (3 name lam pi) |
284 case (3 name lam pi) |
284 have b: "P a (pi \<bullet> lam)" by fact |
285 have b: "P a (pi \<bullet> lam)" by fact |
285 show "P a (pi \<bullet> Lam name lam)" |
286 show "P a (pi \<bullet> Lam name lam)" |
286 apply (simp add: pi_lam) |
287 apply (simp add: pi_lam) |