(* ========================================================================= *)
(* 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]);;