√2が有理数でないこと

チュートリアルにもありますが,以下は既存の定理や補題を統合する,普通の数学と同じ流儀の証明です.

let lem1 = PV9[SQRT_POS_LT; REAL_POS_NZ; ARITH; REAL_LT ]`~(sqrt (&2) = &0)`;;
let lem2 = MESON[REAL_INV_0; REAL_FIELD`~(x / y = &0) ==> ~(x = &0) /\ ~(inv y = &0)`; REAL_INJ]`~(&a / &b = &0) ==> ~(a = 0) /\ ~(b = 0)`;;
let lem12 = MESON[lem1; lem2]`&a / &b = sqrt (&2) ==> ~(a = 0) /\ ~(b = 0)`;;
let lem3 = PV9[GCD_COPRIME_EXISTS; GCD_ZERO; MULT_CLAUSES] `~(a = 0) /\ ~(b = 0) ==> ?a' b' g. a=a'*g /\ b=b'*g /\ coprime (a',b') /\ ~(a' = 0) /\ ~(b' = 0) /\ ~(g = 0)`;;
let lem4 = REAL_FIELD `~(x = &0) /\ ~(y = &0) /\ ~(z = &0) ==> (x*z)/(y*z)=x/y`;;
let lem1234 = PV9[IMP_TRANS lem12 lem3; lem4; REAL_INJ; REAL_MUL]`&a / &b = sqrt (&2) ==> (?a' b'. &(a') / &(b') = sqrt (&2) /\ coprime (a',b') /\ ~(a' = 0) /\ ~(b' = 0))`;;
let lem5 = SIMP_RULE [SQRT_POW_2; ARITH; REAL_LE; REAL_INJ; REAL_MUL] (REAL_FIELD `sqrt (&2) pow 2 = &2 /\ ~(&x = &0) /\ ~(&y = &0) /\ &x / &y=sqrt (&2) ==> &x * &x = &2 * &y * &y`);;
let lem6 = PV9 [EVEN_DOUBLE; EVEN_MULT; EVEN_MOD; EVEN_EXISTS; NUM_RING`(2 * m) * (2 * m) = 2 * b * b <=> b * b = 2 * m * m`; DIVIDES_2; ARITH_RULE `~(2=1)`; coprime] `a' * a' = 2 * b' * b' ==> ~(coprime (a',b'))`;;  
let lem123456 = PV9[lem1234; lem5; lem6]`~(?a b. &a / &b = sqrt (&2))`;; 
let lem7 = MESON[ABS_REFL; SQRT_POS_LE; ARITH; REAL_LE;]`abs(sqrt(&2))=sqrt (&2)`;;
PV9[lem123456; lem7; RATIONAL_ALT]`~rational (sqrt (&2))`;; 

-------- Proof 1 --------

THEOREM PROVED

------ process 2412 exit (max_proofs) ------
CPU time (user): 0.186999999991
val it : thm = |- ~rational (sqrt (&2))