256 apply(default) |
256 apply(default) |
257 sorry |
257 sorry |
258 |
258 |
259 lemma lam_induct_strong: |
259 lemma lam_induct_strong: |
260 fixes a::"'a::fs_name" |
260 fixes a::"'a::fs_name" |
261 shows |
261 assumes a1: "\<And>name b. P b (Var name)" |
262 "\<lbrakk>\<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)" |
263 \<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)" |
264 \<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> lam\<rbrakk> \<Longrightarrow> P b (Lam name lam)\<rbrakk> |
264 shows "P a lam" |
265 \<Longrightarrow> P a lam" |
|
266 proof - |
265 proof - |
267 have "\<And>(pi::name prm). P a (pi \<bullet> lam)" |
266 have "\<And>(pi::name prm). P a (pi \<bullet> lam)" |
268 proof (induct lam rule: lam_induct) |
267 proof (induct lam rule: lam_induct) |
269 case (1 name pi) |
268 case (1 name pi) |
270 show "P a (pi \<bullet> Var name)" |
269 show "P a (pi \<bullet> Var name)" |
271 apply - |
270 apply (simp only: pi_var1) |
|
271 apply (rule a1) |
|
272 done |
|
273 next |
|
274 case (2 lam1 lam2 pi) |
|
275 have b1: "P a (pi \<bullet> lam1)" by fact |
|
276 have b2: "P a (pi \<bullet> lam2)" by fact |
|
277 show "P a (pi \<bullet> App lam1 lam2)" |
|
278 apply (simp only: pi_app) |
|
279 apply (rule a2) |
|
280 using b1 b2 |
272 sorry |
281 sorry |
273 next |
282 next |
274 case (2 lam1 lam2 pi) |
|
275 show "P a (pi \<bullet> App lam1 lam2)" sorry |
|
276 next |
|
277 case (3 name lam pi) |
283 case (3 name lam pi) |
278 show "P a (pi \<bullet> Lam name lam)" sorry |
284 have b: "P a (pi \<bullet> lam)" by fact |
|
285 show "P a (pi \<bullet> Lam name lam)" |
|
286 apply (simp add: pi_lam) |
|
287 using b |
|
288 sorry |
279 qed |
289 qed |
280 then have "P a (([]::name prm) \<bullet> lam)" by blast |
290 then have "P a (([]::name prm) \<bullet> lam)" by blast |
281 then show "P a lam" by simp |
291 then show "P a lam" by simp |
282 qed |
292 qed |
283 |
293 |