759 lemma permute_eqvt:

   759 lemma permute_eqvt:

   760   shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)"

   760   shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)"

   761   unfolding permute_perm_def by simp

   761   unfolding permute_perm_def by simp

   762 

   762 

   763 (* the normal version of this lemma would cause loops *)

   763 (* the normal version of this lemma would cause loops *)

   765   shows "p \<bullet> permute \<equiv> permute"

   765   shows "p \<bullet> permute \<equiv> permute"

   766 apply(simp add: fun_eq_iff permute_fun_def)

   766 apply(simp add: fun_eq_iff permute_fun_def)

   767 apply(subst permute_eqvt)

   767 apply(subst permute_eqvt)

   768 apply(simp)

   768 apply(simp)

   769 done

   769 done

   823 

   823 

   824 lemma ex1_eqvt [eqvt]:

   824 lemma ex1_eqvt [eqvt]:

   825   shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"

   825   shows "p \<bullet> (\<exists>!x. P x) = (\<exists>!x. (p \<bullet> P) x)"

   826   unfolding Ex1_def

   826   unfolding Ex1_def

   827   by (perm_simp) (rule refl)

   827   by (perm_simp) (rule refl)

   848 

   828 

   849 lemma if_eqvt [eqvt]:

   829 lemma if_eqvt [eqvt]:

   850   shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"

   830   shows "p \<bullet> (if b then x else y) = (if p \<bullet> b then p \<bullet> x else p \<bullet> y)"

   851   by (simp add: permute_fun_def permute_bool_def)

   831   by (simp add: permute_fun_def permute_bool_def)

   852 

   832 

   894   apply(simp add: permute_bool_def unique)

   874   apply(simp add: permute_bool_def unique)

   895   apply(simp add: permute_bool_def)

   875   apply(simp add: permute_bool_def)

   896   apply(rule theI'[OF unique])

   876   apply(rule theI'[OF unique])

   897   done

   877   done

   898 

   878 

   900 

   894 

   901 lemma Bex_eqvt [eqvt]:

   895 lemma Bex_eqvt [eqvt]:

   902   shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"

   896   shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"

   903   unfolding Bex_def

   897   unfolding Bex_def

   904   by (perm_simp) (rule refl)

   898   by (perm_simp) (rule refl)

   905 

   899 

   906 lemma Ball_eqvt [eqvt]:

   900 lemma Ball_eqvt [eqvt]:

   907   shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"

   901   shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"

   908   unfolding Ball_def

   902   unfolding Ball_def

   909   by (perm_simp) (rule refl)

   908   by (perm_simp) (rule refl)

   910 

   909 

   911 lemma UNIV_eqvt [eqvt]:

   910 lemma UNIV_eqvt [eqvt]:

   912   shows "p \<bullet> UNIV = UNIV"

   911   shows "p \<bullet> UNIV = UNIV"

   913   unfolding UNIV_def

   912   unfolding UNIV_def

  1037 

  1036 

  1038 

  1037 

  1039 subsubsection {* Equivariance for product operations *}

  1038 subsubsection {* Equivariance for product operations *}

  1040 

  1039 

  1041 lemma fst_eqvt [eqvt]:

  1040 lemma fst_eqvt [eqvt]:

  1044 

  1043 

  1045 lemma snd_eqvt [eqvt]:

  1044 lemma snd_eqvt [eqvt]:

  1048 

  1047 

  1049 lemma split_eqvt [eqvt]: 

  1048 lemma split_eqvt [eqvt]: 

  1050   shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"

  1049   shows "p \<bullet> (split P x) = split (p \<bullet> P) (p \<bullet> x)"

  1051   unfolding split_def

  1050   unfolding split_def

  1052   by (perm_simp) (rule refl)

  1051   by (perm_simp) (rule refl)

  1097 unfolding in_fset

  1096 unfolding in_fset

  1098 by (perm_simp) (simp)

  1097 by (perm_simp) (simp)

  1099 

  1098 

  1100 lemma union_fset_eqvt [eqvt]:

  1099 lemma union_fset_eqvt [eqvt]:

  1101   shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"

  1100   shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"

  1103 

  1102 

  1104 lemma map_fset_eqvt [eqvt]: 

  1103 lemma map_fset_eqvt [eqvt]: 

  1105   shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"

  1104   shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"

  1106   by (lifting map_eqvt)

  1105   by (lifting map_eqvt)

  1107 

  1106 

  1408   by (simp add: fresh_minus_perm)

  1407   by (simp add: fresh_minus_perm)

  1409 

  1408 

  1410 lemma plus_perm_eq:

  1409 lemma plus_perm_eq:

  1411   fixes p q::"perm"

  1410   fixes p q::"perm"

  1412   assumes asm: "supp p \<inter> supp q = {}"

  1411   assumes asm: "supp p \<inter> supp q = {}"

  1414 unfolding perm_eq_iff

  1413 unfolding perm_eq_iff

  1415 proof

  1414 proof

  1416   fix a::"atom"

  1415   fix a::"atom"

  1417   show "(p + q) \<bullet> a = (q + p) \<bullet> a"

  1416   show "(p + q) \<bullet> a = (q + p) \<bullet> a"

  1418   proof -

  1417   proof -

  1491   shows "a \<sharp> ()"

  1490   shows "a \<sharp> ()"

  1492   by (simp add: fresh_def supp_Unit)

  1491   by (simp add: fresh_def supp_Unit)

  1493 

  1492 

  1494 instance prod :: (fs, fs) fs

  1493 instance prod :: (fs, fs) fs

  1495 apply default

  1494 apply default

  1497 apply (simp add: supp_Pair finite_supp)

  1496 apply (simp add: supp_Pair finite_supp)

  1498 done

  1497 done

  1499 

  1498 

  1500 

  1499 

  1501 subsection {* Type @{typ "'a + 'b"} is finitely supported *}

  1500 subsection {* Type @{typ "'a + 'b"} is finitely supported *}

  1516   shows "a \<sharp> Inr y \<longleftrightarrow> a \<sharp> y"

  1515   shows "a \<sharp> Inr y \<longleftrightarrow> a \<sharp> y"

  1517   by (simp add: fresh_def supp_Inr)

  1516   by (simp add: fresh_def supp_Inr)

  1518 

  1517 

  1519 instance sum :: (fs, fs) fs

  1518 instance sum :: (fs, fs) fs

  1520 apply default

  1519 apply default

  1522 apply (simp_all add: supp_Inl supp_Inr finite_supp)

  1521 apply (simp_all add: supp_Inl supp_Inr finite_supp)

  1523 done

  1522 done

  1524 

  1523 

  1525 

  1524 

  1526 subsection {* Type @{typ "'a option"} is finitely supported *}

  1525 subsection {* Type @{typ "'a option"} is finitely supported *}

  1552 

  1551 

  1553 lemma supp_Nil: 

  1552 lemma supp_Nil: 

  1554   shows "supp [] = {}"

  1553   shows "supp [] = {}"

  1555   by (simp add: supp_def)

  1554   by (simp add: supp_def)

  1556 

  1555 

  1557 lemma supp_Cons: 

  1560 lemma supp_Cons: 

  1558   shows "supp (x # xs) = supp x \<union> supp xs"

  1561   shows "supp (x # xs) = supp x \<union> supp xs"

  1559 by (simp add: supp_def Collect_imp_eq Collect_neg_eq)

  1562 by (simp add: supp_def Collect_imp_eq Collect_neg_eq)

  1560 

  1563 

  1561 lemma supp_append:

  1568 lemma supp_append:

  1562   shows "supp (xs @ ys) = supp xs \<union> supp ys"

  1569   shows "supp (xs @ ys) = supp xs \<union> supp ys"

  1563   by (induct xs) (auto simp add: supp_Nil supp_Cons)

  1570   by (induct xs) (auto simp add: supp_Nil supp_Cons)

  1572 

  1571 

  1573 lemma fresh_append:

  1572 lemma fresh_append:

  1574   shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"

  1573   shows "a \<sharp> (xs @ ys) \<longleftrightarrow> a \<sharp> xs \<and> a \<sharp> ys"

  1575   by (induct xs) (simp_all add: fresh_Nil fresh_Cons)

  1574   by (induct xs) (simp_all add: fresh_Nil fresh_Cons)

  1576 

  1575 

  1612   assumes "a \<sharp> f" and "a \<sharp> x" 

  1611   assumes "a \<sharp> f" and "a \<sharp> x" 

  1613   shows "a \<sharp> f x"

  1612   shows "a \<sharp> f x"

  1614   using assms

  1613   using assms

  1615   unfolding fresh_conv_MOST

  1614   unfolding fresh_conv_MOST

  1616   unfolding permute_fun_app_eq

  1615   unfolding permute_fun_app_eq

  1618 

  1617 

  1619 lemma supp_fun_app:

  1618 lemma supp_fun_app:

  1620   shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"

  1619   shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"

  1621   using fresh_fun_app

  1620   using fresh_fun_app

  1622   unfolding fresh_def

  1621   unfolding fresh_def

  1626 subsection {* Equivariance Predicate @{text eqvt} and @{text eqvt_at}*}

  1625 subsection {* Equivariance Predicate @{text eqvt} and @{text eqvt_at}*}

  1627 

  1626 

  1628 definition

  1627 definition

  1629   "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"

  1628   "eqvt f \<equiv> \<forall>p. p \<bullet> f = f"

  1630 

  1629 

  1632 text {* equivariance of a function at a given argument *}

  1630 text {* equivariance of a function at a given argument *}

  1633 

  1631 

  1634 definition

  1632 definition

  1635  "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"

  1633  "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)"

  1637 

  1634 

  1638 lemma eqvtI:

  1635 lemma eqvtI:

  1639   shows "(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f"

  1636   shows "(\<And>p. p \<bullet> f \<equiv> f) \<Longrightarrow> eqvt f"

  1640 unfolding eqvt_def

  1637 unfolding eqvt_def

  1641 by simp

  1638 by simp

  2103 

  2100 

  2104 

  2101 

  2105 

  2102 

  2106 section {* Induction principle for permutations *}

  2103 section {* Induction principle for permutations *}

  2107 

  2104 

  2108 

  2118 

  2109 lemma perm_struct_induct[consumes 1, case_names zero swap]:

  2119 lemma perm_struct_induct[consumes 1, case_names zero swap]:

  2110   assumes S: "supp p \<subseteq> S"

  2120   assumes S: "supp p \<subseteq> S"

  2111   and zero: "P 0"

  2121   and zero: "P 0"

  2112   and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"

  2122   and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"

  2126     { assume "supp p \<noteq> {}"

  2136     { assume "supp p \<noteq> {}"

  2127       then obtain a where a0: "a \<in> supp p" by blast

  2137       then obtain a where a0: "a \<in> supp p" by blast

  2128       then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a"

  2138       then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a"

  2129         using as by (auto simp add: supp_atom supp_perm swap_atom)

  2139         using as by (auto simp add: supp_atom supp_perm swap_atom)

  2130       let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"

  2140       let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"

  2136       then have "P ?q" using ih by simp

  2142       then have "P ?q" using ih by simp

  2137       moreover

  2143       moreover

  2138       have "supp ?q \<subseteq> S" using as a2 by simp

  2144       have "supp ?q \<subseteq> S" using as a2 by simp

  2139       ultimately  have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp 

  2145       ultimately  have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp 

  2140       moreover 

  2146       moreover 

  2211     then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all

  2217     then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all

  2212     then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)

  2218     then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)

  2213   qed

  2219   qed

  2214 qed

  2220 qed

  2215 

  2221 

  2216 lemma supp_perm_eq_test:

  2223 lemma supp_perm_eq_test:

  2217   assumes "(supp x) \<sharp>* p"

  2224   assumes "(supp x) \<sharp>* p"

  2218   shows "p \<bullet> x = x"

  2225   shows "p \<bullet> x = x"

  2219 proof -

  2226 proof -

  2220   from assms have "supp p \<subseteq> {a. a \<sharp> x}"

  2227   from assms have "supp p \<subseteq> {a. a \<sharp> x}"

  2235 qed

  2242 qed

  2236 

  2243 

  2237 lemma perm_supp_eq:

  2244 lemma perm_supp_eq:

  2238   assumes a: "(supp p) \<sharp>* x"

  2245   assumes a: "(supp p) \<sharp>* x"

  2239   shows "p \<bullet> x = x"

  2246   shows "p \<bullet> x = x"

  2242 

  2265 

  2243 lemma supp_perm_perm_eq:

  2266 lemma supp_perm_perm_eq:

  2244   assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"

  2267   assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"

  2245   shows "p \<bullet> x = q \<bullet> x"

  2268   shows "p \<bullet> x = q \<bullet> x"

  2246 proof -

  2269 proof -

  2634   apply(subst inj_image_mem_iff)

  2657   apply(subst inj_image_mem_iff)

  2635   apply(simp add: inj_on_def)

  2658   apply(simp add: inj_on_def)

  2636   apply(simp)

  2659   apply(simp)

  2637   done

  2660   done

  2638 

  2661 

  2640   fixes a::"'a::at_base"

  2663   fixes a::"'a::at_base"

  2641   shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x"

  2664   shows "atom (p \<bullet> a) \<sharp> p \<bullet> x \<longleftrightarrow> atom a \<sharp> x"

  2642   unfolding atom_eqvt[symmetric]

  2665   unfolding atom_eqvt[symmetric]

  2643   by (simp add: fresh_permute_iff)

  2666   by (simp add: fresh_permute_iff)

  2644 

  2667