prioritize_real();;

let rational = new_definition
  `rational(r) <=> ?p q. ~(q = 0) /\ (abs(r) = &p / &q)`;;
horizon := 1;;

let TOBIAS = thm `;
  let f be real->real;
  assume f(&0) = &1 [1];
  assume !x y. f(x + y + &1) = f x + f y [2];
  let r be real;
  assume rational r [3];
  thus f r = r + &1
  proof
    set g = \x. f(x) - &1;
    g(&0) = &0 [4] by 1,REAL_FIELD;
    now [5] let x be real;
      x + &1 = x + &0 + &1 by REAL_FIELD;
      g(x + &1) = (f x + f(&0)) - &1 by 2;
      thus ... = g x + &1 by 1,REAL_FIELD;
    end;
    now [6] let x be real;
      (x - &1) + &1 = x [7] by REAL_FIELD;
      g(x - &1) = (g(x - &1) + &1) - &1 by REAL_FIELD;
      thus ... = g(x) - &1 by 5,7;
    end;
    now [8] let x y be real;
      x + y = (x + y + &1) - &1 by REAL_FIELD;
      g(x + y) = (f x + f y) - &1 - &1 by 2,6;
      thus ... = g x + g y by 2,REAL_FIELD;
    end;
    now [9] let x be real;
      g(&0*x) = &0*(g x) [10] by 4,REAL_MUL_LZERO;
      now [11]
        let n be num;
        assume g(&n*x) = &n*(g x) [12];
        &(SUC n) = &n + &1 [13] by ADD1,REAL_OF_NUM_ADD;
        &(SUC n)*x = &n*x + x by REAL_FIELD;
        g(&(SUC n)*x) = &n*(g x) + g x by 8,12;
        thus ... = &(SUC n)*g x by 13,REAL_FIELD;
      end;
      thus !n. g(&n*x) = &n*g(x) by INDUCT_TAC,10,11;
    end;
    &1 = &0 + &1 /\ -- &1 = &0 - &1 by REAL_FIELD;
    g(&1) = &1 /\ g(-- &1) = -- &1 [14] by 4,5,6;
    consider n m such that ~(m = 0) /\ (abs r = &n/ &m) [15]
      by 3,rational;
    0 < m by ARITH_TAC;
    &0 < &m [16] by REAL_OF_NUM_LT;
    cases by REAL_FIELD;
    suppose &0 <= r;
      r = (&n* &1)/ &m [17] by 15,REAL_FIELD;
      &m*r = &n* &1 [18] by 16,REAL_FIELD;
      &m*g(r) = &n* &1 by 9,14,18;
      f r = r + &1 by 16,17,REAL_FIELD;
    qed;
    suppose r < &0;
      r = (&n*(-- &1))/ &m [19] by 15,REAL_FIELD;
      &m*r = &n*(-- &1) [20] by 16,REAL_FIELD;
      &m*g(r) = &n*(-- &1) by 9,14,20;
      f r = r + &1 by 16,19,REAL_FIELD;
    qed;
  end`;;