223 lemma swap_different_sorts [simp]: |
223 lemma swap_different_sorts [simp]: |
224 "sort_of a \<noteq> sort_of b \<Longrightarrow> (a \<rightleftharpoons> b) = 0" |
224 "sort_of a \<noteq> sort_of b \<Longrightarrow> (a \<rightleftharpoons> b) = 0" |
225 by (rule Rep_perm_ext) (simp add: Rep_perm_simps) |
225 by (rule Rep_perm_ext) (simp add: Rep_perm_simps) |
226 |
226 |
227 lemma swap_cancel: |
227 lemma swap_cancel: |
228 "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0" |
228 shows "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0" |
229 by (rule Rep_perm_ext) |
229 and "(a \<rightleftharpoons> b) + (b \<rightleftharpoons> a) = 0" |
230 (simp add: Rep_perm_simps fun_eq_iff) |
230 by (rule_tac [!] Rep_perm_ext) |
|
231 (simp_all add: Rep_perm_simps fun_eq_iff) |
231 |
232 |
232 lemma swap_self [simp]: |
233 lemma swap_self [simp]: |
233 "(a \<rightleftharpoons> a) = 0" |
234 "(a \<rightleftharpoons> a) = 0" |
234 by (rule Rep_perm_ext, simp add: Rep_perm_simps fun_eq_iff) |
235 by (rule Rep_perm_ext, simp add: Rep_perm_simps fun_eq_iff) |
235 |
236 |
236 lemma minus_swap [simp]: |
237 lemma minus_swap [simp]: |
237 "- (a \<rightleftharpoons> b) = (a \<rightleftharpoons> b)" |
238 "- (a \<rightleftharpoons> b) = (a \<rightleftharpoons> b)" |
238 by (rule minus_unique [OF swap_cancel]) |
239 by (rule minus_unique [OF swap_cancel(1)]) |
239 |
240 |
240 lemma swap_commute: |
241 lemma swap_commute: |
241 "(a \<rightleftharpoons> b) = (b \<rightleftharpoons> a)" |
242 "(a \<rightleftharpoons> b) = (b \<rightleftharpoons> a)" |
242 by (rule Rep_perm_ext) |
243 by (rule Rep_perm_ext) |
243 (simp add: Rep_perm_swap fun_eq_iff) |
244 (simp add: Rep_perm_swap fun_eq_iff) |
1394 assumes "finite S" |
1395 assumes "finite S" |
1395 shows "a \<sharp> S \<longleftrightarrow> a \<notin> S" |
1396 shows "a \<sharp> S \<longleftrightarrow> a \<notin> S" |
1396 unfolding fresh_def |
1397 unfolding fresh_def |
1397 by (simp add: supp_finite_atom_set[OF assms]) |
1398 by (simp add: supp_finite_atom_set[OF assms]) |
1398 |
1399 |
|
1400 lemma fresh_minus_atom_set: |
|
1401 fixes S::"atom set" |
|
1402 assumes "finite S" |
|
1403 shows "a \<sharp> S - T \<longleftrightarrow> (a \<notin> T \<longrightarrow> a \<sharp> S)" |
|
1404 unfolding fresh_def |
|
1405 by (auto simp add: supp_finite_atom_set assms) |
|
1406 |
|
1407 |
1399 lemma Union_fresh: |
1408 lemma Union_fresh: |
1400 shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)" |
1409 shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)" |
1401 unfolding Union_image_eq[symmetric] |
1410 unfolding Union_image_eq[symmetric] |
1402 apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app) |
1411 apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app) |
1403 unfolding eqvt_def |
1412 unfolding eqvt_def |
1607 and fin: "finite as" |
1616 and fin: "finite as" |
1608 shows "supp p \<sharp>* as" |
1617 shows "supp p \<sharp>* as" |
1609 apply(rule fresh_star_supp_conv) |
1618 apply(rule fresh_star_supp_conv) |
1610 apply(simp add: supp_finite_atom_set fin fresh) |
1619 apply(simp add: supp_finite_atom_set fin fresh) |
1611 done |
1620 done |
|
1621 |
|
1622 lemma fresh_star_atom_set_conv: |
|
1623 fixes p::"perm" |
|
1624 assumes fresh: "as \<sharp>* bs" |
|
1625 and fin: "finite as" "finite bs" |
|
1626 shows "bs \<sharp>* as" |
|
1627 using fresh |
|
1628 unfolding fresh_star_def fresh_def |
|
1629 by (auto simp add: supp_finite_atom_set fin) |
1612 |
1630 |
1613 |
1631 |
1614 lemma fresh_star_Pair: |
1632 lemma fresh_star_Pair: |
1615 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
1633 shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" |
1616 by (auto simp add: fresh_star_def fresh_Pair) |
1634 by (auto simp add: fresh_star_def fresh_Pair) |
1769 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
1787 assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)" |
1770 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
1788 assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)" |
1771 shows "P p" |
1789 shows "P p" |
1772 by (rule_tac S="supp p" in perm_struct_induct2) |
1790 by (rule_tac S="supp p" in perm_struct_induct2) |
1773 (auto intro: zero swap plus) |
1791 (auto intro: zero swap plus) |
|
1792 |
|
1793 lemma supp_perm_singleton: |
|
1794 fixes p::"perm" |
|
1795 shows "supp p \<subseteq> {b} \<longleftrightarrow> p = 0" |
|
1796 proof - |
|
1797 { assume "supp p \<subseteq> {b}" |
|
1798 then have "p = 0" |
|
1799 by (induct p rule: perm_struct_induct) (simp_all) |
|
1800 } |
|
1801 then show "supp p \<subseteq> {b} \<longleftrightarrow> p = 0" by (auto simp add: supp_zero_perm) |
|
1802 qed |
|
1803 |
|
1804 lemma supp_perm_pair: |
|
1805 fixes p::"perm" |
|
1806 shows "supp p \<subseteq> {a, b} \<longleftrightarrow> p = 0 \<or> p = (b \<rightleftharpoons> a)" |
|
1807 proof - |
|
1808 { assume "supp p \<subseteq> {a, b}" |
|
1809 then have "p = 0 \<or> p = (b \<rightleftharpoons> a)" |
|
1810 apply (induct p rule: perm_struct_induct) |
|
1811 apply (auto simp add: swap_cancel supp_zero_perm supp_swap) |
|
1812 apply (simp add: swap_commute) |
|
1813 done |
|
1814 } |
|
1815 then show "supp p \<subseteq> {a, b} \<longleftrightarrow> p = 0 \<or> p = (b \<rightleftharpoons> a)" |
|
1816 by (auto simp add: supp_zero_perm supp_swap split: if_splits) |
|
1817 qed |
1774 |
1818 |
1775 lemma supp_perm_eq: |
1819 lemma supp_perm_eq: |
1776 assumes "(supp x) \<sharp>* p" |
1820 assumes "(supp x) \<sharp>* p" |
1777 shows "p \<bullet> x = x" |
1821 shows "p \<bullet> x = x" |
1778 proof - |
1822 proof - |