76 interpret bijection "apply f" |
76 interpret bijection "apply f" |
77 by standard (rule bij_apply) |
77 by standard (rule bij_apply) |
78 assume "card (affected f) = 1" |
78 assume "card (affected f) = 1" |
79 then obtain a where *: "affected f = {a}" |
79 then obtain a where *: "affected f = {a}" |
80 by (rule card_1_singletonE) |
80 by (rule card_1_singletonE) |
81 then have "f \<langle>$\<rangle> a \<noteq> a" |
81 then have **: "f \<langle>$\<rangle> a \<noteq> a" |
82 by (simp add: in_affected [symmetric]) |
82 by (simp add: in_affected [symmetric]) |
83 moreover with * have "f \<langle>$\<rangle> a \<notin> affected f" |
83 with * have "f \<langle>$\<rangle> a \<notin> affected f" |
84 by simp |
84 by simp |
85 then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a" |
85 then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a" |
86 by (simp add: in_affected) |
86 by (simp add: in_affected) |
87 then have "inv (apply f) (f \<langle>$\<rangle> (f \<langle>$\<rangle> a)) = inv (apply f) (f \<langle>$\<rangle> a)" |
87 then have "inv (apply f) (f \<langle>$\<rangle> (f \<langle>$\<rangle> a)) = inv (apply f) (f \<langle>$\<rangle> a)" |
88 by simp |
88 by simp |
89 ultimately show False by simp |
89 with ** show False by simp |
90 qed |
90 qed |
91 |
91 |
92 |
92 |
93 subsection \<open>Identity, composition and inversion\<close> |
93 subsection \<open>Identity, composition and inversion\<close> |
94 |
94 |
201 \<and> f \<langle>$\<rangle> a \<notin> affected f" |
201 \<and> f \<langle>$\<rangle> a \<notin> affected f" |
202 | "a \<notin> affected f \<and> a \<notin> affected g" |
202 | "a \<notin> affected f \<and> a \<notin> affected g" |
203 using assms by auto |
203 using assms by auto |
204 then show "(g * f) \<langle>$\<rangle> a = (f * g) \<langle>$\<rangle> a" |
204 then show "(g * f) \<langle>$\<rangle> a = (f * g) \<langle>$\<rangle> a" |
205 proof cases |
205 proof cases |
206 case 1 moreover with * have "f \<langle>$\<rangle> a \<notin> affected g" |
206 case 1 |
|
207 with * have "f \<langle>$\<rangle> a \<notin> affected g" |
207 by auto |
208 by auto |
208 ultimately show ?thesis by (simp add: in_affected apply_times) |
209 with 1 show ?thesis by (simp add: in_affected apply_times) |
209 next |
210 next |
210 case 2 moreover with * have "g \<langle>$\<rangle> a \<notin> affected f" |
211 case 2 |
|
212 with * have "g \<langle>$\<rangle> a \<notin> affected f" |
211 by auto |
213 by auto |
212 ultimately show ?thesis by (simp add: in_affected apply_times) |
214 with 2 show ?thesis by (simp add: in_affected apply_times) |
213 next |
215 next |
214 case 3 then show ?thesis by (simp add: in_affected apply_times) |
216 case 3 |
|
217 then show ?thesis by (simp add: in_affected apply_times) |
215 qed |
218 qed |
216 qed |
219 qed |
217 |
220 |
218 lemma apply_power: |
221 lemma apply_power: |
219 "apply (f ^ n) = apply f ^^ n" |
222 "apply (f ^ n) = apply f ^^ n" |