Library/iter.ml

   1 (* ========================================================================= *)
   2 (* Iterated application of a function, ITER n f x = f^n(x).                  *)
   3 (*                                                                           *)
   4 (* (c) Marco Maggesi, Graziano Gentili and Gianni Ciolli, 2008.              *)
   5 (* ========================================================================= *)
   6
   7 let ITER = define
   8   `(!f. ITER 0 f x = x) /\
   9    (!f n. ITER (SUC n) f x = f (ITER n f x))`;;
  10
  11 let ITER_POINTLESS = prove
  12   (`(!f. ITER 0 f = I) /\
  13     (!f n. ITER (SUC n) f = f o ITER n f)`,
  14    REWRITE_TAC [FUN_EQ_THM; I_THM; o_THM; ITER]);;
  15
  16 let ITER_ALT = prove
  17   (`(!f x. ITER 0 f x = x) /\
  18     (!f n x. ITER (SUC n) f x = ITER n f (f x))`,
  19    REWRITE_TAC [ITER] THEN GEN_TAC THEN INDUCT_TAC THEN
  20    ASM_REWRITE_TAC [ITER]);;
  21
  22 let ITER_ALT_POINTLESS = prove
  23   (`(!f. ITER 0 f = I) /\
  24     (!f n. ITER (SUC n) f = ITER n f o f)`,
  25    REWRITE_TAC [FUN_EQ_THM; I_THM; o_THM; ITER_ALT]);;
  26
  27 let ITER_1 = prove
  28  (`!f x. ITER 1 f x = f x`,
  29   REWRITE_TAC[num_CONV `1`; ITER]);;
  30
  31 let ITER_ADD = prove
  32   (`!f n m x. ITER n f (ITER m f x) = ITER (n + m) f x`,
  33    GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ITER; ADD]);;
  34
  35 let ITER_MUL = prove
  36   (`!f n m x. ITER n (ITER m f) x = ITER (n * m) f x`,
  37    GEN_TAC THEN INDUCT_TAC THEN
  38    ASM_REWRITE_TAC[ITER; MULT; ITER_ADD; ADD_AC]);;
  39
  40 let ITER_FIXPOINT = prove
  41   (`!f n x. f x = x ==> ITER n f x = x`,
  42    GEN_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC [ITER_ALT]);;
  43
  44 (* ------------------------------------------------------------------------- *)
  45 (* Existence of "order" or "characteristic" in a general setting.            *)
  46 (* ------------------------------------------------------------------------- *)
  47
  48 let ORDER_EXISTENCE_GEN = prove
  49  (`!P f:num->A.
  50          P(f 0) /\ (!m n. P(f m) /\ ~(m = 0) ==> (P(f(m + n)) <=> P(f n)))
  51          ==> ?d. !n. P(f n) <=> d divides n`,
  52   REPEAT STRIP_TAC THEN
  53   ASM_CASES_TAC `!n. ~(n = 0) ==> ~P(f n:A)` THENL
  54    [EXISTS_TAC `0` THEN REWRITE_TAC[NUMBER_RULE `0 divides n <=> n = 0`] THEN
  55     ASM_MESON_TAC[];
  56     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_FORALL_THM])] THEN
  57   GEN_REWRITE_TAC LAND_CONV [num_WOP] THEN MATCH_MP_TAC MONO_EXISTS THEN
  58   X_GEN_TAC `d:num` THEN REWRITE_TAC[NOT_IMP] THEN
  59   REWRITE_TAC[GSYM IMP_CONJ_ALT] THEN STRIP_TAC THEN
  60   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
  61   ASM_CASES_TAC `n = 0` THENL
  62    [ASM_MESON_TAC[NUMBER_RULE `n divides 0`]; ALL_TAC] THEN
  63   ASM_CASES_TAC `d <= n:num` THENL
  64    [ALL_TAC; ASM_MESON_TAC[NOT_LT; DIVIDES_LE]] THEN
  65   SUBGOAL_THEN `n:num = (n - d) + d` SUBST1_TAC THENL
  66    [ASM_ARITH_TAC; ABBREV_TAC `m:num = n - d`] THEN
  67   REWRITE_TAC[NUMBER_RULE `d divides m + d <=> d divides m`] THEN
  68   FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
  69   ANTS_TAC THENL [ASM_ARITH_TAC; ASM_MESON_TAC[ADD_SYM]]);;
  70
  71 let ORDER_EXISTENCE_ITER = prove
  72  (`!R f z:A.
  73         R z z /\
  74         (!x y. R x y ==> R y x) /\
  75         (!x y z. R x y /\ R y z ==> R x z) /\
  76         (!x y. R x y ==> R (f x) (f y))
  77         ==> ?d. !n. R (ITER n f z) z <=> d divides n`,
  78   REPEAT STRIP_TAC THEN
  79   MP_TAC(ISPECL [`\x. (R:A->A->bool) x z`;
  80                  `\n. ITER n f (z:A)`] ORDER_EXISTENCE_GEN) THEN
  81   ASM_REWRITE_TAC[ITER] THEN DISCH_THEN MATCH_MP_TAC THEN
  82   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN X_GEN_TAC `m:num` THEN STRIP_TAC THEN
  83   ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM ITER_ADD] THEN
  84   MP_TAC(MESON[]
  85    `!a b:num->A. (!x y. R x y ==> R y x) /\
  86           (!x y z. R x y /\ R y z ==> R x z) /\
  87           (!n. R (a n) (b n))
  88           ==> (!n. R (a n) z <=> R (b n) z)`) THEN
  89   DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
  90   INDUCT_TAC THEN ASM_REWRITE_TAC[ITER] THEN
  91   ASM_MESON_TAC[]);;
  92
  93 let ORDER_EXISTENCE_CARD = prove
  94  (`!R f z:A k.
  95      FINITE { R(ITER n f z) | n IN (:num)} /\
  96      CARD { R(ITER n f z) | n IN (:num)} <= k /\
  97      R z z /\
  98      (!x y. R x y ==> R y x) /\
  99      (!x y z. R x y /\ R y z ==> R x z) /\
 100      (!x y. R (f x) (f y) <=> R x y)
 101      ==> ?d. 0 < d /\ d <= k /\ !n. R (ITER n f z) z <=> d divides n`,
 102   REPEAT STRIP_TAC THEN
 103   SUBGOAL_THEN
 104    `?m. 0 < m /\ m <= k /\ (R:A->A->bool) (ITER m f z) z`
 105   STRIP_ASSUME_TAC THENL
 106     [MP_TAC(ISPECL [`\n. (R:A->A->bool) (ITER n f z)`; `0..k`]
 107       CARD_IMAGE_EQ_INJ) THEN
 108      REWRITE_TAC[FINITE_NUMSEG; CARD_NUMSEG; SUB_0] THEN
 109      MATCH_MP_TAC(TAUT `~p /\ (~q ==> r) ==> (p <=> q) ==> r`) THEN
 110      CONJ_TAC THENL
 111       [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (ARITH_RULE
 112         `c <= k ==> s <= c ==> ~(s = k + 1)`)) THEN
 113        MATCH_MP_TAC CARD_SUBSET THEN ASM_REWRITE_TAC[] THEN ASM SET_TAC[];
 114        REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; LEFT_IMP_EXISTS_THM] THEN
 115        MATCH_MP_TAC WLOG_LT THEN REWRITE_TAC[] THEN
 116        CONJ_TAC THENL [MESON_TAC[]; ALL_TAC] THEN
 117        MAP_EVERY X_GEN_TAC [`p:num`; `q:num`] THEN
 118        REWRITE_TAC[IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
 119        EXISTS_TAC `q - p:num` THEN
 120        REPEAT(CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC]) THEN
 121        SUBGOAL_THEN
 122         `!d. d <= p
 123              ==> (R:A->A->bool) (ITER (p - d) f z) (ITER (q - d) f z)`
 124        MP_TAC THENL
 125         [INDUCT_TAC THEN ASM_REWRITE_TAC[SUB_0] THENL
 126           [SPEC_TAC(`q:num`,`q:num`) THEN INDUCT_TAC THEN
 127            ASM_REWRITE_TAC[ITER];
 128            DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN
 129            ANTS_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 130            SUBGOAL_THEN `q - d = SUC(q - SUC d) /\ p - d = SUC(p - SUC d)`
 131             (fun th -> REWRITE_TAC[th]) THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 132            ASM_REWRITE_TAC[ITER]];
 133          DISCH_THEN(MP_TAC o SPEC `p:num`) THEN
 134          REWRITE_TAC[LE_REFL; SUB_REFL; ITER] THEN ASM_MESON_TAC[]]];
 135      MP_TAC(ISPECL [`R:A->A->bool`; `f:A->A`; `z:A`] ORDER_EXISTENCE_ITER) THEN
 136      ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN
 137      X_GEN_TAC `d:num` THEN ASM_CASES_TAC `d = 0` THEN ASM_SIMP_TAC[] THEN
 138      DISCH_THEN(MP_TAC o SPEC `m:num`) THEN
 139      ASM_SIMP_TAC[LE_1; NUMBER_RULE `!n. 0 divides n <=> n = 0`] THEN
 140      DISCH_THEN(MP_TAC o MATCH_MP DIVIDES_LE) THEN ASM_ARITH_TAC]);;
 141
 142 let ORDER_EXISTENCE_FINITE = prove
 143  (`!R f z:A.
 144      FINITE { R(ITER n f z) | n IN (:num)} /\
 145      R z z /\
 146      (!x y. R x y ==> R y x) /\
 147      (!x y z. R x y /\ R y z ==> R x z) /\
 148      (!x y. R (f x) (f y) <=> R x y)
 149      ==> ?d. 0 < d /\ !n. R (ITER n f z) z <=> d divides n`,
 150   REPEAT STRIP_TAC THEN
 151   MP_TAC(ISPECL [`R:A->A->bool`; `f:A->A`; `z:A`;
 152    `CARD {(R:A->A->bool)(ITER n f z) | n IN (:num)}`]
 153    ORDER_EXISTENCE_CARD) THEN ASM_REWRITE_TAC[LE_REFL] THEN MESON_TAC[]);;