author  nipkow 
Thu, 22 Oct 2009 09:27:48 +0200  
changeset 33057  764547b68538 
parent 32989  c28279b29ff1 
child 33715  8cce3a34c122 
permissions  rwrr 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

1 
(* Title: Library/Permutations 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

2 
Author: Amine Chaieb, University of Cambridge 
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 

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

5 
header {* Permutations, both general and specifically on finite sets.*} 
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 
32988  8 
imports Finite_Cartesian_Product Parity Fact 
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 

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

11 
definition permutes (infixr "permutes" 41) where 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

12 
"(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

13 

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

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

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

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

17 

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

18 
declare swap_self[simp] 
30488  19 
lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

21 
lemma swap_id_refl: "Fun.swap a a id = id" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

22 
lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

24 
lemma swap_id_idempotent[simp]: "Fun.swap a b id o Fun.swap a b id = id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

26 

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

27 
lemma inv_unique_comp: assumes fg: "f o g = id" and gf: "g o f = id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

28 
shows "inv f = g" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

29 
using fg gf inv_equality[of g f] by (auto simp add: expand_fun_eq) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

30 

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

31 
lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

33 

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

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

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

36 

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

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

38 
(* Basic consequences of the definition. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

40 

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

41 
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

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

43 

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

44 
lemma permutes_image: assumes pS: "p permutes S" shows "p ` S = S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

45 
using pS 
30488  46 
unfolding permutes_def 
47 
apply  

48 
apply (rule set_ext) 

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

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

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

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

52 

30488  53 
lemma permutes_inj: "p permutes S ==> inj p " 
54 
unfolding permutes_def inj_on_def by blast 

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

55 

30488  56 
lemma permutes_surj: "p permutes s ==> surj p" 
57 
unfolding permutes_def surj_def by metis 

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

58 

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

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

60 
shows " p o inv p = id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

61 
and "inv p o p = id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

64 

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

65 

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

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

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

69 
shows "p (inv p x) = x" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

70 
and "inv p (p x) = x" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

72 

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

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

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

75 

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

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

78 

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

79 
lemma permutes_sing[simp]: "p permutes {a} \<longleftrightarrow> p = id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

80 
unfolding expand_fun_eq permutes_def apply simp by metis 
30488  81 

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

82 
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

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

84 

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

85 
lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y" 
33057  86 
unfolding permutes_def inv_def apply auto 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

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

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

94 

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

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

97 

32988  98 
lemma permutes_superset: 
99 
"p permutes S \<Longrightarrow> (\<forall>x \<in> S  T. p x = x) \<Longrightarrow> p permutes T" 

100 
by (simp add: Ball_def permutes_def Diff_iff) metis 

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

101 

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

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

103 
(* Group properties. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

105 

30488  106 
lemma permutes_id: "id permutes S" unfolding permutes_def by simp 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

107 

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

108 
lemma permutes_compose: "p permutes S \<Longrightarrow> q permutes S ==> q o p permutes S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

110 

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

111 
lemma permutes_inv: assumes pS: "p permutes S" shows "inv p permutes S" 
30488  112 
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

113 

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

114 
lemma permutes_inv_inv: assumes pS: "p permutes S" shows "inv (inv p) = p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

117 

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

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

119 
(* The number of permutations on a finite set. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

121 

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

123 
assumes pS: "p permutes (insert a S)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

124 
shows "Fun.swap a (p a) id o p permutes S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

128 
using permutes_in_image[OF pS, of a] apply simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

131 

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

132 
lemma permutes_insert: "{p. p permutes (insert a S)} = 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

133 
(\<lambda>(b,p). Fun.swap a b id o p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

135 

30488  136 
{fix p 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

137 
{assume pS: "p permutes insert a S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

138 
let ?b = "p a" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

139 
let ?q = "Fun.swap a (p a) id o p" 
30488  140 
have th0: "p = Fun.swap a ?b id o ?q" unfolding expand_fun_eq o_assoc by simp 
141 
have th1: "?b \<in> insert a S " unfolding permutes_in_image[OF pS] by simp 

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

142 
from permutes_insert_lemma[OF pS] th0 th1 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

143 
have "\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S" by blast} 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

145 
{fix b q assume bq: "p = Fun.swap a b id o q" "b \<in> insert a S" "q permutes S" 
30488  146 
from permutes_subset[OF bq(3), of "insert a S"] 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

147 
have qS: "q permutes insert a S" by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

148 
have aS: "a \<in> insert a S" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

149 
from bq(1) permutes_compose[OF qS permutes_swap_id[OF aS bq(2)]] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

150 
have "p permutes insert a S" by simp } 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

151 
ultimately have "p permutes insert a S \<longleftrightarrow> (\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S)" by blast} 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

152 
thus ?thesis by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

154 

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

155 
lemma hassize_insert: "a \<notin> F \<Longrightarrow> insert a F hassize n \<Longrightarrow> F hassize (n  1)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

156 
by (auto simp add: hassize_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

157 

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

158 
lemma hassize_permutations: assumes Sn: "S hassize n" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

159 
shows "{p. p permutes S} hassize (fact n)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

161 
from Sn have fS:"finite S" by (simp add: hassize_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

162 

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

163 
have "\<forall>n. (S hassize n) \<longrightarrow> ({p. p permutes S} hassize (fact n))" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

164 
proof(rule finite_induct[where F = S]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

165 
from fS show "finite S" . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

167 
show "\<forall>n. ({} hassize n) \<longrightarrow> ({p. p permutes {}} hassize fact n)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

168 
by (simp add: hassize_def permutes_empty) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

169 
next 
30488  170 
fix x F 
171 
assume fF: "finite F" and xF: "x \<notin> F" 

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

172 
and H: "\<forall>n. (F hassize n) \<longrightarrow> ({p. p permutes F} hassize fact n)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

173 
{fix n assume H0: "insert x F hassize n" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

174 
let ?xF = "{p. p permutes insert x F}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

175 
let ?pF = "{p. p permutes F}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

176 
let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

177 
let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

178 
from permutes_insert[of x F] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

179 
have xfgpF': "?xF = ?g ` ?pF'" . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

180 
from hassize_insert[OF xF H0] have Fs: "F hassize (n  1)" . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

181 
from H Fs have pFs: "?pF hassize fact (n  1)" by blast 
30488  182 
hence pF'f: "finite ?pF'" using H0 unfolding hassize_def 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

183 
apply (simp only: Collect_split Collect_mem_eq) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

184 
apply (rule finite_cartesian_product) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

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

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

187 

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

188 
have ginj: "inj_on ?g ?pF'" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

191 
fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

192 
and eq: "?g (b,p) = ?g (c,q)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

193 
from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

194 
from ths(4) xF eq have "b = ?g (b,p) x" unfolding permutes_def 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

195 
by (auto simp add: swap_def fun_upd_def expand_fun_eq) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

196 
also have "\<dots> = ?g (c,q) x" using ths(5) xF eq 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

197 
by (auto simp add: swap_def fun_upd_def expand_fun_eq) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

198 
also have "\<dots> = c"using ths(5) xF unfolding permutes_def 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

199 
by (auto simp add: swap_def fun_upd_def expand_fun_eq) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

200 
finally have bc: "b = c" . 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

201 
hence "Fun.swap x b id = Fun.swap x c id" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

202 
with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

203 
hence "Fun.swap x b id o (Fun.swap x b id o p) = Fun.swap x b id o (Fun.swap x b id o q)" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

204 
hence "p = q" by (simp add: o_assoc) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

205 
with bc have "(b,p) = (c,q)" by simp } 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

206 
thus ?thesis unfolding inj_on_def by blast 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

208 
from xF H0 have n0: "n \<noteq> 0 " by (auto simp add: hassize_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

209 
hence "\<exists>m. n = Suc m" by arith 
30488  210 
then obtain m where n[simp]: "n = Suc m" by blast 
211 
from pFs H0 have xFc: "card ?xF = fact n" 

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

212 
unfolding xfgpF' card_image[OF ginj] hassize_def 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

213 
apply (simp only: Collect_split Collect_mem_eq card_cartesian_product) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

214 
by simp 
30488  215 
from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

216 
have "?xF hassize fact n" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

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

218 
unfolding hassize_def xFf by blast } 
30488  219 
thus "\<forall>n. (insert x F hassize n) \<longrightarrow> ({p. p permutes insert x F} hassize fact n)" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

222 
with Sn show ?thesis by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

224 

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

225 
lemma finite_permutations: "finite S ==> finite {p. p permutes S}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

226 
using hassize_permutations[of S] unfolding hassize_def by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

227 

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

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

229 
(* Permutations of index set for iterated operations. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

231 

30488  232 
lemma (in ab_semigroup_mult) fold_image_permute: assumes fS: "finite S" and pS: "p permutes S" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

233 
shows "fold_image times f z S = fold_image times (f o p) z S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

234 
using fold_image_reindex[OF fS subset_inj_on[OF permutes_inj[OF pS], of S, simplified], of f z] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

235 
unfolding permutes_image[OF pS] . 
30488  236 
lemma (in ab_semigroup_add) fold_image_permute: assumes fS: "finite S" and pS: "p permutes S" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

237 
shows "fold_image plus f z S = fold_image plus (f o p) z S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

239 
interpret ab_semigroup_mult plus apply unfold_locales apply (simp add: add_assoc) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

241 
from fold_image_reindex[OF fS subset_inj_on[OF permutes_inj[OF pS], of S, simplified], of f z] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

243 
unfolding permutes_image[OF pS] . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

245 

30488  246 
lemma setsum_permute: assumes pS: "p permutes S" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

247 
shows "setsum f S = setsum (f o p) S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

248 
unfolding setsum_def using fold_image_permute[of S p f 0] pS by clarsimp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

249 

30488  250 
lemma setsum_permute_natseg:assumes pS: "p permutes {m .. n}" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

251 
shows "setsum f {m .. n} = setsum (f o p) {m .. n}" 
30488  252 
using setsum_permute[OF pS, of f ] pS by blast 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

253 

30488  254 
lemma setprod_permute: assumes pS: "p permutes S" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

255 
shows "setprod f S = setprod (f o p) S" 
30488  256 
unfolding setprod_def 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

257 
using ab_semigroup_mult_class.fold_image_permute[of S p f 1] pS by clarsimp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

258 

30488  259 
lemma setprod_permute_natseg:assumes pS: "p permutes {m .. n}" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

260 
shows "setprod f {m .. n} = setprod (f o p) {m .. n}" 
30488  261 
using setprod_permute[OF pS, of f ] pS by blast 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

262 

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

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

264 
(* Various combinations of transpositions with 2, 1 and 0 common elements. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

266 

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

267 
lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow> Fun.swap a b id o Fun.swap a c id = Fun.swap b c id o Fun.swap a b id" by (simp add: expand_fun_eq swap_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

268 

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

269 
lemma swap_id_common': "~(a = b) \<Longrightarrow> ~(a = c) \<Longrightarrow> Fun.swap a c id o Fun.swap b c id = Fun.swap b c id o Fun.swap a b id" by (simp add: expand_fun_eq swap_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

270 

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

271 
lemma swap_id_independent: "~(a = c) \<Longrightarrow> ~(a = d) \<Longrightarrow> ~(b = c) \<Longrightarrow> ~(b = d) ==> Fun.swap a b id o Fun.swap c d id = Fun.swap c d id o Fun.swap a b id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

272 
by (simp add: swap_def expand_fun_eq) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

273 

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

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

275 
(* Permutations as transposition sequences. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

277 

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

278 

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

279 
inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

280 
id[simp]: "swapidseq 0 id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

281 
 comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id o p)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

282 

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

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

284 
definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

285 

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

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

287 
(* Some closure properties of the set of permutations, with lengths. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

289 

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

290 
lemma permutation_id[simp]: "permutation id"unfolding permutation_def 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

291 
by (rule exI[where x=0], simp) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

293 

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

294 
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

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

296 
using comp_Suc[of 0 id a b] by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

297 

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

298 
lemma permutation_swap_id: "permutation (Fun.swap a b id)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

299 
apply (cases "a=b", simp_all) 
30488  300 
unfolding permutation_def using swapidseq_swap[of a b] by blast 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

301 

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

302 
lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q ==> swapidseq (n + m) (p o q)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

303 
proof (induct n p arbitrary: m q rule: swapidseq.induct) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

304 
case (id m q) thus ?case by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

305 
next 
30488  306 
case (comp_Suc n p a b m q) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

307 
have th: "Suc n + m = Suc (n + m)" by arith 
30488  308 
show ?case unfolding th o_assoc[symmetric] 
309 
apply (rule swapidseq.comp_Suc) using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3) by blast+ 

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

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

311 

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

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

313 
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

314 

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

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

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

317 
using swapidseq_swap[of a b] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

318 
by (auto simp add: o_assoc[symmetric] intro: swapidseq.comp_Suc) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

319 

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

320 
lemma swapidseq_inverse_exists: "swapidseq n p ==> \<exists>q. swapidseq n q \<and> p o q = id \<and> q o p = id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

322 
case id thus ?case by (rule exI[where x=id], simp) 
30488  323 
next 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

325 
from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

326 
let ?q = "q o Fun.swap a b id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

327 
note H = comp_Suc.hyps 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

328 
from swapidseq_swap[of a b] H(3) have th0: "swapidseq 1 (Fun.swap a b id)" by simp 
30488  329 
from swapidseq_comp_add[OF q(1) th0] have th1:"swapidseq (Suc n) ?q" by simp 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

330 
have "Fun.swap a b id o p o ?q = Fun.swap a b id o (p o q) o Fun.swap a b id" by (simp add: o_assoc) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

331 
also have "\<dots> = id" by (simp add: q(2)) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

332 
finally have th2: "Fun.swap a b id o p o ?q = id" . 
30488  333 
have "?q \<circ> (Fun.swap a b id \<circ> p) = q \<circ> (Fun.swap a b id o Fun.swap a b id) \<circ> p" by (simp only: o_assoc) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

334 
hence "?q \<circ> (Fun.swap a b id \<circ> p) = id" by (simp add: q(3)) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

335 
with th1 th2 show ?case by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

337 

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

338 

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

339 
lemma swapidseq_inverse: assumes H: "swapidseq n p" shows "swapidseq n (inv p)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

340 
using swapidseq_inverse_exists[OF H] inv_unique_comp[of p] by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

341 

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

342 
lemma permutation_inverse: "permutation p ==> permutation (inv p)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

343 
using permutation_def swapidseq_inverse by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

344 

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

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

346 
(* The identity map only has even transposition sequences. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

348 

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

349 
lemma symmetry_lemma:"(\<And>a b c d. P a b c d ==> P a b d c) \<Longrightarrow> 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

350 
(\<And>a b c d. a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> (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) ==> P a b c d) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

351 
==> (\<And>a b c d. a \<noteq> b > c \<noteq> d \<longrightarrow> P a b c d)" by metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

352 

30488  353 
lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> Fun.swap a b id o Fun.swap c d id = id \<or> 
354 
(\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id)" 

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

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

356 
assume H: "a\<noteq>b" "c\<noteq>d" 
30488  357 
have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> 
358 
( Fun.swap a b id o Fun.swap c d id = id \<or> 

359 
(\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id))" 

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

360 
apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d]) 
30488  361 
apply (simp_all only: swapid_sym) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

362 
apply (case_tac "a = c \<and> b = d", clarsimp simp only: swapid_sym swap_id_idempotent) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

363 
apply (case_tac "a = c \<and> b \<noteq> d") 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

368 
apply (clarsimp simp add: expand_fun_eq swap_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

369 
apply (case_tac "a \<noteq> c \<and> b = d") 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

374 
apply (clarsimp simp add: expand_fun_eq swap_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

379 
apply (clarsimp simp add: expand_fun_eq swap_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

380 
done 
30488  381 
with H show ?thesis by metis 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

383 

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

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

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

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

387 

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

388 
lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow> (n=0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = Fun.swap a b id o q \<and> swapidseq m q \<and> a\<noteq> b))" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

402 
assumes spn: "swapidseq n p" and ab: "a\<noteq>b" and pa: "(Fun.swap a b id o p) a = a" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

403 
shows "n \<noteq> 0 \<and> swapidseq (n  1) (Fun.swap a b id o p)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

404 
using spn ab pa 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

405 
proof(induct n arbitrary: p a b) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

406 
case 0 thus ?case by (auto simp add: swap_def fun_upd_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

409 
from Suc.prems(1) swapidseq_cases[of "Suc n" p] obtain 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

410 
c d q m where cdqm: "Suc n = Suc m" "p = Fun.swap c d id o q" "swapidseq m q" "c \<noteq> d" "n = m" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

412 
{assume H: "Fun.swap a b id o Fun.swap c d id = id" 
30488  413 

414 
have ?case apply (simp only: cdqm o_assoc H) 

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

415 
by (simp add: cdqm)} 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

417 
{ fix x y z 
30488  418 
assume H: "x\<noteq>a" "y\<noteq>a" "z \<noteq>a" "x \<noteq>y" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

419 
"Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

420 
from H have az: "a \<noteq> z" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

421 

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

422 
{fix h have "(Fun.swap x y id o h) a = a \<longleftrightarrow> h a = a" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

423 
using H by (simp add: swap_def)} 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

424 
note th3 = this 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

425 
from cdqm(2) have "Fun.swap a b id o p = Fun.swap a b id o (Fun.swap c d id o q)" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

426 
hence "Fun.swap a b id o p = Fun.swap x y id o (Fun.swap a z id o q)" by (simp add: o_assoc H) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

427 
hence "(Fun.swap a b id o p) a = (Fun.swap x y id o (Fun.swap a z id o q)) a" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

428 
hence "(Fun.swap x y id o (Fun.swap a z id o q)) a = a" unfolding Suc by metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

429 
hence th1: "(Fun.swap a z id o q) a = a" unfolding th3 . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

430 
from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az th1] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

431 
have th2: "swapidseq (n  1) (Fun.swap a z id o q)" "n \<noteq> 0" by blast+ 
30488  432 
have th: "Suc n  1 = Suc (n  1)" using th2(2) by auto 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

433 
have ?case unfolding cdqm(2) H o_assoc th 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

434 
apply (simp only: Suc_not_Zero simp_thms o_assoc[symmetric]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

436 
using th2 H apply blast+ 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

437 
done} 
30488  438 
ultimately show ?case 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

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

440 

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

442 
assumes "swapidseq n (id :: 'a \<Rightarrow> 'a)" shows "even n" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

443 
using `swapidseq n id` 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

444 
proof(induct n rule: nat_less_induct) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

446 
assume H: "\<forall>m<n. swapidseq m (id::'a \<Rightarrow> 'a) \<longrightarrow> even m" "swapidseq n (id :: 'a \<Rightarrow> 'a)" 
30488  447 
{assume "n = 0" hence "even n" by arith} 
448 
moreover 

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

449 
{fix a b :: 'a and q m 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

450 
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

451 
from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

452 
have m: "m \<noteq> 0" "swapidseq (m  1) (id :: 'a \<Rightarrow> 'a)" by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

453 
from h m have mn: "m  1 < n" by arith 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

454 
from H(1)[rule_format, OF mn m(2)] h(1) m(1) have "even n" apply arith done} 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

455 
ultimately show "even n" using H(2)[unfolded swapidseq_cases[of n id]] by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

457 

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

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

459 
(* Therefore we have a welldefined notion of parity. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

461 

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

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

463 

30488  464 
lemma swapidseq_even_even: assumes 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

465 
m: "swapidseq m p" and n: "swapidseq n p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

468 
from swapidseq_inverse_exists[OF n] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

469 
obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast 
30488  470 

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

471 
from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

474 

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

475 
lemma evenperm_unique: assumes p: "swapidseq n p" and n:"even n = b" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

479 
apply (rule someI[where x = n]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

480 
using p by blast+ 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

481 

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

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

483 
(* And it has the expected composition properties. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

485 

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

486 
lemma evenperm_id[simp]: "evenperm id = True" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

487 
apply (rule evenperm_unique[where n = 0]) by simp_all 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

488 

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

489 
lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

490 
apply (rule evenperm_unique[where n="if a = b then 0 else 1"]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

491 
by (simp_all add: swapidseq_swap) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

492 

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

494 
assumes p: "permutation p" and q:"permutation q" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

495 
shows "evenperm (p o q) = (evenperm p = evenperm q)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

496 
proof 
30488  497 
from p q obtain 
498 
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

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

500 
note nm = swapidseq_comp_add[OF n m] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

501 
have th: "even (n + m) = (even n \<longleftrightarrow> even m)" by arith 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

503 
evenperm_unique[OF nm th] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

506 

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

507 
lemma evenperm_inv: assumes p: "permutation p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

508 
shows "evenperm (inv p) = evenperm p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

510 
from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

511 
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

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

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

514 

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

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

516 
(* A more abstract characterization of permutations. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

518 

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

519 

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

520 
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

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

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

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

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

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

526 

30488  527 
lemma permutation_bijective: 
528 
assumes p: "permutation p" 

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

529 
shows "bij p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

531 
from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast 
30488  532 
from swapidseq_inverse_exists[OF n] obtain q where 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

533 
q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

534 
thus ?thesis unfolding bij_iff apply (auto simp add: expand_fun_eq) apply metis done 
30488  535 
qed 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

536 

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

537 
lemma permutation_finite_support: assumes p: "permutation p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

538 
shows "finite {x. p x \<noteq> x}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

540 
from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

543 
case id thus ?case by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

546 
let ?S = "insert a (insert b {x. p x \<noteq> x})" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

547 
from comp_Suc.hyps(2) have fS: "finite ?S" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

548 
from `a \<noteq> b` have th: "{x. (Fun.swap a b id o p) x \<noteq> x} \<subseteq> ?S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

549 
by (auto simp add: swap_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

553 

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

554 
lemma bij_inv_eq_iff: "bij p ==> x = inv p y \<longleftrightarrow> p x = y" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

555 
using surj_f_inv_f[of p] inv_f_f[of f] by (auto simp add: bij_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

556 

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

558 
assumes bp: "bij p" shows "Fun.swap a b id o p = Fun.swap (inv p a) (inv p b) p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

559 
using surj_f_inv_f[OF bij_is_surj[OF bp]] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

560 
by (simp add: expand_fun_eq swap_def bij_inv_eq_iff[OF bp]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

561 

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

562 
lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id o p)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

564 
assume H: "bij p" 
30488  565 
show ?thesis 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

566 
unfolding bij_swap_comp[OF H] bij_swap_iff 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

569 

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

571 
assumes fS: "finite S" and p: "bij p" and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

572 
shows "permutation p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

573 
using fS p pS 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

574 
proof(induct S arbitrary: p rule: finite_induct) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

575 
case (empty p) thus ?case by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

577 
case (insert a F p) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

578 
let ?r = "Fun.swap a (p a) id o p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

579 
let ?q = "Fun.swap a (p a) id o ?r " 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

580 
have raa: "?r a = a" by (simp add: swap_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

581 
from bij_swap_ompose_bij[OF insert(4)] 
30488  582 
have br: "bij ?r" . 
583 

584 
from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x" 

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

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

586 
apply (erule_tac x="x" in allE) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

590 
from insert(3)[OF br th] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

591 
have rp: "permutation ?r" . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

592 
have "permutation ?q" by (simp add: permutation_compose permutation_swap_id rp) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

593 
thus ?case by (simp add: o_assoc) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

595 

30488  596 
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

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

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

599 
assume p: ?lhs 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

600 
from p permutation_bijective permutation_finite_support show "?b \<and> ?f" by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

602 
assume bf: "?b \<and> ?f" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

603 
hence bf: "?f" "?b" by blast+ 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

604 
from permutation_lemma[OF bf] show ?lhs by blast 
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 

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

607 
lemma permutation_inverse_works: assumes p: "permutation p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

608 
shows "inv p o p = id" "p o inv p = id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

609 
using permutation_bijective[OF p] surj_iff bij_def inj_iff by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

610 

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

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

612 
assumes p: "permutation p" and q: "permutation q" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

613 
shows "inv (p o q) = inv q o inv p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

616 
note qs = permutation_inverse_works[OF q] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

617 
have "p o q o (inv q o inv p) = p o (q o inv q) o inv p" by (simp add: o_assoc) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

618 
also have "\<dots> = id" by (simp add: ps qs) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

619 
finally have th0: "p o q o (inv q o inv p) = id" . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

620 
have "inv q o inv p o (p o q) = inv q o (inv p o p) o q" by (simp add: o_assoc) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

621 
also have "\<dots> = id" by (simp add: ps qs) 
30488  622 
finally have th1: "inv q o inv p o (p o q) = id" . 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

625 

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

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

627 
(* Relation to "permutes". *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

629 

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

630 
lemma permutation_permutes: "permutation p \<longleftrightarrow> (\<exists>S. finite S \<and> p permutes S)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

631 
unfolding permutation permutes_def bij_iff[symmetric] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

633 
apply (rule exI[where x="{x. p x \<noteq> x}"]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

636 
apply (rule_tac B="S" in finite_subset) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

639 

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

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

641 
(* Hence a sort of induction principle composing by swaps. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

643 

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

644 
lemma permutes_induct: "finite S \<Longrightarrow> P id \<Longrightarrow> (\<And> a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> P p \<Longrightarrow> P p \<Longrightarrow> permutation p ==> P (Fun.swap a b id o p)) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

645 
==> (\<And>p. p permutes S ==> P p)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

646 
proof(induct S rule: finite_induct) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

647 
case empty thus ?case by auto 
30488  648 
next 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

649 
case (insert x F p) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

650 
let ?r = "Fun.swap x (p x) id o p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

651 
let ?q = "Fun.swap x (p x) id o ?r" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

652 
have qp: "?q = p" by (simp add: o_assoc) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

653 
from permutes_insert_lemma[OF insert.prems(3)] insert have Pr: "P ?r" by blast 
30488  654 
from permutes_in_image[OF insert.prems(3), of x] 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

655 
have pxF: "p x \<in> insert x F" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

656 
have xF: "x \<in> insert x F" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

657 
have rp: "permutation ?r" 
30488  658 
unfolding permutation_permutes using insert.hyps(1) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

659 
permutes_insert_lemma[OF insert.prems(3)] by blast 
30488  660 
from insert.prems(2)[OF xF pxF Pr Pr rp] 
661 
show ?case unfolding qp . 

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

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

663 

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

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

665 
(* Sign of a permutation as a real number. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

667 

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

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

669 

30488  670 
lemma sign_nz: "sign p \<noteq> 0" by (simp add: sign_def) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

671 
lemma sign_id: "sign id = 1" by (simp add: sign_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

672 
lemma sign_inverse: "permutation p ==> sign (inv p) = sign p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

674 
lemma sign_compose: "permutation p \<Longrightarrow> permutation q ==> sign (p o q) = sign(p) * sign(q)" by (simp add: sign_def evenperm_comp) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

675 
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

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

677 
lemma sign_idempotent: "sign p * sign p = 1" by (simp add: sign_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

678 

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

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

680 
(* More lemmas about permutations. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

682 

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

683 
lemma permutes_natset_le: 
30037  684 
assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S. p i <= i" shows "p = id" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

688 
using p le 
30037  689 
proof(induct n arbitrary: S rule: less_induct) 
30488  690 
fix n S assume H: "\<And>m S. \<lbrakk>m < n; p permutes S; \<forall>i\<in>S. p i \<le> i\<rbrakk> \<Longrightarrow> p m = m" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

691 
"p permutes S" "\<forall>i \<in>S. p i \<le> i" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

692 
{assume "n \<notin> S" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

693 
with H(2) have "p n = n" unfolding permutes_def by metis} 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

695 
{assume ns: "n \<in> S" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

696 
from H(3) ns have "p n < n \<or> p n = n" by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

697 
moreover{assume h: "p n < n" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

698 
from H h have "p (p n) = p n" by metis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

699 
with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

700 
with h have False by simp} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

701 
ultimately have "p n = n" by blast } 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

702 
ultimately show "p n = n" by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

704 
thus ?thesis by (auto simp add: expand_fun_eq) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

706 

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

707 
lemma permutes_natset_ge: 
30037  708 
assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S. p i \<ge> i" shows "p = id" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

710 
{fix i assume i: "i \<in> S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

711 
from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

712 
with le have "p (inv p i) \<ge> inv p i" by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

713 
with permutes_inverses[OF p] have "i \<ge> inv p i" by simp} 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

714 
then have th: "\<forall>i\<in>S. inv p i \<le> i" by blast 
30488  715 
from permutes_natset_le[OF permutes_inv[OF p] th] 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

716 
have "inv p = inv id" by simp 
30488  717 
then show ?thesis 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

723 

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

724 
lemma image_inverse_permutations: "{inv p p. p permutes S} = {p. p permutes S}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

727 
using permutes_inv_inv permutes_inv apply auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

731 

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

733 
assumes q: "q permutes S" shows "{q o p  p. p permutes S} = {p . p permutes S}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

739 
by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

740 

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

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

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

743 
shows "{p o q  p. p permutes S} = {p . p permutes S}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

749 
by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o o_assoc[symmetric]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

750 

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

751 
lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} ==> 1 <= p i \<and> p i <= n" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

752 

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

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

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

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

756 

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

757 
term setsum 
30036  758 
lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs") 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

759 
proof 
30036  760 
let ?S = "{p . p permutes S}" 
30488  761 
have th0: "inj_on inv ?S" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

762 
proof(auto simp add: inj_on_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

763 
fix q r 
30036  764 
assume q: "q permutes S" and r: "r permutes S" and qr: "inv q = inv r" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

765 
hence "inv (inv q) = inv (inv r)" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

766 
with permutes_inv_inv[OF q] permutes_inv_inv[OF r] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

767 
show "q = r" by metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

769 
have th1: "inv ` ?S = ?S" using image_inverse_permutations by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

770 
have th2: "?rhs = setsum (f o inv) ?S" by (simp add: o_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

771 
from setsum_reindex[OF th0, of f] show ?thesis unfolding th1 th2 . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

773 

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

774 
lemma setum_permutations_compose_left: 
30036  775 
assumes q: "q permutes S" 
776 
shows "setsum f {p. p permutes S} = 

777 
setsum (\<lambda>p. f(q o p)) {p. p permutes S}" (is "?lhs = ?rhs") 

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

778 
proof 
30036  779 
let ?S = "{p. p permutes S}" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

780 
have th0: "?rhs = setsum (f o (op o q)) ?S" by (simp add: o_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

781 
have th1: "inj_on (op o q) ?S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

784 
fix p r 
30036  785 
assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

786 
hence "inv q o q o p = inv q o q o r" by (simp add: o_assoc[symmetric]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

787 
with permutes_inj[OF q, unfolded inj_iff] 
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 
show "p = r" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

791 
have th3: "(op o q) ` ?S = ?S" using image_compose_permutations_left[OF q] by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

792 
from setsum_reindex[OF th1, of f] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

795 

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

796 
lemma sum_permutations_compose_right: 
30036  797 
assumes q: "q permutes S" 
798 
shows "setsum f {p. p permutes S} = 

799 
setsum (\<lambda>p. f(p o q)) {p. p permutes S}" (is "?lhs = ?rhs") 

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

800 
proof 
30036  801 
let ?S = "{p. p permutes S}" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

802 
have th0: "?rhs = setsum (f o (\<lambda>p. p o q)) ?S" by (simp add: o_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

803 
have th1: "inj_on (\<lambda>p. p o q) ?S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

806 
fix p r 
30036  807 
assume "p permutes S" and r:"r permutes S" and rp: "p o q = r o q" 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

808 
hence "p o (q o inv q) = r o (q o inv q)" by (simp add: o_assoc) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

809 
with permutes_surj[OF q, unfolded surj_iff] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

810 

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

811 
show "p = r" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

813 
have th3: "(\<lambda>p. p o q) ` ?S = ?S" using image_compose_permutations_right[OF q] by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

814 
from setsum_reindex[OF th1, of f] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

817 

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

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

819 
(* Sum over a set of permutations (could generalize to iteration). *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

821 

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

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

823 
assumes fS: "finite S" and aS: "a \<notin> S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

824 
shows "setsum f {p. p permutes (insert a S)} = setsum (\<lambda>b. setsum (\<lambda>q. f (Fun.swap a b id o q)) {p. p permutes S}) (insert a S)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

826 
have th0: "\<And>f a b. (\<lambda>(b,p). f (Fun.swap a b id o p)) = f o (\<lambda>(b,p). Fun.swap a b id o p)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

828 
have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}" by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

829 
have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q" by blast 
30488  830 
show ?thesis 
831 
unfolding permutes_insert 

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

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

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

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

835 
proof(rule setsum_reindex) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

836 
let ?f = "(\<lambda>(b, y). Fun.swap a b id \<circ> y)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

837 
let ?P = "{p. p permutes S}" 
30488  838 
{fix b c p q assume b: "b \<in> insert a S" and c: "c \<in> insert a S" 
839 
and p: "p permutes S" and q: "q permutes S" 

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

840 
and eq: "Fun.swap a b id o p = Fun.swap a c id o q" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

841 
from p q aS have pa: "p a = a" and qa: "q a = a" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

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

843 
from eq have "(Fun.swap a b id o p) a = (Fun.swap a c id o q) a" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

844 
hence bc: "b = c" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

845 
by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong split: split_if_asm) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

846 
from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o p) = (\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o q)" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

847 
hence "p = q" unfolding o_assoc swap_id_idempotent 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32456
diff
changeset

848 
by (simp add: o_def) 
29840
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

849 
with bc have "b = c \<and> p = q" by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

850 
} 
30488  851 

852 
then show "inj_on ?f (insert a S \<times> ?P)" 

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

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

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

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

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

857 

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

858 
end 