616 |
616 |
617 subsection {* Permutations for @{typ "'a fset"} *} |
617 subsection {* Permutations for @{typ "'a fset"} *} |
618 |
618 |
619 lemma permute_fset_rsp[quot_respect]: |
619 lemma permute_fset_rsp[quot_respect]: |
620 shows "(op = ===> list_eq ===> list_eq) permute permute" |
620 shows "(op = ===> list_eq ===> list_eq) permute permute" |
621 unfolding fun_rel_def |
621 unfolding rel_fun_def |
622 by (simp add: set_eqvt[symmetric]) |
622 by (simp add: set_eqvt[symmetric]) |
623 |
623 |
624 instantiation fset :: (pt) pt |
624 instantiation fset :: (pt) pt |
625 begin |
625 begin |
626 |
626 |
1189 by (induct xs) (simp_all add: permute_pure) |
1189 by (induct xs) (simp_all add: permute_pure) |
1190 |
1190 |
1191 |
1191 |
1192 subsubsection {* Equivariance for @{typ "'a option"} *} |
1192 subsubsection {* Equivariance for @{typ "'a option"} *} |
1193 |
1193 |
1194 lemma option_map_eqvt[eqvt]: |
1194 lemma map_option_eqvt[eqvt]: |
1195 shows "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)" |
1195 shows "p \<bullet> (map_option f x) = map_option (p \<bullet> f) (p \<bullet> x)" |
1196 by (cases x) (simp_all) |
1196 by (cases x) (simp_all) |
1197 |
1197 |
1198 |
1198 |
1199 subsubsection {* Equivariance for @{typ "'a fset"} *} |
1199 subsubsection {* Equivariance for @{typ "'a fset"} *} |
1200 |
1200 |
1563 fix a::"atom" |
1563 fix a::"atom" |
1564 show "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1564 show "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1565 proof - |
1565 proof - |
1566 { assume "a \<notin> supp p" "a \<notin> supp q" |
1566 { assume "a \<notin> supp p" "a \<notin> supp q" |
1567 then have "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1567 then have "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1568 by (simp add: supp_perm) |
1568 by (simp add: supp_perm) |
1569 } |
1569 } |
1570 moreover |
1570 moreover |
1571 { assume a: "a \<in> supp p" "a \<notin> supp q" |
1571 { assume a: "a \<in> supp p" "a \<notin> supp q" |
1572 then have "p \<bullet> a \<in> supp p" by (simp add: supp_perm) |
1572 then have "p \<bullet> a \<in> supp p" by (simp add: supp_perm) |
1573 then have "p \<bullet> a \<notin> supp q" using asm by auto |
1573 then have "p \<bullet> a \<notin> supp q" using asm by auto |
1574 with a have "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1574 with a have "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1575 by (simp add: supp_perm) |
1575 by (simp add: supp_perm) |
1576 } |
1576 } |
1577 moreover |
1577 moreover |
1578 { assume a: "a \<notin> supp p" "a \<in> supp q" |
1578 { assume a: "a \<notin> supp p" "a \<in> supp q" |
1579 then have "q \<bullet> a \<in> supp q" by (simp add: supp_perm) |
1579 then have "q \<bullet> a \<in> supp q" by (simp add: supp_perm) |
1580 then have "q \<bullet> a \<notin> supp p" using asm by auto |
1580 then have "q \<bullet> a \<notin> supp p" using asm by auto |
1581 with a have "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1581 with a have "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1582 by (simp add: supp_perm) |
1582 by (simp add: supp_perm) |
1583 } |
1583 } |
1584 ultimately show "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1584 ultimately show "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1585 using asm by blast |
1585 using asm by blast |
1586 qed |
1586 qed |
1587 qed |
1587 qed |
2791 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
2791 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
2792 have "\<forall>b \<in> insert a bs. q' \<bullet> b = p \<bullet> b" using 2 * `a \<notin> bs` unfolding q'_def |
2792 have "\<forall>b \<in> insert a bs. q' \<bullet> b = p \<bullet> b" using 2 * `a \<notin> bs` unfolding q'_def |
2793 by (auto simp: swap_atom) |
2793 by (auto simp: swap_atom) |
2794 moreover |
2794 moreover |
2795 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2795 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2796 using ** |
2796 using ** |
2797 apply (auto simp: supp_perm insert_eqvt) |
2797 apply (auto simp: supp_perm insert_eqvt) |
2798 apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs") |
2798 apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs") |
2799 apply(auto)[1] |
2799 apply(auto)[1] |
2800 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2800 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2801 apply(blast) |
2801 apply(blast) |
2802 apply(simp) |
2802 apply(simp) |
2803 done |
2803 done |
2804 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2804 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2805 unfolding supp_swap by auto |
2805 unfolding supp_swap by auto |
2806 moreover |
2806 moreover |
2807 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2807 have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2808 using ** by (auto simp: insert_eqvt) |
2808 using ** by (auto simp: insert_eqvt) |
2809 ultimately |
2809 ultimately |
2810 have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2810 have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" |
2811 unfolding q'_def using supp_plus_perm by blast |
2811 unfolding q'_def using supp_plus_perm by blast |
2812 } |
2812 } |
2813 ultimately |
2813 ultimately |
2860 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
2860 def q' \<equiv> "((q \<bullet> a) \<rightleftharpoons> (p \<bullet> a)) + q" |
2861 have "\<forall>b \<in> set (a # bs). q' \<bullet> b = p \<bullet> b" |
2861 have "\<forall>b \<in> set (a # bs). q' \<bullet> b = p \<bullet> b" |
2862 unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp: swap_atom) |
2862 unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp: swap_atom) |
2863 moreover |
2863 moreover |
2864 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2864 { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2865 using ** |
2865 using ** |
2866 apply (auto simp: supp_perm insert_eqvt) |
2866 apply (auto simp: supp_perm insert_eqvt) |
2867 apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs") |
2867 apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs") |
2868 apply(auto)[1] |
2868 apply(auto)[1] |
2869 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2869 apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}") |
2870 apply(blast) |
2870 apply(blast) |
2871 apply(simp) |
2871 apply(simp) |
2872 done |
2872 done |
2873 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" |
2873 then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" |
2874 unfolding supp_swap by auto |
2874 unfolding supp_swap by auto |
2875 moreover |
2875 moreover |
2876 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2876 have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2877 using ** by (auto simp: insert_eqvt) |
2877 using ** by (auto simp: insert_eqvt) |
2878 ultimately |
2878 ultimately |
2879 have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2879 have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" |
2880 unfolding q'_def using supp_plus_perm by blast |
2880 unfolding q'_def using supp_plus_perm by blast |
2881 } |
2881 } |
2882 ultimately |
2882 ultimately |