(* ------------------------------------------------------------------------- *)
(* From Multivariate/misc.ml                                                 *)
(* ------------------------------------------------------------------------- *)

prioritize_real();;

let REAL_POW_LBOUND = prove                   
 (`!x n. &0 <= x ==> &1 + &n * x <= (&1 + x) pow n`,
  GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
  INDUCT_TAC THEN         
  REWRITE_TAC[real_pow; REAL_MUL_LZERO; REAL_ADD_RID; REAL_LE_REFL] THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_SUC] THEN     
  MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(&1 + x) * (&1 + &n * x)` THEN
  ASM_SIMP_TAC[REAL_LE_LMUL; REAL_ARITH `&0 <= x ==> &0 <= &1 + x`] THEN
  ASM_SIMP_TAC[REAL_LE_MUL; REAL_POS; REAL_ARITH
   `&1 + (n + &1) * x <= (&1 + x) * (&1 + n * x) <=> &0 <= n * x * x`]);;
                               
let REAL_ARCH_POW = prove   
 (`!x y. &1 < x ==> ?n. y < x pow n`,
  REPEAT STRIP_TAC THEN
  MP_TAC(SPEC `x - &1` REAL_ARCH) THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN
  DISCH_THEN(MP_TAC o SPEC `y:real`) THEN MATCH_MP_TAC MONO_EXISTS THEN
  X_GEN_TAC `n:num` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
  EXISTS_TAC `&1 + &n * (x - &1)` THEN
  ASM_SIMP_TAC[REAL_ARITH `x < y ==> x < &1 + y`] THEN
  ASM_MESON_TAC[REAL_POW_LBOUND; REAL_SUB_ADD2; REAL_ARITH
    `&1 < x ==> &0 <= x - &1`]);;

let ABS_CASES = thm `;
  !x. x = &0 \/ &0 < abs(x)`;;

let LL =  REAL_ARITH `&1 < k ==> &0 < k`;;

(* ------------------------------------------------------------------------- *)
(* Miz3 solutions to IMO problem from ICMS 2006.                             *)
(* ------------------------------------------------------------------------- *)

horizon := 0;;

let IMO_1 = thm `;
  !k. &1 < k ==> &0 < k [LL] by REAL_ARITH;
  now
    let f g be real->real;
    let x be real;
    assume !x y. f (x + y) + f (x - y) = &2 * f x * g y [1];
    assume ~(!x. f x = &0) [2];
    assume !x. abs (f x) <= &1 [3];
    now
      let k be real;
      assume sup (IMAGE (\x. abs (f x)) (:real)) = k [4];
      ~(IMAGE (\x. abs (f x)) (:real) = {}) /\ (?b. !x. abs (f x) <= b) [5]
        by ASM SET_TAC[],-,3;
      now
        assume !x. abs (f x) <= k [6];
        assume !b. (!x. abs (f x) <= b) ==> k <= b [7];
        now
          let y be real;
          assume &1 < abs (g y) [8];
          !x. abs (f x) <= k / abs (g y) [9]
            by ASM_MESON_TAC[REAL_LE_RDIV_EQ; REAL_ABS_MUL; LL;
              REAL_ARITH (parse_term
                "u + v = &2 * z /\\ abs u <= k /\\ abs v <= k ==> abs z <= k")
             ],-,1,6;
          ~(k <= k / abs (g y))
            by TIMED_TAC 2
              (ASM_MESON_TAC[REAL_NOT_LE; REAL_LT_LDIV_EQ; REAL_LT_LMUL;
                 REAL_MUL_RID; LL; REAL_ARITH (parse_term
                  "~(z = &0) /\\ abs z <= k ==> &0 < k")
                ]),LL,2,6,8;
          (!x. abs (f x) <= k / abs (g y)) /\ ~(k <= k / abs (g y))
            by CONJ_TAC,-,9;
          ((!x. abs (f x) <= k / abs (g y)) ==> k <= k / abs (g y)) ==> F
            by SIMP_TAC[NOT_IMP; NOT_FORALL_THM],-;
          thus F by FIRST_X_ASSUM(MP_TAC o
            SPEC (parse_term "k / abs(g(y:real))")),-,7;
        end;
        ~(?y. &1 < abs (g y)) by STRIP_TAC,-;
        thus !y. abs (g y) <= &1
          by SIMP_TAC[GSYM REAL_NOT_LT; GSYM NOT_EXISTS_THM],-;
      end;
      (!x. abs (f x) <= k) /\ (!b. (!x. abs (f x) <= b) ==> k <= b)
      ==> (!y. abs (g y) <= &1) by STRIP_TAC,-;
      (~(IMAGE (\x. abs (f x)) (:real) = {}) /\ (?b. !x. abs (f x) <= b)
       ==> (!x. abs (f x) <= k) /\ (!b. (!x. abs (f x) <= b) ==> k <= b))
      ==> (!y. abs (g y) <= &1) by ANTS_TAC,-,5;
      (~(IMAGE (\x. abs (f x)) (:real) = {}) /\
       (?b. !x. x IN IMAGE (\x. abs (f x)) (:real) ==> x <= b)
       ==> (!x. x IN IMAGE (\x. abs (f x)) (:real)
                ==> x <= sup (IMAGE (\x. abs (f x)) (:real))) /\
           (!b. (!x. x IN IMAGE (\x. abs (f x)) (:real) ==> x <= b)
                ==> sup (IMAGE (\x. abs (f x)) (:real)) <= b))
      ==> (!y. abs (g y) <= &1)
        by ASM_SIMP_TAC[FORALL_IN_IMAGE; EXISTS_IN_IMAGE; IN_UNIV],-,4;
      thus !y. abs (g y) <= &1
        by MP_TAC(SPEC (parse_term "IMAGE (\\x. abs(f(x))) (:real)") SUP),-;
    end;
    !y. abs (g y) <= &1
      by ABBREV_TAC (parse_term "k = sup (IMAGE (\\x. abs(f(x))) (:real))"),-;
    thus abs (g x) <= &1
      by SPEC_TAC ((parse_term "x:real"),(parse_term "y:real")),-;
  end;
  thus !f g. (!x y. f(x + y) + f(x - y) = &2 * f(x) * g(y)) /\
             ~(!x. f(x) = &0) /\ (!x. abs(f(x)) <= &1)
             ==> !x. abs(g(x)) <= &1 by REPEAT STRIP_TAC,-`;;

horizon := 1;;

let IMO_2 = thm `;
  let f g be real->real;
  assume !x y. f (x + y) + f (x - y) = &2 * f x * g y [1];
  assume ~(!x. f x = &0) [2];
  assume !x. abs (f x) <= &1 [3];
  thus !x. abs (g x) <= &1
  proof set s = IMAGE (\x. abs (f x)) (:real);
    ~(s = {}) [4] by SET_TAC;
    !b. (!y. y IN s ==> y <= b) <=> (!x. abs (f x) <= b) by IN_IMAGE,IN_UNIV;
    set k = sup s;
    (!x. abs (f x) <= k) /\ !b. (!x. abs (f x) <= b) ==> k <= b [5] by 3,4,SUP;
    assume ~thesis;
    consider y such that &1 < abs (g y) [6] by REAL_NOT_LT;
    &0 < abs (g y) [7] by REAL_ARITH;
    !x. abs (f x) <= k / abs (g y) [8]
    proof let x be real;
      abs (f (x + y)) <= k /\ abs (f (x - y)) <= k /\
      f (x + y) + f (x - y) = &2 * f x * g y by 1,5;
      abs (f x * g y) <= k by REAL_ARITH;
    qed by 7,REAL_ABS_MUL,REAL_LE_RDIV_EQ;
    consider x such that &0 < abs (f x) /\ abs (f x) <= k by 2,5,ABS_CASES;
    &0 < k by REAL_ARITH;
    k / abs (g y) < k by 6,7,REAL_LT_LMUL,REAL_MUL_RID,REAL_LT_LDIV_EQ;
  qed by 5,8,REAL_NOT_LE`;;

let IMO_3 = thm `;
  let f g be real->real;
  assume !x y. f (x + y) + f (x - y) = &2 * f x * g y [1];
  assume ~(!x. f x = &0) [2];
  assume !x. abs (f x) <= &1 [3];
  thus !x. abs (g x) <= &1
  proof
    now [4] let y be real;
      !x. abs (f x * g y pow 0) <= &1 [5] by 3,real_pow,REAL_MUL_RID;
      now let l be num;
        assume !x. abs (f x * g y pow l) <= &1;
        let x be real;
        abs (f (x + y) * g y pow l) <= &1 /\
        abs (f (x - y) * g y pow l) <= &1;
        abs ((f (x + y) + f (x - y)) * g y pow l) <= &2 by REAL_ARITH;
        abs ((&2 * f x * g y) * g y pow l) <= &2 by 1;
        abs (f x * g y * g y pow l) <= &1 by REAL_ARITH;
        thus abs (f x * g y pow SUC l) <= &1 by real_pow,REAL_MUL_RID;
      end;
      thus !l x. abs (f x * g y pow l) <= &1 by INDUCT_TAC,5;
    end;
    !x y. ~(x = &0) /\ &1 < abs(y) ==> ?n. &1 < abs(y pow n * x)
      by SIMP_TAC,REAL_ABS_MUL,REAL_ABS_POW,GSYM REAL_LT_LDIV_EQ,
        GSYM REAL_ABS_NZ,REAL_ARCH_POW;
  qed by 2,4,REAL_NOT_LE,REAL_MUL_SYM`;;