100/sqrt.ml

   1 (* ========================================================================= *)
   2 (* Irrationality of sqrt(2) and more general results.                        *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;              (* For number-theoretic lemmas       *)
   6 needs "Library/floor.ml";;              (* For definition of rationals       *)
   7 needs "Multivariate/vectors.ml";;       (* For square roots                  *)
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Most general irrationality of square root result.                         *)
  11 (* ------------------------------------------------------------------------- *)
  12
  13 let IRRATIONAL_SQRT_NONSQUARE = prove
  14  (`!n. rational(sqrt(&n)) ==> ?m. n = m EXP 2`,
  15   REWRITE_TAC[rational] THEN REPEAT STRIP_TAC THEN
  16   FIRST_ASSUM(MP_TAC o AP_TERM `\x:real. x pow 2`) THEN
  17   SIMP_TAC[SQRT_POW_2; REAL_POS] THEN
  18   ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
  19   REPEAT(FIRST_X_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [integer])) THEN
  20   ASM_REWRITE_TAC[REAL_ABS_DIV] THEN DISCH_THEN(MP_TAC o MATCH_MP(REAL_FIELD
  21    `p = (n / m) pow 2 ==> ~(m = &0) ==> m pow 2 * p = n pow 2`)) THEN
  22   ANTS_TAC THENL [ASM_MESON_TAC[REAL_ABS_ZERO]; ALL_TAC] THEN
  23   REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_MUL; REAL_OF_NUM_EQ] THEN
  24   ASM_MESON_TAC[EXP_MULT_EXISTS; REAL_ABS_ZERO; REAL_OF_NUM_EQ]);;
  25
  26 (* ------------------------------------------------------------------------- *)
  27 (* In particular, prime numbers.                                             *)
  28 (* ------------------------------------------------------------------------- *)
  29
  30 let IRRATIONAL_SQRT_PRIME = prove
  31  (`!p. prime p ==> ~rational(sqrt(&p))`,
  32   GEN_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[] THEN
  33   DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP IRRATIONAL_SQRT_NONSQUARE) THEN
  34   REWRITE_TAC[PRIME_EXP; ARITH_EQ]);;
  35
  36 (* ------------------------------------------------------------------------- *)
  37 (* In particular, sqrt(2) is irrational.                                     *)
  38 (* ------------------------------------------------------------------------- *)
  39
  40 let IRRATIONAL_SQRT_2 = prove
  41  (`~rational(sqrt(&2))`,
  42   SIMP_TAC[IRRATIONAL_SQRT_PRIME; PRIME_2]);;