miz3/Samples/tobias.ml

   1 prioritize_real();;
   2
   3 let rational = new_definition
   4   `rational(r) <=> ?p q. ~(q = 0) /\ (abs(r) = &p / &q)`;;
   5
   6 horizon := 1;;
   7
   8 let TOBIAS = thm `;
   9   let f be real->real;
  10   assume f(&0) = &1 [1];
  11   assume !x y. f(x + y + &1) = f x + f y [2];
  12   let r be real;
  13   assume rational r [3];
  14   thus f r = r + &1
  15   proof
  16     set g = \x. f(x) - &1;
  17     g(&0) = &0 [4] by 1,REAL_FIELD;
  18     now [5] let x be real;
  19       x + &1 = x + &0 + &1 by REAL_FIELD;
  20       g(x + &1) = (f x + f(&0)) - &1 by 2;
  21       thus ... = g x + &1 by 1,REAL_FIELD;
  22     end;
  23     now [6] let x be real;
  24       (x - &1) + &1 = x [7] by REAL_FIELD;
  25       g(x - &1) = (g(x - &1) + &1) - &1 by REAL_FIELD;
  26       thus ... = g(x) - &1 by 5,7;
  27     end;
  28     now [8] let x y be real;
  29       x + y = (x + y + &1) - &1 by REAL_FIELD;
  30       g(x + y) = (f x + f y) - &1 - &1 by 2,6;
  31       thus ... = g x + g y by 2,REAL_FIELD;
  32     end;
  33     now [9] let x be real;
  34       g(&0*x) = &0*(g x) [10] by 4,REAL_MUL_LZERO;
  35       now [11]
  36         let n be num;
  37         assume g(&n*x) = &n*(g x) [12];
  38         &(SUC n) = &n + &1 [13] by ADD1,REAL_OF_NUM_ADD;
  39         &(SUC n)*x = &n*x + x by REAL_FIELD;
  40         g(&(SUC n)*x) = &n*(g x) + g x by 8,12;
  41         thus ... = &(SUC n)*g x by 13,REAL_FIELD;
  42       end;
  43       thus !n. g(&n*x) = &n*g(x) by INDUCT_TAC,10,11;
  44     end;
  45     &1 = &0 + &1 /\ -- &1 = &0 - &1 by REAL_FIELD;
  46     g(&1) = &1 /\ g(-- &1) = -- &1 [14] by 4,5,6;
  47     consider n m such that ~(m = 0) /\ (abs r = &n/ &m) [15]
  48       by 3,rational;
  49     0 < m by ARITH_TAC;
  50     &0 < &m [16] by REAL_OF_NUM_LT;
  51     cases by REAL_FIELD;
  52     suppose &0 <= r;
  53       r = (&n* &1)/ &m [17] by 15,REAL_FIELD;
  54       &m*r = &n* &1 [18] by 16,REAL_FIELD;
  55       &m*g(r) = &n* &1 by 9,14,18;
  56       f r = r + &1 by 16,17,REAL_FIELD;
  57     qed;
  58     suppose r < &0;
  59       r = (&n*(-- &1))/ &m [19] by 15,REAL_FIELD;
  60       &m*r = &n*(-- &1) [20] by 16,REAL_FIELD;
  61       &m*g(r) = &n*(-- &1) by 9,14,20;
  62       f r = r + &1 by 16,19,REAL_FIELD;
  63     qed;
  64   end`;;
  65