author  chaieb 
Mon, 09 Feb 2009 16:42:15 +0000  
changeset 29840  cfab6a76aa13 
child 30036  3a074e3a9a18 
child 30240  5b25fee0362c 
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 
ID: $Id: 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

6 
header {* Permutations, both general and specifically on finite sets.*} 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

7 

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

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

9 
imports Main Finite_Cartesian_Product Parity 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

11 

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

12 
(* Why should I import Main just to solve the Typerep problem! *) 
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 
definition permutes (infixr "permutes" 41) where 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

15 
"(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

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 
(* Transpositions. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

20 

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

21 
declare swap_self[simp] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

22 
lemma swapid_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 (auto simp add: expand_fun_eq swap_def fun_upd_def) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

24 
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

25 
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

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

27 
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

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

29 

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

30 
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

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

32 
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

33 

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

34 
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

35 
by (rule inv_unique_comp, simp_all) 
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 
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

38 
by (simp add: swap_def) 
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 
(* Basic consequences of the definition. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

42 
(*  *) 
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_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

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

46 

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

47 
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

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

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

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

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

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

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

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

55 

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

56 
lemma permutes_inj: "p permutes S ==> inj p " 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

57 
unfolding permutes_def inj_on_def by blast 
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_surj: "p permutes s ==> surj p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

61 

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

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

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

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

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

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

67 

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

68 

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

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

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

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

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

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

74 
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

75 

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

76 
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

77 
unfolding permutes_def by blast 
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_empty[simp]: "p permutes {} \<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 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

81 

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

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

83 
unfolding expand_fun_eq permutes_def apply simp by metis 
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_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

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

87 

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

88 
lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

89 
unfolding permutes_def inv_def apply auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

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

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

97 

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

98 
lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

99 
unfolding permutes_def swap_def fun_upd_def apply auto apply metis done 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

100 

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

101 
lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S  T. p x = x) \<Longrightarrow> p permutes T" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

102 
apply (simp add: Ball_def permutes_def Diff_iff) by metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

103 

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 
(* Group properties. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

106 
(*  *) 
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_id: "id permutes S" unfolding permutes_def by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

109 

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

110 
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

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

112 

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

113 
lemma permutes_inv: assumes pS: "p permutes S" shows "inv p permutes S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

115 

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

116 
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

117 
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

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

119 

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 
(* The number of permutations on a finite set. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

123 

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

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

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

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

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

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

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

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

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

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

133 

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

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

135 
(\<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

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

137 

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

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

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

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

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

142 
have th0: "p = Fun.swap a ?b id o ?q" unfolding expand_fun_eq o_assoc by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

143 
have th1: "?b \<in> insert a S " unfolding permutes_in_image[OF pS] by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

145 
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

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

147 
{fix b q assume bq: "p = Fun.swap a b id o q" "b \<in> insert a S" "q permutes S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

148 
from permutes_subset[OF bq(3), of "insert a S"] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

151 
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

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

153 
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

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

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

156 

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

157 
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

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

159 

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

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

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

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

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

164 

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

165 
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

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

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

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

169 
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

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

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

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

173 
assume fF: "finite F" and xF: "x \<notin> F" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

174 
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

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

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

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

178 
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

179 
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

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

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

182 
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

183 
from H Fs have pFs: "?pF hassize fact (n  1)" by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

184 
hence pF'f: "finite ?pF'" using H0 unfolding hassize_def 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

185 
apply (simp only: Collect_split Collect_mem_eq) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

189 

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

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

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

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

193 
fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

194 
and eq: "?g (b,p) = ?g (c,q)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

195 
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 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

196 
from ths(4) xF eq have "b = ?g (b,p) x" unfolding permutes_def 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

198 
also have "\<dots> = ?g (c,q) x" using ths(5) xF eq 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

200 
also have "\<dots> = c"using ths(5) xF unfolding permutes_def 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

202 
finally have bc: "b = c" . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

203 
hence "Fun.swap x b id = Fun.swap x c id" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

204 
with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

205 
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 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

207 
with bc have "(b,p) = (c,q)" by simp } 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

210 
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

211 
hence "\<exists>m. n = Suc m" by arith 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

212 
then obtain m where n[simp]: "n = Suc m" by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

213 
from pFs H0 have xFc: "card ?xF = fact n" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

214 
unfolding xfgpF' card_image[OF ginj] hassize_def 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

215 
apply (simp only: Collect_split Collect_mem_eq card_cartesian_product) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

218 
have "?xF hassize fact n" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

222 
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 
with Sn show ?thesis by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

226 

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

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

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

229 

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 
(* Permutations of index set for iterated operations. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

233 

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

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

235 
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

236 
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

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

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

239 
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

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

241 
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

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

243 
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

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

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

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

247 

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

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

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

250 
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

251 

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

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

253 
shows "setsum f {m .. n} = setsum (f o p) {m .. n}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

254 
using setsum_permute[OF pS, of f ] pS by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

255 

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

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

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

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

259 
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

260 

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

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

262 
shows "setprod f {m .. n} = setprod (f o p) {m .. n}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

263 
using setprod_permute[OF pS, of f ] pS by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

264 

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 
(* Various combinations of transpositions with 2, 1 and 0 common elements. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

267 
(*  *) 
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 \<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

270 

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

271 
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

272 

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

273 
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

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

275 

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 
(* Permutations as transposition sequences. *) 
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 

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

280 

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

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

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

283 
 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

284 

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

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

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

287 

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 
(* Some closure properties of the set of permutations, with lengths. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

291 

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

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

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

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

295 

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

296 
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

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

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

299 

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

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

301 
apply (cases "a=b", simp_all) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

302 
unfolding permutation_def using swapidseq_swap[of a b] by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

303 

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

304 
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

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

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

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

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

309 
have th: "Suc n + m = Suc (n + m)" by arith 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

310 
show ?case unfolding th o_assoc[symmetric] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

311 
apply (rule swapidseq.comp_Suc) using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3) by blast+ 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

313 

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

314 
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

315 
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

316 

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

317 
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

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

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

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

321 

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

322 
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

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

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

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

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

327 
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

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

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

330 
from swapidseq_swap[of a b] H(3) have th0: "swapidseq 1 (Fun.swap a b id)" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

331 
from swapidseq_comp_add[OF q(1) th0] have th1:"swapidseq (Suc n) ?q" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

332 
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

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

334 
finally have th2: "Fun.swap a b id o p o ?q = id" . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

335 
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) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

336 
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

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

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

339 

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

340 

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

341 
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

342 
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

343 

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

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

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

346 

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 
(* The identity map only has even transposition sequences. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

350 

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

351 
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

352 
(\<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

353 
==> (\<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

354 

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

355 
lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> Fun.swap a b id o Fun.swap c d id = id \<or> 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

356 
(\<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)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

358 
assume H: "a\<noteq>b" "c\<noteq>d" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

359 
have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

360 
( Fun.swap a b id o Fun.swap c d id = id \<or> 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

361 
(\<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))" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

362 
apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d]) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

363 
apply (simp_all only: swapid_sym) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

364 
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

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

366 
apply (rule disjI2) 
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 (rule_tac x="d" in exI) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

372 
apply (rule disjI2) 
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 (rule_tac x="d" in exI) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

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

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

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

383 
with H show ?thesis by metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

385 

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

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

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

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

389 

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

390 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

404 
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

405 
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

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

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

408 
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

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

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

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

412 
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

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

414 
{assume H: "Fun.swap a b id o Fun.swap c d id = id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

415 

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

416 
have ?case apply (simp only: cdqm o_assoc H) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

419 
{ fix x y z 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

420 
assume H: "x\<noteq>a" "y\<noteq>a" "z \<noteq>a" "x \<noteq>y" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

421 
"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

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

423 

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

424 
{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

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

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

427 
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

428 
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

429 
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

430 
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

431 
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

432 
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

433 
have th2: "swapidseq (n  1) (Fun.swap a z id o q)" "n \<noteq> 0" by blast+ 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

434 
have th: "Suc n  1 = Suc (n  1)" using th2(2) by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

440 
ultimately show ?case using swap_general[OF Suc.prems(2) cdqm(4)] by metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

442 

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

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

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

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

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

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

448 
assume H: "\<forall>m<n. swapidseq m (id::'a \<Rightarrow> 'a) \<longrightarrow> even m" "swapidseq n (id :: 'a \<Rightarrow> 'a)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

449 
{assume "n = 0" hence "even n" by arith} 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

452 
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

453 
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

454 
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

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

456 
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

457 
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

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

459 

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 
(* Therefore we have a welldefined notion of parity. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

463 

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

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

465 

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

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

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

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

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

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

471 
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

472 

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

473 
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

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

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

476 

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

477 
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

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

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

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

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

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

483 

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 
(* And it has the expected composition properties. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

487 

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

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

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

490 

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

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

492 
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

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

494 

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

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

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

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

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

499 
from p q obtain 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

503 
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

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

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

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

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

508 

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

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

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

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

512 
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

513 
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

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

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

516 

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 
(* A more abstract characterization of permutations. *) 
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 

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

521 

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

522 
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

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

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

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

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

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

528 

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

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

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

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

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

533 
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

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

535 
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

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

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

538 

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

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

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

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

542 
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

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

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

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

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

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

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

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

550 
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

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

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

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

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

555 

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

556 
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

557 
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

558 

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

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

560 
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

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

562 
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

563 

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

564 
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

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

566 
assume H: "bij p" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

571 

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

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

573 
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

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

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

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

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

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

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

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

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

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

583 
from bij_swap_ompose_bij[OF insert(4)] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

584 
have br: "bij ?r" . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

585 

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

586 
from insert raa have th: "\<forall>x. x \<notin> F \<longrightarrow> ?r x = x" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

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

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

594 
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

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

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

597 

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

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

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

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

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

602 
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

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

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

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

606 
from permutation_lemma[OF bf] show ?lhs by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

608 

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

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

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

611 
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

612 

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

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

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

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

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

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

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

619 
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

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

621 
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

622 
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

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

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

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

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

627 

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 
(* Relation to "permutes". *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

631 

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

632 
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

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

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

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

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

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

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

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

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

641 

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 
(* Hence a sort of induction principle composing by swaps. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

645 

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

646 
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

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

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

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

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

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

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

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

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

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

656 
from permutes_in_image[OF insert.prems(3), of x] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

660 
unfolding permutation_permutes using insert.hyps(1) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

661 
permutes_insert_lemma[OF insert.prems(3)] by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

662 
from insert.prems(2)[OF xF pxF Pr Pr rp] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

663 
show ?case unfolding qp . 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

665 

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

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

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

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

669 

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

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

671 

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

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

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

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

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

676 
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

677 
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

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

679 
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

680 

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 
(* More lemmas about permutations. *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

684 

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

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

686 
assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S. p i <= i" shows "p = id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

692 
fix n S assume H: "\<forall> m< n. \<forall>S. p permutes S \<longrightarrow> (\<forall>i\<in>S. p i \<le> i) \<longrightarrow> p m = m" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

694 
{assume "n \<notin> S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

698 
from H(3) ns have "p n < n \<or> p n = n" by auto 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

699 
moreover{assume h: "p n < n" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

700 
from H h have "p (p n) = p n" by metis 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

701 
with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

702 
with h have False by arith} 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

704 
ultimately show "p n = n" by blast 
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 
thus ?thesis by (auto simp add: expand_fun_eq) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

708 

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

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

710 
assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S. p i \<ge> i" shows "p = id" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

713 
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

714 
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

715 
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

716 
then have th: "\<forall>i\<in>S. inv p i \<le> i" by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

717 
from permutes_natset_le[OF permutes_inv[OF p] th] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

718 
have "inv p = inv id" by simp 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

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

725 

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

726 
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

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

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

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

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

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

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

733 

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

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

735 
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

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

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

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

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

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

741 
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

742 

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

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

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

745 
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

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

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

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

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

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

751 
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

752 

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

753 
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

754 

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

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

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

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

758 

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

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

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

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

762 
let ?S = "{p . p permutes {m .. n}}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

763 
have th0: "inj_on inv ?S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

766 
assume q: "q permutes {m .. n}" and r: "r permutes {m .. n}" and qr: "inv q = inv r" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

772 
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

773 
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

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

775 

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

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

777 
assumes q: "q permutes {m..n}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

778 
shows "setsum f {p. p permutes {m..n}} = 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

779 
setsum (\<lambda>p. f(q o p)) {p. p permutes {m..n}}" (is "?lhs = ?rhs") 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

781 
let ?S = "{p. p permutes {m..n}}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

782 
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

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

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

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

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

787 
assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "q \<circ> p = q \<circ> r" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

788 
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

789 
with permutes_inj[OF q, unfolded inj_iff] 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

790 

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

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

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

793 
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

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

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

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

797 

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

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

799 
assumes q: "q permutes {m..n}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

800 
shows "setsum f {p. p permutes {m..n}} = 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

801 
setsum (\<lambda>p. f(p o q)) {p. p permutes {m..n}}" (is "?lhs = ?rhs") 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

803 
let ?S = "{p. p permutes {m..n}}" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

804 
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

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

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

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

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

809 
assume "p permutes {m..n}" and r:"r permutes {m..n}" and rp: "p o q = r o q" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

810 
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

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

812 

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

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

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

815 
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

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

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

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

819 

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 
(* Sum over a set of permutations (could generalize to iteration). *) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

823 

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

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

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

826 
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

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

828 
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

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

830 
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

831 
have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q" by blast 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

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

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

838 
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

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

840 
{fix b c p q assume b: "b \<in> insert a S" and c: "c \<in> insert a S" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

842 
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

843 
from p q aS have pa: "p a = a" and qa: "q a = a" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

845 
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

846 
hence bc: "b = c" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

848 
apply (cases "a = b", auto) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

849 
by (cases "b = c", auto) 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

850 
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

851 
hence "p = q" unfolding o_assoc swap_id_idempotent 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

855 

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

856 
then show "inj_on ?f (insert a S \<times> ?P)" 
cfab6a76aa13
Permutations, both general and specifically on finite sets.
chaieb
parents:
diff
changeset

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

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

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

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

861 

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

862 
end 