Example (18)

今回は，以前(http://d.hatena.ne.jp/ehito/20111120)，num_WFを用いて証明した
　が有理数でないこと
です．

let lemma01=MESON[GCD_ZERO; GCD_COPRIME_EXISTS]
`~(a=0) ==> ?x y z. a=x*z /\ b=y*z /\ coprime(x,y)`;;
let lemma02=NUM_RING`~(x * z = 0) ==> ~(x=0) /\ ~(z=0)`;;
let lemma03=NUM_RING`(x * z) * x * z = 2 * (y * z) * y * z /\ ~(z=0) ==> x*x=2*y*y`;;
let lemma04=SPECL[`x:num`;`y:num`]COPRIME_BEZOUT_ALT;;
let lemma05=NUM_RING`x * x = 2 * y * y==>(x*x')*(x*x')=2*y*y*x'*x'`;;
let lemma06=NUM_RING`(y * y' + 1) * (y * y' + 1) = 2 * y * y * x' * x'<=>1+y*(2*y'+y*y'*y')=y*(2*y*x'*x')`;;
let lemma07=MESON[ARITH_RULE`1+y*a=y*b<=>y*b-y*a=1`;
SOS_RULE`y*b-y*a=y*(b-a):num`; ]
`1+y*a=y*b<=>y*(b-a)=1`;;
let lemma08=MESON[ARITH_RULE`x<=1 \/ 2<=x`;
SOS_RULE`x<=1==> ~(x*x=2)`;
SOS_RULE`2<=x==> ~(x*x=2)`; ]
`~(x*x=2)`;;

g`!a b. a*a=2*b*b ==> a=0`;;
e(REPEAT STRIP_TAC);;
e(DISJ_CASES_TAC(ARITH_RULE`a=0 \/ ~(a=0)`) THEN ASM_SIMP_TAC);;
e(MP_TAC lemma01 THEN ASM_SIMP_TAC THEN REPEAT STRIP_TAC);;
e(FIRST_X_ASSUM SUBST_ALL_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC);;
e(MP_TAC lemma02 THEN ASM_SIMP_TAC THEN REPEAT STRIP_TAC);;
e(MP_TAC lemma03 THEN ASM_SIMP_TAC THEN REPEAT STRIP_TAC);;
e(MP_TAC lemma04 THEN ASM_SIMP_TAC THEN REPEAT STRIP_TAC);;
e(MP_TAC lemma05 THEN ASM_SIMP_TAC[lemma06; lemma07; MULT_EQ_1]);;
e(DISJ_CASES_TAC(ARITH_RULE`~(y=1) \/ y=1`) THEN ASM_SIMP_TAC);;
e(MP_TAC lemma08 THEN ASM_SIMP_TAC[] THEN ARITH_TAC);;