equal
deleted
inserted
replaced
254 |
254 |
255 instance lam::fs_name |
255 instance lam::fs_name |
256 apply(default) |
256 apply(default) |
257 sorry |
257 sorry |
258 |
258 |
|
259 lemma fresh_lam: |
|
260 "(a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> a \<sharp> t)" |
|
261 sorry |
|
262 |
259 lemma lam_induct_strong: |
263 lemma lam_induct_strong: |
260 fixes a::"'a::fs_name" |
264 fixes a::"'a::fs_name" |
261 assumes a1: "\<And>name b. P b (Var name)" |
265 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)" |
266 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)" |
267 and a3: "\<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lam name lam)" |
264 shows "P a lam" |
268 shows "P a lam" |
265 proof - |
269 proof - |
266 have "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" |
270 have "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" |
267 proof (induct lam rule: lam_induct) |
271 proof (induct lam rule: lam_induct) |
268 case (1 name pi) |
272 case (1 name pi) |
279 apply (rule a2) |
283 apply (rule a2) |
280 apply (rule b1) |
284 apply (rule b1) |
281 apply (rule b2) |
285 apply (rule b2) |
282 done |
286 done |
283 next |
287 next |
284 case (3 name lam pi) |
288 case (3 name lam pi a) |
285 have b: "P a (pi \<bullet> lam)" by fact |
289 have b: "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" by fact |
|
290 obtain c::name where fr: "c\<sharp>(a, pi\<bullet>name, pi\<bullet>lam)" sorry |
|
291 from b fr have p: "P a (Lam c (([(c, pi\<bullet>name)]@pi)\<bullet>lam))" |
|
292 apply - |
|
293 apply(rule a3) |
|
294 apply(blast) |
|
295 apply(simp) |
|
296 done |
|
297 have eq: "[(c, pi\<bullet>name)] \<bullet> Lam (pi \<bullet> name) (pi \<bullet> lam) = Lam (pi \<bullet> name) (pi \<bullet> lam)" |
|
298 apply(rule perm_fresh_fresh) |
|
299 using fr |
|
300 apply(simp add: fresh_lam) |
|
301 apply(simp add: fresh_lam) |
|
302 done |
286 show "P a (pi \<bullet> Lam name lam)" |
303 show "P a (pi \<bullet> Lam name lam)" |
287 apply (simp add: pi_lam) |
304 apply (simp add: pi_lam) |
288 using b |
305 apply(subst eq[symmetric]) |
289 sorry |
306 using p |
|
307 apply(simp only: pi_lam pt_name2 swap_simps) |
|
308 done |
290 qed |
309 qed |
291 then have "P a (([]::name prm) \<bullet> lam)" by blast |
310 then have "P a (([]::name prm) \<bullet> lam)" by blast |
292 then show "P a lam" by simp |
311 then show "P a lam" by simp |
293 qed |
312 qed |
294 |
313 |