513 using a by (auto simp add: swap_atom) |
513 using a by (auto simp add: swap_atom) |
514 |
514 |
515 lemma swap_set_in: |
515 lemma swap_set_in: |
516 assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b" |
516 assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b" |
517 shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S" |
517 shows "(a \<rightleftharpoons> b) \<bullet> S \<noteq> S" |
|
518 unfolding permute_set_eq |
|
519 using a by (auto simp add: swap_atom) |
|
520 |
|
521 lemma swap_set_in_eq: |
|
522 assumes a: "a \<in> S" "b \<notin> S" "sort_of a = sort_of b" |
|
523 shows "(a \<rightleftharpoons> b) \<bullet> S = (S - {a}) \<union> {b}" |
|
524 unfolding permute_set_eq |
|
525 using a by (auto simp add: swap_atom) |
|
526 |
|
527 lemma swap_set_both_in: |
|
528 assumes a: "a \<in> S" "b \<in> S" |
|
529 shows "(a \<rightleftharpoons> b) \<bullet> S = S" |
518 unfolding permute_set_eq |
530 unfolding permute_set_eq |
519 using a by (auto simp add: swap_atom) |
531 using a by (auto simp add: swap_atom) |
520 |
532 |
521 lemma mem_permute_iff: |
533 lemma mem_permute_iff: |
522 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
534 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
1715 and swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)" |
1727 and swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)" |
1716 shows "P p" |
1728 shows "P p" |
1717 by (rule_tac S="supp p" in perm_struct_induct) |
1729 by (rule_tac S="supp p" in perm_struct_induct) |
1718 (auto intro: zero swap) |
1730 (auto intro: zero swap) |
1719 |
1731 |
1720 lemma perm_subset_induct[consumes 1, case_names zero swap plus]: |
1732 lemma perm_struct_induct2[consumes 1, case_names zero swap plus]: |
1721 assumes S: "supp p \<subseteq> S" |
1733 assumes S: "supp p \<subseteq> S" |
1722 assumes zero: "P 0" |
1734 assumes zero: "P 0" |
1723 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
1735 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
1724 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
1736 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
1725 shows "P p" |
1737 shows "P p" |
1726 using S |
1738 using S |
1727 by (induct p rule: perm_struct_induct) |
1739 by (induct p rule: perm_struct_induct) |
1728 (auto intro: zero plus swap simp add: supp_swap) |
1740 (auto intro: zero plus swap simp add: supp_swap) |
|
1741 |
|
1742 lemma perm_simple_struct_induct2[case_names zero swap plus]: |
|
1743 assumes zero: "P 0" |
|
1744 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
|
1745 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
|
1746 shows "P p" |
|
1747 by (rule_tac S="supp p" in perm_struct_induct2) |
|
1748 (auto intro: zero swap plus) |
1729 |
1749 |
1730 lemma supp_perm_eq: |
1750 lemma supp_perm_eq: |
1731 assumes "(supp x) \<sharp>* p" |
1751 assumes "(supp x) \<sharp>* p" |
1732 shows "p \<bullet> x = x" |
1752 shows "p \<bullet> x = x" |
1733 proof - |
1753 proof - |
1749 shows "p \<bullet> x = x" |
1769 shows "p \<bullet> x = x" |
1750 proof - |
1770 proof - |
1751 from assms have "supp p \<subseteq> {a. a \<sharp> x}" |
1771 from assms have "supp p \<subseteq> {a. a \<sharp> x}" |
1752 unfolding supp_perm fresh_star_def fresh_def by auto |
1772 unfolding supp_perm fresh_star_def fresh_def by auto |
1753 then show "p \<bullet> x = x" |
1773 then show "p \<bullet> x = x" |
1754 proof (induct p rule: perm_subset_induct) |
1774 proof (induct p rule: perm_struct_induct2) |
1755 case zero |
1775 case zero |
1756 show "0 \<bullet> x = x" by simp |
1776 show "0 \<bullet> x = x" by simp |
1757 next |
1777 next |
1758 case (swap a b) |
1778 case (swap a b) |
1759 then have "a \<sharp> x" "b \<sharp> x" by simp_all |
1779 then have "a \<sharp> x" "b \<sharp> x" by simp_all |