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

   824 

   824 

   825 lemma ex1_eqvt [eqvt]:

   825 lemma ex1_eqvt [eqvt]:

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

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

   827   unfolding Ex1_def

   827   unfolding Ex1_def

   828   by (perm_simp) (rule refl)

   828   by (perm_simp) (rule refl)

   849 

   829 

   850 lemma if_eqvt [eqvt]:

   830 lemma if_eqvt [eqvt]:

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

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

   852   by (simp add: permute_fun_def permute_bool_def)

   832   by (simp add: permute_fun_def permute_bool_def)

   853 

   833 

   895   apply(simp add: permute_bool_def unique)

   875   apply(simp add: permute_bool_def unique)

   896   apply(simp add: permute_bool_def)

   876   apply(simp add: permute_bool_def)

   897   apply(rule theI'[OF unique])

   877   apply(rule theI'[OF unique])

   898   done

   878   done

   899 

   879 

   901 

   895 

   902 lemma Bex_eqvt [eqvt]:

   896 lemma Bex_eqvt [eqvt]:

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

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

   904   unfolding Bex_def

   898   unfolding Bex_def

   905   by (perm_simp) (rule refl)

   899   by (perm_simp) (rule refl)

   906 

   900 

   907 lemma Ball_eqvt [eqvt]:

   901 lemma Ball_eqvt [eqvt]:

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

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

   909   unfolding Ball_def

   903   unfolding Ball_def

   910   by (perm_simp) (rule refl)

   909   by (perm_simp) (rule refl)

   911 

   910 

   912 lemma UNIV_eqvt [eqvt]:

   911 lemma UNIV_eqvt [eqvt]:

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

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

   914   unfolding UNIV_def

   913   unfolding UNIV_def

   963   unfolding permute_finite permute_bool_def ..

   962   unfolding permute_finite permute_bool_def ..

   964 

   963 

   965 subsubsection {* Equivariance for product operations *}

   964 subsubsection {* Equivariance for product operations *}

   966 

   965 

   967 lemma fst_eqvt [eqvt]:

   966 lemma fst_eqvt [eqvt]:

   970 

   969 

   971 lemma snd_eqvt [eqvt]:

   970 lemma snd_eqvt [eqvt]:

   974 

   973 

   975 lemma split_eqvt [eqvt]: 

   974 lemma split_eqvt [eqvt]: 

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

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

   977   unfolding split_def

   976   unfolding split_def

   978   by (perm_simp) (rule refl)

   977   by (perm_simp) (rule refl)

  1023 unfolding in_fset

  1022 unfolding in_fset

  1024 by (perm_simp) (simp)

  1023 by (perm_simp) (simp)

  1025 

  1024 

  1026 lemma union_fset_eqvt [eqvt]:

  1025 lemma union_fset_eqvt [eqvt]:

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

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

  1029 

  1028 

  1030 lemma map_fset_eqvt [eqvt]: 

  1029 lemma map_fset_eqvt [eqvt]: 

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

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

  1032   by (lifting map_eqvt)

  1031   by (lifting map_eqvt)

  1033 

  1032 

  1334   by (simp add: fresh_minus_perm)

  1333   by (simp add: fresh_minus_perm)

  1335 

  1334 

  1336 lemma plus_perm_eq:

  1335 lemma plus_perm_eq:

  1337   fixes p q::"perm"

  1336   fixes p q::"perm"

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

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

  1340 unfolding perm_eq_iff

  1339 unfolding perm_eq_iff

  1341 proof

  1340 proof

  1342   fix a::"atom"

  1341   fix a::"atom"

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

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

  1344   proof -

  1343   proof -

  1417   shows "a \<sharp> ()"

  1416   shows "a \<sharp> ()"

  1418   by (simp add: fresh_def supp_Unit)

  1417   by (simp add: fresh_def supp_Unit)

  1419 

  1418 

  1420 instance prod :: (fs, fs) fs

  1419 instance prod :: (fs, fs) fs

  1421 apply default

  1420 apply default

  1423 apply (simp add: supp_Pair finite_supp)

  1422 apply (simp add: supp_Pair finite_supp)

  1424 done

  1423 done

  1425 

  1424 

  1426 

  1425 

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

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

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

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

  1443   by (simp add: fresh_def supp_Inr)

  1442   by (simp add: fresh_def supp_Inr)

  1444 

  1443 

  1445 instance sum :: (fs, fs) fs

  1444 instance sum :: (fs, fs) fs

  1446 apply default

  1445 apply default

  1448 apply (simp_all add: supp_Inl supp_Inr finite_supp)

  1447 apply (simp_all add: supp_Inl supp_Inr finite_supp)

  1449 done

  1448 done

  1450 

  1449 

  1451 

  1450 

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

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

  1478 

  1477 

  1479 lemma supp_Nil: 

  1478 lemma supp_Nil: 

  1480   shows "supp [] = {}"

  1479   shows "supp [] = {}"

  1481   by (simp add: supp_def)

  1480   by (simp add: supp_def)

  1482 

  1481 

  1483 lemma supp_Cons: 

  1486 lemma supp_Cons: 

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

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

  1485 by (simp add: supp_def Collect_imp_eq Collect_neg_eq)

  1488 by (simp add: supp_def Collect_imp_eq Collect_neg_eq)

  1486 

  1489 

  1487 lemma supp_append:

  1494 lemma supp_append:

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

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

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

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

  1498 

  1497 

  1499 lemma fresh_append:

  1498 lemma fresh_append:

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

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

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

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

  1502 

  1501 

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

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

  1539   shows "a \<sharp> f x"

  1538   shows "a \<sharp> f x"

  1540   using assms

  1539   using assms

  1541   unfolding fresh_conv_MOST

  1540   unfolding fresh_conv_MOST

  1542   unfolding permute_fun_app_eq

  1541   unfolding permute_fun_app_eq

  1544 

  1543 

  1545 lemma supp_fun_app:

  1544 lemma supp_fun_app:

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

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

  1547   using fresh_fun_app

  1546   using fresh_fun_app

  1548   unfolding fresh_def

  1547   unfolding fresh_def

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

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

  1553 

  1552 

  1554 definition

  1553 definition

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

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

  1556 

  1555 

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

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

  1559 

  1557 

  1560 definition

  1558 definition

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

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

  1563 

  1560 

  1564 lemma eqvtI:

  1561 lemma eqvtI:

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

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

  1566 unfolding eqvt_def

  1563 unfolding eqvt_def

  1567 by simp

  1564 by simp

  2029 

  2026 

  2030 

  2027 

  2031 

  2028 

  2032 section {* Induction principle for permutations *}

  2029 section {* Induction principle for permutations *}

  2033 

  2030 

  2034 

  2044 

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

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

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

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

  2037   and zero: "P 0"

  2047   and zero: "P 0"

  2038   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)"

  2048   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)"

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

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

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

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

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

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

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

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

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

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

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

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

  2063       moreover

  2069       moreover

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

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

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

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

  2066       moreover 

  2072       moreover 

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

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

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

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

  2139   qed

  2145   qed

  2140 qed

  2146 qed

  2141 

  2147 

  2142 lemma supp_perm_eq_test:

  2149 lemma supp_perm_eq_test:

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

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

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

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

  2145 proof -

  2152 proof -

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

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

  2161 qed

  2168 qed

  2162 

  2169 

  2163 lemma perm_supp_eq:

  2170 lemma perm_supp_eq:

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

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

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

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

  2168 

  2191 

  2169 lemma supp_perm_perm_eq:

  2192 lemma supp_perm_perm_eq:

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

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

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

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

  2172 proof -

  2195 proof -

  2560   apply(subst inj_image_mem_iff)

  2583   apply(subst inj_image_mem_iff)

  2561   apply(simp add: inj_on_def)

  2584   apply(simp add: inj_on_def)

  2562   apply(simp)

  2585   apply(simp)

  2563   done

  2586   done

  2564 

  2587 

  2566   fixes a::"'a::at_base"

  2589   fixes a::"'a::at_base"

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

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

  2568   unfolding atom_eqvt[symmetric]

  2591   unfolding atom_eqvt[symmetric]

  2569   by (simp add: fresh_permute_iff)

  2592   by (simp add: fresh_permute_iff)

  2570 

  2593