X-Git-Url: http://colo12-c703.uibk.ac.at/git/?p=G%C3%B6del%27s%20incompleteness%20theorem%2F.git;a=blobdiff_plain;f=Arithmetic%2Fdefinability.ml;fp=Arithmetic%2Fdefinability.ml;h=03a7f079c29a864f01b91169aac4abd4a72841a1;hp=0000000000000000000000000000000000000000;hb=87defde679eb7f7eb6d8f7203472a6f6a8ab2966;hpb=67928fe38836205ca8d0705b3695186e998e3e29

diff --git a/Arithmetic/definability.ml b/Arithmetic/definability.ml
new file mode 100644
index 0000000..03a7f07
--- /dev/null
+++ b/Arithmetic/definability.ml
@@ -0,0 +1,644 @@
+(* ========================================================================= *)
+(* Definability in arithmetic of important notions.                          *)
+(* ========================================================================= *)
+
+prioritize_num();;
+
+(* ------------------------------------------------------------------------- *)
+(* Pairing operation.                                                        *)
+(* ------------------------------------------------------------------------- *)
+
+let NPAIR = new_definition
+  `NPAIR x y = (x + y) EXP 2 + x + 1`;;
+
+let NPAIR_NONZERO = prove
+ (`!x y. ~(NPAIR x y = 0)`,
+  REWRITE_TAC[NPAIR; ADD_EQ_0; ARITH]);;
+
+let NPAIR_INJ_LEMMA = prove
+ (`x1 + y1 < x2 + y2 ==> NPAIR x1 y1 < NPAIR x2 y2`,
+  STRIP_TAC THEN REWRITE_TAC[NPAIR; EXP_2] THEN
+  REWRITE_TAC[ARITH_RULE `x + y + 1 < u + v + 1 <=> x + y < u + v`] THEN
+  MATCH_MP_TAC LTE_TRANS THEN
+  EXISTS_TAC `SUC(x1 + y1) * SUC(x1 + y1)` THEN CONJ_TAC THENL
+   [ARITH_TAC; ASM_MESON_TAC[LE_TRANS; LE_ADD; LE_MULT2; LE_SUC_LT]]);;
+
+let NPAIR_INJ = prove
+ (`(NPAIR x y = NPAIR x' y') <=> (x = x') /\ (y = y')`,
+  EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
+  SUBGOAL_THEN `x' + y' = x + y` ASSUME_TAC THENL
+   [ASM_MESON_TAC[LT_CASES; NPAIR_INJ_LEMMA; LT_REFL];
+    UNDISCH_TAC `NPAIR x y = NPAIR x' y'` THEN
+    UNDISCH_TAC `x' + y' = x + y` THEN
+    SIMP_TAC[NPAIR; EXP_2] THEN ARITH_TAC]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Decreasingness.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+let NPAIR_LT = prove
+ (`!x y. x < NPAIR x y /\ y < NPAIR x y`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[NPAIR] THEN
+  REWRITE_TAC[ARITH_RULE `x < a + x + 1`] THEN
+  MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `(x + y) + x + 1` THEN
+  REWRITE_TAC[LE_ADD_RCANCEL; EXP_2; LE_SQUARE_REFL] THEN
+  ARITH_TAC);;
+
+(* ------------------------------------------------------------------------- *)
+(* Auxiliary concepts needed. NB: these are Delta so can be negated freely.  *)
+(* ------------------------------------------------------------------------- *)
+
+let primepow = new_definition
+  `primepow p x <=> prime(p) /\ ?n. x = p EXP n`;;
+
+let divides_DELTA = prove
+ (`m divides n <=> ?x. x <= n /\ n = m * x`,
+  REWRITE_TAC[divides] THEN ASM_CASES_TAC `m = 0` THENL
+   [ASM_REWRITE_TAC[MULT_CLAUSES] THEN MESON_TAC[LE_REFL]; ALL_TAC] THEN
+  AP_TERM_TAC THEN ABS_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN
+  FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE `~(m = 0) ==> 1 <= m`)) THEN
+  SIMP_TAC[LE_EXISTS; LEFT_IMP_EXISTS_THM;
+           RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
+  MESON_TAC[]);;
+
+let prime_DELTA = prove
+ (`prime(p) <=> 2 <= p /\ !n. n < p ==> n divides p ==> n = 1`,
+  ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[ARITH; PRIME_0] THEN
+  ASM_CASES_TAC `p = 1` THEN ASM_REWRITE_TAC[ARITH; PRIME_1] THEN EQ_TAC THENL
+   [ASM_MESON_TAC[prime; LT_REFL; PRIME_GE_2];
+    ASM_MESON_TAC[prime;  DIVIDES_LE; LE_LT]]);;
+
+let primepow_DELTA = prove
+ (`primepow p x <=>
+        prime(p) /\ ~(x = 0) /\
+        !z. z <= x ==> z divides x ==> z = 1 \/ p divides z`,
+  REWRITE_TAC[primepow; TAUT `a ==> b \/ c <=> a /\ ~b ==> c`] THEN
+  ASM_CASES_TAC `prime(p)` THEN
+  ASM_REWRITE_TAC[] THEN EQ_TAC THENL
+   [DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN
+    ASM_REWRITE_TAC[EXP_EQ_0] THEN
+    ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[] THENL
+     [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
+    REPEAT STRIP_TAC THEN
+    FIRST_ASSUM(MP_TAC o SPEC `z:num` o MATCH_MP PRIME_COPRIME) THEN
+    ASM_REWRITE_TAC[] THEN
+    ASM_CASES_TAC `p divides z` THEN ASM_REWRITE_TAC[] THEN
+    ONCE_REWRITE_TAC[COPRIME_SYM] THEN
+    DISCH_THEN(MP_TAC o SPEC `n:num` o MATCH_MP COPRIME_EXP) THEN
+    ASM_MESON_TAC[COPRIME; DIVIDES_REFL];
+    SPEC_TAC(`x:num`,`x:num`) THEN MATCH_MP_TAC num_WF THEN
+    REPEAT STRIP_TAC THEN ASM_CASES_TAC `x = 1` THENL
+     [EXISTS_TAC `0` THEN ASM_REWRITE_TAC[EXP]; ALL_TAC] THEN
+    FIRST_ASSUM(X_CHOOSE_THEN `q:num` MP_TAC o MATCH_MP PRIME_FACTOR) THEN
+    STRIP_TAC THEN
+    UNDISCH_TAC `!z. z <= x ==> z divides x /\ ~(z = 1) ==> p divides z` THEN
+    DISCH_THEN(fun th -> ASSUME_TAC th THEN MP_TAC th) THEN
+    DISCH_THEN(MP_TAC o SPEC `q:num`) THEN ASM_REWRITE_TAC[] THEN
+    ASM_CASES_TAC `q = 1` THENL [ASM_MESON_TAC[PRIME_1]; ALL_TAC] THEN
+    ASM_REWRITE_TAC[] THEN
+    SUBGOAL_THEN `q <= x` ASSUME_TAC THENL
+     [ASM_MESON_TAC[DIVIDES_LE]; ASM_REWRITE_TAC[]] THEN
+    SUBGOAL_THEN `p divides x` MP_TAC THENL
+     [ASM_MESON_TAC[DIVIDES_TRANS]; ALL_TAC] THEN
+    REWRITE_TAC[divides] THEN DISCH_THEN(X_CHOOSE_TAC `y:num`) THEN
+    SUBGOAL_THEN `y < x` (ANTE_RES_THEN MP_TAC) THENL
+     [MATCH_MP_TAC PRIME_FACTOR_LT THEN
+      EXISTS_TAC `p:num` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
+    ASM_CASES_TAC `y = 0` THENL
+     [UNDISCH_TAC `x = p * y` THEN ASM_REWRITE_TAC[MULT_CLAUSES]; ALL_TAC] THEN
+    ASM_REWRITE_TAC[] THEN
+    SUBGOAL_THEN `!z. z <= y ==> z divides y /\ ~(z = 1) ==> p divides z`
+    (fun th -> REWRITE_TAC[th]) THENL
+     [REPEAT STRIP_TAC THEN
+      FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE
+        [IMP_IMP]) THEN
+      REPEAT CONJ_TAC THENL
+       [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `y:num` THEN
+        ASM_REWRITE_TAC[] THEN
+        GEN_REWRITE_TAC LAND_CONV [ARITH_RULE `y = 1 * y`] THEN
+        REWRITE_TAC[LE_MULT_RCANCEL] THEN
+        ASM_REWRITE_TAC[GSYM NOT_LT] THEN
+        REWRITE_TAC[num_CONV `1`; LT; DE_MORGAN_THM] THEN
+        ASM_MESON_TAC[PRIME_0; PRIME_1];
+        ASM_REWRITE_TAC[] THEN MATCH_MP_TAC DIVIDES_LMUL THEN
+        ASM_REWRITE_TAC[];
+        ASM_REWRITE_TAC[]];
+      DISCH_THEN(X_CHOOSE_THEN `n:num` SUBST1_TAC) THEN
+      EXISTS_TAC `SUC n` THEN ASM_REWRITE_TAC[EXP]]]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Sigma-representability of reflexive transitive closure.                   *)
+(* ------------------------------------------------------------------------- *)
+
+let PSEQ = new_recursive_definition num_RECURSION
+  `(PSEQ p f m 0 = 0) /\
+   (PSEQ p f m (SUC n) = f m + p * PSEQ p f (SUC m) n)`;;
+
+let PSEQ_SPLIT = prove
+ (`!f p n m r.
+        PSEQ p f m (n + r) = PSEQ p f m n + p EXP n * PSEQ p f (m + n) r`,
+  GEN_TAC THEN GEN_TAC THEN
+  INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; EXP; MULT_CLAUSES; PSEQ] THEN
+  ASM_REWRITE_TAC[GSYM ADD_ASSOC; EQ_ADD_LCANCEL] THEN
+  REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_AC; ADD_CLAUSES]);;
+
+let PSEQ_1 = prove
+ (`PSEQ p f m 1 = f m`,
+  REWRITE_TAC[num_CONV `1`; ADD_CLAUSES; MULT_CLAUSES; PSEQ]);;
+
+let PSEQ_BOUND = prove
+ (`!n. ~(p = 0) /\ (!i. i < n ==> f i < p) ==> PSEQ p f 0 n < p EXP n`,
+  ASM_CASES_TAC `p = 0` THEN ASM_REWRITE_TAC[] THEN
+  INDUCT_TAC THENL [REWRITE_TAC[PSEQ; EXP; ARITH]; ALL_TAC] THEN
+  DISCH_TAC THEN
+  MP_TAC(SPECL [`f:num->num`; `p:num`; `n:num`; `0`; `1`]
+               PSEQ_SPLIT) THEN
+  SIMP_TAC[ADD1; ADD_CLAUSES] THEN REPEAT STRIP_TAC THEN
+  MATCH_MP_TAC LTE_TRANS THEN
+  EXISTS_TAC `p EXP n + p EXP n * PSEQ p f n 1` THEN
+  ASM_SIMP_TAC[LT_ADD_RCANCEL; ARITH_RULE `i < n ==> i < SUC n`] THEN
+  REWRITE_TAC[ARITH_RULE `p + p * q = p * (q + 1)`] THEN
+  ASM_REWRITE_TAC[EXP_ADD; LE_MULT_LCANCEL; EXP_EQ_0] THEN
+  MATCH_MP_TAC(ARITH_RULE `x < p ==> x + 1 <= p`) THEN
+  ASM_SIMP_TAC[EXP_1; PSEQ_1; LT]);;
+
+let RELPOW_LEMMA_1 = prove
+ (`(f 0 = x) /\
+   (f n = y) /\
+   (!i. i < n ==> R (f i) (f(SUC i)))
+   ==> ?p. (?i. i <= n /\ p <= SUC(FACT(f i))) /\
+           prime p /\
+           (?m. m < p EXP (SUC n) /\
+                x < p /\ y < p /\
+                (?qx. m = x + p * qx) /\
+                (?ry. ry < p EXP n /\ (m = ry + p EXP n * y)) /\
+                !q. q < p EXP n
+                    ==> primepow p q
+                        ==> ?r. r < q /\
+                                ?a. a < p /\
+                                    ?b. b < p /\
+                                        R a b /\
+                                        ?s. s <= m /\
+                                            (m =
+                                             r + q * (a + p * (b + p * s))))`,
+  REPEAT STRIP_TAC THEN
+  SUBGOAL_THEN `?j. j <= n /\ !i. i <= n ==> f i <= f j` MP_TAC THENL
+   [SPEC_TAC(`n:num`,`n:num`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN
+    INDUCT_TAC THENL
+     [SIMP_TAC[LE] THEN MESON_TAC[LE_REFL]; ALL_TAC] THEN
+    FIRST_ASSUM(X_CHOOSE_THEN `j:num` STRIP_ASSUME_TAC) THEN
+    DISJ_CASES_TAC(ARITH_RULE `f(SUC n) <= f(j) \/ f(j) <= f(SUC n)`) THENL
+     [EXISTS_TAC `j:num` THEN
+      ASM_SIMP_TAC[ARITH_RULE `j <= n ==> j <= SUC n`] THEN
+      REWRITE_TAC[LE] THEN REPEAT STRIP_TAC THEN
+      ASM_SIMP_TAC[] THEN ASM_MESON_TAC[];
+      EXISTS_TAC `SUC n` THEN REWRITE_TAC[LE_REFL] THEN
+      REWRITE_TAC[LE] THEN REPEAT STRIP_TAC THEN
+      ASM_SIMP_TAC[LE_REFL] THEN ASM_MESON_TAC[LE_TRANS]];
+    ALL_TAC] THEN
+  DISCH_THEN(X_CHOOSE_THEN `ibig:num` STRIP_ASSUME_TAC) THEN
+  MP_TAC(SPEC `(f:num->num) ibig` EUCLID_BOUND) THEN
+  DISCH_THEN(X_CHOOSE_THEN `p:num` STRIP_ASSUME_TAC) THEN
+  EXISTS_TAC `p:num` THEN CONJ_TAC THENL
+   [EXISTS_TAC `ibig:num` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
+  SUBGOAL_THEN `~(p = 0)` ASSUME_TAC THENL
+     [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
+  CONJ_TAC THENL [FIRST_ASSUM ACCEPT_TAC; ALL_TAC] THEN
+  SUBGOAL_THEN `!i. i <= n ==> f i < p` ASSUME_TAC THENL
+   [ASM_MESON_TAC[LET_TRANS]; ALL_TAC] THEN
+  EXISTS_TAC `PSEQ p f 0 (SUC n)` THEN CONJ_TAC THENL
+   [MATCH_MP_TAC PSEQ_BOUND THEN ASM_SIMP_TAC[LT_SUC_LE]; ALL_TAC] THEN
+  CONJ_TAC THENL [ASM_MESON_TAC[LE_0]; ALL_TAC] THEN
+  CONJ_TAC THENL [ASM_MESON_TAC[LE_REFL]; ALL_TAC] THEN
+  REPEAT CONJ_TAC THENL
+   [ASM_REWRITE_TAC[PSEQ] THEN MESON_TAC[];
+    MP_TAC(SPECL [`f:num->num`; `p:num`; `n:num`; `0`; `1`] PSEQ_SPLIT) THEN
+    ASM_SIMP_TAC[ADD1; ADD_CLAUSES] THEN
+    DISCH_THEN(K ALL_TAC) THEN EXISTS_TAC `PSEQ p f 0 n` THEN
+    ASM_SIMP_TAC[PSEQ_BOUND; PSEQ_1; LT_IMP_LE];
+    ALL_TAC] THEN
+  ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b ==> a ==> c`] THEN
+  ASM_SIMP_TAC[primepow; LEFT_IMP_EXISTS_THM] THEN
+  GEN_TAC THEN X_GEN_TAC `i:num` THEN DISCH_THEN(K ALL_TAC) THEN
+  ASM_REWRITE_TAC[LT_EXP] THEN STRIP_TAC THEN
+  MP_TAC(SPECL [`f:num->num`; `p:num`; `i:num`; `0`; `SUC n - i`]
+               PSEQ_SPLIT) THEN
+  ASM_SIMP_TAC[ARITH_RULE `i < n ==> (i + SUC n - i = SUC n)`] THEN
+  DISCH_THEN(K ALL_TAC) THEN
+  EXISTS_TAC `PSEQ p f 0 i` THEN REWRITE_TAC[EQ_ADD_LCANCEL] THEN
+  ASM_REWRITE_TAC[EQ_MULT_LCANCEL; EXP_EQ_0; ADD_CLAUSES] THEN
+  CONJ_TAC THENL
+   [ASM_MESON_TAC[PSEQ_BOUND; LT_TRANS; LT_IMP_LE]; ALL_TAC] THEN
+  MP_TAC(SPECL [`f:num->num`; `p:num`; `1`; `i:num`; `n - i`]
+               PSEQ_SPLIT) THEN
+  ASM_SIMP_TAC[ARITH_RULE `i < n ==> (1 + n - i = SUC n - i)`] THEN
+  DISCH_THEN(K ALL_TAC) THEN EXISTS_TAC `PSEQ p f i 1` THEN
+  ASM_REWRITE_TAC[EQ_ADD_LCANCEL; EQ_MULT_LCANCEL; EXP_1] THEN
+  ASM_SIMP_TAC[PSEQ_1; LT_IMP_LE] THEN
+  MP_TAC(SPECL [`f:num->num`; `p:num`; `1`; `i + 1`; `n - i - 1`]
+               PSEQ_SPLIT) THEN
+  ASM_SIMP_TAC[ARITH_RULE `i < n ==> (1 + n - i - 1 = n - i)`] THEN
+  DISCH_THEN(K ALL_TAC) THEN EXISTS_TAC `PSEQ p f (i + 1) 1` THEN
+  ASM_REWRITE_TAC[EQ_ADD_LCANCEL; EQ_MULT_LCANCEL; EXP_1] THEN
+  ASM_SIMP_TAC[PSEQ_1; ARITH_RULE `i < n ==> i + 1 <= n`] THEN
+  ASM_SIMP_TAC[GSYM ADD1] THEN REWRITE_TAC[ADD1] THEN
+  ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[UNWIND_THM1] THEN
+  REWRITE_TAC[LEFT_ADD_DISTRIB; MULT_ASSOC; ADD_ASSOC] THEN
+  MATCH_MP_TAC(ARITH_RULE `1 * a <= c ==> a <= b + c`) THEN
+  REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
+  ASM_REWRITE_TAC[ARITH_RULE `1 <= x <=> ~(x = 0)`; MULT_EQ_0; EXP_EQ_0]);;
+
+let RELPOW_LEMMA_2 = prove
+ (`prime p /\ x < p /\ y < p /\
+   (?qx. m = x + p * qx) /\
+   (?ry. ry < p EXP n /\ (m = ry + p EXP n * y)) /\
+   (!q. q < p EXP n
+        ==> primepow p q
+            ==> ?r a b s. (m = r + q * (a + p * (b + p * s))) /\
+                          r < q /\ a < p /\ b < p /\ R a b)
+   ==> RELPOW n R x y`,
+  STRIP_TAC THEN REWRITE_TAC[RELPOW_SEQUENCE] THEN
+  EXISTS_TAC `\i. (m DIV (p EXP i)) MOD p` THEN
+  SUBGOAL_THEN `~(p = 0)` ASSUME_TAC THENL
+   [ASM_MESON_TAC[PRIME_0]; ALL_TAC] THEN
+  REWRITE_TAC[EXP; DIV_1] THEN REPEAT CONJ_TAC THENL
+   [MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `qx:num` THEN
+    ASM_REWRITE_TAC[ADD_AC; MULT_AC];
+    MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `0` THEN
+    REWRITE_TAC[ASSUME `y < p`; MULT_CLAUSES; ADD_CLAUSES] THEN
+    MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `ry:num` THEN
+    REWRITE_TAC[ASSUME `m = ry + p EXP n * y`] THEN
+    ASM_REWRITE_TAC[ADD_AC; MULT_AC];
+    ALL_TAC] THEN
+  X_GEN_TAC `i:num` THEN DISCH_TAC THEN
+  FIRST_X_ASSUM(MP_TAC o SPEC `p EXP i`) THEN
+  ASM_SIMP_TAC[LT_EXP; PRIME_GE_2] THEN
+  ASM_REWRITE_TAC[primepow] THEN
+  W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL
+   [MESON_TAC[]; ALL_TAC] THEN
+  DISCH_THEN(REPEAT_TCL CHOOSE_THEN MP_TAC) THEN
+  DISCH_THEN(CONJUNCTS_THEN2 SUBST1_TAC STRIP_ASSUME_TAC) THEN
+  UNDISCH_TAC `(R:num->num->bool) a b` THEN
+  MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN BINOP_TAC THENL
+   [MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `b + p * s` THEN
+    ASM_REWRITE_TAC[] THEN
+    MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `r:num` THEN ASM_REWRITE_TAC[] THEN
+    REWRITE_TAC[ADD_AC; MULT_AC];
+    MATCH_MP_TAC MOD_UNIQ THEN EXISTS_TAC `s:num` THEN ASM_REWRITE_TAC[] THEN
+    MATCH_MP_TAC DIV_UNIQ THEN EXISTS_TAC `r + a * p EXP i` THEN
+    CONJ_TAC THENL
+     [REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
+      REWRITE_TAC[ADD_AC; MULT_AC]; ALL_TAC] THEN
+    MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `p EXP i + a * p EXP i` THEN
+    ASM_REWRITE_TAC[LT_ADD_RCANCEL] THEN
+    REWRITE_TAC[ARITH_RULE `p + q * p = (q + 1) * p`] THEN
+    ASM_REWRITE_TAC[LE_MULT_RCANCEL; EXP_EQ_0] THEN
+    UNDISCH_TAC `a < p` THEN ARITH_TAC]);;
+
+let RELPOW_LEMMA = prove
+ (`RELPOW n R x y <=>
+        ?m p. prime p /\ x < p /\ y < p /\
+              (?qx. m = x + p * qx) /\
+              (?ry. ry < p EXP n /\ (m = ry + p EXP n * y)) /\
+              !q. q < p EXP n
+                  ==> primepow p q
+                      ==> ?r a b s. (m = r + q * (a + p * (b + p * s))) /\
+                                    r < q /\ a < p /\ b < p /\ R a b`,
+  EQ_TAC THENL
+   [ALL_TAC; REWRITE_TAC[RELPOW_LEMMA_2; LEFT_IMP_EXISTS_THM]] THEN
+  REWRITE_TAC[RELPOW_SEQUENCE] THEN
+  DISCH_THEN(CHOOSE_THEN(MP_TAC o GEN_ALL o MATCH_MP RELPOW_LEMMA_1)) THEN
+  REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN
+  GEN_REWRITE_TAC RAND_CONV [SWAP_EXISTS_THM] THEN
+  MATCH_MP_TAC MONO_EXISTS THEN
+  GEN_TAC THEN MATCH_MP_TAC MONO_EXISTS THEN
+  SIMP_TAC[] THEN MESON_TAC[]);;
+
+let RTC_SIGMA = prove
+ (`RTC R x y <=>
+        ?m p Q. primepow p Q /\ x < p /\ y < p /\
+                (?s. m = x + p * s) /\
+                (?r. r < Q /\ (m = r + Q * y)) /\
+                !q. q < Q
+                    ==> primepow p q
+                        ==> ?r a b s. (m = r + q * (a + p * (b + p * s))) /\
+                                      r < q /\ a < p /\ b < p /\ R a b`,
+  REWRITE_TAC[RTC_RELPOW] THEN EQ_TAC THENL
+   [DISCH_THEN(X_CHOOSE_THEN `n:num` MP_TAC) THEN
+    REWRITE_TAC[RELPOW_LEMMA] THEN
+    MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
+    MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
+    DISCH_TAC THEN EXISTS_TAC `p EXP n` THEN ASM_REWRITE_TAC[primepow] THEN
+    MESON_TAC[];
+    REWRITE_TAC[primepow] THEN
+    ONCE_REWRITE_TAC[TAUT `(a /\ b) /\ c <=> b /\ a /\ c`] THEN
+    REWRITE_TAC[GSYM primepow] THEN
+    GEN_REWRITE_TAC (LAND_CONV o funpow 3 BINDER_CONV)
+     [LEFT_AND_EXISTS_THM] THEN
+    GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV o BINDER_CONV)
+     [SWAP_EXISTS_THM] THEN
+    REWRITE_TAC[UNWIND_THM2] THEN
+    GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [SWAP_EXISTS_THM] THEN
+    GEN_REWRITE_TAC LAND_CONV [SWAP_EXISTS_THM] THEN
+    REWRITE_TAC[GSYM RELPOW_LEMMA]]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Partially automate actual definability in object language.                *)
+(* ------------------------------------------------------------------------- *)
+
+let arith_pair = new_definition
+  `arith_pair s t = (s ++ t) ** (s ++ t) ++ s ++ Suc Z`;;
+
+let ARITH_PAIR = prove
+ (`!s t v. termval v (arith_pair s t) = NPAIR (termval v s) (termval v t)`,
+  REWRITE_TAC[termval; arith_pair; NPAIR; EXP_2; ARITH_SUC]);;
+
+let FVT_PAIR = prove
+ (`FVT(arith_pair s t) = FVT(s) UNION FVT(t)`,
+  REWRITE_TAC[arith_pair; FVT] THEN SET_TAC[]);;
+
+let OBJECTIFY =
+  let is_add = is_binop `(+):num->num->num`
+  and is_mul = is_binop `(*):num->num->num`
+  and is_le = is_binop `(<=):num->num->bool`
+  and is_lt = is_binop `(<):num->num->bool`
+  and zero_tm = `0`
+  and suc_tm = `SUC`
+  and osuc_tm = `Suc`
+  and oz_tm = `Z`
+  and ov_tm = `V`
+  and oadd_tm = `(++)`
+  and omul_tm = `(**)`
+  and oeq_tm = `(===)`
+  and ole_tm = `(<<=)`
+  and olt_tm = `(<<)`
+  and oiff_tm = `(<->)`
+  and oimp_tm = `(-->)`
+  and oand_tm = `(&&)`
+  and oor_tm = `(||)`
+  and onot_tm = `Not`
+  and oall_tm = `!!`
+  and oex_tm = `??`
+  and numeral_tm = `numeral`
+  and assign_tm = `(|->):num->term->(num->term)->(num->term)`
+  and term_ty = `:term`
+  and form_ty = `:form`
+  and num_ty = `:num`
+  and formsubst_tm = `formsubst`
+  and holdsv_tm = `holds v`
+  and v_tm = `v:num->num` in
+  let objectify1 fn op env tm = mk_comb(op,fn env (rand tm)) in
+  let objectify2 fn op env tm =
+    mk_comb(mk_comb(op,fn env (lhand tm)),fn env (rand tm)) in
+  fun defs ->
+    let defs' = [TERMVAL_NUMERAL; ARITH_PAIR] @ defs in
+    let rec objectify_term env tm =
+      if is_var tm then mk_comb(ov_tm,apply env tm)
+      else if tm = zero_tm then oz_tm
+      else if is_numeral tm then mk_comb(numeral_tm,tm)
+      else if is_add tm then objectify2 objectify_term oadd_tm env tm
+      else if is_mul tm then objectify2 objectify_term omul_tm env tm
+      else if is_comb tm & rator tm = suc_tm
+        then objectify1 objectify_term osuc_tm env tm
+      else
+        let f,args = strip_comb tm in
+        let args' = map (objectify_term env) args in
+        try let dth = find
+              (fun th -> fst(strip_comb(rand(snd(strip_forall(concl th))))) = f)
+              defs' in
+            let l,r = dest_eq(snd(strip_forall(concl dth))) in
+            list_mk_comb(fst(strip_comb(rand l)),args')
+        with Failure _ ->
+            let ty = itlist (mk_fun_ty o type_of) args' form_ty in
+            let v = mk_var(fst(dest_var f),ty) in
+            list_mk_comb(v,args') in
+    let rec objectify_formula env fm =
+      if is_forall fm then
+        let x,bod = dest_forall fm in
+        let n = mk_small_numeral
+          (itlist (max o dest_small_numeral) (ran env) 0 + 1) in
+        mk_comb(mk_comb(oall_tm,n),objectify_formula ((x |-> n) env) bod)
+      else if is_exists fm then
+        let x,bod = dest_exists fm in
+        let n = mk_small_numeral
+          (itlist (max o dest_small_numeral) (ran env) 0 + 1) in
+        mk_comb(mk_comb(oex_tm,n),objectify_formula ((x |-> n) env) bod)
+      else if is_iff fm then objectify2 objectify_formula oiff_tm env fm
+      else if is_imp fm then objectify2 objectify_formula oimp_tm env fm
+      else if is_conj fm then objectify2 objectify_formula oand_tm env fm
+      else if is_disj fm then objectify2 objectify_formula oor_tm env fm
+      else if is_neg fm then objectify1 objectify_formula onot_tm env fm
+      else if is_le fm then objectify2 objectify_term ole_tm env fm
+      else if is_lt fm then objectify2 objectify_term olt_tm env fm
+      else if is_eq fm then objectify2 objectify_term oeq_tm env fm
+      else objectify_term env fm in
+   fun nam th ->
+     let ptm,tm = dest_eq(snd(strip_forall(concl th))) in
+     let vs = filter (fun v -> type_of v = num_ty) (snd(strip_comb ptm)) in
+     let ns = 1--(length vs) in
+     let env = itlist2 (fun v n -> v |-> mk_small_numeral n) vs ns undefined in
+     let otm = objectify_formula env tm in
+     let vs' = map (fun v -> mk_var(fst(dest_var v),term_ty)) vs in
+     let stm = itlist2
+       (fun v n a -> mk_comb(mk_comb(mk_comb(assign_tm,mk_small_numeral
+         n),v),a))
+       vs' ns ov_tm in
+     let rside = mk_comb(mk_comb(formsubst_tm,stm),otm) in
+     let vs'' = subtract (frees rside) vs' @ vs' in
+     let lty = itlist (mk_fun_ty o type_of) vs'' (type_of rside) in
+     let lside = list_mk_comb(mk_var(nam,lty),vs'') in
+     let def = mk_eq(lside,rside) in
+     let dth = new_definition def in
+     let clside = lhs(snd(strip_forall(concl dth))) in
+     let etm = mk_comb(holdsv_tm,clside) in
+     let thm =
+       (REWRITE_CONV ([dth; holds; HOLDS_FORMSUBST] @ defs') THENC
+        REWRITE_CONV [termval; ARITH_EQ; o_THM; valmod] THENC
+        GEN_REWRITE_CONV I [GSYM th]) etm in
+     dth,DISCH_ALL (GENL (v_tm::vs') thm);;
+
+(* ------------------------------------------------------------------------- *)
+(* Some sort of common tactic for free variables.                            *)
+(* ------------------------------------------------------------------------- *)
+
+let FV_TAC ths =
+  let ths' = ths @
+   [FV; FORMSUBST_FV; FVT; TERMSUBST_FVT; IN_ELIM_THM;
+    NOT_IN_EMPTY; IN_UNION; IN_DELETE; IN_SING]
+  and tac =
+     REWRITE_TAC[DISJ_ACI; TAUT `(a \/ b) /\ c <=> a /\ c \/ b /\ c`] THEN
+     REWRITE_TAC[EXISTS_OR_THM; GSYM CONJ_ASSOC; UNWIND_THM2; ARITH_EQ] THEN
+     REWRITE_TAC[valmod; ARITH_EQ; FVT] THEN REWRITE_TAC[DISJ_ACI] in
+  REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [EXTENSION] THEN
+  ASM_REWRITE_TAC ths' THEN tac THEN ASM_SIMP_TAC ths' THEN tac;;
+
+(* ------------------------------------------------------------------------- *)
+(* So do the formula-level stuff (more) automatically.                       *)
+(* ------------------------------------------------------------------------- *)
+
+let arith_divides,ARITH_DIVIDES =
+  OBJECTIFY [] "arith_divides" divides_DELTA;;
+
+let FV_DIVIDES = prove
+ (`!s t. FV(arith_divides s t) = FVT(s) UNION FVT(t)`,
+  FV_TAC[arith_divides]);;
+
+let arith_prime,ARITH_PRIME =
+  OBJECTIFY [ARITH_DIVIDES] "arith_prime" prime_DELTA;;
+
+let FV_PRIME = prove
+ (`!t. FV(arith_prime t) = FVT(t)`,
+  FV_TAC[arith_prime; FVT_NUMERAL; FV_DIVIDES]);;
+
+let arith_primepow,ARITH_PRIMEPOW =
+  OBJECTIFY [ARITH_PRIME; ARITH_DIVIDES] "arith_primepow" primepow_DELTA;;
+
+let FV_PRIMEPOW = prove
+ (`!s t. FV(arith_primepow s t) = FVT(s) UNION FVT(t)`,
+  FV_TAC[arith_primepow; FVT_NUMERAL; FV_DIVIDES; FV_PRIME]);;
+
+let arith_rtc,ARITH_RTC =
+  OBJECTIFY
+   [ARITH_PRIMEPOW;
+    ASSUME `!v s t. holds v (R s t) <=> r (termval v s) (termval v t)`]
+   "arith_rtc" RTC_SIGMA;;
+
+let FV_RTC = prove
+ (`!R. (!s t. FV(R s t) = FVT(s) UNION FVT(t))
+       ==> !s t. FV(arith_rtc R s t) = FVT(s) UNION FVT(t)`,
+  FV_TAC[arith_rtc; FV_PRIMEPOW]);;
+
+(* ------------------------------------------------------------------------- *)
+(* Automate RTC constructions, including parametrized ones.                  *)
+(* ------------------------------------------------------------------------- *)
+
+let OBJECTIFY_RTC =
+  let pth = prove
+   (`(!v x y. holds v (f x y) <=> f' (termval v x) (termval v y))
+     ==> !g. (!n. g n = formsubst ((0 |-> n) V)
+                                  (arith_rtc f (numeral 0)
+                                               (arith_pair (V 0) (numeral 0))))
+             ==> !v n. holds v (g n) <=> RTC f' 0 (NPAIR (termval v n) 0)`,
+    DISCH_THEN(MP_TAC o MATCH_MP ARITH_RTC) THEN SIMP_TAC[HOLDS_FORMSUBST] THEN
+    REWRITE_TAC[termval; o_DEF; ARITH_EQ; valmod;
+                ARITH_PAIR; TERMVAL_NUMERAL]) in
+  fun def nam th ->
+    let th1 = MATCH_MP pth def in
+    let v = fst(dest_forall(concl th1)) in
+    let th2 = SPEC (mk_var(nam,type_of v)) th1 in
+    let dth = new_definition (fst(dest_imp(concl th2))) in
+    dth,ONCE_REWRITE_RULE[GSYM th] (MATCH_MP th2 dth);;
+
+let RTCP = new_definition
+  `RTCP R m x y <=> RTC (R m) x y`;;
+
+let RTCP_SIGMA = REWRITE_RULE[GSYM RTCP]
+        (INST [`(R:num->num->num->bool) m`,`R:num->num->bool`] RTC_SIGMA);;
+
+let arith_rtcp,ARITH_RTCP =
+  OBJECTIFY
+   [ARITH_PRIMEPOW;
+    ASSUME `!v m s t. holds v (R m s t) <=>
+                   r (termval v m) (termval v s) (termval v t)`]
+   "arith_rtcp" RTCP_SIGMA;;
+
+let ARITH_RTC_PARAMETRIZED = REWRITE_RULE[RTCP] ARITH_RTCP;;
+
+let FV_RTCP = prove
+ (`!R. (!s t u. FV(R s t u) = FVT(s) UNION FVT(t) UNION FVT(u))
+       ==> !s t u. FV(arith_rtcp R s t u) = FVT(s) UNION FVT(t) UNION FVT(u)`,
+  FV_TAC[arith_rtcp; FV_PRIMEPOW]);;
+
+let OBJECTIFY_RTCP =
+  let pth = prove
+   (`(!v m x y. holds v (f m x y) <=>
+                f' (termval v m) (termval v x) (termval v y))
+     ==> !g. (!m n. g m n = formsubst ((1 |-> m) ((0 |-> n) V))
+                                  (arith_rtcp f (V 1) (numeral 0)
+                                               (arith_pair (V 0) (numeral 0))))
+             ==> !v m n. holds v (g m n) <=>
+                          RTC (f' (termval v m)) 0 (NPAIR (termval v n) 0)`,
+    DISCH_THEN(MP_TAC o MATCH_MP ARITH_RTC_PARAMETRIZED) THEN
+    SIMP_TAC[HOLDS_FORMSUBST] THEN
+    REWRITE_TAC[termval; o_DEF; ARITH_EQ; valmod;
+                ARITH_PAIR; TERMVAL_NUMERAL]) in
+  fun def nam th ->
+    let th1 = MATCH_MP pth def in
+    let v = fst(dest_forall(concl th1)) in
+    let th2 = SPEC (mk_var(nam,type_of v)) th1 in
+    let dth = new_definition (fst(dest_imp(concl th2))) in
+    dth,ONCE_REWRITE_RULE[GSYM th] (MATCH_MP th2 dth);;
+
+(* ------------------------------------------------------------------------- *)
+(* Generic result about primitive recursion.                                 *)
+(* ------------------------------------------------------------------------- *)
+
+let PRIMREC_SIGMA = prove
+ (`(fn 0 = e) /\
+   (!n. fn (SUC n) = f (fn n) n)
+   ==> !x y. RTC (\x y. ?n r. (x = NPAIR n r) /\ (y = NPAIR (SUC n) (f r n)))
+                 (NPAIR 0 e) (NPAIR x y) <=>
+             (fn(x) = y)`,
+  REPEAT GEN_TAC THEN STRIP_TAC THEN INDUCT_TAC THEN
+  ONCE_REWRITE_TAC[RTC_CASES_L] THEN ASM_REWRITE_TAC[NPAIR_INJ; NOT_SUC] THEN
+  REWRITE_TAC[SUC_INJ; RIGHT_AND_EXISTS_THM] THEN GEN_TAC THEN
+  ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
+  GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [SWAP_EXISTS_THM] THEN
+  ONCE_REWRITE_TAC[TAUT `a /\ b /\ c <=> b /\ a /\ c`] THEN
+  ASM_REWRITE_TAC[UNWIND_THM2] THEN ASM_MESON_TAC[]);;
+
+let arith_primrecstep = new_definition
+ `arith_primrecstep R s t =
+        (formsubst ((0 |-> s) ((1 |-> t) V))
+                  (?? 2 (?? 3 (?? 4
+                  (V 0 === arith_pair (V 2) (V 3) &&
+                   V 1 === arith_pair (Suc(V 2)) (V 4) &&
+                   R (V 3) (V 2) (V 4))))))`;;
+
+let ARITH_PRIMRECSTEP = prove
+ (`(!v x y z. holds v (R x y z) <=>
+              (f (termval v x) (termval v y) = termval v z))
+    ==> !v s t. holds v (arith_primrecstep R s t) <=>
+                ?n r. (termval v s = NPAIR n r) /\
+                      (termval v t = NPAIR (SUC n) (f r n))`,
+  STRIP_TAC THEN
+  ASM_REWRITE_TAC[arith_primrecstep; holds; HOLDS_FORMSUBST] THEN
+  ASM_REWRITE_TAC[termval; valmod; o_DEF; ARITH_EQ; ARITH_PAIR] THEN
+  MESON_TAC[]);;
+
+let FV_PRIMRECSTEP = prove
+ (`!R. (!s t u. FV(R s t u) SUBSET (FVT(s) UNION FVT(t) UNION FVT(u)))
+       ==> !s t. FV(arith_primrecstep R s t) = FVT(s) UNION FVT(t)`,
+  REWRITE_TAC[SUBSET; IN_UNION] THEN FV_TAC[arith_primrecstep; FVT_PAIR] THEN
+  GEN_TAC THEN MATCH_MP_TAC(TAUT `~a ==> (a \/ b <=> b)`) THEN
+  DISCH_THEN(CHOOSE_THEN
+   (CONJUNCTS_THEN2(ANTE_RES_THEN MP_TAC) ASSUME_TAC)) THEN
+  ASM_REWRITE_TAC[FVT; IN_SING]);;
+
+let arith_primrec = new_definition
+  `arith_primrec R c s t =
+        arith_rtc (arith_primrecstep R)
+            (arith_pair Z c) (arith_pair s t)`;;
+
+let ARITH_PRIMREC = prove
+ (`!fn e f R c.
+        (fn 0 = e) /\ (!n. fn (SUC n) = f (fn n) n) /\
+        (!v. termval v c = e) /\
+                  (!v x y z. holds v (R x y z) <=>
+                             (f (termval v x) (termval v y) = termval v z))
+                  ==> !v s t. holds v (arith_primrec R c s t) <=>
+                               (fn(termval v s) = termval v t)`,
+  REPEAT STRIP_TAC THEN
+  FIRST_ASSUM(MP_TAC o MATCH_MP ARITH_PRIMRECSTEP) THEN
+  DISCH_THEN(MP_TAC o MATCH_MP ARITH_RTC) THEN
+  CONV_TAC(TOP_DEPTH_CONV ETA_CONV) THEN
+  SIMP_TAC[arith_primrec; ARITH_PAIR; termval] THEN
+  ASM_SIMP_TAC[PRIMREC_SIGMA]);;
+
+let FV_PRIMREC = prove
+ (`!R c. (FVT c = {}) /\
+         (!s t u. FV(R s t u) SUBSET (FVT(s) UNION FVT(t) UNION FVT(u)))
+         ==> !s t. FV(arith_primrec R c s t) = FVT(s) UNION FVT(t)`,
+  REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[arith_primrec] THEN
+  ASM_SIMP_TAC[FV_RTC; FVT_PAIR; FV_PRIMRECSTEP;
+                 UNION_EMPTY; UNION_ACI; FVT]);;