author  bulwahn 
Thu, 08 Dec 2016 17:22:51 +0100  
changeset 64543  6b13586ef1a2 
parent 64284  f3b905b2eee2 
child 64966  d53d7ca3303e 
permissions  rwrr 
41959  1 
(* Title: HOL/Library/Permutations.thy 
2 
Author: Amine Chaieb, University of Cambridge 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

3 
*) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

4 

60500  5 
section \<open>Permutations, both general and specifically on finite sets.\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

6 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

7 
theory Permutations 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

8 
imports Binomial Multiset Disjoint_Sets 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

9 
begin 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

10 

60500  11 
subsection \<open>Transpositions\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

12 

56608  13 
lemma swap_id_idempotent [simp]: 
14 
"Fun.swap a b id \<circ> Fun.swap a b id = id" 

56545  15 
by (rule ext, auto simp add: Fun.swap_def) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

16 

56608  17 
lemma inv_swap_id: 
18 
"inv (Fun.swap a b id) = Fun.swap a b id" 

54681  19 
by (rule inv_unique_comp) simp_all 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

20 

56608  21 
lemma swap_id_eq: 
22 
"Fun.swap a b id x = (if x = a then b else if x = b then a else x)" 

56545  23 
by (simp add: Fun.swap_def) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

24 

64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

25 
lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y" 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

26 
using surj_f_inv_f[of p] by (auto simp add: bij_def) 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

27 

f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

28 
lemma bij_swap_comp: 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

29 
assumes bp: "bij p" 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

30 
shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p" 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

31 
using surj_f_inv_f[OF bij_is_surj[OF bp]] 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

32 
by (simp add: fun_eq_iff Fun.swap_def bij_inv_eq_iff[OF bp]) 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

33 

64543
6b13586ef1a2
remove typo in bij_swap_compose_bij theorem name; tune proof
bulwahn
parents:
64284
diff
changeset

34 
lemma bij_swap_compose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)" 
64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

35 
proof  
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

36 
assume H: "bij p" 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

37 
show ?thesis 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

38 
unfolding bij_swap_comp[OF H] bij_swap_iff 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

39 
using H . 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

40 
qed 
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

41 

54681  42 

60500  43 
subsection \<open>Basic consequences of the definition\<close> 
54681  44 

45 
definition permutes (infixr "permutes" 41) 

46 
where "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

47 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

48 
lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

49 
unfolding permutes_def by metis 
64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

50 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

51 
lemma permutes_not_in: 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

52 
assumes "f permutes S" "x \<notin> S" shows "f x = x" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

53 
using assms by (auto simp: permutes_def) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

54 

54681  55 
lemma permutes_image: "p permutes S \<Longrightarrow> p ` S = S" 
30488  56 
unfolding permutes_def 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

57 
apply (rule set_eqI) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

58 
apply (simp add: image_iff) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

59 
apply metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

60 
done 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

61 

54681  62 
lemma permutes_inj: "p permutes S \<Longrightarrow> inj p" 
30488  63 
unfolding permutes_def inj_on_def by blast 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

64 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

65 
lemma permutes_inj_on: "f permutes S \<Longrightarrow> inj_on f A" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

66 
unfolding permutes_def inj_on_def by auto 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

67 

54681  68 
lemma permutes_surj: "p permutes s \<Longrightarrow> surj p" 
30488  69 
unfolding permutes_def surj_def by metis 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

70 

60601  71 
lemma permutes_bij: "p permutes s \<Longrightarrow> bij p" 
72 
unfolding bij_def by (metis permutes_inj permutes_surj) 

73 

59474  74 
lemma permutes_imp_bij: "p permutes S \<Longrightarrow> bij_betw p S S" 
60601  75 
by (metis UNIV_I bij_betw_subset permutes_bij permutes_image subsetI) 
59669
de7792ea4090
renaming HOL/Fact.thy > Binomial.thy
paulson <lp15@cam.ac.uk>
parents:
59474
diff
changeset

76 

59474  77 
lemma bij_imp_permutes: "bij_betw p S S \<Longrightarrow> (\<And>x. x \<notin> S \<Longrightarrow> p x = x) \<Longrightarrow> p permutes S" 
78 
unfolding permutes_def bij_betw_def inj_on_def 

79 
by auto (metis image_iff)+ 

80 

54681  81 
lemma permutes_inv_o: 
82 
assumes pS: "p permutes S" 

83 
shows "p \<circ> inv p = id" 

84 
and "inv p \<circ> p = id" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

85 
using permutes_inj[OF pS] permutes_surj[OF pS] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

86 
unfolding inj_iff[symmetric] surj_iff[symmetric] by blast+ 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

87 

30488  88 
lemma permutes_inverses: 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

89 
fixes p :: "'a \<Rightarrow> 'a" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

90 
assumes pS: "p permutes S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

91 
shows "p (inv p x) = x" 
54681  92 
and "inv p (p x) = x" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

93 
using permutes_inv_o[OF pS, unfolded fun_eq_iff o_def] by auto 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

94 

54681  95 
lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> p permutes T" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

96 
unfolding permutes_def by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

97 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

98 
lemma permutes_empty[simp]: "p permutes {} \<longleftrightarrow> p = id" 
54681  99 
unfolding fun_eq_iff permutes_def by simp metis 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

100 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

101 
lemma permutes_sing[simp]: "p permutes {a} \<longleftrightarrow> p = id" 
54681  102 
unfolding fun_eq_iff permutes_def by simp metis 
30488  103 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

104 
lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

105 
unfolding permutes_def by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

106 

54681  107 
lemma permutes_inv_eq: "p permutes S \<Longrightarrow> inv p y = x \<longleftrightarrow> p x = y" 
108 
unfolding permutes_def inv_def 

109 
apply auto 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

110 
apply (erule allE[where x=y]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

111 
apply (erule allE[where x=y]) 
54681  112 
apply (rule someI_ex) 
113 
apply blast 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

114 
apply (rule some1_equality) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

115 
apply blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

116 
apply blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

117 
done 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

118 

54681  119 
lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> Fun.swap a b id permutes S" 
56545  120 
unfolding permutes_def Fun.swap_def fun_upd_def by auto metis 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

121 

54681  122 
lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S  T. p x = x) \<Longrightarrow> p permutes T" 
123 
by (simp add: Ball_def permutes_def) metis 

124 

63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

125 
(* Next three lemmas contributed by Lukas Bulwahn *) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

126 
lemma permutes_bij_inv_into: 
64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

127 
fixes A :: "'a set" and B :: "'b set" 
63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

128 
assumes "p permutes A" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

129 
assumes "bij_betw f A B" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

130 
shows "(\<lambda>x. if x \<in> B then f (p (inv_into A f x)) else x) permutes B" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

131 
proof (rule bij_imp_permutes) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

132 
have "bij_betw p A A" "bij_betw f A B" "bij_betw (inv_into A f) B A" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

133 
using assms by (auto simp add: permutes_imp_bij bij_betw_inv_into) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

134 
from this have "bij_betw (f o p o inv_into A f) B B" by (simp add: bij_betw_trans) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

135 
from this show "bij_betw (\<lambda>x. if x \<in> B then f (p (inv_into A f x)) else x) B B" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

136 
by (subst bij_betw_cong[where g="f o p o inv_into A f"]) auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

137 
next 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

138 
fix x 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

139 
assume "x \<notin> B" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

140 
from this show "(if x \<in> B then f (p (inv_into A f x)) else x) = x" by auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

141 
qed 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

142 

0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

143 
lemma permutes_image_mset: 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

144 
assumes "p permutes A" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

145 
shows "image_mset p (mset_set A) = mset_set A" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

146 
using assms by (metis image_mset_mset_set bij_betw_imp_inj_on permutes_imp_bij permutes_image) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

147 

0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

148 
lemma permutes_implies_image_mset_eq: 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

149 
assumes "p permutes A" "\<And>x. x \<in> A \<Longrightarrow> f x = f' (p x)" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

150 
shows "image_mset f' (mset_set A) = image_mset f (mset_set A)" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

151 
proof  
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

152 
have "f x = f' (p x)" if x: "x \<in># mset_set A" for x 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

153 
using assms(2)[of x] x by (cases "finite A") auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

154 
from this have "image_mset f (mset_set A) = image_mset (f' o p) (mset_set A)" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

155 
using assms by (auto intro!: image_mset_cong) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

156 
also have "\<dots> = image_mset f' (image_mset p (mset_set A))" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

157 
by (simp add: image_mset.compositionality) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

158 
also have "\<dots> = image_mset f' (mset_set A)" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

159 
proof  
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

160 
from assms have "image_mset p (mset_set A) = mset_set A" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

161 
using permutes_image_mset by blast 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

162 
from this show ?thesis by simp 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

163 
qed 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

164 
finally show ?thesis .. 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

165 
qed 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

166 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

167 

60500  168 
subsection \<open>Group properties\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

169 

54681  170 
lemma permutes_id: "id permutes S" 
171 
unfolding permutes_def by simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

172 

54681  173 
lemma permutes_compose: "p permutes S \<Longrightarrow> q permutes S \<Longrightarrow> q \<circ> p permutes S" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

174 
unfolding permutes_def o_def by metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

175 

54681  176 
lemma permutes_inv: 
177 
assumes pS: "p permutes S" 

178 
shows "inv p permutes S" 

30488  179 
using pS unfolding permutes_def permutes_inv_eq[OF pS] by metis 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

180 

54681  181 
lemma permutes_inv_inv: 
182 
assumes pS: "p permutes S" 

183 
shows "inv (inv p) = p" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

184 
unfolding fun_eq_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]] 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

185 
by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

186 

64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

187 
lemma permutes_invI: 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

188 
assumes perm: "p permutes S" 
64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

189 
and inv: "\<And>x. x \<in> S \<Longrightarrow> p' (p x) = x" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

190 
and outside: "\<And>x. x \<notin> S \<Longrightarrow> p' x = x" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

191 
shows "inv p = p'" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

192 
proof 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

193 
fix x show "inv p x = p' x" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

194 
proof (cases "x \<in> S") 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

195 
assume [simp]: "x \<in> S" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

196 
from assms have "p' x = p' (p (inv p x))" by (simp add: permutes_inverses) 
64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

197 
also from permutes_inv[OF perm] 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

198 
have "\<dots> = inv p x" by (subst inv) (simp_all add: permutes_in_image) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

199 
finally show "inv p x = p' x" .. 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

200 
qed (insert permutes_inv[OF perm], simp_all add: outside permutes_not_in) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

201 
qed 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

202 

af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

203 
lemma permutes_vimage: "f permutes A \<Longrightarrow> f ` A = A" 
64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

204 
by (simp add: bij_vimage_eq_inv_image permutes_bij permutes_image[OF permutes_inv]) 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

205 

54681  206 

60500  207 
subsection \<open>The number of permutations on a finite set\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

208 

30488  209 
lemma permutes_insert_lemma: 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

210 
assumes pS: "p permutes (insert a S)" 
54681  211 
shows "Fun.swap a (p a) id \<circ> p permutes S" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

212 
apply (rule permutes_superset[where S = "insert a S"]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

213 
apply (rule permutes_compose[OF pS]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

214 
apply (rule permutes_swap_id, simp) 
54681  215 
using permutes_in_image[OF pS, of a] 
216 
apply simp 

56545  217 
apply (auto simp add: Ball_def Fun.swap_def) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

218 
done 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

219 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

220 
lemma permutes_insert: "{p. p permutes (insert a S)} = 
54681  221 
(\<lambda>(b,p). Fun.swap a b id \<circ> p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}" 
222 
proof  

223 
{ 

224 
fix p 

225 
{ 

226 
assume pS: "p permutes insert a S" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

227 
let ?b = "p a" 
54681  228 
let ?q = "Fun.swap a (p a) id \<circ> p" 
229 
have th0: "p = Fun.swap a ?b id \<circ> ?q" 

230 
unfolding fun_eq_iff o_assoc by simp 

231 
have th1: "?b \<in> insert a S" 

232 
unfolding permutes_in_image[OF pS] by simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

233 
from permutes_insert_lemma[OF pS] th0 th1 
54681  234 
have "\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S" by blast 
235 
} 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

236 
moreover 
54681  237 
{ 
238 
fix b q 

239 
assume bq: "p = Fun.swap a b id \<circ> q" "b \<in> insert a S" "q permutes S" 

30488  240 
from permutes_subset[OF bq(3), of "insert a S"] 
54681  241 
have qS: "q permutes insert a S" 
242 
by auto 

243 
have aS: "a \<in> insert a S" 

244 
by simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

245 
from bq(1) permutes_compose[OF qS permutes_swap_id[OF aS bq(2)]] 
54681  246 
have "p permutes insert a S" 
247 
by simp 

248 
} 

249 
ultimately have "p permutes insert a S \<longleftrightarrow> 

250 
(\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S)" 

251 
by blast 

252 
} 

253 
then show ?thesis 

254 
by auto 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

255 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

256 

54681  257 
lemma card_permutations: 
258 
assumes Sn: "card S = n" 

259 
and fS: "finite S" 

33715  260 
shows "card {p. p permutes S} = fact n" 
54681  261 
using fS Sn 
262 
proof (induct arbitrary: n) 

263 
case empty 

264 
then show ?case by simp 

33715  265 
next 
266 
case (insert x F) 

54681  267 
{ 
268 
fix n 

269 
assume H0: "card (insert x F) = n" 

33715  270 
let ?xF = "{p. p permutes insert x F}" 
271 
let ?pF = "{p. p permutes F}" 

272 
let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}" 

273 
let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)" 

274 
from permutes_insert[of x F] 

275 
have xfgpF': "?xF = ?g ` ?pF'" . 

54681  276 
have Fs: "card F = n  1" 
60500  277 
using \<open>x \<notin> F\<close> H0 \<open>finite F\<close> by auto 
54681  278 
from insert.hyps Fs have pFs: "card ?pF = fact (n  1)" 
60500  279 
using \<open>finite F\<close> by auto 
54681  280 
then have "finite ?pF" 
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59669
diff
changeset

281 
by (auto intro: card_ge_0_finite) 
54681  282 
then have pF'f: "finite ?pF'" 
60500  283 
using H0 \<open>finite F\<close> 
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
60601
diff
changeset

284 
apply (simp only: Collect_case_prod Collect_mem_eq) 
33715  285 
apply (rule finite_cartesian_product) 
286 
apply simp_all 

287 
done 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

288 

33715  289 
have ginj: "inj_on ?g ?pF'" 
54681  290 
proof  
33715  291 
{ 
54681  292 
fix b p c q 
293 
assume bp: "(b,p) \<in> ?pF'" 

294 
assume cq: "(c,q) \<in> ?pF'" 

295 
assume eq: "?g (b,p) = ?g (c,q)" 

296 
from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" 

297 
"p permutes F" "q permutes F" 

298 
by auto 

60500  299 
from ths(4) \<open>x \<notin> F\<close> eq have "b = ?g (b,p) x" 
54681  300 
unfolding permutes_def 
56545  301 
by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff) 
54681  302 
also have "\<dots> = ?g (c,q) x" 
60500  303 
using ths(5) \<open>x \<notin> F\<close> eq 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

304 
by (auto simp add: swap_def fun_upd_def fun_eq_iff) 
54681  305 
also have "\<dots> = c" 
60500  306 
using ths(5) \<open>x \<notin> F\<close> 
54681  307 
unfolding permutes_def 
56545  308 
by (auto simp add: Fun.swap_def fun_upd_def fun_eq_iff) 
33715  309 
finally have bc: "b = c" . 
54681  310 
then have "Fun.swap x b id = Fun.swap x c id" 
311 
by simp 

312 
with eq have "Fun.swap x b id \<circ> p = Fun.swap x b id \<circ> q" 

313 
by simp 

314 
then have "Fun.swap x b id \<circ> (Fun.swap x b id \<circ> p) = 

315 
Fun.swap x b id \<circ> (Fun.swap x b id \<circ> q)" 

316 
by simp 

317 
then have "p = q" 

318 
by (simp add: o_assoc) 

319 
with bc have "(b, p) = (c, q)" 

320 
by simp 

33715  321 
} 
54681  322 
then show ?thesis 
323 
unfolding inj_on_def by blast 

33715  324 
qed 
60500  325 
from \<open>x \<notin> F\<close> H0 have n0: "n \<noteq> 0" 
326 
using \<open>finite F\<close> by auto 

54681  327 
then have "\<exists>m. n = Suc m" 
328 
by presburger 

329 
then obtain m where n[simp]: "n = Suc m" 

330 
by blast 

33715  331 
from pFs H0 have xFc: "card ?xF = fact n" 
54681  332 
unfolding xfgpF' card_image[OF ginj] 
60500  333 
using \<open>finite F\<close> \<open>finite ?pF\<close> 
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
60601
diff
changeset

334 
apply (simp only: Collect_case_prod Collect_mem_eq card_cartesian_product) 
54681  335 
apply simp 
336 
done 

337 
from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" 

338 
unfolding xfgpF' by simp 

33715  339 
have "card ?xF = fact n" 
340 
using xFf xFc unfolding xFf by blast 

341 
} 

54681  342 
then show ?case 
343 
using insert by simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

344 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

345 

54681  346 
lemma finite_permutations: 
347 
assumes fS: "finite S" 

348 
shows "finite {p. p permutes S}" 

64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

349 
using card_permutations[OF refl fS] 
33715  350 
by (auto intro: card_ge_0_finite) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

351 

54681  352 

60500  353 
subsection \<open>Permutations of index set for iterated operations\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

354 

51489  355 
lemma (in comm_monoid_set) permute: 
356 
assumes "p permutes S" 

54681  357 
shows "F g S = F (g \<circ> p) S" 
51489  358 
proof  
60500  359 
from \<open>p permutes S\<close> have "inj p" 
54681  360 
by (rule permutes_inj) 
361 
then have "inj_on p S" 

362 
by (auto intro: subset_inj_on) 

363 
then have "F g (p ` S) = F (g \<circ> p) S" 

364 
by (rule reindex) 

60500  365 
moreover from \<open>p permutes S\<close> have "p ` S = S" 
54681  366 
by (rule permutes_image) 
367 
ultimately show ?thesis 

368 
by simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

369 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

370 

54681  371 

60500  372 
subsection \<open>Various combinations of transpositions with 2, 1 and 0 common elements\<close> 
54681  373 

374 
lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow> 

375 
Fun.swap a b id \<circ> Fun.swap a c id = Fun.swap b c id \<circ> Fun.swap a b id" 

56545  376 
by (simp add: fun_eq_iff Fun.swap_def) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

377 

54681  378 
lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> 
379 
Fun.swap a c id \<circ> Fun.swap b c id = Fun.swap b c id \<circ> Fun.swap a b id" 

56545  380 
by (simp add: fun_eq_iff Fun.swap_def) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

381 

54681  382 
lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow> 
383 
Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap c d id \<circ> Fun.swap a b id" 

56545  384 
by (simp add: fun_eq_iff Fun.swap_def) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

385 

54681  386 

60500  387 
subsection \<open>Permutations as transposition sequences\<close> 
54681  388 

389 
inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" 

390 
where 

391 
id[simp]: "swapidseq 0 id" 

392 
 comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id \<circ> p)" 

393 

394 
declare id[unfolded id_def, simp] 

395 

396 
definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

397 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

398 

60500  399 
subsection \<open>Some closure properties of the set of permutations, with lengths\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

400 

54681  401 
lemma permutation_id[simp]: "permutation id" 
402 
unfolding permutation_def by (rule exI[where x=0]) simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

403 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

404 
declare permutation_id[unfolded id_def, simp] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

405 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

406 
lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

407 
apply clarsimp 
54681  408 
using comp_Suc[of 0 id a b] 
409 
apply simp 

410 
done 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

411 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

412 
lemma permutation_swap_id: "permutation (Fun.swap a b id)" 
54681  413 
apply (cases "a = b") 
414 
apply simp_all 

415 
unfolding permutation_def 

416 
using swapidseq_swap[of a b] 

417 
apply blast 

418 
done 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

419 

54681  420 
lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q \<Longrightarrow> swapidseq (n + m) (p \<circ> q)" 
421 
proof (induct n p arbitrary: m q rule: swapidseq.induct) 

422 
case (id m q) 

423 
then show ?case by simp 

424 
next 

425 
case (comp_Suc n p a b m q) 

426 
have th: "Suc n + m = Suc (n + m)" 

427 
by arith 

428 
show ?case 

429 
unfolding th comp_assoc 

430 
apply (rule swapidseq.comp_Suc) 

431 
using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3) 

432 
apply blast+ 

433 
done 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

434 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

435 

54681  436 
lemma permutation_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> permutation (p \<circ> q)" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

437 
unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

438 

54681  439 
lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (p \<circ> Fun.swap a b id)" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

440 
apply (induct n p rule: swapidseq.induct) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

441 
using swapidseq_swap[of a b] 
54681  442 
apply (auto simp add: comp_assoc intro: swapidseq.comp_Suc) 
443 
done 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

444 

54681  445 
lemma swapidseq_inverse_exists: "swapidseq n p \<Longrightarrow> \<exists>q. swapidseq n q \<and> p \<circ> q = id \<and> q \<circ> p = id" 
446 
proof (induct n p rule: swapidseq.induct) 

447 
case id 

448 
then show ?case 

449 
by (rule exI[where x=id]) simp 

30488  450 
next 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

451 
case (comp_Suc n p a b) 
54681  452 
from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" 
453 
by blast 

454 
let ?q = "q \<circ> Fun.swap a b id" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

455 
note H = comp_Suc.hyps 
54681  456 
from swapidseq_swap[of a b] H(3) have th0: "swapidseq 1 (Fun.swap a b id)" 
457 
by simp 

458 
from swapidseq_comp_add[OF q(1) th0] have th1: "swapidseq (Suc n) ?q" 

459 
by simp 

460 
have "Fun.swap a b id \<circ> p \<circ> ?q = Fun.swap a b id \<circ> (p \<circ> q) \<circ> Fun.swap a b id" 

461 
by (simp add: o_assoc) 

462 
also have "\<dots> = id" 

463 
by (simp add: q(2)) 

464 
finally have th2: "Fun.swap a b id \<circ> p \<circ> ?q = id" . 

465 
have "?q \<circ> (Fun.swap a b id \<circ> p) = q \<circ> (Fun.swap a b id \<circ> Fun.swap a b id) \<circ> p" 

466 
by (simp only: o_assoc) 

467 
then have "?q \<circ> (Fun.swap a b id \<circ> p) = id" 

468 
by (simp add: q(3)) 

469 
with th1 th2 show ?case 

470 
by blast 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

471 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

472 

54681  473 
lemma swapidseq_inverse: 
474 
assumes H: "swapidseq n p" 

475 
shows "swapidseq n (inv p)" 

476 
using swapidseq_inverse_exists[OF H] inv_unique_comp[of p] by auto 

477 

478 
lemma permutation_inverse: "permutation p \<Longrightarrow> permutation (inv p)" 

479 
using permutation_def swapidseq_inverse by blast 

480 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

481 

60500  482 
subsection \<open>The identity map only has even transposition sequences\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

483 

54681  484 
lemma symmetry_lemma: 
485 
assumes "\<And>a b c d. P a b c d \<Longrightarrow> P a b d c" 

486 
and "\<And>a b c d. a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> 

487 
a = c \<and> b = d \<or> a = c \<and> b \<noteq> d \<or> a \<noteq> c \<and> b = d \<or> a \<noteq> c \<and> a \<noteq> d \<and> b \<noteq> c \<and> b \<noteq> d \<Longrightarrow> 

488 
P a b c d" 

489 
shows "\<And>a b c d. a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> P a b c d" 

490 
using assms by metis 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

491 

54681  492 
lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> 
493 
Fun.swap a b id \<circ> Fun.swap c d id = id \<or> 

494 
(\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> 

495 
Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id)" 

496 
proof  

497 
assume H: "a \<noteq> b" "c \<noteq> d" 

498 
have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> 

499 
(Fun.swap a b id \<circ> Fun.swap c d id = id \<or> 

500 
(\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> 

501 
Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id))" 

502 
apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d]) 

56545  503 
apply (simp_all only: swap_commute) 
54681  504 
apply (case_tac "a = c \<and> b = d") 
56608  505 
apply (clarsimp simp only: swap_commute swap_id_idempotent) 
54681  506 
apply (case_tac "a = c \<and> b \<noteq> d") 
507 
apply (rule disjI2) 

508 
apply (rule_tac x="b" in exI) 

509 
apply (rule_tac x="d" in exI) 

510 
apply (rule_tac x="b" in exI) 

56545  511 
apply (clarsimp simp add: fun_eq_iff Fun.swap_def) 
54681  512 
apply (case_tac "a \<noteq> c \<and> b = d") 
513 
apply (rule disjI2) 

514 
apply (rule_tac x="c" in exI) 

515 
apply (rule_tac x="d" in exI) 

516 
apply (rule_tac x="c" in exI) 

56545  517 
apply (clarsimp simp add: fun_eq_iff Fun.swap_def) 
54681  518 
apply (rule disjI2) 
519 
apply (rule_tac x="c" in exI) 

520 
apply (rule_tac x="d" in exI) 

521 
apply (rule_tac x="b" in exI) 

56545  522 
apply (clarsimp simp add: fun_eq_iff Fun.swap_def) 
54681  523 
done 
524 
with H show ?thesis by metis 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

525 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

526 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

527 
lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

528 
using swapidseq.cases[of 0 p "p = id"] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

529 
by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

530 

54681  531 
lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow> 
532 
n = 0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = Fun.swap a b id \<circ> q \<and> swapidseq m q \<and> a \<noteq> b)" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

533 
apply (rule iffI) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

534 
apply (erule swapidseq.cases[of n p]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

535 
apply simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

536 
apply (rule disjI2) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

537 
apply (rule_tac x= "a" in exI) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

538 
apply (rule_tac x= "b" in exI) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

539 
apply (rule_tac x= "pa" in exI) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

540 
apply (rule_tac x= "na" in exI) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

541 
apply simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

542 
apply auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

543 
apply (rule comp_Suc, simp_all) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

544 
done 
54681  545 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

546 
lemma fixing_swapidseq_decrease: 
54681  547 
assumes spn: "swapidseq n p" 
548 
and ab: "a \<noteq> b" 

549 
and pa: "(Fun.swap a b id \<circ> p) a = a" 

550 
shows "n \<noteq> 0 \<and> swapidseq (n  1) (Fun.swap a b id \<circ> p)" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

551 
using spn ab pa 
54681  552 
proof (induct n arbitrary: p a b) 
553 
case 0 

554 
then show ?case 

56545  555 
by (auto simp add: Fun.swap_def fun_upd_def) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

556 
next 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

557 
case (Suc n p a b) 
54681  558 
from Suc.prems(1) swapidseq_cases[of "Suc n" p] 
559 
obtain c d q m where 

560 
cdqm: "Suc n = Suc m" "p = Fun.swap c d id \<circ> q" "swapidseq m q" "c \<noteq> d" "n = m" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

561 
by auto 
54681  562 
{ 
563 
assume H: "Fun.swap a b id \<circ> Fun.swap c d id = id" 

564 
have ?case by (simp only: cdqm o_assoc H) (simp add: cdqm) 

565 
} 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

566 
moreover 
54681  567 
{ 
568 
fix x y z 

569 
assume H: "x \<noteq> a" "y \<noteq> a" "z \<noteq> a" "x \<noteq> y" 

570 
"Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id" 

571 
from H have az: "a \<noteq> z" 

572 
by simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

573 

54681  574 
{ 
575 
fix h 

576 
have "(Fun.swap x y id \<circ> h) a = a \<longleftrightarrow> h a = a" 

56545  577 
using H by (simp add: Fun.swap_def) 
54681  578 
} 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

579 
note th3 = this 
54681  580 
from cdqm(2) have "Fun.swap a b id \<circ> p = Fun.swap a b id \<circ> (Fun.swap c d id \<circ> q)" 
581 
by simp 

582 
then have "Fun.swap a b id \<circ> p = Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)" 

583 
by (simp add: o_assoc H) 

584 
then have "(Fun.swap a b id \<circ> p) a = (Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a" 

585 
by simp 

586 
then have "(Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a = a" 

587 
unfolding Suc by metis 

588 
then have th1: "(Fun.swap a z id \<circ> q) a = a" 

589 
unfolding th3 . 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

590 
from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az th1] 
54681  591 
have th2: "swapidseq (n  1) (Fun.swap a z id \<circ> q)" "n \<noteq> 0" 
592 
by blast+ 

593 
have th: "Suc n  1 = Suc (n  1)" 

594 
using th2(2) by auto 

595 
have ?case 

596 
unfolding cdqm(2) H o_assoc th 

49739  597 
apply (simp only: Suc_not_Zero simp_thms comp_assoc) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

598 
apply (rule comp_Suc) 
54681  599 
using th2 H 
600 
apply blast+ 

601 
done 

602 
} 

603 
ultimately show ?case 

604 
using swap_general[OF Suc.prems(2) cdqm(4)] by metis 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

605 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

606 

30488  607 
lemma swapidseq_identity_even: 
54681  608 
assumes "swapidseq n (id :: 'a \<Rightarrow> 'a)" 
609 
shows "even n" 

60500  610 
using \<open>swapidseq n id\<close> 
54681  611 
proof (induct n rule: nat_less_induct) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

612 
fix n 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

613 
assume H: "\<forall>m<n. swapidseq m (id::'a \<Rightarrow> 'a) \<longrightarrow> even m" "swapidseq n (id :: 'a \<Rightarrow> 'a)" 
54681  614 
{ 
615 
assume "n = 0" 

616 
then have "even n" by presburger 

617 
} 

30488  618 
moreover 
54681  619 
{ 
620 
fix a b :: 'a and q m 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

621 
assume h: "n = Suc m" "(id :: 'a \<Rightarrow> 'a) = Fun.swap a b id \<circ> q" "swapidseq m q" "a \<noteq> b" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

622 
from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]] 
54681  623 
have m: "m \<noteq> 0" "swapidseq (m  1) (id :: 'a \<Rightarrow> 'a)" 
624 
by auto 

625 
from h m have mn: "m  1 < n" 

626 
by arith 

627 
from H(1)[rule_format, OF mn m(2)] h(1) m(1) have "even n" 

628 
by presburger 

629 
} 

630 
ultimately show "even n" 

631 
using H(2)[unfolded swapidseq_cases[of n id]] by auto 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

632 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

633 

54681  634 

60500  635 
subsection \<open>Therefore we have a welldefined notion of parity\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

636 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

637 
definition "evenperm p = even (SOME n. swapidseq n p)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

638 

54681  639 
lemma swapidseq_even_even: 
640 
assumes m: "swapidseq m p" 

641 
and n: "swapidseq n p" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

642 
shows "even m \<longleftrightarrow> even n" 
54681  643 
proof  
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

644 
from swapidseq_inverse_exists[OF n] 
54681  645 
obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" 
646 
by blast 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

647 
from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]] 
54681  648 
show ?thesis 
649 
by arith 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

650 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

651 

54681  652 
lemma evenperm_unique: 
653 
assumes p: "swapidseq n p" 

654 
and n:"even n = b" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

655 
shows "evenperm p = b" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

656 
unfolding n[symmetric] evenperm_def 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

657 
apply (rule swapidseq_even_even[where p = p]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

658 
apply (rule someI[where x = n]) 
54681  659 
using p 
660 
apply blast+ 

661 
done 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

662 

54681  663 

60500  664 
subsection \<open>And it has the expected composition properties\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

665 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

666 
lemma evenperm_id[simp]: "evenperm id = True" 
54681  667 
by (rule evenperm_unique[where n = 0]) simp_all 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

668 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

669 
lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)" 
54681  670 
by (rule evenperm_unique[where n="if a = b then 0 else 1"]) (simp_all add: swapidseq_swap) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

671 

30488  672 
lemma evenperm_comp: 
54681  673 
assumes p: "permutation p" 
674 
and q:"permutation q" 

675 
shows "evenperm (p \<circ> q) = (evenperm p = evenperm q)" 

676 
proof  

677 
from p q obtain n m where n: "swapidseq n p" and m: "swapidseq m q" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

678 
unfolding permutation_def by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

679 
note nm = swapidseq_comp_add[OF n m] 
54681  680 
have th: "even (n + m) = (even n \<longleftrightarrow> even m)" 
681 
by arith 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

682 
from evenperm_unique[OF n refl] evenperm_unique[OF m refl] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

683 
evenperm_unique[OF nm th] 
54681  684 
show ?thesis 
685 
by blast 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

686 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

687 

54681  688 
lemma evenperm_inv: 
689 
assumes p: "permutation p" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

690 
shows "evenperm (inv p) = evenperm p" 
54681  691 
proof  
692 
from p obtain n where n: "swapidseq n p" 

693 
unfolding permutation_def by blast 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

694 
from evenperm_unique[OF swapidseq_inverse[OF n] evenperm_unique[OF n refl, symmetric]] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

695 
show ?thesis . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

696 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

697 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

698 

60500  699 
subsection \<open>A more abstract characterization of permutations\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

700 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

701 
lemma bij_iff: "bij f \<longleftrightarrow> (\<forall>x. \<exists>!y. f y = x)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

702 
unfolding bij_def inj_on_def surj_def 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

703 
apply auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

704 
apply metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

705 
apply metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

706 
done 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

707 

30488  708 
lemma permutation_bijective: 
709 
assumes p: "permutation p" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

710 
shows "bij p" 
54681  711 
proof  
712 
from p obtain n where n: "swapidseq n p" 

713 
unfolding permutation_def by blast 

714 
from swapidseq_inverse_exists[OF n] 

715 
obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" 

716 
by blast 

717 
then show ?thesis unfolding bij_iff 

718 
apply (auto simp add: fun_eq_iff) 

719 
apply metis 

720 
done 

30488  721 
qed 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

722 

54681  723 
lemma permutation_finite_support: 
724 
assumes p: "permutation p" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

725 
shows "finite {x. p x \<noteq> x}" 
54681  726 
proof  
727 
from p obtain n where n: "swapidseq n p" 

728 
unfolding permutation_def by blast 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

729 
from n show ?thesis 
54681  730 
proof (induct n p rule: swapidseq.induct) 
731 
case id 

732 
then show ?case by simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

733 
next 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

734 
case (comp_Suc n p a b) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

735 
let ?S = "insert a (insert b {x. p x \<noteq> x})" 
54681  736 
from comp_Suc.hyps(2) have fS: "finite ?S" 
737 
by simp 

60500  738 
from \<open>a \<noteq> b\<close> have th: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S" 
56545  739 
by (auto simp add: Fun.swap_def) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

740 
from finite_subset[OF th fS] show ?case . 
54681  741 
qed 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

742 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

743 

30488  744 
lemma permutation_lemma: 
54681  745 
assumes fS: "finite S" 
746 
and p: "bij p" 

747 
and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

748 
shows "permutation p" 
54681  749 
using fS p pS 
750 
proof (induct S arbitrary: p rule: finite_induct) 

751 
case (empty p) 

752 
then show ?case by simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

753 
next 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

754 
case (insert a F p) 
54681  755 
let ?r = "Fun.swap a (p a) id \<circ> p" 
756 
let ?q = "Fun.swap a (p a) id \<circ> ?r" 

757 
have raa: "?r a = a" 

56545  758 
by (simp add: Fun.swap_def) 
64543
6b13586ef1a2
remove typo in bij_swap_compose_bij theorem name; tune proof
bulwahn
parents:
64284
diff
changeset

759 
from bij_swap_compose_bij[OF insert(4)] have br: "bij ?r" . 
30488  760 
from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x" 
64543
6b13586ef1a2
remove typo in bij_swap_compose_bij theorem name; tune proof
bulwahn
parents:
64284
diff
changeset

761 
by (metis bij_pointE comp_apply id_apply insert_iff swap_apply(3)) 
6b13586ef1a2
remove typo in bij_swap_compose_bij theorem name; tune proof
bulwahn
parents:
64284
diff
changeset

762 
from insert(3)[OF br th] have rp: "permutation ?r" . 
54681  763 
have "permutation ?q" 
764 
by (simp add: permutation_compose permutation_swap_id rp) 

765 
then show ?case 

766 
by (simp add: o_assoc) 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

767 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

768 

30488  769 
lemma permutation: "permutation p \<longleftrightarrow> bij p \<and> finite {x. p x \<noteq> x}" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

770 
(is "?lhs \<longleftrightarrow> ?b \<and> ?f") 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

771 
proof 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

772 
assume p: ?lhs 
54681  773 
from p permutation_bijective permutation_finite_support show "?b \<and> ?f" 
774 
by auto 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

775 
next 
54681  776 
assume "?b \<and> ?f" 
777 
then have "?f" "?b" by blast+ 

778 
from permutation_lemma[OF this] show ?lhs 

779 
by blast 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

780 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

781 

54681  782 
lemma permutation_inverse_works: 
783 
assumes p: "permutation p" 

784 
shows "inv p \<circ> p = id" 

785 
and "p \<circ> inv p = id" 

44227
78e033e8ba05
get Library/Permutations.thy compiled and working again
huffman
parents:
41959
diff
changeset

786 
using permutation_bijective [OF p] 
78e033e8ba05
get Library/Permutations.thy compiled and working again
huffman
parents:
41959
diff
changeset

787 
unfolding bij_def inj_iff surj_iff by auto 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

788 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

789 
lemma permutation_inverse_compose: 
54681  790 
assumes p: "permutation p" 
791 
and q: "permutation q" 

792 
shows "inv (p \<circ> q) = inv q \<circ> inv p" 

793 
proof  

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

794 
note ps = permutation_inverse_works[OF p] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

795 
note qs = permutation_inverse_works[OF q] 
54681  796 
have "p \<circ> q \<circ> (inv q \<circ> inv p) = p \<circ> (q \<circ> inv q) \<circ> inv p" 
797 
by (simp add: o_assoc) 

798 
also have "\<dots> = id" 

799 
by (simp add: ps qs) 

800 
finally have th0: "p \<circ> q \<circ> (inv q \<circ> inv p) = id" . 

801 
have "inv q \<circ> inv p \<circ> (p \<circ> q) = inv q \<circ> (inv p \<circ> p) \<circ> q" 

802 
by (simp add: o_assoc) 

803 
also have "\<dots> = id" 

804 
by (simp add: ps qs) 

805 
finally have th1: "inv q \<circ> inv p \<circ> (p \<circ> q) = id" . 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

806 
from inv_unique_comp[OF th0 th1] show ?thesis . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

807 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

808 

54681  809 

60500  810 
subsection \<open>Relation to "permutes"\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

811 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

812 
lemma permutation_permutes: "permutation p \<longleftrightarrow> (\<exists>S. finite S \<and> p permutes S)" 
54681  813 
unfolding permutation permutes_def bij_iff[symmetric] 
814 
apply (rule iffI, clarify) 

815 
apply (rule exI[where x="{x. p x \<noteq> x}"]) 

816 
apply simp 

817 
apply clarsimp 

818 
apply (rule_tac B="S" in finite_subset) 

819 
apply auto 

820 
done 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

821 

54681  822 

60500  823 
subsection \<open>Hence a sort of induction principle composing by swaps\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

824 

54681  825 
lemma permutes_induct: "finite S \<Longrightarrow> P id \<Longrightarrow> 
826 
(\<And> a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> P p \<Longrightarrow> P p \<Longrightarrow> permutation p \<Longrightarrow> P (Fun.swap a b id \<circ> p)) \<Longrightarrow> 

827 
(\<And>p. p permutes S \<Longrightarrow> P p)" 

828 
proof (induct S rule: finite_induct) 

829 
case empty 

830 
then show ?case by auto 

30488  831 
next 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

832 
case (insert x F p) 
54681  833 
let ?r = "Fun.swap x (p x) id \<circ> p" 
834 
let ?q = "Fun.swap x (p x) id \<circ> ?r" 

835 
have qp: "?q = p" 

836 
by (simp add: o_assoc) 

837 
from permutes_insert_lemma[OF insert.prems(3)] insert have Pr: "P ?r" 

838 
by blast 

30488  839 
from permutes_in_image[OF insert.prems(3), of x] 
54681  840 
have pxF: "p x \<in> insert x F" 
841 
by simp 

842 
have xF: "x \<in> insert x F" 

843 
by simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

844 
have rp: "permutation ?r" 
30488  845 
unfolding permutation_permutes using insert.hyps(1) 
54681  846 
permutes_insert_lemma[OF insert.prems(3)] 
847 
by blast 

30488  848 
from insert.prems(2)[OF xF pxF Pr Pr rp] 
54681  849 
show ?case 
850 
unfolding qp . 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

851 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

852 

54681  853 

60500  854 
subsection \<open>Sign of a permutation as a real number\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

855 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

856 
definition "sign p = (if evenperm p then (1::int) else 1)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

857 

54681  858 
lemma sign_nz: "sign p \<noteq> 0" 
859 
by (simp add: sign_def) 

860 

861 
lemma sign_id: "sign id = 1" 

862 
by (simp add: sign_def) 

863 

864 
lemma sign_inverse: "permutation p \<Longrightarrow> sign (inv p) = sign p" 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

865 
by (simp add: sign_def evenperm_inv) 
54681  866 

867 
lemma sign_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> sign (p \<circ> q) = sign p * sign q" 

868 
by (simp add: sign_def evenperm_comp) 

869 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

870 
lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else 1)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

871 
by (simp add: sign_def evenperm_swap) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

872 

54681  873 
lemma sign_idempotent: "sign p * sign p = 1" 
874 
by (simp add: sign_def) 

875 

64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

876 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

877 
subsection \<open>Permuting a list\<close> 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

878 

af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

879 
text \<open>This function permutes a list by applying a permutation to the indices.\<close> 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

880 

af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

881 
definition permute_list :: "(nat \<Rightarrow> nat) \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

882 
"permute_list f xs = map (\<lambda>i. xs ! (f i)) [0..<length xs]" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

883 

64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

884 
lemma permute_list_map: 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

885 
assumes "f permutes {..<length xs}" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

886 
shows "permute_list f (map g xs) = map g (permute_list f xs)" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

887 
using permutes_in_image[OF assms] by (auto simp: permute_list_def) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

888 

af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

889 
lemma permute_list_nth: 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

890 
assumes "f permutes {..<length xs}" "i < length xs" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

891 
shows "permute_list f xs ! i = xs ! f i" 
64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

892 
using permutes_in_image[OF assms(1)] assms(2) 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

893 
by (simp add: permute_list_def) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

894 

af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

895 
lemma permute_list_Nil [simp]: "permute_list f [] = []" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

896 
by (simp add: permute_list_def) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

897 

af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

898 
lemma length_permute_list [simp]: "length (permute_list f xs) = length xs" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

899 
by (simp add: permute_list_def) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

900 

64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

901 
lemma permute_list_compose: 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

902 
assumes "g permutes {..<length xs}" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

903 
shows "permute_list (f \<circ> g) xs = permute_list g (permute_list f xs)" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

904 
using assms[THEN permutes_in_image] by (auto simp add: permute_list_def) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

905 

af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

906 
lemma permute_list_ident [simp]: "permute_list (\<lambda>x. x) xs = xs" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

907 
by (simp add: permute_list_def map_nth) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

908 

af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

909 
lemma permute_list_id [simp]: "permute_list id xs = xs" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

910 
by (simp add: id_def) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

911 

af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

912 
lemma mset_permute_list [simp]: 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

913 
assumes "f permutes {..<length (xs :: 'a list)}" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

914 
shows "mset (permute_list f xs) = mset xs" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

915 
proof (rule multiset_eqI) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

916 
fix y :: 'a 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

917 
from assms have [simp]: "f x < length xs \<longleftrightarrow> x < length xs" for x 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

918 
using permutes_in_image[OF assms] by auto 
64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

919 
have "count (mset (permute_list f xs)) y = 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

920 
card ((\<lambda>i. xs ! f i) ` {y} \<inter> {..<length xs})" 
64543
6b13586ef1a2
remove typo in bij_swap_compose_bij theorem name; tune proof
bulwahn
parents:
64284
diff
changeset

921 
by (simp add: permute_list_def count_image_mset atLeast0LessThan) 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

922 
also have "(\<lambda>i. xs ! f i) ` {y} \<inter> {..<length xs} = f ` {i. i < length xs \<and> y = xs ! i}" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

923 
by auto 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

924 
also from assms have "card \<dots> = card {i. i < length xs \<and> y = xs ! i}" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

925 
by (intro card_vimage_inj) (auto simp: permutes_inj permutes_surj) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

926 
also have "\<dots> = count (mset xs) y" by (simp add: count_mset length_filter_conv_card) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

927 
finally show "count (mset (permute_list f xs)) y = count (mset xs) y" by simp 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

928 
qed 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

929 

64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

930 
lemma set_permute_list [simp]: 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

931 
assumes "f permutes {..<length xs}" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

932 
shows "set (permute_list f xs) = set xs" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

933 
by (rule mset_eq_setD[OF mset_permute_list]) fact 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

934 

af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

935 
lemma distinct_permute_list [simp]: 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

936 
assumes "f permutes {..<length xs}" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

937 
shows "distinct (permute_list f xs) = distinct xs" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

938 
by (simp add: distinct_count_atmost_1 assms) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

939 

64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

940 
lemma permute_list_zip: 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

941 
assumes "f permutes A" "A = {..<length xs}" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

942 
assumes [simp]: "length xs = length ys" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

943 
shows "permute_list f (zip xs ys) = zip (permute_list f xs) (permute_list f ys)" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

944 
proof  
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

945 
from permutes_in_image[OF assms(1)] assms(2) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

946 
have [simp]: "f i < length ys \<longleftrightarrow> i < length ys" for i by simp 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

947 
have "permute_list f (zip xs ys) = map (\<lambda>i. zip xs ys ! f i) [0..<length ys]" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

948 
by (simp_all add: permute_list_def zip_map_map) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

949 
also have "\<dots> = map (\<lambda>(x, y). (xs ! f x, ys ! f y)) (zip [0..<length ys] [0..<length ys])" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

950 
by (intro nth_equalityI) simp_all 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

951 
also have "\<dots> = zip (permute_list f xs) (permute_list f ys)" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

952 
by (simp_all add: permute_list_def zip_map_map) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

953 
finally show ?thesis . 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

954 
qed 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

955 

64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

956 
lemma map_of_permute: 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

957 
assumes "\<sigma> permutes fst ` set xs" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

958 
shows "map_of xs \<circ> \<sigma> = map_of (map (\<lambda>(x,y). (inv \<sigma> x, y)) xs)" (is "_ = map_of (map ?f _)") 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

959 
proof 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

960 
fix x 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

961 
from assms have "inj \<sigma>" "surj \<sigma>" by (simp_all add: permutes_inj permutes_surj) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

962 
thus "(map_of xs \<circ> \<sigma>) x = map_of (map ?f xs) x" 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

963 
by (induction xs) (auto simp: inv_f_f surj_f_inv_f) 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

964 
qed 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

965 

54681  966 

60500  967 
subsection \<open>More lemmas about permutations\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

968 

63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

969 
text \<open> 
63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

970 
The following few lemmas were contributed by Lukas Bulwahn. 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

971 
\<close> 
63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

972 

0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

973 
lemma count_image_mset_eq_card_vimage: 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

974 
assumes "finite A" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

975 
shows "count (image_mset f (mset_set A)) b = card {a \<in> A. f a = b}" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

976 
using assms 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

977 
proof (induct A) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

978 
case empty 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

979 
show ?case by simp 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

980 
next 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

981 
case (insert x F) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

982 
show ?case 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

983 
proof cases 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

984 
assume "f x = b" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

985 
from this have "count (image_mset f (mset_set (insert x F))) b = Suc (card {a \<in> F. f a = f x})" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

986 
using insert.hyps by auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

987 
also have "\<dots> = card (insert x {a \<in> F. f a = f x})" 
64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

988 
using insert.hyps(1,2) by simp 
63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

989 
also have "card (insert x {a \<in> F. f a = f x}) = card {a \<in> insert x F. f a = b}" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

990 
using \<open>f x = b\<close> by (auto intro: arg_cong[where f="card"]) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

991 
finally show ?thesis using insert by auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

992 
next 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

993 
assume A: "f x \<noteq> b" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

994 
hence "{a \<in> F. f a = b} = {a \<in> insert x F. f a = b}" by auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

995 
with insert A show ?thesis by simp 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

996 
qed 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

997 
qed 
64284
f3b905b2eee2
HOLAnalysis: more theorems from Sébastien Gouëzel's Ergodic_Theory
hoelzl
parents:
64267
diff
changeset

998 

63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

999 
(* Prove image_mset_eq_implies_permutes *) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1000 
lemma image_mset_eq_implies_permutes: 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1001 
fixes f :: "'a \<Rightarrow> 'b" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1002 
assumes "finite A" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1003 
assumes mset_eq: "image_mset f (mset_set A) = image_mset f' (mset_set A)" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1004 
obtains p where "p permutes A" and "\<forall>x\<in>A. f x = f' (p x)" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

1005 
proof  
63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1006 
from \<open>finite A\<close> have [simp]: "finite {a \<in> A. f a = (b::'b)}" for f b by auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1007 
have "f ` A = f' ` A" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1008 
proof  
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1009 
have "f ` A = f ` (set_mset (mset_set A))" using \<open>finite A\<close> by simp 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1010 
also have "\<dots> = f' ` (set_mset (mset_set A))" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1011 
by (metis mset_eq multiset.set_map) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1012 
also have "\<dots> = f' ` A" using \<open>finite A\<close> by simp 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1013 
finally show ?thesis . 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1014 
qed 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1015 
have "\<forall>b\<in>(f ` A). \<exists>p. bij_betw p {a \<in> A. f a = b} {a \<in> A. f' a = b}" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

1016 
proof 
63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1017 
fix b 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1018 
from mset_eq have 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1019 
"count (image_mset f (mset_set A)) b = count (image_mset f' (mset_set A)) b" by simp 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1020 
from this have "card {a \<in> A. f a = b} = card {a \<in> A. f' a = b}" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1021 
using \<open>finite A\<close> 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1022 
by (simp add: count_image_mset_eq_card_vimage) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1023 
from this show "\<exists>p. bij_betw p {a\<in>A. f a = b} {a \<in> A. f' a = b}" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

1024 
by (intro finite_same_card_bij) simp_all 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

1025 
qed 
63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1026 
hence "\<exists>p. \<forall>b\<in>f ` A. bij_betw (p b) {a \<in> A. f a = b} {a \<in> A. f' a = b}" 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

1027 
by (rule bchoice) 
63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1028 
then guess p .. note p = this 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1029 
define p' where "p' = (\<lambda>a. if a \<in> A then p (f a) a else a)" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1030 
have "p' permutes A" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1031 
proof (rule bij_imp_permutes) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1032 
have "disjoint_family_on (\<lambda>i. {a \<in> A. f' a = i}) (f ` A)" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1033 
unfolding disjoint_family_on_def by auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1034 
moreover have "bij_betw (\<lambda>a. p (f a) a) {a \<in> A. f a = b} {a \<in> A. f' a = b}" if b: "b \<in> f ` A" for b 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1035 
using p b by (subst bij_betw_cong[where g="p b"]) auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1036 
ultimately have "bij_betw (\<lambda>a. p (f a) a) (\<Union>b\<in>f ` A. {a \<in> A. f a = b}) (\<Union>b\<in>f ` A. {a \<in> A. f' a = b})" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1037 
by (rule bij_betw_UNION_disjoint) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1038 
moreover have "(\<Union>b\<in>f ` A. {a \<in> A. f a = b}) = A" by auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1039 
moreover have "(\<Union>b\<in>f ` A. {a \<in> A. f' a = b}) = A" using \<open>f ` A = f' ` A\<close> by auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1040 
ultimately show "bij_betw p' A A" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1041 
unfolding p'_def by (subst bij_betw_cong[where g="(\<lambda>a. p (f a) a)"]) auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1042 
next 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1043 
fix x 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1044 
assume "x \<notin> A" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1045 
from this show "p' x = x" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1046 
unfolding p'_def by simp 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

1047 
qed 
63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1048 
moreover from p have "\<forall>x\<in>A. f x = f' (p' x)" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1049 
unfolding p'_def using bij_betwE by fastforce 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1050 
ultimately show ?thesis by (rule that) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1051 
qed 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

1052 

63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1053 
lemma mset_set_upto_eq_mset_upto: 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1054 
"mset_set {..<n} = mset [0..<n]" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1055 
by (induct n) (auto simp add: add.commute lessThan_Suc) 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

1056 

63921
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1057 
(* and derive the existing property: *) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1058 
lemma mset_eq_permutation: 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1059 
assumes mset_eq: "mset (xs::'a list) = mset ys" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1060 
obtains p where "p permutes {..<length ys}" "permute_list p ys = xs" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1061 
proof  
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1062 
from mset_eq have length_eq: "length xs = length ys" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1063 
using mset_eq_length by blast 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1064 
have "mset_set {..<length ys} = mset [0..<length ys]" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1065 
using mset_set_upto_eq_mset_upto by blast 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1066 
from mset_eq length_eq this have 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1067 
"image_mset (\<lambda>i. xs ! i) (mset_set {..<length ys}) = image_mset (\<lambda>i. ys ! i) (mset_set {..<length ys})" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1068 
by (metis map_nth mset_map) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1069 
from image_mset_eq_implies_permutes[OF _ this] 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1070 
obtain p where "p permutes {..<length ys}" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1071 
and "\<forall>i\<in>{..<length ys}. xs ! i = ys ! (p i)" by auto 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1072 
moreover from this length_eq have "permute_list p ys = xs" 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1073 
by (auto intro!: nth_equalityI simp add: permute_list_nth) 
0a5184877cb7
Additions to permutations (contributed by Lukas Bulwahn)
eberlm <eberlm@in.tum.de>
parents:
63539
diff
changeset

1074 
ultimately show thesis using that by blast 
63099
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

1075 
qed 
af0e964aad7b
Moved material from AFP/Randomised_Social_Choice to distribution
eberlm
parents:
62390
diff
changeset

1076 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1077 
lemma permutes_natset_le: 
54681  1078 
fixes S :: "'a::wellorder set" 
1079 
assumes p: "p permutes S" 

1080 
and le: "\<forall>i \<in> S. p i \<le> i" 

1081 
shows "p = id" 

1082 
proof  

1083 
{ 

1084 
fix n 

30488  1085 
have "p n = n" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1086 
using p le 
54681  1087 
proof (induct n arbitrary: S rule: less_induct) 
1088 
fix n S 

1089 
assume H: 

1090 
"\<And>m S. m < n \<Longrightarrow> p permutes S \<Longrightarrow> \<forall>i\<in>S. p i \<le> i \<Longrightarrow> p m = m" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

1091 
"p permutes S" "\<forall>i \<in>S. p i \<le> i" 
54681  1092 
{ 
1093 
assume "n \<notin> S" 

1094 
with H(2) have "p n = n" 

1095 
unfolding permutes_def by metis 

1096 
} 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1097 
moreover 
54681  1098 
{ 
1099 
assume ns: "n \<in> S" 

1100 
from H(3) ns have "p n < n \<or> p n = n" 

1101 
by auto 

1102 
moreover { 

1103 
assume h: "p n < n" 

1104 
from H h have "p (p n) = p n" 

1105 
by metis 

1106 
with permutes_inj[OF H(2)] have "p n = n" 

1107 
unfolding inj_on_def by blast 

1108 
with h have False 

1109 
by simp 

1110 
} 

1111 
ultimately have "p n = n" 

1112 
by blast 

1113 
} 

1114 
ultimately show "p n = n" 

1115 
by blast 

1116 
qed 

1117 
} 

1118 
then show ?thesis 

1119 
by (auto simp add: fun_eq_iff) 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1120 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1121 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1122 
lemma permutes_natset_ge: 
54681  1123 
fixes S :: "'a::wellorder set" 
1124 
assumes p: "p permutes S" 

1125 
and le: "\<forall>i \<in> S. p i \<ge> i" 

1126 
shows "p = id" 

1127 
proof  

1128 
{ 

1129 
fix i 

1130 
assume i: "i \<in> S" 

1131 
from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S" 

1132 
by simp 

1133 
with le have "p (inv p i) \<ge> inv p i" 

1134 
by blast 

1135 
with permutes_inverses[OF p] have "i \<ge> inv p i" 

1136 
by simp 

1137 
} 

1138 
then have th: "\<forall>i\<in>S. inv p i \<le> i" 

1139 
by blast 

30488  1140 
from permutes_natset_le[OF permutes_inv[OF p] th] 
54681  1141 
have "inv p = inv id" 
1142 
by simp 

30488  1143 
then show ?thesis 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1144 
apply (subst permutes_inv_inv[OF p, symmetric]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1145 
apply (rule inv_unique_comp) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1146 
apply simp_all 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1147 
done 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1148 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1149 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1150 
lemma image_inverse_permutations: "{inv p p. p permutes S} = {p. p permutes S}" 
54681  1151 
apply (rule set_eqI) 
1152 
apply auto 

1153 
using permutes_inv_inv permutes_inv 

1154 
apply auto 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1155 
apply (rule_tac x="inv x" in exI) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1156 
apply auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1157 
done 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1158 

30488  1159 
lemma image_compose_permutations_left: 
54681  1160 
assumes q: "q permutes S" 
1161 
shows "{q \<circ> p  p. p permutes S} = {p . p permutes S}" 

1162 
apply (rule set_eqI) 

1163 
apply auto 

1164 
apply (rule permutes_compose) 

1165 
using q 

1166 
apply auto 

1167 
apply (rule_tac x = "inv q \<circ> x" in exI) 

1168 
apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o) 

1169 
done 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1170 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1171 
lemma image_compose_permutations_right: 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1172 
assumes q: "q permutes S" 
54681  1173 
shows "{p \<circ> q  p. p permutes S} = {p . p permutes S}" 
1174 
apply (rule set_eqI) 

1175 
apply auto 

1176 
apply (rule permutes_compose) 

1177 
using q 

1178 
apply auto 

1179 
apply (rule_tac x = "x \<circ> inv q" in exI) 

1180 
apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc) 

1181 
done 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1182 

54681  1183 
lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} \<Longrightarrow> 1 \<le> p i \<and> p i \<le> n" 
1184 
by (simp add: permutes_def) metis 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1185 

64267  1186 
lemma sum_permutations_inverse: 
1187 
"sum f {p. p permutes S} = sum (\<lambda>p. f(inv p)) {p. p permutes S}" 

54681  1188 
(is "?lhs = ?rhs") 
1189 
proof  

30036  1190 
let ?S = "{p . p permutes S}" 
54681  1191 
have th0: "inj_on inv ?S" 
1192 
proof (auto simp add: inj_on_def) 

1193 
fix q r 

1194 
assume q: "q permutes S" 

1195 
and r: "r permutes S" 

1196 
and qr: "inv q = inv r" 

1197 
then have "inv (inv q) = inv (inv r)" 

1198 
by simp 

1199 
with permutes_inv_inv[OF q] permutes_inv_inv[OF r] show "q = r" 

1200 
by metis 

1201 
qed 

1202 
have th1: "inv ` ?S = ?S" 

1203 
using image_inverse_permutations by blast 

64267  1204 
have th2: "?rhs = sum (f \<circ> inv) ?S" 
54681  1205 
by (simp add: o_def) 
64267  1206 
from sum.reindex[OF th0, of f] show ?thesis unfolding th1 th2 . 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1207 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1208 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1209 
lemma setum_permutations_compose_left: 
30036  1210 
assumes q: "q permutes S" 
64267  1211 
shows "sum f {p. p permutes S} = sum (\<lambda>p. f(q \<circ> p)) {p. p permutes S}" 
54681  1212 
(is "?lhs = ?rhs") 
1213 
proof  

30036  1214 
let ?S = "{p. p permutes S}" 
64267  1215 
have th0: "?rhs = sum (f \<circ> (op \<circ> q)) ?S" 
54681  1216 
by (simp add: o_def) 
1217 
have th1: "inj_on (op \<circ> q) ?S" 

1218 
proof (auto simp add: inj_on_def) 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1219 
fix p r 
54681  1220 
assume "p permutes S" 
1221 
and r: "r permutes S" 

1222 
and rp: "q \<circ> p = q \<circ> r" 

1223 
then have "inv q \<circ> q \<circ> p = inv q \<circ> q \<circ> r" 

1224 
by (simp add: comp_assoc) 

1225 
with permutes_inj[OF q, unfolded inj_iff] show "p = r" 

1226 
by simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1227 
qed 
54681  1228 
have th3: "(op \<circ> q) ` ?S = ?S" 
1229 
using image_compose_permutations_left[OF q] by auto 

64267  1230 
from sum.reindex[OF th1, of f] show ?thesis unfolding th0 th1 th3 . 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1231 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1232 

cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1233 
lemma sum_permutations_compose_right: 
30036  1234 
assumes q: "q permutes S" 
64267  1235 
shows "sum f {p. p permutes S} = sum (\<lambda>p. f(p \<circ> q)) {p. p permutes S}" 
54681  1236 
(is "?lhs = ?rhs") 
1237 
proof  

30036  1238 
let ?S = "{p. p permutes S}" 
64267  1239 
have th0: "?rhs = sum (f \<circ> (\<lambda>p. p \<circ> q)) ?S" 
54681  1240 
by (simp add: o_def) 
1241 
have th1: "inj_on (\<lambda>p. p \<circ> q) ?S" 

1242 
proof (auto simp add: inj_on_def) 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1243 
fix p r 
54681  1244 
assume "p permutes S" 
1245 
and r: "r permutes S" 

1246 
and rp: "p \<circ> q = r \<circ> q" 

1247 
then have "p \<circ> (q \<circ> inv q) = r \<circ> (q \<circ> inv q)" 

1248 
by (simp add: o_assoc) 

1249 
with permutes_surj[OF q, unfolded surj_iff] show "p = r" 

1250 
by simp 

29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1251 
qed 
54681  1252 
have th3: "(\<lambda>p. p \<circ> q) ` ?S = ?S" 
1253 
using image_compose_permutations_right[OF q] by auto 

64267  1254 
from sum.reindex[OF th1, of f] 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1255 
show ?thesis unfolding th0 th1 th3 . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1256 
qed 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1257 

54681  1258 

60500  1259 
subsection \<open>Sum over a set of permutations (could generalize to iteration)\<close> 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1260 

64267  1261 
lemma sum_over_permutations_insert: 
54681  1262 
assumes fS: "finite S" 
1263 
and aS: "a \<notin> S" 

64267
b9a1486e79be
setsum > sum
nipkow< 