1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
(* ========================================================================= *)
(* 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]);;
|
