1(* ------------------------------------------------------------------------- *)
2(* The Iteration Period                                                      *)
3(* ------------------------------------------------------------------------- *)
4
5(*===========================================================================*)
6
7(* add all dependent libraries for script *)
8open HolKernel boolLib bossLib Parse;
9
10(* declare new theory at start *)
11val _ = new_theory "iterate";
12
13(* ------------------------------------------------------------------------- *)
14
15
16(* open dependent theories *)
17val _ = load("helperFunctionTheory");
18(* open helperTheory; -- skip helper, so no FUNPOW_closure *)
19open helperFunctionTheory;
20open helperSetTheory;
21open helperNumTheory;
22
23(* arithmeticTheory -- load by default *)
24open arithmeticTheory pred_setTheory;
25open dividesTheory; (* for divides_def *)
26
27
28(* ------------------------------------------------------------------------- *)
29(* Iteration Period Documentation                                            *)
30(* ------------------------------------------------------------------------- *)
31(*
32
33   Helper Theorems:
34
35   FUNPOW Theorems:
36   LINV_permutes       |- !f s. f PERMUTES s ==> LINV f s PERMUTES s
37   FUNPOW_permutes     |- !f s n. f PERMUTES s ==> FUNPOW f n PERMUTES s
38   FUNPOW_LINV_permutes|- !f s n. f PERMUTES s ==> FUNPOW (LINV f s) n PERMUTES s
39   FUNPOW_LINV_closure |- !f s x n. f PERMUTES s /\ x IN s ==> FUNPOW (LINV f s) n x IN s
40   FUNPOW_LINV_EQ      |- !f s x n. f PERMUTES s /\ x IN s ==>
41                                    FUNPOW f n (FUNPOW (LINV f s) n x) = x
42   FUNPOW_EQ_LINV      |- !f s x n. f PERMUTES s /\ x IN s ==>
43                                    FUNPOW (LINV f s) n (FUNPOW f n x) = x
44   FUNPOW_SUB_LINV1    |- !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==>
45                          FUNPOW f (n - m) x = FUNPOW f n (FUNPOW (LINV f s) m x)
46   FUNPOW_SUB_LINV2    |- !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==>
47                          FUNPOW f (n - m) x = FUNPOW (LINV f s) m (FUNPOW f n x)
48   FUNPOW_LINV_SUB1    |- !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==>
49                          FUNPOW (LINV f s) (n - m) x = FUNPOW (LINV f s) n (FUNPOW f m x)
50   FUNPOW_LINV_SUB2    |- !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==>
51                          FUNPOW (LINV f s) (n - m) x = FUNPOW f m (FUNPOW (LINV f s) n x)
52   FUNPOW_LINV_INV     |- !f s x y n. f PERMUTES s /\ x IN s /\ y IN s ==>
53                          (x = FUNPOW f n y <=> y = FUNPOW (LINV f s) n x)
54
55   Iteration Period:
56   iterate_period_def  |- !f x. iterate_period f x =
57                                case OLEAST k. 0 < k /\ FUNPOW f k x = x of
58                                  NONE => 0
59                                | SOME k => k
60   iterate_period_property
61                       |- !f x. FUNPOW f (iterate_period f x) x = x
62   iterate_period_minimal
63                       |- !f x n. 0 < n /\ n < iterate_period f x ==> FUNPOW f n x <> x
64   iterate_period_thm  |- !f x n. 0 < n ==>
65                          (iterate_period f x = n <=>
66                           FUNPOW f n x = x /\ !m. 0 < m /\ m < n ==> FUNPOW f m x <> x)
67   iterate_fix_0       |- !f x n. n < iterate_period f x /\ FUNPOW f n x = x ==> n = 0
68   iterate_not_distinct|- !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==>
69                            ?h k. FUNPOW f h x = FUNPOW f k x /\ h <> k
70   iterate_period_exists
71                       |- !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==>
72                              ?n. 0 < n /\ n = iterate_period f x
73   iterate_mod_period  |- !f s x n. FINITE s /\ f PERMUTES s /\ x IN s ==>
74                                    FUNPOW f n x = FUNPOW f (n MOD iterate_period f x) x
75   iterate_reduce      |- !f s x n. FINITE s /\ f PERMUTES s /\ x IN s ==>
76                                ?m. FUNPOW f n x = FUNPOW f m x /\ m < iterate_period f x
77   iterate_period_eq_0 |- !f x. iterate_period f x = 0 <=> !n. 0 < n ==> FUNPOW f n x <> x
78   iterate_period_eq_1 |- !f x. iterate_period f x = 1 <=> f x = x
79   iterate_period_eq_2 |- !f x. iterate_period f x = 2 <=> f x <> x /\ f (f x) = x
80   iterate_period_multiple
81                       |- !f x n. FUNPOW f n x = x <=> ?k. n = k * iterate_period f x
82   iterate_period_mod  |- !f x n p. 0 < p /\ p = iterate_period f x ==>
83                                    (FUNPOW f n x = x <=> n MOD p = 0)
84   iterate_period_mod_eq
85                       |- !f s p x i j. FINITE s /\ f PERMUTES s /\ x IN s /\
86                                        p = iterate_period f x ==>
87                                        (FUNPOW f i x = FUNPOW f j x <=> i MOD p = j MOD p)
88   iterate_period_funpow_inj
89                       |- !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\
90                                    p = iterate_period f x ==>
91                                    INJ (\j. FUNPOW f j x) (count p) s
92   iterate_period_upper|- !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\
93                                    p = iterate_period f x ==> p <= CARD s
94   iterate_period_inv  |- !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==>
95                                  iterate_period (LINV f s) x = iterate_period f x
96   iterate_period_inv_alt
97                       |- !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\
98                                    p = iterate_period f x ==>
99                                    iterate_period (LINV f s) x = p
100   iterate_period_iterate
101                       |- !f s x y. FINITE s /\ f PERMUTES s /\ x IN s /\
102                                    y = FUNPOW f j x ==>
103                                    iterate_period f y = iterate_period f x
104*)
105
106(* ------------------------------------------------------------------------- *)
107(* Helper Theorems                                                           *)
108(* ------------------------------------------------------------------------- *)
109
110(* ------------------------------------------------------------------------- *)
111(* FUNPOW Theorems                                                           *)
112(* ------------------------------------------------------------------------- *)
113
114(* Theorem: f PERMUTES s ==> (LINV f s) PERMUTES s *)
115(* Proof: by BIJ_LINV_BIJ *)
116Theorem LINV_permutes:
117  !f s. f PERMUTES s ==> (LINV f s) PERMUTES s
118Proof
119  rw[BIJ_LINV_BIJ]
120QED
121
122(* Theorem: f PERMUTES s ==> (FUNPOW f n) PERMUTES s *)
123(* Proof:
124   By induction on n.
125   Base: FUNPOW f 0 PERMUTES s
126      Note FUNPOW f 0 = I         by FUN_EQ_THM, FUNPOW_0
127       and I PERMUTES s           by BIJ_I_SAME
128      thus true.
129   Step: f PERMUTES s /\ FUNPOW f n PERMUTES s ==>
130         FUNPOW f (SUC n) PERMUTES s
131      Note FUNPOW f (SUC n)
132         = f o (FUNPOW f n)       by FUN_EQ_THM, FUNPOW_SUC
133      Thus true                   by BIJ_COMPOSE
134*)
135Theorem FUNPOW_permutes:
136  !f s n. f PERMUTES s ==> (FUNPOW f n) PERMUTES s
137Proof
138  rpt strip_tac >>
139  Induct_on `n` >| [
140    `FUNPOW f 0 = I` by rw[FUN_EQ_THM] >>
141    simp[BIJ_I_SAME],
142    `FUNPOW f (SUC n) = f o (FUNPOW f n)` by rw[FUN_EQ_THM, FUNPOW_SUC] >>
143    metis_tac[BIJ_COMPOSE]
144  ]
145QED
146
147(* Theorem: f PERMUTES s ==> FUNPOW (LINV f s) n PERMUTES s *)
148(* Proof: by LINV_permutes, FUNPOW_permutes *)
149Theorem FUNPOW_LINV_permutes:
150  !f s n. f PERMUTES s ==> FUNPOW (LINV f s) n PERMUTES s
151Proof
152  simp[LINV_permutes, FUNPOW_permutes]
153QED
154
155(* Theorem: f PERMUTES s /\ x IN s ==> FUNPOW f n x IN s *)
156(* Proof:
157   By induction on n.
158   Base: FUNPOW (LINV f s) 0 x IN s
159         Since FUNPOW (LINV f s) 0 x = x   by FUNPOW_0
160         This is trivially true.
161   Step: FUNPOW (LINV f s) n x IN s ==> FUNPOW (LINV f s) (SUC n) x IN s
162           FUNPOW (LINV f s) (SUC n) x
163         = (LINV f s) (FUNPOW (LINV f s) n x)   by FUNPOW_SUC
164         But FUNPOW (LINV f s) n x IN s         by induction hypothesis
165         and (LINV f s) PERMUTES s              by LINV_permutes
166          so (LINV f s) (FUNPOW (LINV f s) n x) IN s
167                                                by BIJ_ELEMENT
168*)
169Theorem FUNPOW_LINV_closure:
170  !f s x n. f PERMUTES s /\ x IN s ==> FUNPOW (LINV f s) n x IN s
171Proof
172  rpt strip_tac >>
173  Induct_on `n` >-
174  rw[] >>
175  `(LINV f s) PERMUTES s` by rw[LINV_permutes] >>
176  prove_tac[FUNPOW_SUC, BIJ_ELEMENT]
177QED
178
179(* Theorem: f PERMUTES s /\ x IN s ==> FUNPOW f n (FUNPOW (LINV f s) n x) = x *)
180(* Proof:
181   By induction on n.
182   Base: FUNPOW f 0 (FUNPOW (LINV f s) 0 x) = x
183           FUNPOW f 0 (FUNPOW (LINV f s) 0 x)
184         = FUNPOW f 0 x              by FUNPOW_0
185         = x                         by FUNPOW_0
186   Step: FUNPOW f n (FUNPOW (LINV f s) n x) = x ==>
187         FUNPOW f (SUC n) (FUNPOW (LINV f s) (SUC n) x) = x
188         Note (FUNPOW (LINV f s) n x) IN s        by FUNPOW_LINV_closure
189           FUNPOW f (SUC n) (FUNPOW (LINV f s) (SUC n) x)
190         = FUNPOW f (SUC n) ((LINV f s) (FUNPOW (LINV f s) n x))  by FUNPOW_SUC
191         = FUNPOW f n (f ((LINV f s) (FUNPOW (LINV f s) n x)))    by FUNPOW
192         = FUNPOW f n (FUNPOW (LINV f s) n x)                     by BIJ_LINV_THM
193         = x                                      by induction hypothesis
194*)
195Theorem FUNPOW_LINV_EQ:
196  !f s x n. f PERMUTES s /\ x IN s ==> FUNPOW f n (FUNPOW (LINV f s) n x) = x
197Proof
198  rpt strip_tac >>
199  Induct_on `n` >-
200  rw[] >>
201  `FUNPOW f (SUC n) (FUNPOW (LINV f s) (SUC n) x)
202    = FUNPOW f (SUC n) ((LINV f s) (FUNPOW (LINV f s) n x))` by rw[FUNPOW_SUC] >>
203  `_ = FUNPOW f n (f ((LINV f s) (FUNPOW (LINV f s) n x)))` by rw[FUNPOW] >>
204  `_ = FUNPOW f n (FUNPOW (LINV f s) n x)` by metis_tac[BIJ_LINV_THM, FUNPOW_LINV_closure] >>
205  simp[]
206QED
207
208(* Theorem: f PERMUTES s /\ x IN s ==> FUNPOW (LINV f s) n (FUNPOW f n x) = x *)
209(* Proof:
210   By induction on n.
211   Base: FUNPOW (LINV f s) 0 (FUNPOW f 0 x) = x
212           FUNPOW (LINV f s) 0 (FUNPOW f 0 x)
213         = FUNPOW (LINV f s) 0 x     by FUNPOW_0
214         = x                         by FUNPOW_0
215   Step: FUNPOW (LINV f s) n (FUNPOW f n x) = x ==>
216         FUNPOW (LINV f s) (SUC n) (FUNPOW f (SUC n) x) = x
217         Note (FUNPOW f n x) IN s        by FUNPOW_closure
218           FUNPOW (LINV f s) (SUC n) (FUNPOW f (SUC n) x)
219         = FUNPOW (LINV f s) (SUC n) (f (FUNPOW f n x))  by FUNPOW_SUC
220         = FUNPOW (LINV f s) n ((LINV f s) (f (FUNPOW f n x)))    by FUNPOW
221         = FUNPOW (LINV f s) n (FUNPOW f n x)                     by BIJ_LINV_THM
222         = x                                      by induction hypothesis
223*)
224Theorem FUNPOW_EQ_LINV:
225  !f s x n. f PERMUTES s /\ x IN s ==> FUNPOW (LINV f s) n (FUNPOW f n x) = x
226Proof
227  rpt strip_tac >>
228  Induct_on `n` >-
229  rw[] >>
230  `FUNPOW (LINV f s) (SUC n) (FUNPOW f (SUC n) x)
231    = FUNPOW (LINV f s) (SUC n) (f (FUNPOW f n x))` by rw[FUNPOW_SUC] >>
232  `_ = FUNPOW (LINV f s) n ((LINV f s) (f (FUNPOW f n x)))` by rw[FUNPOW] >>
233  `_ = FUNPOW (LINV f s) n (FUNPOW f n x)` by metis_tac[BIJ_LINV_THM, FUNPOW_closure] >>
234  simp[]
235QED
236
237(* Theorem: f PERMUTES s /\ x IN s /\ m <= n ==>
238            FUNPOW f (n - m) x = FUNPOW f n (FUNPOW (LINV f s) m x) *)
239(* Proof:
240     FUNPOW f n (FUNPOW (LINV f s) m x)
241   = FUNPOW f (n - m + m) (FUNPOW (LINV f s) m x)   by SUB_ADD, m <= n
242   = FUNPOW f (n - m) (FUNPOW f m (FUNPOW (LINV f s) m x))  by FUNPOW_ADD
243   = FUNPOW f (n - m) x                             by FUNPOW_LINV_EQ
244*)
245Theorem FUNPOW_SUB_LINV1:
246  !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==>
247              FUNPOW f (n - m) x = FUNPOW f n (FUNPOW (LINV f s) m x)
248Proof
249  rpt strip_tac >>
250  `FUNPOW f n (FUNPOW (LINV f s) m x)
251  = FUNPOW f (n - m + m) (FUNPOW (LINV f s) m x)` by simp[] >>
252  `_ = FUNPOW f (n - m) (FUNPOW f m (FUNPOW (LINV f s) m x))` by rw[FUNPOW_ADD] >>
253  `_ = FUNPOW f (n - m) x` by rw[FUNPOW_LINV_EQ] >>
254  simp[]
255QED
256
257(* Theorem: f PERMUTES s /\ x IN s /\ m <= n ==>
258            FUNPOW f (n - m) x = FUNPOW (LINV f s) m (FUNPOW f n x) *)
259(* Proof:
260   Note FUNPOW f (n - m) x IN s                      by FUNPOW_closure
261     FUNPOW (LINV f s) m (FUNPOW f n x)
262   = FUNPOW (LINV f s) m (FUNPOW f (n - m + m) x)    by SUB_ADD, m <= n
263   = FUNPOW (LINV f s) m (FUNPOW f (m + (n - m)) x)  by ADD_COMM
264   = FUNPOW (LINV f s) m (FUNPOW f m (FUNPOW f (n - m) x))  by FUNPOW_ADD
265   = FUNPOW f (n - m) x                              by FUNPOW_EQ_LINV
266*)
267Theorem FUNPOW_SUB_LINV2:
268  !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==>
269              FUNPOW f (n - m) x = FUNPOW (LINV f s) m (FUNPOW f n x)
270Proof
271  rpt strip_tac >>
272  `FUNPOW (LINV f s) m (FUNPOW f n x)
273  = FUNPOW (LINV f s) m (FUNPOW f (n - m + m) x)` by simp[] >>
274  `_ = FUNPOW (LINV f s) m (FUNPOW f (m + (n - m)) x)` by metis_tac[ADD_COMM] >>
275  `_ = FUNPOW (LINV f s) m (FUNPOW f m (FUNPOW f (n - m) x))` by rw[FUNPOW_ADD] >>
276  `_ = FUNPOW f (n - m) x` by rw[FUNPOW_EQ_LINV, FUNPOW_closure] >>
277  simp[]
278QED
279
280(* Theorem: f PERMUTES s /\ x IN s /\ m <= n ==>
281            FUNPOW (LINV f s) (n - m) x = FUNPOW (LINV f s) n (FUNPOW f m x) *)
282(* Proof:
283     FUNPOW (LINV f s) n (FUNPOW f m x)
284   = FUNPOW (LINV f s) (n - m + m) (FUNPOW f m x)    by SUB_ADD, m <= n
285   = FUNPOW (LINV f s) (n - m) (FUNPOW (LINV f s) m (FUNPOW f m x))  by FUNPOW_ADD
286   = FUNPOW (LINV f s) (n - m) x                     by FUNPOW_EQ_LINV
287*)
288Theorem FUNPOW_LINV_SUB1:
289  !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==>
290              FUNPOW (LINV f s) (n - m) x = FUNPOW (LINV f s) n (FUNPOW f m x)
291Proof
292  rpt strip_tac >>
293  `FUNPOW (LINV f s) n (FUNPOW f m x)
294  = FUNPOW (LINV f s) (n - m + m) (FUNPOW f m x)` by simp[] >>
295  `_ = FUNPOW (LINV f s) (n - m) (FUNPOW (LINV f s) m (FUNPOW f m x))` by rw[FUNPOW_ADD] >>
296  `_ = FUNPOW (LINV f s) (n - m) x` by rw[FUNPOW_EQ_LINV] >>
297  simp[]
298QED
299
300(* Theorem: f PERMUTES s /\ x IN s /\ m <= n ==>
301            FUNPOW (LINV f s) (n - m) x = FUNPOW f m (FUNPOW (LINV f s) n x) *)
302(* Proof:
303   Note FUNPOW (LINV f s) (n - m) x IN s             by FUNPOW_LINV_closure
304     FUNPOW f m (FUNPOW (LINV f s) n x)
305   = FUNPOW f m (FUNPOW (LINV f s) (n - m + m) x)    by SUB_ADD, m <= n
306   = FUNPOW f m (FUNPOW (LINV f s) (m + (n - m)) x)  by ADD_COMM
307   = FUNPOW f m (FUNPOW (LINV f s) m (FUNPOW (LINV f s) (n - m) x))  by FUNPOW_ADD
308   = FUNPOW (LINV f s) (n - m) x                     by FUNPOW_LINV_EQ
309*)
310Theorem FUNPOW_LINV_SUB2:
311  !f s x m n. f PERMUTES s /\ x IN s /\ m <= n ==>
312              FUNPOW (LINV f s) (n - m) x = FUNPOW f m (FUNPOW (LINV f s) n x)
313Proof
314  rpt strip_tac >>
315  `FUNPOW f m (FUNPOW (LINV f s) n x)
316  = FUNPOW f m (FUNPOW (LINV f s) (n - m + m) x)` by simp[] >>
317  `_ = FUNPOW f m (FUNPOW (LINV f s) (m + (n - m)) x)` by metis_tac[ADD_COMM] >>
318  `_ = FUNPOW f m (FUNPOW (LINV f s) m (FUNPOW (LINV f s) (n - m) x))` by rw[FUNPOW_ADD] >>
319  `_ = FUNPOW (LINV f s) (n - m) x` by rw[FUNPOW_LINV_EQ, FUNPOW_LINV_closure] >>
320  simp[]
321QED
322
323(* Theorem: f PERMUTES s /\ x IN s /\ y IN s ==>
324            (x = FUNPOW f n y <=> y = FUNPOW (LINV f s) n x) *)
325(* Proof:
326   If part: x = FUNPOW f n y ==> y = FUNPOW (LINV f s) n x)
327        FUNPOW (LINV f s) n x)
328      = FUNPOW (LINV f s) n (FUNPOW f n y))   by x = FUNPOW f n y
329      = y                                     by FUNPOW_EQ_LINV
330   Only-if part: y = FUNPOW (LINV f s) n x) ==> x = FUNPOW f n y
331        FUNPOW f n y
332      = FUNPOW f n (FUNPOW (LINV f s) n x))   by y = FUNPOW (LINV f s) n x)
333      = x                                     by FUNPOW_LINV_EQ
334*)
335Theorem FUNPOW_LINV_INV:
336  !f s x y n. f PERMUTES s /\ x IN s /\ y IN s ==>
337              (x = FUNPOW f n y <=> y = FUNPOW (LINV f s) n x)
338Proof
339  rw[EQ_IMP_THM] >-
340  rw[FUNPOW_EQ_LINV] >>
341  rw[FUNPOW_LINV_EQ]
342QED
343
344(* ------------------------------------------------------------------------- *)
345(* Iteration Period                                                          *)
346(* ------------------------------------------------------------------------- *)
347
348(* Define period = optional LEAST index for FUNPOW f k x to return to x. *)
349val iterate_period_def = zDefine`
350    iterate_period (f:'a -> 'a) (x:'a) =
351      case OLEAST k. 0 < k /\ FUNPOW f k x = x of
352           NONE => 0
353         | SOME k => k
354`;
355(* use zDefine here since this is not computationally effective. *)
356
357(* Theorem: FUNPOW f (iterate_period f x) x = x *)
358(* Proof:
359   If iterate_period f x k returns SOME k,
360        FUNPOW f (iterate_period f x) x
361      = FUNPOW f k x              by iterate_period_def
362      = x                         by definition condition
363   Otherwise iterate_period f x k returns NONE,
364        FUNPOW f (iterate_period f x) x
365      = FUNPOW f 0 x              by iterate_period_def
366      = x                         by FUNPOW_0
367*)
368Theorem iterate_period_property:
369  !f x. FUNPOW f (iterate_period f x) x = x
370Proof
371  rpt strip_tac >>
372  simp[iterate_period_def] >>
373  DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >>
374  simp[]
375QED
376
377(* Theorem: 0 < n /\ n < iterate_period f x ==> FUNPOW f n x <> x *)
378(* Proof: by iterate_period_def, and definition of OLEAST. *)
379Theorem iterate_period_minimal:
380  !f x n. 0 < n /\ n < iterate_period f x ==> FUNPOW f n x <> x
381Proof
382  ntac 2 strip_tac >>
383  simp[iterate_period_def] >>
384  DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >>
385  rw_tac std_ss[] >>
386  metis_tac[]
387QED
388
389(* Theorem: 0 < n ==> (iterate_period f x = n <=>
390            FUNPOW f n x = x /\ !m. 0 < m /\ m < n ==> FUNPOW f m x <> x) *)
391(* Proof:
392   If part: iterate_period f x = n ==>
393            FUNPOW f n x = x /\ !m. 0 < m /\ m < n ==> FUNPOW f m x <> x)
394      This is to show:
395      (1) FUNPOW f n x = x, true by iterate_period_property
396      (2) !m. 0 < m /\ m < n ==> FUNPOW f m x <> x, true by iterate_period_minimal
397   Only-if part: FUNPOW f n x = x /\ !m. 0 < m /\ m < n ==> FUNPOW f m x <> x) ==>
398                 iterate_period f x = n
399      Expanding by iterate_period_def, this is to show:
400      (1) 0 < n /\ !n'. ~(0 < n') \/ FUNPOW f n' x <> x ==> 0 = n
401          Putting n' = n, the assumption is contradictory.
402      (2) 0 < n /\ 0 < n' /\ !m. m < n' ==> ~(0 < m) \/ FUNPOW f m x <> x ==> n' = n
403          The assumptions implies ~(n' < n), and ~(n < n'), hence n' = n.
404*)
405Theorem iterate_period_thm:
406  !f x n. 0 < n ==>
407          (iterate_period f x = n <=>
408           FUNPOW f n x = x /\ !m. 0 < m /\ m < n ==> FUNPOW f m x <> x)
409Proof
410  rw[EQ_IMP_THM] >-
411  simp[iterate_period_property] >-
412  simp[iterate_period_minimal] >>
413  simp[iterate_period_def] >>
414  DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >>
415  rw_tac std_ss[] >-
416  metis_tac[] >>
417  `~(n' < n) /\ ~(n < n')` by metis_tac[] >>
418  decide_tac
419QED
420
421(* Theorem: n < iterate_period f x /\ FUNPOW f n x = x ==> n = 0 *)
422(* Proof: by iterate_period_minimal, ~(0 < n), so n = 0. *)
423Theorem iterate_fix_0:
424  !f x n. n < iterate_period f x /\ FUNPOW f n x = x ==> n = 0
425Proof
426  metis_tac[iterate_period_minimal, NOT_ZERO]
427QED
428
429(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==>
430            ?h k. FUNPOW f h x = FUNPOW f k x /\ (h <> k) *)
431(* Proof:
432   By contradiction, suppose !h k. FUNPOW f h x = FUNPOW f k x ==> (h = k).
433   Since s is FINITE, let c = CARD s.
434   Let fun = (\n. FUNPOW f n x), t = count (SUC c).
435   Then INJ fun t s since:
436   (1) !n. fun n x IN s                        by INJ_DEF, FUNPOW_closure, x IN s
437   (2) !h k. fun h x = fun k x ==> h = k       by assumption
438   But c < SUC c
439   and SUC c = CARD (count (SUC c)) = CARD t   by CARD_COUNT
440   This contradicts the Pigeonhole Principle   by PHP
441*)
442Theorem iterate_not_distinct:
443  !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==>
444           ?h k. FUNPOW f h x = FUNPOW f k x /\ (h <> k)
445Proof
446  spose_not_then strip_assume_tac >>
447  qabbrev_tac `c = CARD s` >>
448  `INJ (\n. FUNPOW f n x) (count (SUC c)) s` by rw[INJ_DEF, FUNPOW_closure] >>
449  `c < SUC c` by decide_tac >>
450  metis_tac[CARD_COUNT, PHP]
451QED
452
453(* Unfortunately, this is too weak in this case.
454Say the actual period is 3, so FUNPOW f 3 x = x.
455That means h k can be 1, 4, or 1, 7, or 4, 61.
456There is no guarantee that their difference is the period.
457This is because the group is (Z, +), which is INFINITE.
458Next one is stronger.
459*)
460
461(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==>
462            ?n. 0 < n /\ n = iterate_period f x *)
463(* Proof:
464   Note FINITE s /\ f PERMUTES s /\ x IN s
465    ==> ?h k. FUNPOW f h x = FUNPOW f k x /\
466              (h < k)                         by use of iterate_not_distinct
467   Let n = (k - h), then 0 < n                by h < k
468        FUNPOW f n x
469      = FUNPOW f (k - h) x                    by n = k - h, above
470      = FUNPOW (LINV f s) h (FUNPOW f k x)    by FUNPOW_SUB_LINV2, h <= k, x IN s
471      = FUNPOW (LINV f s) h (FUNPOW f h x)    by FUNPOW f h x = FUNPOW f k x
472      = x                                     by FUNPOW_EQ_LINV
473
474   Let t = {n | 0 < n /\ FUNPOW f n x = x}, m = MIN_SET t.
475   Thus n IN t, so t <> EMPTY                 by MEMBER_NOT_EMPTY
476    and m IN t                                by MIN_SET_IN_SET, t <> EMPTY
477    ==> 0 < m /\ (FUNPOW f m x = x)           by m IN t
478
479   Claim: !j. 0 < j /\ j < m ==> (FUNPOW f j x <> x)
480   Proof: By contradiction,
481          suppose ?j. 0 < j /\ j < m /\ (FUNPOW f j x = x).
482          Then j IN t, and m <= j             by MIN_SET_PROPERTY, t <> EMPTY
483          This contradicts j < m.
484
485   Thus m = iterate_period f x, and 0 < m.
486*)
487Theorem iterate_period_exists:
488  !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==>
489          ?n. 0 < n /\ n = iterate_period f x
490Proof
491  rpt strip_tac >>
492  `?h k. FUNPOW f h x = FUNPOW f k x /\ (h < k)` by
493  (`?h k. FUNPOW f h x = FUNPOW f k x /\ (h <> k)` by metis_tac[iterate_not_distinct] >>
494  Cases_on `h < k` >-
495  metis_tac[] >>
496  `k < h` by decide_tac >>
497  metis_tac[]
498  ) >>
499  `0 < k - h` by decide_tac >>
500  qabbrev_tac `n = k - h` >>
501  `FUNPOW f n x = FUNPOW f (k - h) x` by rw[Abbr`n`] >>
502  `_ = FUNPOW (LINV f s) h (FUNPOW f k x)` by rw[FUNPOW_SUB_LINV2] >>
503  `_ = FUNPOW (LINV f s) h (FUNPOW f h x)` by fs[] >>
504  `_ = x` by rw[FUNPOW_EQ_LINV] >>
505  qabbrev_tac `t = {n | 0 < n /\ FUNPOW f n x = x}` >>
506  qabbrev_tac `m = MIN_SET t` >>
507  `n IN t` by rw[Abbr`t`] >>
508  `m IN t` by metis_tac[MIN_SET_IN_SET, MEMBER_NOT_EMPTY] >>
509  `0 < m /\ (FUNPOW f m x = x)` by fs[Abbr`t`] >>
510  `!j. 0 < j /\ j < m ==> (FUNPOW f j x <> x)` by
511    (spose_not_then strip_assume_tac >>
512  `j IN t` by rw[Abbr`t`] >>
513  `m <= j` by metis_tac[MIN_SET_PROPERTY, MEMBER_NOT_EMPTY] >>
514  decide_tac) >>
515  metis_tac[iterate_period_thm]
516QED
517
518(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==> 0 < iterate_period f x *)
519(* Proof: by iterate_period_exists *)
520Theorem iterate_period_pos:
521  !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==> 0 < iterate_period f x
522Proof
523  metis_tac[iterate_period_exists]
524QED
525
526(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==>
527            FUNPOW f n x = FUNPOW f (n MOD iterate_period f x) x *)
528(* Proof:
529   Let p = iterate_period f x.
530   Then 0 < p                      by iterate_period_pos
531    and FUNPOW f p x = x           by iterate_period_property
532        FUNPOW f n x
533      = FUNPOW f (n MOD p) x       by FUNPOW_MOD, FUNPOW f p x = x
534*)
535Theorem iterate_mod_period:
536  !f s x n. FINITE s /\ f PERMUTES s /\ x IN s ==>
537            FUNPOW f n x = FUNPOW f (n MOD iterate_period f x) x
538Proof
539  rpt strip_tac >>
540  qabbrev_tac `p = iterate_period f x` >>
541  `0 < p` by metis_tac[iterate_period_pos] >>
542  `FUNPOW f p x = x` by rw[iterate_period_property, Abbr`p`] >>
543  simp[FUNPOW_MOD]
544QED
545
546(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==>
547            ?m. FUNPOW f n x = FUNPOW f m x /\ m < iterate_period f x *)
548(* Proof:
549   Let p = iterate_period f x.
550   Then 0 < p                          by iterate_period_pos
551   Let m = n MOD p, then m < p         by MOD_LESS
552    and FUNPOW f n x = FUNPOW f m x    by iterate_mod_period
553*)
554Theorem iterate_reduce:
555  !f s x n. FINITE s /\ f PERMUTES s /\ x IN s ==>
556            ?m. FUNPOW f n x = FUNPOW f m x /\ m < iterate_period f x
557Proof
558  metis_tac[iterate_period_pos, iterate_mod_period, MOD_LESS]
559QED
560
561(* Theorem: iterate_period f x = 0 <=> !n. 0 < n ==> FUNPOW f n x <> x *)
562(* Proof: by iterate_period_def *)
563Theorem iterate_period_eq_0:
564  !f x. iterate_period f x = 0 <=> !n. 0 < n ==> FUNPOW f n x <> x
565Proof
566  rw[iterate_period_def] >>
567  DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >>
568  simp[] >>
569  metis_tac[NOT_ZERO]
570QED
571
572(* Theorem: iterate_period f x = 1 <=> f x = x *)
573(* Proof:
574   Since 0 < 1,
575       iterate_period f x = 1
576   <=> (FUNPOW f 1 x = x) /\         by iterate_period_thm
577       !m. 0 < m /\ m < 1 ==> FUNPOW f m x <> x)
578   <=> f x = x /\ T                by FUNPOW_1
579   <=> f x = x                     by simplification
580*)
581Theorem iterate_period_eq_1:
582  !f x. iterate_period f x = 1 <=> f x = x
583Proof
584  rw[iterate_period_thm]
585QED
586
587(* Theorem: iterate_period f x = 2 <=> (f x <> x /\ f (f x) = x) *)
588(* Proof:
589   Since 0 < 2,
590       iterate_period f x = 2
591   <=> (FUNPOW f 2 x = x) /\       by iterate_period_thm
592       !m. 0 < m /\ m < 2 ==> FUNPOW f m x <> x)
593   <=> f (f x) = x /\ f x <> x     by FUNPOW_1, FUNPOW_2
594*)
595Theorem iterate_period_eq_2:
596  !f x. iterate_period f x = 2 <=> (f x <> x /\ f (f x) = x)
597Proof
598  rw[iterate_period_thm, FUNPOW_2, EQ_IMP_THM] >-
599  metis_tac[FUNPOW_1, DECIDE``0 < 1 /\ 1 < 2``] >>
600  `m = 1` by decide_tac >>
601  simp[]
602QED
603
604(* Theorem: FUNPOW f n x = x <=> ?k. n = k * (iterate_period f x) *)
605(* Proof:
606   Let p = iterate_period f x.
607   When p = 0,
608      If part: FUNPOW f n x = x ==> ?k. n = k * 0, that is: n = 0.
609         By contradiction, suppose n <> 0.
610         Then 0 < n, giving FUNPOW f n x <> x     by iterate_period_eq_0
611         This contradicts FUNPOW f n x = x.
612      Only-if part: n = 0 ==> FUNPOW f n x = x
613         That is FUNPOW f 0 x = x, true           by FUNPOW_0
614   When p <> 0, then 0 < p.
615      Note FUNPOW f p x = x                       by iterate_period_property
616      If part: FUNPOW f n x = x ==> ?k. n = k * p
617         Let k = n DIV p, r = n MOD p.
618         Then (n = k * p + r) /\ (r < p)          by DIVISION, 0 < p
619         so n = FUNPOW f n x                      by given
620              = FUNPOW f (r + k * p) x            by above
621              = FUNPOW f r (FUNPOW f (k * p) x)   by FUNPOW_ADD
622              = FUNPOW f r x                      by FUNPOW_MULTIPLE
623         Thus r = 0                               by iterate_period_minimal
624         so take k = n DIV p.
625      Only-if part: n = k * p ==> FUNPOW f n x = x
626         This is true                             by FUNPOW_MULTIPLE
627*)
628Theorem iterate_period_multiple:
629  !f x n. FUNPOW f n x = x <=> ?k. n = k * (iterate_period f x)
630Proof
631  rpt strip_tac >>
632  qabbrev_tac `p = iterate_period f x` >>
633  Cases_on `p = 0` >| [
634    rw[EQ_IMP_THM] >>
635    metis_tac[iterate_period_eq_0, NOT_ZERO],
636    `0 < p` by decide_tac >>
637    `FUNPOW f p x = x` by rw[iterate_period_property, Abbr`p`] >>
638    REVERSE (rw[EQ_IMP_THM]) >-
639    rw[FUNPOW_MULTIPLE] >>
640    qabbrev_tac `k = n DIV p` >>
641    qabbrev_tac `r = n MOD p` >>
642    `(n = k * p + r) /\ (r < p)` by rw[DIVISION, Abbr`k`, Abbr`r`] >>
643    `FUNPOW f n x = FUNPOW f (r + k * p) x` by fs[] >>
644    `_ = FUNPOW f r (FUNPOW f (k * p) x)` by rw[FUNPOW_ADD] >>
645    `_ = FUNPOW f r x` by rw[FUNPOW_MULTIPLE] >>
646    `~(0 < r)` by metis_tac[iterate_period_minimal] >>
647    `r = 0` by decide_tac >>
648    metis_tac[ADD_0]
649  ]
650QED
651
652(* Theorem: 0 < p /\ p = iterate_period f x ==>
653            (FUNPOW f n x = x <=> n MOD p = 0) *)
654(* Proof:
655       FUNPOW f n x = x
656   <=> ?k. n = k * p               by iterate_period_multiple
657   <=> n MOD p = 0                 by MOD_EQ_0_DIVISOR, 0 < p
658*)
659Theorem iterate_period_mod:
660  !f x n p. 0 < p /\ p = iterate_period f x ==>
661            (FUNPOW f n x = x <=> n MOD p = 0)
662Proof
663  simp[iterate_period_multiple, MOD_EQ_0_DIVISOR]
664QED
665
666(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\ p = iterate_period f x ==>
667            (FUNPOW f i x = FUNPOW f j x <=> i MOD p = j MOD p) *)
668(* Proof:
669   Note 0 < p                     by iterate_period_pos
670    and FUNPOW f i x IN s         by FUNPOW_closure
671    and FUNPOW f j x IN s         by FUNPOW_closure
672   If i = j, the equivalence is trivial. Otherwise,
673
674       FUNPOW f i x = FUNPOW f j x
675   <=> x = FUNPOW (LINV f s) i (FUNPOW f j x)
676    or FUNPOW (LINV f s) j (FUNPOW f i x) = x     by FUNPOW_LINV_INV
677   <=> x = FUNPOW f (j - i) x   if i <= j
678    or x = FUNPOW f (i - j) x   if j <= i         by FUNPOW_SUB_LINV2
679   <=> (j - i) MOD p = 0 or (i - j) MOD p = 0     by iterate_period_mod
680   <=> i MOD p = j MOD p                          by MOD_EQ, 0 < p
681*)
682Theorem iterate_period_mod_eq:
683  !f s p x i j. FINITE s /\ f PERMUTES s /\ x IN s /\
684                p = iterate_period f x ==>
685                (FUNPOW f i x = FUNPOW f j x <=> i MOD p = j MOD p)
686Proof
687  rpt strip_tac >>
688  `0 < p` by metis_tac[iterate_period_pos] >>
689  `(i = j) \/ (i < j) \/ (j < i)` by decide_tac >-
690  fs[] >-
691 (`i <= j` by decide_tac >>
692  `FUNPOW f j x IN s` by rw[FUNPOW_closure] >>
693  `FUNPOW f i x = FUNPOW f j x <=> (x = FUNPOW (LINV f s) i (FUNPOW f j x))` by metis_tac[FUNPOW_LINV_INV] >>
694  `_ = (x = FUNPOW f (j - i) x)` by fs[GSYM FUNPOW_SUB_LINV2] >>
695  `_ = ((j - i) MOD p = 0)` by metis_tac[iterate_period_mod] >>
696  fs[MOD_EQ]) >>
697  `j <= i` by decide_tac >>
698  `FUNPOW f i x IN s` by rw[FUNPOW_closure] >>
699  `FUNPOW f i x = FUNPOW f j x <=> (x = FUNPOW (LINV f s) j (FUNPOW f i x))` by metis_tac[FUNPOW_LINV_INV] >>
700  `_ = (x = FUNPOW f (i - j) x)` by fs[GSYM FUNPOW_SUB_LINV2] >>
701  `_ = ((i - j) MOD p = 0)` by metis_tac[iterate_period_mod] >>
702  fs[MOD_EQ]
703QED
704
705(* Another proof of the same theorem. *)
706(* This is 'elementary' in the sense that LINV is not used, but same concept. *)
707
708(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\ p = iterate_period f x ==>
709            (FUNPOW f i x = FUNPOW f j x <=> i MOD p = j MOD p) *)
710(* Proof:
711   Let h = i MOD p, k = j MOD p.
712   Note 0 < p                           by iterate_period_pos
713    and FUNPOW f i x = FUNPOW f h x     by iterate_mod_period
714    and FUNPOW f j x = FUNPOW f k x     by iterate_mod_period
715    and h < p, k < p                    by MOD_LESS, 0 < p
716   Thus the goal is: FUNPOW f h x = FUNPOW f k x <=> h = k.
717   The only-if part is trivial, so just do the if part.
718
719   Let d = p - h, the difference        by h < p
720   Then p = h + d = d + h               by arithmetic
721        x = FUNPOW f p x                by iterate_period_property
722          = FUNPOW f d (FUNPOW f h x)   by FUNPOW_ADD
723          = FUNPOW f d (FUNPOW f k x)   by given
724          = FUNPOW f (d + k) x          by FUNPOW_ADD
725   Thus (d + k) MOD p = 0               by iterate_period_mod
726     or p divides (d + k)               by DIVIDES_MOD_0, 0 < p
727    But d + k < p + p = 2 * p           by arithmetic
728    and 0 < d + k                       by arithmetic
729   Also p divides p                     by DIVIDES_REFL
730    ==> d + k = p                       by MULTIPLE_INTERVAL
731     so k = p - d = h                   by arithmetic
732*)
733Theorem iterate_period_mod_eq:
734  !f s p x i j. FINITE s /\ f PERMUTES s /\ x IN s /\
735                p = iterate_period f x ==>
736                (FUNPOW f i x = FUNPOW f j x <=> i MOD p = j MOD p)
737Proof
738  rpt strip_tac >>
739  `0 < p` by metis_tac[iterate_period_pos] >>
740  qabbrev_tac `h = i MOD p` >>
741  qabbrev_tac `k = j MOD p` >>
742  `FUNPOW f h x = FUNPOW f k x <=> (h = k)` suffices_by metis_tac[iterate_mod_period] >>
743  simp[EQ_IMP_THM] >>
744  strip_tac >>
745  `h < p /\ k < p` by rw[Abbr`h`, Abbr`k`] >>
746  `p = p - h + h` by decide_tac >>
747  qabbrev_tac `d = p - h` >>
748  `x = FUNPOW f p x` by metis_tac[iterate_period_property] >>
749  `_ = FUNPOW f (d + k) x` by rfs[FUNPOW_ADD] >>
750  `p divides (d + k)` by metis_tac[iterate_period_multiple, divides_def] >>
751  `d + k < p + p` by decide_tac >>
752  `p - p < d + k` by decide_tac >>
753  `p divides p` by fs[] >>
754  `d + k = p` by metis_tac[MULTIPLE_INTERVAL] >>
755  decide_tac
756QED
757
758(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\ p = iterate_period f x ==>
759            INJ (\j. FUNPOW f j x) (count p) s *)
760(* Proof:
761   By INJ_DEF, this is to show:
762   (1) j < p ==> FUNPOW f j x IN s, true    by FUNPOW_closure
763   (2) j < p /\ j' < p /\ FUNPOW f j x = FUNPOW f j' x ==> j = j'
764           FUNPOW f j x = FUNPOW f j' x
765       ==>      j MOD p = j' MOD p          by iterate_period_mod_eq
766       ==>            j = j'                by LESS_MOD, j < p, j' < p
767*)
768Theorem iterate_period_funpow_inj:
769  !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\
770            p = iterate_period f x ==>
771            INJ (\j. FUNPOW f j x) (count p) s
772Proof
773  rw[INJ_DEF] >-
774  fs[FUNPOW_closure] >>
775  metis_tac[iterate_period_mod_eq, LESS_MOD]
776QED
777
778(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\
779            p = iterate_period f x ==> p <= CARD s *)
780(* Proof:
781   Note INJ (\j. FUNPOW f j x) (count p) s    by iterate_period_funpow_inj
782    and FINITE (count p)                      by FINITE_COUNT
783    and CARD (count p) = p                    by CARD_COUNT
784    ==> p <= CARD s                           by INJ_CARD
785*)
786Theorem iterate_period_upper:
787  !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\
788            p = iterate_period f x ==> p <= CARD s
789Proof
790  metis_tac[iterate_period_funpow_inj, INJ_CARD, FINITE_COUNT, CARD_COUNT]
791QED
792
793(* Idea: period is unchanged for a permutation. *)
794
795(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s ==>
796            iterate_period (LINV f s) x = iterate_period f x *)
797(* Proof:
798   Note LINV f s PERMUTES s             by LINV_permutes
799   Let q = iterate_period (LINV f s) x
800   Then 0 < q                           by iterate_period_pos
801   By iterate_period_thm, this is to show:
802   (1) FUNPOW f q x = x.
803       Let y = FUNPOW f q x
804       Then y IN s                      by FUNPOW_closure
805         so x = FUNPOW (LINV f s) q y   by FUNPOW_LINV_INV
806              = y                       by iterate_period_property
807   (2) !m. 0 < m /\ m < q ==> FUNPOW f m x <> x
808       Let y = FUNPOW f m x.
809       Then y IN s                      by FUNPOW_closure
810         so x = FUNPOW (LINV f s) m y   by FUNPOW_LINV_INV
811        ==> FUNPOW f m x <> x           by iterate_period_minimal
812*)
813Theorem iterate_period_inv:
814  !f s x. FINITE s /\ f PERMUTES s /\ x IN s ==>
815          iterate_period (LINV f s) x = iterate_period f x
816Proof
817  rpt strip_tac >>
818  `LINV f s PERMUTES s` by rw[LINV_permutes] >>
819  qabbrev_tac `q = iterate_period (LINV f s) x` >>
820  `0 < q` by metis_tac[iterate_period_pos] >>
821  simp[iterate_period_thm] >>
822  rpt strip_tac >| [
823    qabbrev_tac `y = FUNPOW f q x` >>
824    `y IN s` by rw[FUNPOW_closure, Abbr`y`] >>
825    metis_tac[FUNPOW_LINV_INV, iterate_period_property],
826    qabbrev_tac `y = FUNPOW f m x` >>
827    `y IN s` by rw[FUNPOW_closure, Abbr`y`] >>
828    metis_tac[FUNPOW_LINV_INV, iterate_period_minimal]
829  ]
830QED
831
832(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\ p = iterate_period f x ==>
833            iterate_period (LINV f s) x = p *)
834(* Proof: by iterate_period_inv. *)
835Theorem iterate_period_inv_alt:
836  !f s p x. FINITE s /\ f PERMUTES s /\ x IN s /\ p = iterate_period f x ==>
837            iterate_period (LINV f s) x = p
838Proof
839  simp[iterate_period_inv]
840QED
841
842(* Idea: all elements in the orbit have the same period. *)
843
844(* Theorem: FINITE s /\ f PERMUTES s /\ x IN s /\ y = FUNPOW f j x ==>
845            iterate_period f y = iterate_period f x *)
846(* Proof:
847   Let p = iterate_period f x,
848       q = iterate_period f y,
849       k = j MOD p.
850   Then y = FUNPOW f k x               by iterate_mod_period
851   Note y IN s /\ FUNPOW f q x IN s    by FUNPOW_closure
852    and 0 < p /\ 0 < q                 by iterate_period_pos, y IN s
853    and k < p                          by MOD_LESS, 0 < p
854
855   Step 1: show FUNPOW f p y = y
856   Note p = k + p - k = p - k + k      by k < p
857        FUNPOW f p y
858      = FUNPOW f (k + p - k) y
859      = FUNPOW f k (FUNPOW f (p - k) y)   by FUNPOW_ADD
860      = FUNPOW f k (FUNPOW f (p - k) (FUNPOW f k x))
861      = FUNPOW f k (FUNPOW f p x)         by FUNPOW_ADD
862      = FUNPOW f k x                   by iterate_period_property
863      = y
864   Thus p MOD q = 0                    by iterate_period_mod
865     or q divides p                    by DIVIDES_MOD_0, 0 < q
866
867   Step 2: show FUNPOW f q x = x
868        FUNPOW f k x
869      = y                              by given
870      = FUNPOW f q y                   by iterate_period_property
871      = FUNPOW f q (FUNPOW f k x)
872      = FUNPOW f k (FUNPOW f q x)      by FUNPOW_COMM
873   Note (FUNPOW f k) PERMUTES s        by FUNPOW_permutes
874    ==> FUNPOW f q x = x               by BIJ_DEF, INJ_DEF
875   Thus q MOD p = 0                    by iterate_period_mod
876     or p divides q                    by DIVIDES_MOD_0, 0 < q
877
878   Thus p = q                          by DIVIDES_ANTISYM, [1][2]
879*)
880Theorem iterate_period_iterate:
881  !f s x y. FINITE s /\ f PERMUTES s /\ x IN s /\ y = FUNPOW f j x ==>
882            iterate_period f y = iterate_period f x
883Proof
884  rpt strip_tac >>
885  qabbrev_tac `p = iterate_period f x` >>
886  qabbrev_tac `q = iterate_period f y` >>
887  qabbrev_tac `k = j MOD p` >>
888  `y = FUNPOW f k x` by metis_tac[iterate_mod_period] >>
889  `y IN s` by rw[FUNPOW_closure] >>
890  `0 < p /\ 0 < q` by metis_tac[iterate_period_pos] >>
891  `k < p` by rw[Abbr`k`] >>
892  `p = p - k + k` by decide_tac >>
893  `FUNPOW f p y = FUNPOW f (k + p - k) y` by simp[] >>
894  `_ = FUNPOW f k (FUNPOW f (p - k) y)` by rw[GSYM FUNPOW_ADD] >>
895  `_ = FUNPOW f k (FUNPOW f p x)` by metis_tac[FUNPOW_ADD] >>
896  `_ = y` by fs[iterate_period_property, Abbr`p`] >>
897  `p MOD q = 0` by metis_tac[iterate_period_mod] >>
898  `q divides p` by fs[DIVIDES_MOD_0] >>
899  `FUNPOW f k x = y` by simp[] >>
900  `_ = FUNPOW f q y` by rw[iterate_period_property, Abbr`q`] >>
901  `_ = FUNPOW f q (FUNPOW f k x)` by rfs[] >>
902  `_ = FUNPOW f k (FUNPOW f q x)` by rw[FUNPOW_COMM] >>
903  `(FUNPOW f k) PERMUTES s` by rw[FUNPOW_permutes] >>
904  `FUNPOW f q x IN s` by rw[FUNPOW_closure] >>
905  `FUNPOW f q x = x` by metis_tac[BIJ_DEF, INJ_DEF] >>
906  `q MOD p = 0` by metis_tac[iterate_period_mod] >>
907  `p divides q` by fs[DIVIDES_MOD_0] >>
908  simp[DIVIDES_ANTISYM]
909QED
910
911(* ------------------------------------------------------------------------- *)
912
913(* export theory at end *)
914val _ = export_theory();
915
916(*===========================================================================*)
917