[FOM] Formal verification

[Freek Wiedijk]

Dear Lasse,

As a followup, here is this same thing

>***
>Let f be a real-valued function on the real line, such
>that f(x)>x for all x.  Let x_0 be a real number, and
>define the sequence (x_n) recursively by
>x_{n+1} := f(x_n). Then x_n diverges to infinity.
>***

formalized using my declarative miz3 language for HOL Light
(to be run with "horizon := -1;;").

  let LASSE = thm `;
    let f be real->real;
    assume !x. f contl x;
    assume !x. f x > x;
    let x be num->real;
    assume !n. x (n + 1) = f (x n);
    thus !y. ?n. x n > y
    proof
      mono x by MONO_SUC,ADD1,REAL_LE_LT,real_ge,real_gt;
      cases;
      suppose convergent x;
        consider l such that x tends_num_real l by convergent;
        (\n. x n) tends_num_real f l
        proof
          (\n. x (SUC n)) = (\n. f (x n)) by ADD1,REWRITE_TAC;
          (\n. (\n. x n) (SUC n)) tends_num_real f l by CONTL_SEQ;
        qed by ONCE_REWRITE_TAC[SEQ_SUC] from -;
        x = (\n. x n) by ETA_AX;
      qed by SEQ_UNIQ,REAL_LT_REFL,real_gt;
      suppose ~convergent x;
        !n. x 0 <= x n
        proof
          x 0 <= x 0 [1];
          now [2] let n be num;
            assume x 0 <= x n;
            thus x 0 <= x (SUC n)
              by ADD1,REAL_LET_TRANS,REAL_LE_LT,real_gt;
          end;
        qed by INDUCT_TAC from 1,2;
      qed by SEQ_BCONV,SEQ_BOUNDED_2,real_le,real_gt;
    end`;;

So this uses 13 lemmas from the library (ADD1, CONTL_SEQ,
ETA_AX, MONO_SUC, real_ge, real_gt, REAL_LE_LT,
REAL_LET_TRANS, REAL_LT_REFL, SEQ_BCONV, SEQ_BOUNDED_2,
SEQ_SUC and SEQ_UNIQ), of which about half are just for
moving between SUC n and n + 1, and between <, >, <=, etc.
Statements of some of the more meaningful lemmas are:

  MONO_SUC;;
    !f. mono f <=> (!n. f (SUC n) >= f n) \/ (!n. f (SUC n) <= f n)
  CONTL_SEQ
    !f x l.
        f contl l /\ x tends_num_real l ==> (\n. f (x n)) tends_num_real f l
  SEQ_BCONV
    !f. bounded (mr1,(>=)) f /\ mono f ==> convergent f
  SEQ_BOUNDED_2;;
    !f k K. (!n. k <= f n /\ f n <= K) ==> bounded (mr1,(>=)) f
  SEQ_SUC
    !f l. f tends_num_real l <=> (\n. f (SUC n)) tends_num_real l

Freek