(* ========================================================================= *)
(* Iterated application of a function, ITER n f x = f^n(x).                  *)
(*                                                                           *)
(* (c) Marco Maggesi, Graziano Gentili and Gianni Ciolli, 2008.              *)
(* ========================================================================= *)

let ITER = define
  `(!f. ITER 0 f x = x) /\
   (!f n. ITER (SUC n) f x = f (ITER n f x))`;;
let ITER_POINTLESS = 
prove (`(!f. ITER 0 f = I) /\ (!f n. ITER (SUC n) f = f o ITER n f)`,
REWRITE_TAC [FUN_EQ_THM; I_THM; o_THM; ITER]);;
let ITER_ALT = 
prove (`(!f x. ITER 0 f x = x) /\ (!f n x. ITER (SUC n) f x = ITER n f (f x))`,
REWRITE_TAC [ITER] THEN GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC [ITER]);;
let ITER_ALT_POINTLESS = 
prove (`(!f. ITER 0 f = I) /\ (!f n. ITER (SUC n) f = ITER n f o f)`,
REWRITE_TAC [FUN_EQ_THM; I_THM; o_THM; ITER_ALT]);;
let ITER_1 = 
prove (`!f x. ITER 1 f x = f x`,
REWRITE_TAC[num_CONV `1`; ITER]);;
let ITER_ADD = 
prove (`!f n m x. ITER n f (ITER m f x) = ITER (n + m) f x`,
GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER; ADD]);;
let ITER_MUL = 
prove (`!f n m x. ITER n (ITER m f) x = ITER (n * m) f x`,
GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER; MULT; ITER_ADD; ADD_AC]);;
let ITER_FIXPOINT = 
prove (`!f n x. f x = x ==> ITER n f x = x`,
GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC [ITER_ALT]);;
(* ------------------------------------------------------------------------- *) (* Existence of "order" or "characteristic" in a general setting. *) (* ------------------------------------------------------------------------- *)
let ORDER_EXISTENCE_GEN = 
prove (`!P f:num->A. P(f 0) /\ (!m n. P(f m) /\ ~(m = 0) ==> (P(f(m + n)) <=> P(f n))) ==> ?d. !n. P(f n) <=> d divides n`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `!n. ~(n = 0) ==> ~P(f n:A)` THENL [EXISTS_TAC `0` THEN REWRITE_TAC[NUMBER_RULE `0 divides n <=> n = 0`] THEN ASM_MESON_TAC[]; FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_FORALL_THM])] THEN GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:num` THEN REWRITE_TAC[NOT_IMP] THEN REWRITE_TAC[GSYM IMP_CONJ_ALT] THEN STRIP_TAC THEN MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN ASM_CASES_TAC `n = 0` THENL [ASM_MESON_TAC[NUMBER_RULE `n divides 0`]; ALL_TAC] THEN ASM_CASES_TAC `d <= n:num` THENL [ALL_TAC; ASM_MESON_TAC[NOT_LT; DIVIDES_LE]] THEN SUBGOAL_THEN `n:num = (n - d) + d` SUBST1_TAC THENL [ASM_ARITH_TAC; ABBREV_TAC `m:num = n - d`] THEN REWRITE_TAC[NUMBER_RULE `d divides m + d <=> d divides m`] THEN FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN ANTS_TAC THENL [ASM_ARITH_TAC; ASM_MESON_TAC[ADD_SYM]]);;
let ORDER_EXISTENCE_ITER = 
prove (`!R f z:A. R z z /\ (!x y. R x y ==> R y x) /\ (!x y z. R x y /\ R y z ==> R x z) /\ (!x y. R x y ==> R (f x) (f y)) ==> ?d. !n. R (ITER n f z) z <=> d divides n`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`\x. (R:A->A->bool) x z`; `\n. ITER n f (z:A)`] ORDER_EXISTENCE_GEN) THEN ASM_REWRITE_TAC[ITER] THEN DISCH_THEN MATCH_MP_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN X_GEN_TAC `m:num` THEN STRIP_TAC THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM ITER_ADD] THEN MP_TAC(MESON[] `!a b:num->A. (!x y. R x y ==> R y x) /\ (!x y z. R x y /\ R y z ==> R x z) /\ (!n. R (a n) (b n)) ==> (!n. R (a n) z <=> R (b n) z)`) THEN DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER] THEN ASM_MESON_TAC[]);;
let ORDER_EXISTENCE_CARD = 
prove (`!R f z:A k. FINITE { R(ITER n f z) | n IN (:num)} /\ CARD { R(ITER n f z) | n IN (:num)} <= k /\ R z z /\ (!x y. R x y ==> R y x) /\ (!x y z. R x y /\ R y z ==> R x z) /\ (!x y. R (f x) (f y) <=> R x y) ==> ?d. 0 < d /\ d <= k /\ !n. R (ITER n f z) z <=> d divides n`,
REPEAT STRIP_TAC THEN SUBGOAL_THEN `?m. 0 < m /\ m <= k /\ (R:A->A->bool) (ITER m f z) z` STRIP_ASSUME_TAC THENL [MP_TAC(ISPECL [`\n. (R:A->A->bool) (ITER n f z)`; `0..k`] CARD_IMAGE_EQ_INJ) THEN REWRITE_TAC[FINITE_NUMSEG; CARD_NUMSEG; SUB_0] THEN MATCH_MP_TAC(TAUT `~p /\ (~q ==> r) ==> (p <=> q) ==> r`) THEN CONJ_TAC THENL [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE `c <= k ==> s <= c ==> ~(s = k + 1)`)) THEN MATCH_MP_TAC CARD_SUBSET THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[]; REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; LEFT_IMP_EXISTS_THM] THEN MATCH_MP_TAC WLOG_LT THEN REWRITE_TAC[] THEN CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN MAP_EVERY X_GEN_TAC [`p:num`; `q:num`] THEN REWRITE_TAC[IN_NUMSEG] THEN REPEAT STRIP_TAC THEN EXISTS_TAC `q - p:num` THEN REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN SUBGOAL_THEN `!d. d <= p ==> (R:A->A->bool) (ITER (p - d) f z) (ITER (q - d) f z)` MP_TAC THENL [INDUCT_TAC THEN ASM_REWRITE_TAC[SUB_0] THENL [SPEC_TAC(`q:num`,`q:num`) THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER]; DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `q - d = SUC(q - SUC d) /\ p - d = SUC(p - SUC d)` (fun th -> REWRITE_TAC[th]) THENL [ASM_ARITH_TAC; ALL_TAC] THEN ASM_REWRITE_TAC[ITER]]; DISCH_THEN(MP_TAC o SPEC `p:num`) THEN REWRITE_TAC[LE_REFL; SUB_REFL; ITER] THEN ASM_MESON_TAC[]]]; MP_TAC(ISPECL [`R:A->A->bool`; `f:A->A`; `z:A`] ORDER_EXISTENCE_ITER) THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:num` THEN ASM_CASES_TAC `d = 0` THEN ASM_SIMP_TAC[] THEN DISCH_THEN(MP_TAC o SPEC `m:num`) THEN ASM_SIMP_TAC[LE_1; NUMBER_RULE `!n. 0 divides n <=> n = 0`] THEN DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN ASM_ARITH_TAC]);;
let ORDER_EXISTENCE_FINITE = 
prove (`!R f z:A. FINITE { R(ITER n f z) | n IN (:num)} /\ R z z /\ (!x y. R x y ==> R y x) /\ (!x y z. R x y /\ R y z ==> R x z) /\ (!x y. R (f x) (f y) <=> R x y) ==> ?d. 0 < d /\ !n. R (ITER n f z) z <=> d divides n`,
REPEAT STRIP_TAC THEN MP_TAC(ISPECL [`R:A->A->bool`; `f:A->A`; `z:A`; `CARD {(R:A->A->bool)(ITER n f z) | n IN (:num)}`] ORDER_EXISTENCE_CARD) THEN ASM_REWRITE_TAC[LE_REFL] THEN MESON_TAC[]);;