Arithmetic/definability.ml

   1 (* ========================================================================= *)
   2 (* Definability in arithmetic of important notions.                          *)
   3 (* ========================================================================= *)
   4
   5 prioritize_num();;
   6
   7 (* ------------------------------------------------------------------------- *)
   8 (* Pairing operation.                                                        *)
   9 (* ------------------------------------------------------------------------- *)
  10
  11 let NPAIR = new_definition
  12   `NPAIR x y = (x + y) EXP 2 + x + 1`;;
  13
  14 let NPAIR_NONZERO = prove
  15  (`!x y. ~(NPAIR x y = 0)`,
  16   REWRITE_TAC[NPAIR; ADD_EQ_0; ARITH]);;
  17
  18 let NPAIR_INJ_LEMMA = prove
  19  (`x1 + y1 < x2 + y2 ==> NPAIR x1 y1 < NPAIR x2 y2`,
  20   STRIP_TAC THEN REWRITE_TAC[NPAIR; EXP_2] THEN
  21   REWRITE_TAC[ARITH_RULE `x + y + 1 < u + v + 1 <=> x + y < u + v`] THEN
  22   MATCH_MP_TAC LTE_TRANS THEN
  23   EXISTS_TAC `SUC(x1 + y1) * SUC(x1 + y1)` THEN CONJ_TAC THENL
  24    [ARITH_TAC; ASM_MESON_TAC[LE_TRANS; LE_ADD; LE_MULT2; LE_SUC_LT]]);;
  25
  26 let NPAIR_INJ = prove
  27  (`(NPAIR x y = NPAIR x' y') <=> (x = x') /\ (y = y')`,
  28   EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  29   SUBGOAL_THEN `x' + y' = x + y` ASSUME_TAC THENL
  30    [ASM_MESON_TAC[LT_CASES; NPAIR_INJ_LEMMA; LT_REFL];
  31     UNDISCH_TAC `NPAIR x y = NPAIR x' y'` THEN
  32     UNDISCH_TAC `x' + y' = x + y` THEN
  33     SIMP_TAC[NPAIR; EXP_2] THEN ARITH_TAC]);;
  34
  35 (* ------------------------------------------------------------------------- *)
  36 (* Decreasingness.                                                           *)
  37 (* ------------------------------------------------------------------------- *)
  38
  39 let NPAIR_LT = prove
  40  (`!x y. x < NPAIR x y /\ y < NPAIR x y`,
  41   REPEAT GEN_TAC THEN REWRITE_TAC[NPAIR] THEN
  42   REWRITE_TAC[ARITH_RULE `x < a + x + 1`] THEN
  43   MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `(x + y) + x + 1` THEN
  44   REWRITE_TAC[LE_ADD_RCANCEL; EXP_2; LE_SQUARE_REFL] THEN
  45   ARITH_TAC);;
  46
  47 (* ------------------------------------------------------------------------- *)
  48 (* Auxiliary concepts needed. NB: these are Delta so can be negated freely.  *)
  49 (* ------------------------------------------------------------------------- *)
  50
  51 let primepow = new_definition
  52   `primepow p x <=> prime(p) /\ ?n. x = p EXP n`;;
  53
  54 let divides_DELTA = prove
  55  (`m divides n <=> ?x. x <= n /\ n = m * x`,
  56   REWRITE_TAC[divides] THEN ASM_CASES_TAC `m = 0` THENL
  57    [ASM_REWRITE_TAC[MULT_CLAUSES] THEN MESON_TAC[LE_REFL]; ALL_TAC] THEN
  58   AP_TERM_TAC THEN ABS_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
  59   FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `~(m = 0) ==> 1 <= m`)) THEN
  60   SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM;
  61            RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
  62   MESON_TAC[]);;
  63
  64 let prime_DELTA = prove
  65  (`prime(p) <=> 2 <= p /\ !n. n < p ==> n divides p ==> n = 1`,
  66   ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[ARITH; PRIME_0] THEN
  67   ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[ARITH; PRIME_1] THEN EQ_TAC THENL
  68    [ASM_MESON_TAC[prime; LT_REFL; PRIME_GE_2];
  69     ASM_MESON_TAC[prime;  DIVIDES_LE; LE_LT]]);;
  70
  71 let primepow_DELTA = prove
  72  (`primepow p x <=>
  73         prime(p) /\ ~(x = 0) /\
  74         !z. z <= x ==> z divides x ==> z = 1 \/ p divides z`,
  75   REWRITE_TAC[primepow; TAUT `a ==> b \/ c <=> a /\ ~b ==> c`] THEN
  76   ASM_CASES_TAC `prime(p)` THEN
  77   ASM_REWRITE_TAC[] THEN EQ_TAC THENL
  78    [DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN
  79     ASM_REWRITE_TAC[EXP_EQ_0] THEN
  80     ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[] THENL
  81      [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
  82     REPEAT STRIP_TAC THEN
  83     FIRST_ASSUM(MP_TAC o SPEC `z:num` o MATCH_MP PRIME_COPRIME) THEN
  84     ASM_REWRITE_TAC[] THEN
  85     ASM_CASES_TAC `p divides z` THEN ASM_REWRITE_TAC[] THEN
  86     ONCE_REWRITE_TAC[COPRIME_SYM] THEN
  87     DISCH_THEN(MP_TAC o SPEC `n:num` o MATCH_MP COPRIME_EXP) THEN
  88     ASM_MESON_TAC[COPRIME; DIVIDES_REFL];
  89     SPEC_TAC(`x:num`,`x:num`) THEN MATCH_MP_TAC num_WF THEN
  90     REPEAT STRIP_TAC THEN ASM_CASES_TAC `x = 1` THENL
  91      [EXISTS_TAC `0` THEN ASM_REWRITE_TAC[EXP]; ALL_TAC] THEN
  92     FIRST_ASSUM(X_CHOOSE_THEN `q:num` MP_TAC o MATCH_MP PRIME_FACTOR) THEN
  93     STRIP_TAC THEN
  94     UNDISCH_TAC `!z. z <= x ==> z divides x /\ ~(z = 1) ==> p divides z` THEN
  95     DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
  96     DISCH_THEN(MP_TAC o SPEC `q:num`) THEN ASM_REWRITE_TAC[] THEN
  97     ASM_CASES_TAC `q = 1` THENL [ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN
  98     ASM_REWRITE_TAC[] THEN
  99     SUBGOAL_THEN `q <= x` ASSUME_TAC THENL
 100      [ASM_MESON_TAC[DIVIDES_LE]; ASM_REWRITE_TAC[]] THEN
 101     SUBGOAL_THEN `p divides x` MP_TAC THENL
 102      [ASM_MESON_TAC[DIVIDES_TRANS]; ALL_TAC] THEN
 103     REWRITE_TAC[divides] THEN DISCH_THEN(X_CHOOSE_TAC `y:num`) THEN
 104     SUBGOAL_THEN `y < x` (ANTE_RES_THEN MP_TAC) THENL
 105      [MATCH_MP_TAC PRIME_FACTOR_LT THEN
 106       EXISTS_TAC `p:num` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
 107     ASM_CASES_TAC `y = 0` THENL
 108      [UNDISCH_TAC `x = p * y` THEN ASM_REWRITE_TAC[MULT_CLAUSES]; ALL_TAC] THEN
 109     ASM_REWRITE_TAC[] THEN
 110     SUBGOAL_THEN `!z. z <= y ==> z divides y /\ ~(z = 1) ==> p divides z`
 111     (fun th -> REWRITE_TAC[th]) THENL
 112      [REPEAT STRIP_TAC THEN
 113       FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE
 114         [IMP_IMP]) THEN
 115       REPEAT CONJ_TAC THENL
 116        [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `y:num` THEN
 117         ASM_REWRITE_TAC[] THEN
 118         GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `y = 1 * y`] THEN
 119         REWRITE_TAC[LE_MULT_RCANCEL] THEN
 120         ASM_REWRITE_TAC[GSYM NOT_LT] THEN
 121         REWRITE_TAC[num_CONV `1`; LT; DE_MORGAN_THM] THEN
 122         ASM_MESON_TAC[PRIME_0; PRIME_1];
 123         ASM_REWRITE_TAC[] THEN MATCH_MP_TAC DIVIDES_LMUL THEN
 124         ASM_REWRITE_TAC[];
 125         ASM_REWRITE_TAC[]];
 126       DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN
 127       EXISTS_TAC `SUC n` THEN ASM_REWRITE_TAC[EXP]]]);;
 128
 129 (* ------------------------------------------------------------------------- *)
 130 (* Sigma-representability of reflexive transitive closure.                   *)
 131 (* ------------------------------------------------------------------------- *)
 132
 133 let PSEQ = new_recursive_definition num_RECURSION
 134   `(PSEQ p f m 0 = 0) /\
 135    (PSEQ p f m (SUC n) = f m + p * PSEQ p f (SUC m) n)`;;
 136
 137 let PSEQ_SPLIT = prove
 138  (`!f p n m r.
 139         PSEQ p f m (n + r) = PSEQ p f m n + p EXP n * PSEQ p f (m + n) r`,
 140   GEN_TAC THEN GEN_TAC THEN
 141   INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; EXP; MULT_CLAUSES; PSEQ] THEN
 142   ASM_REWRITE_TAC[GSYM ADD_ASSOC; EQ_ADD_LCANCEL] THEN
 143   REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_AC; ADD_CLAUSES]);;
 144
 145 let PSEQ_1 = prove
 146  (`PSEQ p f m 1 = f m`,
 147   REWRITE_TAC[num_CONV `1`; ADD_CLAUSES; MULT_CLAUSES; PSEQ]);;
 148
 149 let PSEQ_BOUND = prove
 150  (`!n. ~(p = 0) /\ (!i. i < n ==> f i < p) ==> PSEQ p f 0 n < p EXP n`,
 151   ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[] THEN
 152   INDUCT_TAC THENL [REWRITE_TAC[PSEQ; EXP; ARITH]; ALL_TAC] THEN
 153   DISCH_TAC THEN
 154   MP_TAC(SPECL [`f:num->num`; `p:num`; `n:num`; `0`; `1`]
 155                PSEQ_SPLIT) THEN
 156   SIMP_TAC[ADD1; ADD_CLAUSES] THEN REPEAT STRIP_TAC THEN
 157   MATCH_MP_TAC LTE_TRANS THEN
 158   EXISTS_TAC `p EXP n + p EXP n * PSEQ p f n 1` THEN
 159   ASM_SIMP_TAC[LT_ADD_RCANCEL; ARITH_RULE `i < n ==> i < SUC n`] THEN
 160   REWRITE_TAC[ARITH_RULE `p + p * q = p * (q + 1)`] THEN
 161   ASM_REWRITE_TAC[EXP_ADD; LE_MULT_LCANCEL; EXP_EQ_0] THEN
 162   MATCH_MP_TAC(ARITH_RULE `x < p ==> x + 1 <= p`) THEN
 163   ASM_SIMP_TAC[EXP_1; PSEQ_1; LT]);;
 164
 165 let RELPOW_LEMMA_1 = prove
 166  (`(f 0 = x) /\
 167    (f n = y) /\
 168    (!i. i < n ==> R (f i) (f(SUC i)))
 169    ==> ?p. (?i. i <= n /\ p <= SUC(FACT(f i))) /\
 170            prime p /\
 171            (?m. m < p EXP (SUC n) /\
 172                 x < p /\ y < p /\
 173                 (?qx. m = x + p * qx) /\
 174                 (?ry. ry < p EXP n /\ (m = ry + p EXP n * y)) /\
 175                 !q. q < p EXP n
 176                     ==> primepow p q
 177                         ==> ?r. r < q /\
 178                                 ?a. a < p /\
 179                                     ?b. b < p /\
 180                                         R a b /\
 181                                         ?s. s <= m /\
 182                                             (m =
 183                                              r + q * (a + p * (b + p * s))))`,
 184   REPEAT STRIP_TAC THEN
 185   SUBGOAL_THEN `?j. j <= n /\ !i. i <= n ==> f i <= f j` MP_TAC THENL
 186    [SPEC_TAC(`n:num`,`n:num`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
 187     INDUCT_TAC THENL
 188      [SIMP_TAC[LE] THEN MESON_TAC[LE_REFL]; ALL_TAC] THEN
 189     FIRST_ASSUM(X_CHOOSE_THEN `j:num` STRIP_ASSUME_TAC) THEN
 190     DISJ_CASES_TAC(ARITH_RULE `f(SUC n) <= f(j) \/ f(j) <= f(SUC n)`) THENL
 191      [EXISTS_TAC `j:num` THEN
 192       ASM_SIMP_TAC[ARITH_RULE `j <= n ==> j <= SUC n`] THEN
 193       REWRITE_TAC[LE] THEN REPEAT STRIP_TAC THEN
 194       ASM_SIMP_TAC[] THEN ASM_MESON_TAC[];
 195       EXISTS_TAC `SUC n` THEN REWRITE_TAC[LE_REFL] THEN
 196       REWRITE_TAC[LE] THEN REPEAT STRIP_TAC THEN
 197       ASM_SIMP_TAC[LE_REFL] THEN ASM_MESON_TAC[LE_TRANS]];
 198     ALL_TAC] THEN
 199   DISCH_THEN(X_CHOOSE_THEN `ibig:num` STRIP_ASSUME_TAC) THEN
 200   MP_TAC(SPEC `(f:num->num) ibig` EUCLID_BOUND) THEN
 201   DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
 202   EXISTS_TAC `p:num` THEN CONJ_TAC THENL
 203    [EXISTS_TAC `ibig:num` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
 204   SUBGOAL_THEN `~(p = 0)` ASSUME_TAC THENL
 205      [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
 206   CONJ_TAC THENL [FIRST_ASSUM ACCEPT_TAC; ALL_TAC] THEN
 207   SUBGOAL_THEN `!i. i <= n ==> f i < p` ASSUME_TAC THENL
 208    [ASM_MESON_TAC[LET_TRANS]; ALL_TAC] THEN
 209   EXISTS_TAC `PSEQ p f 0 (SUC n)` THEN CONJ_TAC THENL
 210    [MATCH_MP_TAC PSEQ_BOUND THEN ASM_SIMP_TAC[LT_SUC_LE]; ALL_TAC] THEN
 211   CONJ_TAC THENL [ASM_MESON_TAC[LE_0]; ALL_TAC] THEN
 212   CONJ_TAC THENL [ASM_MESON_TAC[LE_REFL]; ALL_TAC] THEN
 213   REPEAT CONJ_TAC THENL
 214    [ASM_REWRITE_TAC[PSEQ] THEN MESON_TAC[];
 215     MP_TAC(SPECL [`f:num->num`; `p:num`; `n:num`; `0`; `1`] PSEQ_SPLIT) THEN
 216     ASM_SIMP_TAC[ADD1; ADD_CLAUSES] THEN
 217     DISCH_THEN(K ALL_TAC) THEN EXISTS_TAC `PSEQ p f 0 n` THEN
 218     ASM_SIMP_TAC[PSEQ_BOUND; PSEQ_1; LT_IMP_LE];
 219     ALL_TAC] THEN
 220   ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b ==> a ==> c`] THEN
 221   ASM_SIMP_TAC[primepow; LEFT_IMP_EXISTS_THM] THEN
 222   GEN_TAC THEN X_GEN_TAC `i:num` THEN DISCH_THEN(K ALL_TAC) THEN
 223   ASM_REWRITE_TAC[LT_EXP] THEN STRIP_TAC THEN
 224   MP_TAC(SPECL [`f:num->num`; `p:num`; `i:num`; `0`; `SUC n - i`]
 225                PSEQ_SPLIT) THEN
 226   ASM_SIMP_TAC[ARITH_RULE `i < n ==> (i + SUC n - i = SUC n)`] THEN
 227   DISCH_THEN(K ALL_TAC) THEN
 228   EXISTS_TAC `PSEQ p f 0 i` THEN REWRITE_TAC[EQ_ADD_LCANCEL] THEN
 229   ASM_REWRITE_TAC[EQ_MULT_LCANCEL; EXP_EQ_0; ADD_CLAUSES] THEN
 230   CONJ_TAC THENL
 231    [ASM_MESON_TAC[PSEQ_BOUND; LT_TRANS; LT_IMP_LE]; ALL_TAC] THEN
 232   MP_TAC(SPECL [`f:num->num`; `p:num`; `1`; `i:num`; `n - i`]
 233                PSEQ_SPLIT) THEN
 234   ASM_SIMP_TAC[ARITH_RULE `i < n ==> (1 + n - i = SUC n - i)`] THEN
 235   DISCH_THEN(K ALL_TAC) THEN EXISTS_TAC `PSEQ p f i 1` THEN
 236   ASM_REWRITE_TAC[EQ_ADD_LCANCEL; EQ_MULT_LCANCEL; EXP_1] THEN
 237   ASM_SIMP_TAC[PSEQ_1; LT_IMP_LE] THEN
 238   MP_TAC(SPECL [`f:num->num`; `p:num`; `1`; `i + 1`; `n - i - 1`]
 239                PSEQ_SPLIT) THEN
 240   ASM_SIMP_TAC[ARITH_RULE `i < n ==> (1 + n - i - 1 = n - i)`] THEN
 241   DISCH_THEN(K ALL_TAC) THEN EXISTS_TAC `PSEQ p f (i + 1) 1` THEN
 242   ASM_REWRITE_TAC[EQ_ADD_LCANCEL; EQ_MULT_LCANCEL; EXP_1] THEN
 243   ASM_SIMP_TAC[PSEQ_1; ARITH_RULE `i < n ==> i + 1 <= n`] THEN
 244   ASM_SIMP_TAC[GSYM ADD1] THEN REWRITE_TAC[ADD1] THEN
 245   ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[UNWIND_THM1] THEN
 246   REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_ASSOC; ADD_ASSOC] THEN
 247   MATCH_MP_TAC(ARITH_RULE `1 * a <= c ==> a <= b + c`) THEN
 248   REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
 249   ASM_REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; MULT_EQ_0; EXP_EQ_0]);;
 250
 251 let RELPOW_LEMMA_2 = prove
 252  (`prime p /\ x < p /\ y < p /\
 253    (?qx. m = x + p * qx) /\
 254    (?ry. ry < p EXP n /\ (m = ry + p EXP n * y)) /\
 255    (!q. q < p EXP n
 256         ==> primepow p q
 257             ==> ?r a b s. (m = r + q * (a + p * (b + p * s))) /\
 258                           r < q /\ a < p /\ b < p /\ R a b)
 259    ==> RELPOW n R x y`,
 260   STRIP_TAC THEN REWRITE_TAC[RELPOW_SEQUENCE] THEN
 261   EXISTS_TAC `\i. (m DIV (p EXP i)) MOD p` THEN
 262   SUBGOAL_THEN `~(p = 0)` ASSUME_TAC THENL
 263    [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
 264   REWRITE_TAC[EXP; DIV_1] THEN REPEAT CONJ_TAC THENL
 265    [MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `qx:num` THEN
 266     ASM_REWRITE_TAC[ADD_AC; MULT_AC];
 267     MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `0` THEN
 268     REWRITE_TAC[ASSUME `y < p`; MULT_CLAUSES; ADD_CLAUSES] THEN
 269     MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `ry:num` THEN
 270     REWRITE_TAC[ASSUME `m = ry + p EXP n * y`] THEN
 271     ASM_REWRITE_TAC[ADD_AC; MULT_AC];
 272     ALL_TAC] THEN
 273   X_GEN_TAC `i:num` THEN DISCH_TAC THEN
 274   FIRST_X_ASSUM(MP_TAC o SPEC `p EXP i`) THEN
 275   ASM_SIMP_TAC[LT_EXP; PRIME_GE_2] THEN
 276   ASM_REWRITE_TAC[primepow] THEN
 277   W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
 278    [MESON_TAC[]; ALL_TAC] THEN
 279   DISCH_THEN(REPEAT_TCL CHOOSE_THEN MP_TAC) THEN
 280   DISCH_THEN(CONJUNCTS_THEN2 SUBST1_TAC STRIP_ASSUME_TAC) THEN
 281   UNDISCH_TAC `(R:num->num->bool) a b` THEN
 282   MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN BINOP_TAC THENL
 283    [MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `b + p * s` THEN
 284     ASM_REWRITE_TAC[] THEN
 285     MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `r:num` THEN ASM_REWRITE_TAC[] THEN
 286     REWRITE_TAC[ADD_AC; MULT_AC];
 287     MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `s:num` THEN ASM_REWRITE_TAC[] THEN
 288     MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `r + a * p EXP i` THEN
 289     CONJ_TAC THENL
 290      [REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
 291       REWRITE_TAC[ADD_AC; MULT_AC]; ALL_TAC] THEN
 292     MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `p EXP i + a * p EXP i` THEN
 293     ASM_REWRITE_TAC[LT_ADD_RCANCEL] THEN
 294     REWRITE_TAC[ARITH_RULE `p + q * p = (q + 1) * p`] THEN
 295     ASM_REWRITE_TAC[LE_MULT_RCANCEL; EXP_EQ_0] THEN
 296     UNDISCH_TAC `a < p` THEN ARITH_TAC]);;
 297
 298 let RELPOW_LEMMA = prove
 299  (`RELPOW n R x y <=>
 300         ?m p. prime p /\ x < p /\ y < p /\
 301               (?qx. m = x + p * qx) /\
 302               (?ry. ry < p EXP n /\ (m = ry + p EXP n * y)) /\
 303               !q. q < p EXP n
 304                   ==> primepow p q
 305                       ==> ?r a b s. (m = r + q * (a + p * (b + p * s))) /\
 306                                     r < q /\ a < p /\ b < p /\ R a b`,
 307   EQ_TAC THENL
 308    [ALL_TAC; REWRITE_TAC[RELPOW_LEMMA_2; LEFT_IMP_EXISTS_THM]] THEN
 309   REWRITE_TAC[RELPOW_SEQUENCE] THEN
 310   DISCH_THEN(CHOOSE_THEN(MP_TAC o GEN_ALL o MATCH_MP RELPOW_LEMMA_1)) THEN
 311   REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
 312   GEN_REWRITE_TAC RAND_CONV [SWAP_EXISTS_THM] THEN
 313   MATCH_MP_TAC MONO_EXISTS THEN
 314   GEN_TAC THEN MATCH_MP_TAC MONO_EXISTS THEN
 315   SIMP_TAC[] THEN MESON_TAC[]);;
 316
 317 let RTC_SIGMA = prove
 318  (`RTC R x y <=>
 319         ?m p Q. primepow p Q /\ x < p /\ y < p /\
 320                 (?s. m = x + p * s) /\
 321                 (?r. r < Q /\ (m = r + Q * y)) /\
 322                 !q. q < Q
 323                     ==> primepow p q
 324                         ==> ?r a b s. (m = r + q * (a + p * (b + p * s))) /\
 325                                       r < q /\ a < p /\ b < p /\ R a b`,
 326   REWRITE_TAC[RTC_RELPOW] THEN EQ_TAC THENL
 327    [DISCH_THEN(X_CHOOSE_THEN `n:num` MP_TAC) THEN
 328     REWRITE_TAC[RELPOW_LEMMA] THEN
 329     MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
 330     MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
 331     DISCH_TAC THEN EXISTS_TAC `p EXP n` THEN ASM_REWRITE_TAC[primepow] THEN
 332     MESON_TAC[];
 333     REWRITE_TAC[primepow] THEN
 334     ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN
 335     REWRITE_TAC[GSYM primepow] THEN
 336     GEN_REWRITE_TAC (LAND_CONV o funpow 3 BINDER_CONV)
 337      [LEFT_AND_EXISTS_THM] THEN
 338     GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV o BINDER_CONV)
 339      [SWAP_EXISTS_THM] THEN
 340     REWRITE_TAC[UNWIND_THM2] THEN
 341     GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [SWAP_EXISTS_THM] THEN
 342     GEN_REWRITE_TAC LAND_CONV [SWAP_EXISTS_THM] THEN
 343     REWRITE_TAC[GSYM RELPOW_LEMMA]]);;
 344
 345 (* ------------------------------------------------------------------------- *)
 346 (* Partially automate actual definability in object language.                *)
 347 (* ------------------------------------------------------------------------- *)
 348
 349 let arith_pair = new_definition
 350   `arith_pair s t = (s ++ t) ** (s ++ t) ++ s ++ Suc Z`;;
 351
 352 let ARITH_PAIR = prove
 353  (`!s t v. termval v (arith_pair s t) = NPAIR (termval v s) (termval v t)`,
 354   REWRITE_TAC[termval; arith_pair; NPAIR; EXP_2; ARITH_SUC]);;
 355
 356 let FVT_PAIR = prove
 357  (`FVT(arith_pair s t) = FVT(s) UNION FVT(t)`,
 358   REWRITE_TAC[arith_pair; FVT] THEN SET_TAC[]);;
 359
 360 let OBJECTIFY =
 361   let is_add = is_binop `(+):num->num->num`
 362   and is_mul = is_binop `(*):num->num->num`
 363   and is_le = is_binop `(<=):num->num->bool`
 364   and is_lt = is_binop `(<):num->num->bool`
 365   and zero_tm = `0`
 366   and suc_tm = `SUC`
 367   and osuc_tm = `Suc`
 368   and oz_tm = `Z`
 369   and ov_tm = `V`
 370   and oadd_tm = `(++)`
 371   and omul_tm = `(**)`
 372   and oeq_tm = `(===)`
 373   and ole_tm = `(<<=)`
 374   and olt_tm = `(<<)`
 375   and oiff_tm = `(<->)`
 376   and oimp_tm = `(-->)`
 377   and oand_tm = `(&&)`
 378   and oor_tm = `(||)`
 379   and onot_tm = `Not`
 380   and oall_tm = `!!`
 381   and oex_tm = `??`
 382   and numeral_tm = `numeral`
 383   and assign_tm = `(|->):num->term->(num->term)->(num->term)`
 384   and term_ty = `:term`
 385   and form_ty = `:form`
 386   and num_ty = `:num`
 387   and formsubst_tm = `formsubst`
 388   and holdsv_tm = `holds v`
 389   and v_tm = `v:num->num` in
 390   let objectify1 fn op env tm = mk_comb(op,fn env (rand tm)) in
 391   let objectify2 fn op env tm =
 392     mk_comb(mk_comb(op,fn env (lhand tm)),fn env (rand tm)) in
 393   fun defs ->
 394     let defs' = [TERMVAL_NUMERAL; ARITH_PAIR] @ defs in
 395     let rec objectify_term env tm =
 396       if is_var tm then mk_comb(ov_tm,apply env tm)
 397       else if tm = zero_tm then oz_tm
 398       else if is_numeral tm then mk_comb(numeral_tm,tm)
 399       else if is_add tm then objectify2 objectify_term oadd_tm env tm
 400       else if is_mul tm then objectify2 objectify_term omul_tm env tm
 401       else if is_comb tm & rator tm = suc_tm
 402         then objectify1 objectify_term osuc_tm env tm
 403       else
 404         let f,args = strip_comb tm in
 405         let args' = map (objectify_term env) args in
 406         try let dth = find
 407               (fun th -> fst(strip_comb(rand(snd(strip_forall(concl th))))) = f)
 408               defs' in
 409             let l,r = dest_eq(snd(strip_forall(concl dth))) in
 410             list_mk_comb(fst(strip_comb(rand l)),args')
 411         with Failure _ ->
 412             let ty = itlist (mk_fun_ty o type_of) args' form_ty in
 413             let v = mk_var(fst(dest_var f),ty) in
 414             list_mk_comb(v,args') in
 415     let rec objectify_formula env fm =
 416       if is_forall fm then
 417         let x,bod = dest_forall fm in
 418         let n = mk_small_numeral
 419           (itlist (max o dest_small_numeral) (ran env) 0 + 1) in
 420         mk_comb(mk_comb(oall_tm,n),objectify_formula ((x |-> n) env) bod)
 421       else if is_exists fm then
 422         let x,bod = dest_exists fm in
 423         let n = mk_small_numeral
 424           (itlist (max o dest_small_numeral) (ran env) 0 + 1) in
 425         mk_comb(mk_comb(oex_tm,n),objectify_formula ((x |-> n) env) bod)
 426       else if is_iff fm then objectify2 objectify_formula oiff_tm env fm
 427       else if is_imp fm then objectify2 objectify_formula oimp_tm env fm
 428       else if is_conj fm then objectify2 objectify_formula oand_tm env fm
 429       else if is_disj fm then objectify2 objectify_formula oor_tm env fm
 430       else if is_neg fm then objectify1 objectify_formula onot_tm env fm
 431       else if is_le fm then objectify2 objectify_term ole_tm env fm
 432       else if is_lt fm then objectify2 objectify_term olt_tm env fm
 433       else if is_eq fm then objectify2 objectify_term oeq_tm env fm
 434       else objectify_term env fm in
 435    fun nam th ->
 436      let ptm,tm = dest_eq(snd(strip_forall(concl th))) in
 437      let vs = filter (fun v -> type_of v = num_ty) (snd(strip_comb ptm)) in
 438      let ns = 1--(length vs) in
 439      let env = itlist2 (fun v n -> v |-> mk_small_numeral n) vs ns undefined in
 440      let otm = objectify_formula env tm in
 441      let vs' = map (fun v -> mk_var(fst(dest_var v),term_ty)) vs in
 442      let stm = itlist2
 443        (fun v n a -> mk_comb(mk_comb(mk_comb(assign_tm,mk_small_numeral
 444          n),v),a))
 445        vs' ns ov_tm in
 446      let rside = mk_comb(mk_comb(formsubst_tm,stm),otm) in
 447      let vs'' = subtract (frees rside) vs' @ vs' in
 448      let lty = itlist (mk_fun_ty o type_of) vs'' (type_of rside) in
 449      let lside = list_mk_comb(mk_var(nam,lty),vs'') in
 450      let def = mk_eq(lside,rside) in
 451      let dth = new_definition def in
 452      let clside = lhs(snd(strip_forall(concl dth))) in
 453      let etm = mk_comb(holdsv_tm,clside) in
 454      let thm =
 455        (REWRITE_CONV ([dth; holds; HOLDS_FORMSUBST] @ defs') THENC
 456         REWRITE_CONV [termval; ARITH_EQ; o_THM; valmod] THENC
 457         GEN_REWRITE_CONV I [GSYM th]) etm in
 458      dth,DISCH_ALL (GENL (v_tm::vs') thm);;
 459
 460 (* ------------------------------------------------------------------------- *)
 461 (* Some sort of common tactic for free variables.                            *)
 462 (* ------------------------------------------------------------------------- *)
 463
 464 let FV_TAC ths =
 465   let ths' = ths @
 466    [FV; FORMSUBST_FV; FVT; TERMSUBST_FVT; IN_ELIM_THM;
 467     NOT_IN_EMPTY; IN_UNION; IN_DELETE; IN_SING]
 468   and tac =
 469      REWRITE_TAC[DISJ_ACI; TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN
 470      REWRITE_TAC[EXISTS_OR_THM; GSYM CONJ_ASSOC; UNWIND_THM2; ARITH_EQ] THEN
 471      REWRITE_TAC[valmod; ARITH_EQ; FVT] THEN REWRITE_TAC[DISJ_ACI] in
 472   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
 473   ASM_REWRITE_TAC ths' THEN tac THEN ASM_SIMP_TAC ths' THEN tac;;
 474
 475 (* ------------------------------------------------------------------------- *)
 476 (* So do the formula-level stuff (more) automatically.                       *)
 477 (* ------------------------------------------------------------------------- *)
 478
 479 let arith_divides,ARITH_DIVIDES =
 480   OBJECTIFY [] "arith_divides" divides_DELTA;;
 481
 482 let FV_DIVIDES = prove
 483  (`!s t. FV(arith_divides s t) = FVT(s) UNION FVT(t)`,
 484   FV_TAC[arith_divides]);;
 485
 486 let arith_prime,ARITH_PRIME =
 487   OBJECTIFY [ARITH_DIVIDES] "arith_prime" prime_DELTA;;
 488
 489 let FV_PRIME = prove
 490  (`!t. FV(arith_prime t) = FVT(t)`,
 491   FV_TAC[arith_prime; FVT_NUMERAL; FV_DIVIDES]);;
 492
 493 let arith_primepow,ARITH_PRIMEPOW =
 494   OBJECTIFY [ARITH_PRIME; ARITH_DIVIDES] "arith_primepow" primepow_DELTA;;
 495
 496 let FV_PRIMEPOW = prove
 497  (`!s t. FV(arith_primepow s t) = FVT(s) UNION FVT(t)`,
 498   FV_TAC[arith_primepow; FVT_NUMERAL; FV_DIVIDES; FV_PRIME]);;
 499
 500 let arith_rtc,ARITH_RTC =
 501   OBJECTIFY
 502    [ARITH_PRIMEPOW;
 503     ASSUME `!v s t. holds v (R s t) <=> r (termval v s) (termval v t)`]
 504    "arith_rtc" RTC_SIGMA;;
 505
 506 let FV_RTC = prove
 507  (`!R. (!s t. FV(R s t) = FVT(s) UNION FVT(t))
 508        ==> !s t. FV(arith_rtc R s t) = FVT(s) UNION FVT(t)`,
 509   FV_TAC[arith_rtc; FV_PRIMEPOW]);;
 510
 511 (* ------------------------------------------------------------------------- *)
 512 (* Automate RTC constructions, including parametrized ones.                  *)
 513 (* ------------------------------------------------------------------------- *)
 514
 515 let OBJECTIFY_RTC =
 516   let pth = prove
 517    (`(!v x y. holds v (f x y) <=> f' (termval v x) (termval v y))
 518      ==> !g. (!n. g n = formsubst ((0 |-> n) V)
 519                                   (arith_rtc f (numeral 0)
 520                                                (arith_pair (V 0) (numeral 0))))
 521              ==> !v n. holds v (g n) <=> RTC f' 0 (NPAIR (termval v n) 0)`,
 522     DISCH_THEN(MP_TAC o MATCH_MP ARITH_RTC) THEN SIMP_TAC[HOLDS_FORMSUBST] THEN
 523     REWRITE_TAC[termval; o_DEF; ARITH_EQ; valmod;
 524                 ARITH_PAIR; TERMVAL_NUMERAL]) in
 525   fun def nam th ->
 526     let th1 = MATCH_MP pth def in
 527     let v = fst(dest_forall(concl th1)) in
 528     let th2 = SPEC (mk_var(nam,type_of v)) th1 in
 529     let dth = new_definition (fst(dest_imp(concl th2))) in
 530     dth,ONCE_REWRITE_RULE[GSYM th] (MATCH_MP th2 dth);;
 531
 532 let RTCP = new_definition
 533   `RTCP R m x y <=> RTC (R m) x y`;;
 534
 535 let RTCP_SIGMA = REWRITE_RULE[GSYM RTCP]
 536         (INST [`(R:num->num->num->bool) m`,`R:num->num->bool`] RTC_SIGMA);;
 537
 538 let arith_rtcp,ARITH_RTCP =
 539   OBJECTIFY
 540    [ARITH_PRIMEPOW;
 541     ASSUME `!v m s t. holds v (R m s t) <=>
 542                    r (termval v m) (termval v s) (termval v t)`]
 543    "arith_rtcp" RTCP_SIGMA;;
 544
 545 let ARITH_RTC_PARAMETRIZED = REWRITE_RULE[RTCP] ARITH_RTCP;;
 546
 547 let FV_RTCP = prove
 548  (`!R. (!s t u. FV(R s t u) = FVT(s) UNION FVT(t) UNION FVT(u))
 549        ==> !s t u. FV(arith_rtcp R s t u) = FVT(s) UNION FVT(t) UNION FVT(u)`,
 550   FV_TAC[arith_rtcp; FV_PRIMEPOW]);;
 551
 552 let OBJECTIFY_RTCP =
 553   let pth = prove
 554    (`(!v m x y. holds v (f m x y) <=>
 555                 f' (termval v m) (termval v x) (termval v y))
 556      ==> !g. (!m n. g m n = formsubst ((1 |-> m) ((0 |-> n) V))
 557                                   (arith_rtcp f (V 1) (numeral 0)
 558                                                (arith_pair (V 0) (numeral 0))))
 559              ==> !v m n. holds v (g m n) <=>
 560                           RTC (f' (termval v m)) 0 (NPAIR (termval v n) 0)`,
 561     DISCH_THEN(MP_TAC o MATCH_MP ARITH_RTC_PARAMETRIZED) THEN
 562     SIMP_TAC[HOLDS_FORMSUBST] THEN
 563     REWRITE_TAC[termval; o_DEF; ARITH_EQ; valmod;
 564                 ARITH_PAIR; TERMVAL_NUMERAL]) in
 565   fun def nam th ->
 566     let th1 = MATCH_MP pth def in
 567     let v = fst(dest_forall(concl th1)) in
 568     let th2 = SPEC (mk_var(nam,type_of v)) th1 in
 569     let dth = new_definition (fst(dest_imp(concl th2))) in
 570     dth,ONCE_REWRITE_RULE[GSYM th] (MATCH_MP th2 dth);;
 571
 572 (* ------------------------------------------------------------------------- *)
 573 (* Generic result about primitive recursion.                                 *)
 574 (* ------------------------------------------------------------------------- *)
 575
 576 let PRIMREC_SIGMA = prove
 577  (`(fn 0 = e) /\
 578    (!n. fn (SUC n) = f (fn n) n)
 579    ==> !x y. RTC (\x y. ?n r. (x = NPAIR n r) /\ (y = NPAIR (SUC n) (f r n)))
 580                  (NPAIR 0 e) (NPAIR x y) <=>
 581              (fn(x) = y)`,
 582   REPEAT GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN
 583   ONCE_REWRITE_TAC[RTC_CASES_L] THEN ASM_REWRITE_TAC[NPAIR_INJ; NOT_SUC] THEN
 584   REWRITE_TAC[SUC_INJ; RIGHT_AND_EXISTS_THM] THEN GEN_TAC THEN
 585   ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
 586   GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [SWAP_EXISTS_THM] THEN
 587   ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> b /\ a /\ c`] THEN
 588   ASM_REWRITE_TAC[UNWIND_THM2] THEN ASM_MESON_TAC[]);;
 589
 590 let arith_primrecstep = new_definition
 591  `arith_primrecstep R s t =
 592         (formsubst ((0 |-> s) ((1 |-> t) V))
 593                   (?? 2 (?? 3 (?? 4
 594                   (V 0 === arith_pair (V 2) (V 3) &&
 595                    V 1 === arith_pair (Suc(V 2)) (V 4) &&
 596                    R (V 3) (V 2) (V 4))))))`;;
 597
 598 let ARITH_PRIMRECSTEP = prove
 599  (`(!v x y z. holds v (R x y z) <=>
 600               (f (termval v x) (termval v y) = termval v z))
 601     ==> !v s t. holds v (arith_primrecstep R s t) <=>
 602                 ?n r. (termval v s = NPAIR n r) /\
 603                       (termval v t = NPAIR (SUC n) (f r n))`,
 604   STRIP_TAC THEN
 605   ASM_REWRITE_TAC[arith_primrecstep; holds; HOLDS_FORMSUBST] THEN
 606   ASM_REWRITE_TAC[termval; valmod; o_DEF; ARITH_EQ; ARITH_PAIR] THEN
 607   MESON_TAC[]);;
 608
 609 let FV_PRIMRECSTEP = prove
 610  (`!R. (!s t u. FV(R s t u) SUBSET (FVT(s) UNION FVT(t) UNION FVT(u)))
 611        ==> !s t. FV(arith_primrecstep R s t) = FVT(s) UNION FVT(t)`,
 612   REWRITE_TAC[SUBSET; IN_UNION] THEN FV_TAC[arith_primrecstep; FVT_PAIR] THEN
 613   GEN_TAC THEN MATCH_MP_TAC(TAUT `~a ==> (a \/ b <=> b)`) THEN
 614   DISCH_THEN(CHOOSE_THEN
 615    (CONJUNCTS_THEN2(ANTE_RES_THEN MP_TAC) ASSUME_TAC)) THEN
 616   ASM_REWRITE_TAC[FVT; IN_SING]);;
 617
 618 let arith_primrec = new_definition
 619   `arith_primrec R c s t =
 620         arith_rtc (arith_primrecstep R)
 621             (arith_pair Z c) (arith_pair s t)`;;
 622
 623 let ARITH_PRIMREC = prove
 624  (`!fn e f R c.
 625         (fn 0 = e) /\ (!n. fn (SUC n) = f (fn n) n) /\
 626         (!v. termval v c = e) /\
 627                   (!v x y z. holds v (R x y z) <=>
 628                              (f (termval v x) (termval v y) = termval v z))
 629                   ==> !v s t. holds v (arith_primrec R c s t) <=>
 630                                (fn(termval v s) = termval v t)`,
 631   REPEAT STRIP_TAC THEN
 632   FIRST_ASSUM(MP_TAC o MATCH_MP ARITH_PRIMRECSTEP) THEN
 633   DISCH_THEN(MP_TAC o MATCH_MP ARITH_RTC) THEN
 634   CONV_TAC(TOP_DEPTH_CONV ETA_CONV) THEN
 635   SIMP_TAC[arith_primrec; ARITH_PAIR; termval] THEN
 636   ASM_SIMP_TAC[PRIMREC_SIGMA]);;
 637
 638 let FV_PRIMREC = prove
 639  (`!R c. (FVT c = {}) /\
 640          (!s t u. FV(R s t u) SUBSET (FVT(s) UNION FVT(t) UNION FVT(u)))
 641          ==> !s t. FV(arith_primrec R c s t) = FVT(s) UNION FVT(t)`,
 642   REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[arith_primrec] THEN
 643   ASM_SIMP_TAC[FV_RTC; FVT_PAIR; FV_PRIMRECSTEP;
 644                  UNION_EMPTY; UNION_ACI; FVT]);;