582 lemma supp_fv: |
582 lemma supp_fv: |
583 shows "supp t = fv t" |
583 shows "supp t = fv t" |
584 apply(induct t rule: lam_induct) |
584 apply(induct t rule: lam_induct) |
585 apply(simp add: var_supp) |
585 apply(simp add: var_supp) |
586 apply(simp add: app_supp) |
586 apply(simp add: app_supp) |
587 apply(subgoal_tac "supp (Lam name lam) = supp (Abs {atom name} lam)") |
587 apply(subgoal_tac "supp (Lam name lam) = supp (Abst {atom name} lam)") |
588 apply(simp add: supp_Abs) |
588 apply(simp add: supp_Abst) |
589 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
589 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
590 apply(simp add: Lam_pseudo_inject) |
590 apply(simp add: Lam_pseudo_inject) |
591 apply(simp add: abs_eq) |
591 apply(simp add: abs_eq alpha_gen) |
592 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
592 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
593 done |
593 done |
594 |
594 |
595 lemma lam_supp2: |
595 lemma lam_supp2: |
596 shows "supp (Lam x t) = supp (Abs {atom x} t)" |
596 shows "supp (Lam x t) = supp (Abst {atom x} t)" |
597 apply(simp add: supp_def permute_set_eq atom_eqvt) |
597 apply(simp add: supp_def permute_set_eq atom_eqvt) |
598 apply(simp add: Lam_pseudo_inject) |
598 apply(simp add: Lam_pseudo_inject) |
599 apply(simp add: abs_eq supp_fv) |
599 apply(simp add: abs_eq supp_fv alpha_gen) |
600 sorry |
600 done |
601 |
601 |
602 lemma lam_supp: |
602 lemma lam_supp: |
603 shows "supp (Lam x t) = ((supp t) - {atom x})" |
603 shows "supp (Lam x t) = ((supp t) - {atom x})" |
604 apply(simp add: lam_supp2) |
604 apply(simp add: lam_supp2) |
605 apply(simp add: supp_Abs) |
605 apply(simp add: supp_Abst) |
606 done |
606 done |
607 |
607 |
608 lemma fresh_lam: |
608 lemma fresh_lam: |
609 "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)" |
609 "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)" |
610 apply(simp add: fresh_def) |
610 apply(simp add: fresh_def) |