45 fixes p q::perm |
45 fixes p q::perm |
46 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
46 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
47 unfolding fresh_star_def |
47 unfolding fresh_star_def |
48 by (simp add: fresh_plus) |
48 by (simp add: fresh_plus) |
49 |
49 |
50 lemma supp_finite_set: |
|
51 fixes S::"atom set" |
|
52 assumes "finite S" |
|
53 shows "supp S = S" |
|
54 apply(rule finite_supp_unique) |
|
55 apply(simp add: supports_def) |
|
56 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
57 apply(metis) |
|
58 apply(rule assms) |
|
59 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
60 done |
|
61 |
|
62 |
50 |
63 atom_decl name |
51 atom_decl name |
64 |
52 |
65 datatype rlam = |
53 datatype rlam = |
66 rVar "name" |
54 rVar "name" |
582 lemma supp_fv: |
570 lemma supp_fv: |
583 shows "supp t = fv t" |
571 shows "supp t = fv t" |
584 apply(induct t rule: lam_induct) |
572 apply(induct t rule: lam_induct) |
585 apply(simp add: var_supp) |
573 apply(simp add: var_supp) |
586 apply(simp add: app_supp) |
574 apply(simp add: app_supp) |
587 apply(subgoal_tac "supp (Lam name lam) = supp (Abst {atom name} lam)") |
575 apply(subgoal_tac "supp (Lam name lam) = supp (Abs {atom name} lam)") |
588 apply(simp add: supp_Abst) |
576 apply(simp add: supp_Abs) |
589 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
577 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt) |
590 apply(simp add: Lam_pseudo_inject) |
578 apply(simp add: Lam_pseudo_inject) |
591 apply(simp add: abs_eq alpha_gen) |
579 apply(simp add: Abs_eq_iff alpha_gen) |
592 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
580 apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric]) |
593 done |
581 done |
594 |
582 |
595 lemma lam_supp2: |
583 lemma lam_supp2: |
596 shows "supp (Lam x t) = supp (Abst {atom x} t)" |
584 shows "supp (Lam x t) = supp (Abs {atom x} t)" |
597 apply(simp add: supp_def permute_set_eq atom_eqvt) |
585 apply(simp add: supp_def permute_set_eq atom_eqvt) |
598 apply(simp add: Lam_pseudo_inject) |
586 apply(simp add: Lam_pseudo_inject) |
599 apply(simp add: abs_eq supp_fv alpha_gen) |
587 apply(simp add: Abs_eq_iff supp_fv alpha_gen) |
600 done |
588 done |
601 |
589 |
602 lemma lam_supp: |
590 lemma lam_supp: |
603 shows "supp (Lam x t) = ((supp t) - {atom x})" |
591 shows "supp (Lam x t) = ((supp t) - {atom x})" |
604 apply(simp add: lam_supp2) |
592 apply(simp add: lam_supp2) |
605 apply(simp add: supp_Abst) |
593 apply(simp add: supp_Abs) |
606 done |
594 done |
607 |
595 |
608 lemma fresh_lam: |
596 lemma fresh_lam: |
609 "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)" |
597 "(atom a \<sharp> Lam b t) \<longleftrightarrow> (a = b) \<or> (a \<noteq> b \<and> atom a \<sharp> t)" |
610 apply(simp add: fresh_def) |
598 apply(simp add: fresh_def) |