303 "(alpha ===> op =) rfv rfv" |
296 "(alpha ===> op =) rfv rfv" |
304 apply(simp add: alpha_rfv) |
297 apply(simp add: alpha_rfv) |
305 done |
298 done |
306 |
299 |
307 |
300 |
308 |
|
309 (* NOT SURE see above |
|
310 lemma fresh_rsp: |
|
311 "(op = ===> alpha ===> op =) fresh fresh" |
|
312 apply(auto) |
|
313 *) |
|
314 |
|
315 section {* lifted theorems *} |
301 section {* lifted theorems *} |
316 |
302 |
317 lemma lam_induct: |
303 lemma lam_induct: |
318 "\<lbrakk>\<And>name. P (Var name); |
304 "\<lbrakk>\<And>name. P (Var name); |
319 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
305 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
373 \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s \<and> pi \<bullet> a = b\<rbrakk> |
359 \<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> (fv t - {atom a}) \<sharp>* pi \<and> (pi \<bullet> t) = s \<and> pi \<bullet> a = b\<rbrakk> |
374 \<Longrightarrow> P\<rbrakk> |
360 \<Longrightarrow> P\<rbrakk> |
375 \<Longrightarrow> P" |
361 \<Longrightarrow> P" |
376 by (lifting alpha.cases) |
362 by (lifting alpha.cases) |
377 |
363 |
|
364 (* not sure whether needed *) |
378 lemma alpha_induct: |
365 lemma alpha_induct: |
379 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
366 "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b); |
380 \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
367 \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc); |
381 \<And>t a s b. |
368 \<And>t a s b. |
382 \<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> |
369 \<lbrakk>\<exists>pi. fv t - {atom a} = fv s - {atom b} \<and> |
448 apply(simp only: permute_lam supp_def lam_inject) |
435 apply(simp only: permute_lam supp_def lam_inject) |
449 apply(simp add: Collect_imp_eq Collect_neg_eq) |
436 apply(simp add: Collect_imp_eq Collect_neg_eq) |
450 done |
437 done |
451 |
438 |
452 (* needs thinking *) |
439 (* needs thinking *) |
453 lemma lam_supp: |
440 lemma lam_supp1: |
454 shows "supp (Lam x t) = ((supp t) - {atom x})" |
441 shows "(supp (atom x, t)) supports (Lam x t) " |
455 apply(simp add: supp_def) |
442 apply(simp add: supports_def) |
456 sorry |
443 apply(fold fresh_def) |
457 |
444 apply(simp add: fresh_Pair swap_fresh_fresh) |
|
445 apply(clarify) |
|
446 apply(subst swap_at_base_simps(3)) |
|
447 apply(simp_all add: fresh_atom) |
|
448 done |
|
449 |
|
450 lemma lam_fsupp1: |
|
451 assumes a: "finite (supp t)" |
|
452 shows "finite (supp (Lam x t))" |
|
453 apply(rule supports_finite) |
|
454 apply(rule lam_supp1) |
|
455 apply(simp add: a supp_Pair supp_atom) |
|
456 done |
458 |
457 |
459 instance lam :: fs |
458 instance lam :: fs |
460 apply(default) |
459 apply(default) |
461 apply(induct_tac x rule: lam_induct) |
460 apply(induct_tac x rule: lam_induct) |
462 apply(simp add: var_supp) |
461 apply(simp add: var_supp) |
463 apply(simp add: app_supp) |
462 apply(simp add: app_supp) |
464 apply(simp add: lam_supp) |
463 apply(simp add: lam_fsupp1) |
465 done |
464 done |
|
465 |
|
466 lemma lam_fresh1: |
|
467 assumes f: "finite (supp t)" |
|
468 and a1: "b \<sharp> t" |
|
469 and a2: "atom a \<noteq> b" |
|
470 shows "b \<sharp> Lam a t" |
|
471 proof - |
|
472 have "\<exists>c. c \<sharp> (b, a ,t, Lam a t)" sorry |
|
473 then obtain c where fr1: "c \<noteq> b" |
|
474 and fr2: "c \<noteq> atom a" |
|
475 and fr3: "c \<sharp> t" |
|
476 and fr4: "c \<sharp> Lam a t" |
|
477 and fr5: "sort_of b = sort_of c" |
|
478 apply(auto simp add: fresh_Pair fresh_atom) |
|
479 sorry |
|
480 have e: "(c \<rightleftharpoons> b) \<bullet> (Lam a t) = Lam a ((c \<rightleftharpoons> b) \<bullet> t)" using a2 fr1 fr2 |
|
481 by simp |
|
482 from fr4 have "((c \<rightleftharpoons> b) \<bullet>c) \<sharp> ((c \<rightleftharpoons> b) \<bullet>(Lam a t))" |
|
483 by (simp only: fresh_permute_iff) |
|
484 then have "b \<sharp> (Lam a ((c \<rightleftharpoons> b) \<bullet> t))" using fr1 fr2 fr5 e |
|
485 by simp |
|
486 then show ?thesis using a1 fr3 |
|
487 by (simp only: swap_fresh_fresh) |
|
488 qed |
|
489 |
|
490 lemma lam_fresh2: |
|
491 assumes f: "finite (supp t)" |
|
492 shows "(atom a) \<sharp> Lam a t" |
|
493 sorry |
|
494 |
|
495 |
|
496 lemma lam_supp: |
|
497 shows "supp (Lam x t) = ((supp t) - {atom x})" |
|
498 apply(default) |
|
499 apply(simp_all add: supp_conv_fresh) |
|
500 apply(auto) |
|
501 sorry |
466 |
502 |
467 lemma fresh_lam: |
503 lemma fresh_lam: |
468 "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)" |
504 "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)" |
469 apply(simp add: fresh_def) |
505 apply(simp add: fresh_def) |
470 apply(simp add: lam_supp) |
506 apply(simp add: lam_supp) |