File: Wellfounded_induction.ml

package info (click to toggle)
hol-light 20190729-4
  • links: PTS, VCS
  • area: main
  • in suites: bullseye
  • size: 42,676 kB
  • sloc: ml: 637,078; cpp: 439; makefile: 301; lisp: 286; java: 279; sh: 239; yacc: 108; perl: 78; ansic: 57; sed: 39; python: 13
file content (11 lines) | stat: -rw-r--r-- 577 bytes parent folder | download | duplicates (6) 
1
2
3
4
5
6
7
8
9
10
11
 
let NSQRT_2 = prove
 (`!p q. p * p = 2 * q * q ==> q = 0`,
  MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
  REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM `EVEN`) THEN
  REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
  DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o SPECL [`q:num`; `m:num`]) THEN
  ASM_REWRITE_TAC[ARITH_RULE
   `q < 2 * m ==> q * q = 2 * m * m ==> m = 0 <=>
    (2 * m) * 2 * m = 2 * q * q ==> 2 * m <= q`] THEN
  ASM_MESON_TAC[LE_MULT2; MULT_EQ_0; ARITH_RULE `2 * x <= x <=> x = 0`]);;