|
1 (* Author: Lars Noschinski |
|
2 *) |
|
3 |
|
4 section \<open>Permutation orbits\<close> |
|
5 |
|
6 theory Orbits |
|
7 imports |
|
8 "HOL-Library.FuncSet" |
|
9 "HOL-Combinatorics.Permutations" |
|
10 begin |
|
11 |
|
12 subsection \<open>Orbits and cyclic permutations\<close> |
|
13 |
|
14 inductive_set orbit :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a set" for f x where |
|
15 base: "f x \<in> orbit f x" | |
|
16 step: "y \<in> orbit f x \<Longrightarrow> f y \<in> orbit f x" |
|
17 |
|
18 definition cyclic_on :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
19 "cyclic_on f S \<longleftrightarrow> (\<exists>s\<in>S. S = orbit f s)" |
|
20 |
|
21 lemma orbit_altdef: "orbit f x = {(f ^^ n) x | n. 0 < n}" (is "?L = ?R") |
|
22 proof (intro set_eqI iffI) |
|
23 fix y assume "y \<in> ?L" then show "y \<in> ?R" |
|
24 by (induct rule: orbit.induct) (auto simp: exI[where x=1] exI[where x="Suc n" for n]) |
|
25 next |
|
26 fix y assume "y \<in> ?R" |
|
27 then obtain n where "y = (f ^^ n) x" "0 < n" by blast |
|
28 then show "y \<in> ?L" |
|
29 proof (induction n arbitrary: y) |
|
30 case (Suc n) then show ?case by (cases "n = 0") (auto intro: orbit.intros) |
|
31 qed simp |
|
32 qed |
|
33 |
|
34 lemma orbit_trans: |
|
35 assumes "s \<in> orbit f t" "t \<in> orbit f u" shows "s \<in> orbit f u" |
|
36 using assms by induct (auto intro: orbit.intros) |
|
37 |
|
38 lemma orbit_subset: |
|
39 assumes "s \<in> orbit f (f t)" shows "s \<in> orbit f t" |
|
40 using assms by (induct) (auto intro: orbit.intros) |
|
41 |
|
42 lemma orbit_sim_step: |
|
43 assumes "s \<in> orbit f t" shows "f s \<in> orbit f (f t)" |
|
44 using assms by induct (auto intro: orbit.intros) |
|
45 |
|
46 lemma orbit_step: |
|
47 assumes "y \<in> orbit f x" "f x \<noteq> y" shows "y \<in> orbit f (f x)" |
|
48 using assms |
|
49 proof induction |
|
50 case (step y) then show ?case by (cases "x = y") (auto intro: orbit.intros) |
|
51 qed simp |
|
52 |
|
53 lemma self_in_orbit_trans: |
|
54 assumes "s \<in> orbit f s" "t \<in> orbit f s" shows "t \<in> orbit f t" |
|
55 using assms(2,1) by induct (auto intro: orbit_sim_step) |
|
56 |
|
57 lemma orbit_swap: |
|
58 assumes "s \<in> orbit f s" "t \<in> orbit f s" shows "s \<in> orbit f t" |
|
59 using assms(2,1) |
|
60 proof induction |
|
61 case base then show ?case by (cases "f s = s") (auto intro: orbit_step) |
|
62 next |
|
63 case (step x) then show ?case by (cases "f x = s") (auto intro: orbit_step) |
|
64 qed |
|
65 |
|
66 lemma permutation_self_in_orbit: |
|
67 assumes "permutation f" shows "s \<in> orbit f s" |
|
68 unfolding orbit_altdef using permutation_self[OF assms, of s] by simp metis |
|
69 |
|
70 lemma orbit_altdef_self_in: |
|
71 assumes "s \<in> orbit f s" shows "orbit f s = {(f ^^ n) s | n. True}" |
|
72 proof (intro set_eqI iffI) |
|
73 fix x assume "x \<in> {(f ^^ n) s | n. True}" |
|
74 then obtain n where "x = (f ^^ n) s" by auto |
|
75 then show "x \<in> orbit f s" using assms by (cases "n = 0") (auto simp: orbit_altdef) |
|
76 qed (auto simp: orbit_altdef) |
|
77 |
|
78 lemma orbit_altdef_permutation: |
|
79 assumes "permutation f" shows "orbit f s = {(f ^^ n) s | n. True}" |
|
80 using assms by (intro orbit_altdef_self_in permutation_self_in_orbit) |
|
81 |
|
82 lemma orbit_altdef_bounded: |
|
83 assumes "(f ^^ n) s = s" "0 < n" shows "orbit f s = {(f ^^ m) s| m. m < n}" |
|
84 proof - |
|
85 from assms have "s \<in> orbit f s" |
|
86 by (auto simp add: orbit_altdef) metis |
|
87 then have "orbit f s = {(f ^^ m) s|m. True}" by (rule orbit_altdef_self_in) |
|
88 also have "\<dots> = {(f ^^ m) s| m. m < n}" |
|
89 using assms |
|
90 by (auto simp: funpow_mod_eq intro: exI[where x="m mod n" for m]) |
|
91 finally show ?thesis . |
|
92 qed |
|
93 |
|
94 lemma funpow_in_orbit: |
|
95 assumes "s \<in> orbit f t" shows "(f ^^ n) s \<in> orbit f t" |
|
96 using assms by (induct n) (auto intro: orbit.intros) |
|
97 |
|
98 lemma finite_orbit: |
|
99 assumes "s \<in> orbit f s" shows "finite (orbit f s)" |
|
100 proof - |
|
101 from assms obtain n where n: "0 < n" "(f ^^ n) s = s" |
|
102 by (auto simp: orbit_altdef) |
|
103 then show ?thesis by (auto simp: orbit_altdef_bounded) |
|
104 qed |
|
105 |
|
106 lemma self_in_orbit_step: |
|
107 assumes "s \<in> orbit f s" shows "orbit f (f s) = orbit f s" |
|
108 proof (intro set_eqI iffI) |
|
109 fix t assume "t \<in> orbit f s" then show "t \<in> orbit f (f s)" |
|
110 using assms by (auto intro: orbit_step orbit_sim_step) |
|
111 qed (auto intro: orbit_subset) |
|
112 |
|
113 lemma permutation_orbit_step: |
|
114 assumes "permutation f" shows "orbit f (f s) = orbit f s" |
|
115 using assms by (intro self_in_orbit_step permutation_self_in_orbit) |
|
116 |
|
117 lemma orbit_nonempty: |
|
118 "orbit f s \<noteq> {}" |
|
119 using orbit.base by fastforce |
|
120 |
|
121 lemma orbit_inv_eq: |
|
122 assumes "permutation f" |
|
123 shows "orbit (inv f) x = orbit f x" (is "?L = ?R") |
|
124 proof - |
|
125 { fix g y assume A: "permutation g" "y \<in> orbit (inv g) x" |
|
126 have "y \<in> orbit g x" |
|
127 proof - |
|
128 have inv_g: "\<And>y. x = g y \<Longrightarrow> inv g x = y" "\<And>y. inv g (g y) = y" |
|
129 by (metis A(1) bij_inv_eq_iff permutation_bijective)+ |
|
130 |
|
131 { fix y assume "y \<in> orbit g x" |
|
132 then have "inv g y \<in> orbit g x" |
|
133 by (cases) (simp_all add: inv_g A(1) permutation_self_in_orbit) |
|
134 } note inv_g_in_orb = this |
|
135 |
|
136 from A(2) show ?thesis |
|
137 by induct (simp_all add: inv_g_in_orb A permutation_self_in_orbit) |
|
138 qed |
|
139 } note orb_inv_ss = this |
|
140 |
|
141 have "inv (inv f) = f" |
|
142 by (simp add: assms inv_inv_eq permutation_bijective) |
|
143 then show ?thesis |
|
144 using orb_inv_ss[OF assms] orb_inv_ss[OF permutation_inverse[OF assms]] by auto |
|
145 qed |
|
146 |
|
147 lemma cyclic_on_alldef: |
|
148 "cyclic_on f S \<longleftrightarrow> S \<noteq> {} \<and> (\<forall>s\<in>S. S = orbit f s)" |
|
149 unfolding cyclic_on_def by (auto intro: orbit.step orbit_swap orbit_trans) |
|
150 |
|
151 lemma cyclic_on_funpow_in: |
|
152 assumes "cyclic_on f S" "s \<in> S" shows "(f^^n) s \<in> S" |
|
153 using assms unfolding cyclic_on_def by (auto intro: funpow_in_orbit) |
|
154 |
|
155 lemma finite_cyclic_on: |
|
156 assumes "cyclic_on f S" shows "finite S" |
|
157 using assms by (auto simp: cyclic_on_def finite_orbit) |
|
158 |
|
159 lemma cyclic_on_singleI: |
|
160 assumes "s \<in> S" "S = orbit f s" shows "cyclic_on f S" |
|
161 using assms unfolding cyclic_on_def by blast |
|
162 |
|
163 lemma cyclic_on_inI: |
|
164 assumes "cyclic_on f S" "s \<in> S" shows "f s \<in> S" |
|
165 using assms by (auto simp: cyclic_on_def intro: orbit.intros) |
|
166 |
|
167 lemma orbit_inverse: |
|
168 assumes self: "a \<in> orbit g a" |
|
169 and eq: "\<And>x. x \<in> orbit g a \<Longrightarrow> g' (f x) = f (g x)" |
|
170 shows "f ` orbit g a = orbit g' (f a)" (is "?L = ?R") |
|
171 proof (intro set_eqI iffI) |
|
172 fix x assume "x \<in> ?L" |
|
173 then obtain x0 where "x0 \<in> orbit g a" "x = f x0" by auto |
|
174 then show "x \<in> ?R" |
|
175 proof (induct arbitrary: x) |
|
176 case base then show ?case by (auto simp: self orbit.base eq[symmetric]) |
|
177 next |
|
178 case step then show ?case by cases (auto simp: eq[symmetric] orbit.intros) |
|
179 qed |
|
180 next |
|
181 fix x assume "x \<in> ?R" |
|
182 then show "x \<in> ?L" |
|
183 proof (induct arbitrary: ) |
|
184 case base then show ?case by (auto simp: self orbit.base eq) |
|
185 next |
|
186 case step then show ?case by cases (auto simp: eq orbit.intros) |
|
187 qed |
|
188 qed |
|
189 |
|
190 lemma cyclic_on_image: |
|
191 assumes "cyclic_on f S" |
|
192 assumes "\<And>x. x \<in> S \<Longrightarrow> g (h x) = h (f x)" |
|
193 shows "cyclic_on g (h ` S)" |
|
194 using assms by (auto simp: cyclic_on_def) (meson orbit_inverse) |
|
195 |
|
196 lemma cyclic_on_f_in: |
|
197 assumes "f permutes S" "cyclic_on f A" "f x \<in> A" |
|
198 shows "x \<in> A" |
|
199 proof - |
|
200 from assms have fx_in_orb: "f x \<in> orbit f (f x)" by (auto simp: cyclic_on_alldef) |
|
201 from assms have "A = orbit f (f x)" by (auto simp: cyclic_on_alldef) |
|
202 moreover |
|
203 then have "\<dots> = orbit f x" using \<open>f x \<in> A\<close> by (auto intro: orbit_step orbit_subset) |
|
204 ultimately |
|
205 show ?thesis by (metis (no_types) orbit.simps permutes_inverses(2)[OF assms(1)]) |
|
206 qed |
|
207 |
|
208 lemma orbit_cong0: |
|
209 assumes "x \<in> A" "f \<in> A \<rightarrow> A" "\<And>y. y \<in> A \<Longrightarrow> f y = g y" shows "orbit f x = orbit g x" |
|
210 proof - |
|
211 { fix n have "(f ^^ n) x = (g ^^ n) x \<and> (f ^^ n) x \<in> A" |
|
212 by (induct n rule: nat.induct) (insert assms, auto) |
|
213 } then show ?thesis by (auto simp: orbit_altdef) |
|
214 qed |
|
215 |
|
216 lemma orbit_cong: |
|
217 assumes self_in: "t \<in> orbit f t" and eq: "\<And>s. s \<in> orbit f t \<Longrightarrow> g s = f s" |
|
218 shows "orbit g t = orbit f t" |
|
219 using assms(1) _ assms(2) by (rule orbit_cong0) (auto simp: orbit.step eq) |
|
220 |
|
221 lemma cyclic_cong: |
|
222 assumes "\<And>s. s \<in> S \<Longrightarrow> f s = g s" shows "cyclic_on f S = cyclic_on g S" |
|
223 proof - |
|
224 have "(\<exists>s\<in>S. orbit f s = orbit g s) \<Longrightarrow> cyclic_on f S = cyclic_on g S" |
|
225 by (metis cyclic_on_alldef cyclic_on_def) |
|
226 then show ?thesis by (metis assms orbit_cong cyclic_on_def) |
|
227 qed |
|
228 |
|
229 lemma permutes_comp_preserves_cyclic1: |
|
230 assumes "g permutes B" "cyclic_on f C" |
|
231 assumes "A \<inter> B = {}" "C \<subseteq> A" |
|
232 shows "cyclic_on (f o g) C" |
|
233 proof - |
|
234 have *: "\<And>c. c \<in> C \<Longrightarrow> f (g c) = f c" |
|
235 using assms by (subst permutes_not_in [of g]) auto |
|
236 with assms(2) show ?thesis by (simp cong: cyclic_cong) |
|
237 qed |
|
238 |
|
239 lemma permutes_comp_preserves_cyclic2: |
|
240 assumes "f permutes A" "cyclic_on g C" |
|
241 assumes "A \<inter> B = {}" "C \<subseteq> B" |
|
242 shows "cyclic_on (f o g) C" |
|
243 proof - |
|
244 obtain c where c: "c \<in> C" "C = orbit g c" "c \<in> orbit g c" |
|
245 using \<open>cyclic_on g C\<close> by (auto simp: cyclic_on_def) |
|
246 then have "\<And>c. c \<in> C \<Longrightarrow> f (g c) = g c" |
|
247 using assms c by (subst permutes_not_in [of f]) (auto intro: orbit.intros) |
|
248 with assms(2) show ?thesis by (simp cong: cyclic_cong) |
|
249 qed |
|
250 |
|
251 lemma permutes_orbit_subset: |
|
252 assumes "f permutes S" "x \<in> S" shows "orbit f x \<subseteq> S" |
|
253 proof |
|
254 fix y assume "y \<in> orbit f x" |
|
255 then show "y \<in> S" by induct (auto simp: permutes_in_image assms) |
|
256 qed |
|
257 |
|
258 lemma cyclic_on_orbit': |
|
259 assumes "permutation f" shows "cyclic_on f (orbit f x)" |
|
260 unfolding cyclic_on_alldef using orbit_nonempty[of f x] |
|
261 by (auto intro: assms orbit_swap orbit_trans permutation_self_in_orbit) |
|
262 |
|
263 lemma cyclic_on_orbit: |
|
264 assumes "f permutes S" "finite S" shows "cyclic_on f (orbit f x)" |
|
265 using assms by (intro cyclic_on_orbit') (auto simp: permutation_permutes) |
|
266 |
|
267 lemma orbit_cyclic_eq3: |
|
268 assumes "cyclic_on f S" "y \<in> S" shows "orbit f y = S" |
|
269 using assms unfolding cyclic_on_alldef by simp |
|
270 |
|
271 lemma orbit_eq_singleton_iff: "orbit f x = {x} \<longleftrightarrow> f x = x" (is "?L \<longleftrightarrow> ?R") |
|
272 proof |
|
273 assume A: ?R |
|
274 { fix y assume "y \<in> orbit f x" then have "y = x" |
|
275 by induct (auto simp: A) |
|
276 } then show ?L by (metis orbit_nonempty singletonI subsetI subset_singletonD) |
|
277 next |
|
278 assume A: ?L |
|
279 then have "\<And>y. y \<in> orbit f x \<Longrightarrow> f x = y" |
|
280 by - (erule orbit.cases, simp_all) |
|
281 then show ?R using A by blast |
|
282 qed |
|
283 |
|
284 lemma eq_on_cyclic_on_iff1: |
|
285 assumes "cyclic_on f S" "x \<in> S" |
|
286 obtains "f x \<in> S" "f x = x \<longleftrightarrow> card S = 1" |
|
287 proof |
|
288 from assms show "f x \<in> S" by (auto simp: cyclic_on_def intro: orbit.intros) |
|
289 from assms have "S = orbit f x" by (auto simp: cyclic_on_alldef) |
|
290 then have "f x = x \<longleftrightarrow> S = {x}" by (metis orbit_eq_singleton_iff) |
|
291 then show "f x = x \<longleftrightarrow> card S = 1" using \<open>x \<in> S\<close> by (auto simp: card_Suc_eq) |
|
292 qed |
|
293 |
|
294 lemma orbit_eqI: |
|
295 "y = f x \<Longrightarrow> y \<in> orbit f x" |
|
296 "z = f y \<Longrightarrow>y \<in> orbit f x \<Longrightarrow>z \<in> orbit f x" |
|
297 by (metis orbit.base) (metis orbit.step) |
|
298 |
|
299 |
|
300 subsection \<open>Decomposition of arbitrary permutations\<close> |
|
301 |
|
302 definition perm_restrict :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'a)" where |
|
303 "perm_restrict f S x \<equiv> if x \<in> S then f x else x" |
|
304 |
|
305 lemma perm_restrict_comp: |
|
306 assumes "A \<inter> B = {}" "cyclic_on f B" |
|
307 shows "perm_restrict f A o perm_restrict f B = perm_restrict f (A \<union> B)" |
|
308 proof - |
|
309 have "\<And>x. x \<in> B \<Longrightarrow> f x \<in> B" using \<open>cyclic_on f B\<close> by (rule cyclic_on_inI) |
|
310 with assms show ?thesis by (auto simp: perm_restrict_def fun_eq_iff) |
|
311 qed |
|
312 |
|
313 lemma perm_restrict_simps: |
|
314 "x \<in> S \<Longrightarrow> perm_restrict f S x = f x" |
|
315 "x \<notin> S \<Longrightarrow> perm_restrict f S x = x" |
|
316 by (auto simp: perm_restrict_def) |
|
317 |
|
318 lemma perm_restrict_perm_restrict: |
|
319 "perm_restrict (perm_restrict f A) B = perm_restrict f (A \<inter> B)" |
|
320 by (auto simp: perm_restrict_def) |
|
321 |
|
322 lemma perm_restrict_union: |
|
323 assumes "perm_restrict f A permutes A" "perm_restrict f B permutes B" "A \<inter> B = {}" |
|
324 shows "perm_restrict f A o perm_restrict f B = perm_restrict f (A \<union> B)" |
|
325 using assms by (auto simp: fun_eq_iff perm_restrict_def permutes_def) (metis Diff_iff Diff_triv) |
|
326 |
|
327 lemma perm_restrict_id[simp]: |
|
328 assumes "f permutes S" shows "perm_restrict f S = f" |
|
329 using assms by (auto simp: permutes_def perm_restrict_def) |
|
330 |
|
331 lemma cyclic_on_perm_restrict: |
|
332 "cyclic_on (perm_restrict f S) S \<longleftrightarrow> cyclic_on f S" |
|
333 by (simp add: perm_restrict_def cong: cyclic_cong) |
|
334 |
|
335 lemma perm_restrict_diff_cyclic: |
|
336 assumes "f permutes S" "cyclic_on f A" |
|
337 shows "perm_restrict f (S - A) permutes (S - A)" |
|
338 proof - |
|
339 { fix y |
|
340 have "\<exists>x. perm_restrict f (S - A) x = y" |
|
341 proof cases |
|
342 assume A: "y \<in> S - A" |
|
343 with \<open>f permutes S\<close> obtain x where "f x = y" "x \<in> S" |
|
344 unfolding permutes_def by auto metis |
|
345 moreover |
|
346 with A have "x \<notin> A" by (metis Diff_iff assms(2) cyclic_on_inI) |
|
347 ultimately |
|
348 have "perm_restrict f (S - A) x = y" by (simp add: perm_restrict_simps) |
|
349 then show ?thesis .. |
|
350 next |
|
351 assume "y \<notin> S - A" |
|
352 then have "perm_restrict f (S - A) y = y" by (simp add: perm_restrict_simps) |
|
353 then show ?thesis .. |
|
354 qed |
|
355 } note X = this |
|
356 |
|
357 { fix x y assume "perm_restrict f (S - A) x = perm_restrict f (S - A) y" |
|
358 with assms have "x = y" |
|
359 by (auto simp: perm_restrict_def permutes_def split: if_splits intro: cyclic_on_f_in) |
|
360 } note Y = this |
|
361 |
|
362 show ?thesis by (auto simp: permutes_def perm_restrict_simps X intro: Y) |
|
363 qed |
|
364 |
|
365 lemma permutes_decompose: |
|
366 assumes "f permutes S" "finite S" |
|
367 shows "\<exists>C. (\<forall>c \<in> C. cyclic_on f c) \<and> \<Union>C = S \<and> (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {})" |
|
368 using assms(2,1) |
|
369 proof (induction arbitrary: f rule: finite_psubset_induct) |
|
370 case (psubset S) |
|
371 |
|
372 show ?case |
|
373 proof (cases "S = {}") |
|
374 case True then show ?thesis by (intro exI[where x="{}"]) auto |
|
375 next |
|
376 case False |
|
377 then obtain s where "s \<in> S" by auto |
|
378 with \<open>f permutes S\<close> have "orbit f s \<subseteq> S" |
|
379 by (rule permutes_orbit_subset) |
|
380 have cyclic_orbit: "cyclic_on f (orbit f s)" |
|
381 using \<open>f permutes S\<close> \<open>finite S\<close> by (rule cyclic_on_orbit) |
|
382 |
|
383 let ?f' = "perm_restrict f (S - orbit f s)" |
|
384 |
|
385 have "f s \<in> S" using \<open>f permutes S\<close> \<open>s \<in> S\<close> by (auto simp: permutes_in_image) |
|
386 then have "S - orbit f s \<subset> S" using orbit.base[of f s] \<open>s \<in> S\<close> by blast |
|
387 moreover |
|
388 have "?f' permutes (S - orbit f s)" |
|
389 using \<open>f permutes S\<close> cyclic_orbit by (rule perm_restrict_diff_cyclic) |
|
390 ultimately |
|
391 obtain C where C: "\<And>c. c \<in> C \<Longrightarrow> cyclic_on ?f' c" "\<Union>C = S - orbit f s" |
|
392 "\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {}" |
|
393 using psubset.IH by metis |
|
394 |
|
395 { fix c assume "c \<in> C" |
|
396 then have *: "\<And>x. x \<in> c \<Longrightarrow> perm_restrict f (S - orbit f s) x = f x" |
|
397 using C(2) \<open>f permutes S\<close> by (auto simp add: perm_restrict_def) |
|
398 then have "cyclic_on f c" using C(1)[OF \<open>c \<in> C\<close>] by (simp cong: cyclic_cong add: *) |
|
399 } note in_C_cyclic = this |
|
400 |
|
401 have Un_ins: "\<Union>(insert (orbit f s) C) = S" |
|
402 using \<open>\<Union>C = _\<close> \<open>orbit f s \<subseteq> S\<close> by blast |
|
403 |
|
404 have Disj_ins: "(\<forall>c1 \<in> insert (orbit f s) C. \<forall>c2 \<in> insert (orbit f s) C. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {})" |
|
405 using C by auto |
|
406 |
|
407 show ?thesis |
|
408 by (intro conjI Un_ins Disj_ins exI[where x="insert (orbit f s) C"]) |
|
409 (auto simp: cyclic_orbit in_C_cyclic) |
|
410 qed |
|
411 qed |
|
412 |
|
413 |
|
414 subsection \<open>Function-power distance between values\<close> |
|
415 |
|
416 definition funpow_dist :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> nat" where |
|
417 "funpow_dist f x y \<equiv> LEAST n. (f ^^ n) x = y" |
|
418 |
|
419 abbreviation funpow_dist1 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> nat" where |
|
420 "funpow_dist1 f x y \<equiv> Suc (funpow_dist f (f x) y)" |
|
421 |
|
422 lemma funpow_dist_0: |
|
423 assumes "x = y" shows "funpow_dist f x y = 0" |
|
424 using assms unfolding funpow_dist_def by (intro Least_eq_0) simp |
|
425 |
|
426 lemma funpow_dist_least: |
|
427 assumes "n < funpow_dist f x y" shows "(f ^^ n) x \<noteq> y" |
|
428 proof (rule notI) |
|
429 assume "(f ^^ n) x = y" |
|
430 then have "funpow_dist f x y \<le> n" unfolding funpow_dist_def by (rule Least_le) |
|
431 with assms show False by linarith |
|
432 qed |
|
433 |
|
434 lemma funpow_dist1_least: |
|
435 assumes "0 < n" "n < funpow_dist1 f x y" shows "(f ^^ n) x \<noteq> y" |
|
436 proof (rule notI) |
|
437 assume "(f ^^ n) x = y" |
|
438 then have "(f ^^ (n - 1)) (f x) = y" |
|
439 using \<open>0 < n\<close> by (cases n) (simp_all add: funpow_swap1) |
|
440 then have "funpow_dist f (f x) y \<le> n - 1" unfolding funpow_dist_def by (rule Least_le) |
|
441 with assms show False by simp |
|
442 qed |
|
443 |
|
444 lemma funpow_dist_prop: |
|
445 "y \<in> orbit f x \<Longrightarrow> (f ^^ funpow_dist f x y) x = y" |
|
446 unfolding funpow_dist_def by (rule LeastI_ex) (auto simp: orbit_altdef) |
|
447 |
|
448 lemma funpow_dist_0_eq: |
|
449 assumes "y \<in> orbit f x" shows "funpow_dist f x y = 0 \<longleftrightarrow> x = y" |
|
450 using assms by (auto simp: funpow_dist_0 dest: funpow_dist_prop) |
|
451 |
|
452 lemma funpow_dist_step: |
|
453 assumes "x \<noteq> y" "y \<in> orbit f x" shows "funpow_dist f x y = Suc (funpow_dist f (f x) y)" |
|
454 proof - |
|
455 from \<open>y \<in> _\<close> obtain n where "(f ^^ n) x = y" by (auto simp: orbit_altdef) |
|
456 with \<open>x \<noteq> y\<close> obtain n' where [simp]: "n = Suc n'" by (cases n) auto |
|
457 |
|
458 show ?thesis |
|
459 unfolding funpow_dist_def |
|
460 proof (rule Least_Suc2) |
|
461 show "(f ^^ n) x = y" by fact |
|
462 then show "(f ^^ n') (f x) = y" by (simp add: funpow_swap1) |
|
463 show "(f ^^ 0) x \<noteq> y" using \<open>x \<noteq> y\<close> by simp |
|
464 show "\<forall>k. ((f ^^ Suc k) x = y) = ((f ^^ k) (f x) = y)" |
|
465 by (simp add: funpow_swap1) |
|
466 qed |
|
467 qed |
|
468 |
|
469 lemma funpow_dist1_prop: |
|
470 assumes "y \<in> orbit f x" shows "(f ^^ funpow_dist1 f x y) x = y" |
|
471 by (metis assms funpow_dist_prop funpow_dist_step funpow_simps_right(2) o_apply self_in_orbit_step) |
|
472 |
|
473 (*XXX simplify? *) |
|
474 lemma funpow_neq_less_funpow_dist: |
|
475 assumes "y \<in> orbit f x" "m \<le> funpow_dist f x y" "n \<le> funpow_dist f x y" "m \<noteq> n" |
|
476 shows "(f ^^ m) x \<noteq> (f ^^ n) x" |
|
477 proof (rule notI) |
|
478 assume A: "(f ^^ m) x = (f ^^ n) x" |
|
479 |
|
480 define m' n' where "m' = min m n" and "n' = max m n" |
|
481 with A assms have A': "m' < n'" "(f ^^ m') x = (f ^^ n') x" "n' \<le> funpow_dist f x y" |
|
482 by (auto simp: min_def max_def) |
|
483 |
|
484 have "y = (f ^^ funpow_dist f x y) x" |
|
485 using \<open>y \<in> _\<close> by (simp only: funpow_dist_prop) |
|
486 also have "\<dots> = (f ^^ ((funpow_dist f x y - n') + n')) x" |
|
487 using \<open>n' \<le> _\<close> by simp |
|
488 also have "\<dots> = (f ^^ ((funpow_dist f x y - n') + m')) x" |
|
489 by (simp add: funpow_add \<open>(f ^^ m') x = _\<close>) |
|
490 also have "(f ^^ ((funpow_dist f x y - n') + m')) x \<noteq> y" |
|
491 using A' by (intro funpow_dist_least) linarith |
|
492 finally show "False" by simp |
|
493 qed |
|
494 |
|
495 (* XXX reduce to funpow_neq_less_funpow_dist? *) |
|
496 lemma funpow_neq_less_funpow_dist1: |
|
497 assumes "y \<in> orbit f x" "m < funpow_dist1 f x y" "n < funpow_dist1 f x y" "m \<noteq> n" |
|
498 shows "(f ^^ m) x \<noteq> (f ^^ n) x" |
|
499 proof (rule notI) |
|
500 assume A: "(f ^^ m) x = (f ^^ n) x" |
|
501 |
|
502 define m' n' where "m' = min m n" and "n' = max m n" |
|
503 with A assms have A': "m' < n'" "(f ^^ m') x = (f ^^ n') x" "n' < funpow_dist1 f x y" |
|
504 by (auto simp: min_def max_def) |
|
505 |
|
506 have "y = (f ^^ funpow_dist1 f x y) x" |
|
507 using \<open>y \<in> _\<close> by (simp only: funpow_dist1_prop) |
|
508 also have "\<dots> = (f ^^ ((funpow_dist1 f x y - n') + n')) x" |
|
509 using \<open>n' < _\<close> by simp |
|
510 also have "\<dots> = (f ^^ ((funpow_dist1 f x y - n') + m')) x" |
|
511 by (simp add: funpow_add \<open>(f ^^ m') x = _\<close>) |
|
512 also have "(f ^^ ((funpow_dist1 f x y - n') + m')) x \<noteq> y" |
|
513 using A' by (intro funpow_dist1_least) linarith+ |
|
514 finally show "False" by simp |
|
515 qed |
|
516 |
|
517 lemma inj_on_funpow_dist: |
|
518 assumes "y \<in> orbit f x" shows "inj_on (\<lambda>n. (f ^^ n) x) {0..funpow_dist f x y}" |
|
519 using funpow_neq_less_funpow_dist[OF assms] by (intro inj_onI) auto |
|
520 |
|
521 lemma inj_on_funpow_dist1: |
|
522 assumes "y \<in> orbit f x" shows "inj_on (\<lambda>n. (f ^^ n) x) {0..<funpow_dist1 f x y}" |
|
523 using funpow_neq_less_funpow_dist1[OF assms] by (intro inj_onI) auto |
|
524 |
|
525 lemma orbit_conv_funpow_dist1: |
|
526 assumes "x \<in> orbit f x" |
|
527 shows "orbit f x = (\<lambda>n. (f ^^ n) x) ` {0..<funpow_dist1 f x x}" (is "?L = ?R") |
|
528 using funpow_dist1_prop[OF assms] |
|
529 by (auto simp: orbit_altdef_bounded[where n="funpow_dist1 f x x"]) |
|
530 |
|
531 lemma funpow_dist1_prop1: |
|
532 assumes "(f ^^ n) x = y" "0 < n" shows "(f ^^ funpow_dist1 f x y) x = y" |
|
533 proof - |
|
534 from assms have "y \<in> orbit f x" by (auto simp: orbit_altdef) |
|
535 then show ?thesis by (rule funpow_dist1_prop) |
|
536 qed |
|
537 |
|
538 lemma funpow_dist1_dist: |
|
539 assumes "funpow_dist1 f x y < funpow_dist1 f x z" |
|
540 assumes "{y,z} \<subseteq> orbit f x" |
|
541 shows "funpow_dist1 f x z = funpow_dist1 f x y + funpow_dist1 f y z" (is "?L = ?R") |
|
542 proof - |
|
543 define n where \<open>n = funpow_dist1 f x z - funpow_dist1 f x y - 1\<close> |
|
544 with assms have *: \<open>funpow_dist1 f x z = Suc (funpow_dist1 f x y + n)\<close> |
|
545 by simp |
|
546 have x_z: "(f ^^ funpow_dist1 f x z) x = z" using assms by (blast intro: funpow_dist1_prop) |
|
547 have x_y: "(f ^^ funpow_dist1 f x y) x = y" using assms by (blast intro: funpow_dist1_prop) |
|
548 |
|
549 have "(f ^^ (funpow_dist1 f x z - funpow_dist1 f x y)) y |
|
550 = (f ^^ (funpow_dist1 f x z - funpow_dist1 f x y)) ((f ^^ funpow_dist1 f x y) x)" |
|
551 using x_y by simp |
|
552 also have "\<dots> = z" |
|
553 using assms x_z by (simp add: * funpow_add ac_simps funpow_swap1) |
|
554 finally have y_z_diff: "(f ^^ (funpow_dist1 f x z - funpow_dist1 f x y)) y = z" . |
|
555 then have "(f ^^ funpow_dist1 f y z) y = z" |
|
556 using assms by (intro funpow_dist1_prop1) auto |
|
557 then have "(f ^^ funpow_dist1 f y z) ((f ^^ funpow_dist1 f x y) x) = z" |
|
558 using x_y by simp |
|
559 then have "(f ^^ (funpow_dist1 f y z + funpow_dist1 f x y)) x = z" |
|
560 by (simp add: * funpow_add funpow_swap1) |
|
561 show ?thesis |
|
562 proof (rule antisym) |
|
563 from y_z_diff have "(f ^^ funpow_dist1 f y z) y = z" |
|
564 using assms by (intro funpow_dist1_prop1) auto |
|
565 then have "(f ^^ funpow_dist1 f y z) ((f ^^ funpow_dist1 f x y) x) = z" |
|
566 using x_y by simp |
|
567 then have "(f ^^ (funpow_dist1 f y z + funpow_dist1 f x y)) x = z" |
|
568 by (simp add: * funpow_add funpow_swap1) |
|
569 then have "funpow_dist1 f x z \<le> funpow_dist1 f y z + funpow_dist1 f x y" |
|
570 using funpow_dist1_least not_less by fastforce |
|
571 then show "?L \<le> ?R" by presburger |
|
572 next |
|
573 have "funpow_dist1 f y z \<le> funpow_dist1 f x z - funpow_dist1 f x y" |
|
574 using y_z_diff assms(1) by (metis not_less zero_less_diff funpow_dist1_least) |
|
575 then show "?R \<le> ?L" by linarith |
|
576 qed |
|
577 qed |
|
578 |
|
579 lemma funpow_dist1_le_self: |
|
580 assumes "(f ^^ m) x = x" "0 < m" "y \<in> orbit f x" |
|
581 shows "funpow_dist1 f x y \<le> m" |
|
582 proof (cases "x = y") |
|
583 case True with assms show ?thesis by (auto dest!: funpow_dist1_least) |
|
584 next |
|
585 case False |
|
586 have "(f ^^ funpow_dist1 f x y) x = (f ^^ (funpow_dist1 f x y mod m)) x" |
|
587 using assms by (simp add: funpow_mod_eq) |
|
588 with False \<open>y \<in> orbit f x\<close> have "funpow_dist1 f x y \<le> funpow_dist1 f x y mod m" |
|
589 by auto (metis \<open>(f ^^ funpow_dist1 f x y) x = (f ^^ (funpow_dist1 f x y mod m)) x\<close> funpow_dist1_prop funpow_dist_least funpow_dist_step leI) |
|
590 with \<open>m > 0\<close> show ?thesis |
|
591 by (auto intro: order_trans) |
|
592 qed |
|
593 |
|
594 end |