equal
deleted
inserted
replaced
1652 apply(rule fresh_star_supp_conv) |
1652 apply(rule fresh_star_supp_conv) |
1653 apply(simp add: supp_finite_atom_set fin fresh) |
1653 apply(simp add: supp_finite_atom_set fin fresh) |
1654 done |
1654 done |
1655 |
1655 |
1656 lemma fresh_star_atom_set_conv: |
1656 lemma fresh_star_atom_set_conv: |
1657 fixes p::"perm" |
|
1658 assumes fresh: "as \<sharp>* bs" |
1657 assumes fresh: "as \<sharp>* bs" |
1659 and fin: "finite as" "finite bs" |
1658 and fin: "finite as" "finite bs" |
1660 shows "bs \<sharp>* as" |
1659 shows "bs \<sharp>* as" |
1661 using fresh |
1660 using fresh |
|
1661 unfolding fresh_star_def fresh_def |
|
1662 by (auto simp add: supp_finite_atom_set fin) |
|
1663 |
|
1664 lemma atom_fresh_star_disjoint: |
|
1665 assumes fin: "finite bs" |
|
1666 shows "as \<sharp>* bs \<longleftrightarrow> (as \<inter> bs = {})" |
|
1667 |
1662 unfolding fresh_star_def fresh_def |
1668 unfolding fresh_star_def fresh_def |
1663 by (auto simp add: supp_finite_atom_set fin) |
1669 by (auto simp add: supp_finite_atom_set fin) |
1664 |
1670 |
1665 |
1671 |
1666 lemma fresh_star_Pair: |
1672 lemma fresh_star_Pair: |
1745 apply(simp add: all_eqvt) |
1751 apply(simp add: all_eqvt) |
1746 apply(subst permute_fun_def) |
1752 apply(subst permute_fun_def) |
1747 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt) |
1753 apply(simp add: imp_eqvt fresh_eqvt mem_eqvt) |
1748 done |
1754 done |
1749 |
1755 |
1750 lemma at_fresh_star_inter: |
|
1751 assumes a: "(p \<bullet> bs) \<sharp>* bs" |
|
1752 and b: "finite bs" |
|
1753 shows "p \<bullet> bs \<inter> bs = {}" |
|
1754 using a b |
|
1755 unfolding fresh_star_def |
|
1756 unfolding fresh_def |
|
1757 by (auto simp add: supp_finite_atom_set) |
|
1758 |
1756 |
1759 |
1757 |
1760 section {* Induction principle for permutations *} |
1758 section {* Induction principle for permutations *} |
1761 |
1759 |
1762 |
1760 |