424 lemma fv_lam [simp]: |
424 lemma fv_lam [simp]: |
425 shows "fv (Var a) = {atom a}" |
425 shows "fv (Var a) = {atom a}" |
426 and "fv (App t1 t2) = fv t1 \<union> fv t2" |
426 and "fv (App t1 t2) = fv t1 \<union> fv t2" |
427 and "fv (Lam a t) = fv t - {atom a}" |
427 and "fv (Lam a t) = fv t - {atom a}" |
428 apply(lifting rfv_var rfv_app rfv_lam) |
428 apply(lifting rfv_var rfv_app rfv_lam) |
|
429 done |
|
430 |
|
431 lemma fv_eqvt: |
|
432 shows "(p \<bullet> fv t) = fv (p \<bullet> t)" |
|
433 apply(lifting rfv_eqvt) |
429 done |
434 done |
430 |
435 |
431 lemma a1: |
436 lemma a1: |
432 "a = b \<Longrightarrow> Var a = Var b" |
437 "a = b \<Longrightarrow> Var a = Var b" |
433 by (lifting a1) |
438 by (lifting a1) |
545 shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)" |
550 shows "supp (App t1 t2) = (supp t1) \<union> (supp t2)" |
546 apply(simp only: permute_lam supp_def lam_inject) |
551 apply(simp only: permute_lam supp_def lam_inject) |
547 apply(simp add: Collect_imp_eq Collect_neg_eq) |
552 apply(simp add: Collect_imp_eq Collect_neg_eq) |
548 done |
553 done |
549 |
554 |
550 (* needs thinking *) |
555 (* supp for lam *) |
551 lemma lam_supp1: |
556 lemma lam_supp1: |
552 shows "(supp (atom x, t)) supports (Lam x t) " |
557 shows "(supp (atom x, t)) supports (Lam x t) " |
553 apply(simp add: supports_def) |
558 apply(simp add: supports_def) |
554 apply(fold fresh_def) |
559 apply(fold fresh_def) |
555 apply(simp add: fresh_Pair swap_fresh_fresh) |
560 apply(simp add: fresh_Pair swap_fresh_fresh) |
572 apply(simp add: var_supp) |
577 apply(simp add: var_supp) |
573 apply(simp add: app_supp) |
578 apply(simp add: app_supp) |
574 apply(simp add: lam_fsupp1) |
579 apply(simp add: lam_fsupp1) |
575 done |
580 done |
576 |
581 |
|
582 lemma supp_fv: |
|
583 shows "supp t = fv t" |
|
584 apply(induct t rule: lam_induct) |
|
585 apply(simp add: var_supp) |
|
586 apply(simp add: app_supp) |
|
587 apply(subgoal_tac "supp (Lam name lam) = supp (Abs {atom name} lam)") |
|
588 apply(simp add: supp_Abs) |
|
589 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
|
590 apply(simp add: Lam_pseudo_inject) |
|
591 apply(simp add: abs_eq) |
|
592 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
|
593 done |
|
594 |
577 lemma lam_supp2: |
595 lemma lam_supp2: |
578 shows "supp (Lam x t) = supp (Abs {atom x} t)" |
596 shows "supp (Lam x t) = supp (Abs {atom x} t)" |
579 apply(simp add: supp_def permute_set_eq atom_eqvt) |
597 apply(simp add: supp_def permute_set_eq atom_eqvt) |
580 apply(simp add: Lam_pseudo_inject) |
598 apply(simp add: Lam_pseudo_inject) |
581 apply(simp add: abs_eq) |
599 apply(simp add: abs_eq supp_fv) |
582 sorry |
600 sorry |
583 |
601 |
584 lemma lam_supp: |
602 lemma lam_supp: |
585 shows "supp (Lam x t) = ((supp t) - {atom x})" |
603 shows "supp (Lam x t) = ((supp t) - {atom x})" |
586 apply(simp add: lam_supp2) |
604 apply(simp add: lam_supp2) |