equal
deleted
inserted
replaced
144 "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2" |
144 "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2" |
145 by (simp add: fun_eq_iff Rep_perm_inject [symmetric]) |
145 by (simp add: fun_eq_iff Rep_perm_inject [symmetric]) |
146 |
146 |
147 instance perm :: size .. |
147 instance perm :: size .. |
148 |
148 |
149 subsection {* Permutations form a group *} |
149 subsection {* Permutations form a (multiplicative) group *} |
|
150 |
150 |
151 |
151 instantiation perm :: group_add |
152 instantiation perm :: group_add |
152 begin |
153 begin |
153 |
154 |
154 definition |
155 definition |
341 "sort_of a = sort_of b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> a = b" |
342 "sort_of a = sort_of b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> a = b" |
342 "sort_of a = sort_of b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> b = a" |
343 "sort_of a = sort_of b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> b = a" |
343 "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> c = c" |
344 "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> c = c" |
344 unfolding swap_atom by simp_all |
345 unfolding swap_atom by simp_all |
345 |
346 |
346 lemma expand_perm_eq: |
347 lemma perm_eq_iff: |
347 fixes p q :: "perm" |
348 fixes p q :: "perm" |
348 shows "p = q \<longleftrightarrow> (\<forall>a::atom. p \<bullet> a = q \<bullet> a)" |
349 shows "p = q \<longleftrightarrow> (\<forall>a::atom. p \<bullet> a = q \<bullet> a)" |
349 unfolding permute_atom_def |
350 unfolding permute_atom_def |
350 by (metis Rep_perm_ext ext) |
351 by (metis Rep_perm_ext ext) |
351 |
352 |
369 lemma permute_self: |
370 lemma permute_self: |
370 shows "p \<bullet> p = p" |
371 shows "p \<bullet> p = p" |
371 unfolding permute_perm_def |
372 unfolding permute_perm_def |
372 by (simp add: diff_minus add_assoc) |
373 by (simp add: diff_minus add_assoc) |
373 |
374 |
|
375 lemma pemute_minus_self: |
|
376 shows "- p \<bullet> p = p" |
|
377 unfolding permute_perm_def |
|
378 by (simp add: diff_minus add_assoc) |
|
379 |
374 lemma permute_eqvt: |
380 lemma permute_eqvt: |
375 shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)" |
381 shows "p \<bullet> (q \<bullet> x) = (p \<bullet> q) \<bullet> (p \<bullet> x)" |
376 unfolding permute_perm_def by simp |
382 unfolding permute_perm_def by simp |
377 |
383 |
378 lemma zero_perm_eqvt: |
384 lemma zero_perm_eqvt: |
381 |
387 |
382 lemma add_perm_eqvt: |
388 lemma add_perm_eqvt: |
383 fixes p p1 p2 :: perm |
389 fixes p p1 p2 :: perm |
384 shows "p \<bullet> (p1 + p2) = p \<bullet> p1 + p \<bullet> p2" |
390 shows "p \<bullet> (p1 + p2) = p \<bullet> p1 + p \<bullet> p2" |
385 unfolding permute_perm_def |
391 unfolding permute_perm_def |
386 by (simp add: expand_perm_eq) |
392 by (simp add: perm_eq_iff) |
387 |
393 |
388 lemma swap_eqvt: |
394 lemma swap_eqvt: |
389 shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)" |
395 shows "p \<bullet> (a \<rightleftharpoons> b) = (p \<bullet> a \<rightleftharpoons> p \<bullet> b)" |
390 unfolding permute_perm_def |
396 unfolding permute_perm_def |
391 by (auto simp add: swap_atom expand_perm_eq) |
397 by (auto simp add: swap_atom perm_eq_iff) |
392 |
398 |
393 lemma uminus_eqvt: |
399 lemma uminus_eqvt: |
394 fixes p q::"perm" |
400 fixes p q::"perm" |
395 shows "p \<bullet> (- q) = - (p \<bullet> q)" |
401 shows "p \<bullet> (- q) = - (p \<bullet> q)" |
396 unfolding permute_perm_def |
402 unfolding permute_perm_def |
475 |
481 |
476 subsection {* Permutations for sets *} |
482 subsection {* Permutations for sets *} |
477 |
483 |
478 lemma permute_set_eq: |
484 lemma permute_set_eq: |
479 fixes x::"'a::pt" |
485 fixes x::"'a::pt" |
480 and p::"perm" |
|
481 shows "(p \<bullet> X) = {p \<bullet> x | x. x \<in> X}" |
486 shows "(p \<bullet> X) = {p \<bullet> x | x. x \<in> X}" |
482 unfolding permute_fun_def |
487 unfolding permute_fun_def |
483 unfolding permute_bool_def |
488 unfolding permute_bool_def |
484 apply(auto simp add: mem_def) |
489 apply(auto simp add: mem_def) |
485 apply(rule_tac x="- p \<bullet> x" in exI) |
490 apply(rule_tac x="- p \<bullet> x" in exI) |
765 definition |
770 definition |
766 supp :: "'a \<Rightarrow> atom set" |
771 supp :: "'a \<Rightarrow> atom set" |
767 where |
772 where |
768 "supp x = {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}}" |
773 "supp x = {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}}" |
769 |
774 |
770 end |
|
771 |
|
772 definition |
775 definition |
773 fresh :: "atom \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp> _" [55, 55] 55) |
776 fresh :: "atom \<Rightarrow> 'a \<Rightarrow> bool" ("_ \<sharp> _" [55, 55] 55) |
774 where |
777 where |
775 "a \<sharp> x \<equiv> a \<notin> supp x" |
778 "a \<sharp> x \<equiv> a \<notin> supp x" |
|
779 |
|
780 end |
776 |
781 |
777 lemma supp_conv_fresh: |
782 lemma supp_conv_fresh: |
778 shows "supp x = {a. \<not> a \<sharp> x}" |
783 shows "supp x = {a. \<not> a \<sharp> x}" |
779 unfolding fresh_def by simp |
784 unfolding fresh_def by simp |
780 |
785 |
879 proof (rule ccontr) |
884 proof (rule ccontr) |
880 assume "\<not> (supp x \<subseteq> S)" |
885 assume "\<not> (supp x \<subseteq> S)" |
881 then obtain a where b1: "a \<in> supp x" and b2: "a \<notin> S" by auto |
886 then obtain a where b1: "a \<in> supp x" and b2: "a \<notin> S" by auto |
882 from a1 b2 have "\<forall>b. b \<notin> S \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x" unfolding supports_def by auto |
887 from a1 b2 have "\<forall>b. b \<notin> S \<longrightarrow> (a \<rightleftharpoons> b) \<bullet> x = x" unfolding supports_def by auto |
883 then have "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x} \<subseteq> S" by auto |
888 then have "{b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x} \<subseteq> S" by auto |
884 with a2 have "finite {b. (a \<rightleftharpoons> b)\<bullet>x \<noteq> x}" by (simp add: finite_subset) |
889 with a2 have "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}" by (simp add: finite_subset) |
885 then have "a \<notin> (supp x)" unfolding supp_def by simp |
890 then have "a \<notin> (supp x)" unfolding supp_def by simp |
886 with b1 show False by simp |
891 with b1 show False by simp |
887 qed |
892 qed |
888 |
893 |
889 lemma supports_finite: |
894 lemma supports_finite: |
1024 shows "supp p = {a. p \<bullet> a \<noteq> a}" |
1029 shows "supp p = {a. p \<bullet> a \<noteq> a}" |
1025 apply (rule finite_supp_unique) |
1030 apply (rule finite_supp_unique) |
1026 apply (rule supports_perm) |
1031 apply (rule supports_perm) |
1027 apply (rule finite_perm_lemma) |
1032 apply (rule finite_perm_lemma) |
1028 apply (simp add: perm_swap_eq swap_eqvt) |
1033 apply (simp add: perm_swap_eq swap_eqvt) |
1029 apply (auto simp add: expand_perm_eq swap_atom) |
1034 apply (auto simp add: perm_eq_iff swap_atom) |
1030 done |
1035 done |
1031 |
1036 |
1032 lemma fresh_perm: |
1037 lemma fresh_perm: |
1033 shows "a \<sharp> p \<longleftrightarrow> p \<bullet> a = a" |
1038 shows "a \<sharp> p \<longleftrightarrow> p \<bullet> a = a" |
1034 unfolding fresh_def |
1039 unfolding fresh_def |
1079 |
1084 |
1080 lemma plus_perm_eq: |
1085 lemma plus_perm_eq: |
1081 fixes p q::"perm" |
1086 fixes p q::"perm" |
1082 assumes asm: "supp p \<inter> supp q = {}" |
1087 assumes asm: "supp p \<inter> supp q = {}" |
1083 shows "p + q = q + p" |
1088 shows "p + q = q + p" |
1084 unfolding expand_perm_eq |
1089 unfolding perm_eq_iff |
1085 proof |
1090 proof |
1086 fix a::"atom" |
1091 fix a::"atom" |
1087 show "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1092 show "(p + q) \<bullet> a = (q + p) \<bullet> a" |
1088 proof - |
1093 proof - |
1089 { assume "a \<notin> supp p" "a \<notin> supp q" |
1094 { assume "a \<notin> supp p" "a \<notin> supp q" |
1271 lemma fresh_fun_app: |
1276 lemma fresh_fun_app: |
1272 assumes "a \<sharp> f" and "a \<sharp> x" |
1277 assumes "a \<sharp> f" and "a \<sharp> x" |
1273 shows "a \<sharp> f x" |
1278 shows "a \<sharp> f x" |
1274 using assms |
1279 using assms |
1275 unfolding fresh_conv_MOST |
1280 unfolding fresh_conv_MOST |
1276 unfolding permute_fun_app_eq |
1281 unfolding permute_fun_app_eq |
1277 by (elim MOST_rev_mp, simp) |
1282 by (elim MOST_rev_mp, simp) |
1278 |
1283 |
1279 lemma supp_fun_app: |
1284 lemma supp_fun_app: |
1280 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
1285 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
1281 using fresh_fun_app |
1286 using fresh_fun_app |
1282 unfolding fresh_def |
1287 unfolding fresh_def |
1283 by auto |
1288 by auto |
1284 |
1289 |
1285 text {* Equivariant Functions *} |
1290 |
|
1291 subsection {* Equivariance *} |
1286 |
1292 |
1287 definition |
1293 definition |
1288 "eqvt f \<equiv> \<forall>p. p \<bullet> f = f" |
1294 "eqvt f \<equiv> \<forall>p. p \<bullet> f = f" |
1289 |
1295 |
1290 lemma eqvtI: |
1296 lemma eqvtI: |
1309 unfolding fresh_def |
1315 unfolding fresh_def |
1310 using supp_fun_app by auto |
1316 using supp_fun_app by auto |
1311 qed |
1317 qed |
1312 |
1318 |
1313 text {* equivariance of a function at a given argument *} |
1319 text {* equivariance of a function at a given argument *} |
|
1320 |
1314 definition |
1321 definition |
1315 "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)" |
1322 "eqvt_at f x \<equiv> \<forall>p. p \<bullet> (f x) = f (p \<bullet> x)" |
1316 |
1323 |
1317 lemma supp_eqvt_at: |
1324 lemma supp_eqvt_at: |
1318 assumes asm: "eqvt_at f x" |
1325 assumes asm: "eqvt_at f x" |
1769 proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct) |
1776 proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct) |
1770 case (psubset p) |
1777 case (psubset p) |
1771 then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto |
1778 then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto |
1772 have as: "supp p \<subseteq> S" by fact |
1779 have as: "supp p \<subseteq> S" by fact |
1773 { assume "supp p = {}" |
1780 { assume "supp p = {}" |
1774 then have "p = 0" by (simp add: supp_perm expand_perm_eq) |
1781 then have "p = 0" by (simp add: supp_perm perm_eq_iff) |
1775 then have "P p" using zero by simp |
1782 then have "P p" using zero by simp |
1776 } |
1783 } |
1777 moreover |
1784 moreover |
1778 { assume "supp p \<noteq> {}" |
1785 { assume "supp p \<noteq> {}" |
1779 then obtain a where a0: "a \<in> supp p" by blast |
1786 then obtain a where a0: "a \<in> supp p" by blast |
1788 then have "P ?q" using ih by simp |
1795 then have "P ?q" using ih by simp |
1789 moreover |
1796 moreover |
1790 have "supp ?q \<subseteq> S" using as a2 by simp |
1797 have "supp ?q \<subseteq> S" using as a2 by simp |
1791 ultimately have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp |
1798 ultimately have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp |
1792 moreover |
1799 moreover |
1793 have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq) |
1800 have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: perm_eq_iff) |
1794 ultimately have "P p" by simp |
1801 ultimately have "P p" by simp |
1795 } |
1802 } |
1796 ultimately show "P p" by blast |
1803 ultimately show "P p" by blast |
1797 qed |
1804 qed |
1798 qed |
1805 qed |