Example (18.2)

　さらに計算系のproverの利用を控えるなら

let lemma01=MESON[real_div; REAL_INV_0; REAL_MUL_RZERO]
            `x / y = z /\ y = &0 ==> z = &0`;;
let lemma02=MESON[REAL_DIV_RMUL]
            `x / y = z /\ ~(y = &0) ==> x = z * y`;;
(*
let lemma02=REAL_FIELD
            `x / y = z /\ ~(y = &0) ==> x = z * y`;;
*)
let lemma03=MESON[lemma01; lemma02]
            `~(z = &0) ==> (x / y = z ==> x = z * y /\ ~(y = &0))`;;
let lemma04=MESON[ARITH_RULE`&0< &2`; SQRT_POS_LT; REAL_POS_NZ]
            `~(sqrt(&2) = &0)`;;
(*
let lemma04=MESON[LT_0; TWO; REAL_LT; SQRT_POS_LT; REAL_POS_NZ]
            `~(sqrt(&2) = &0)`;;
*)
let lemma05=MATCH_MP lemma03 lemma04;;
(*
let lemma05=MESON[lemma03; lemma04]
            `x / y = sqrt(&2) ==> x = sqrt(&2) * y /\ ~(y = &0)`;;
*)
g`x = sqrt(&2) * y  /\ ~(y = &0) ==> x * x = sqrt(&2) pow 2 * y * y  /\ ~(y = &0)`;;
e(REPEAT STRIP_TAC);;
e(ASM_SIMP_TAC[REAL_MUL_AC; POW_2]);;
e(ASM_MESON_TAC[]);;
let lemma06=top_thm();;
(*
MESON[REAL_MUL_AC; POW_2]`x = sqrt(&2) * y  /\ ~(y = &0) ==> x * x = sqrt(&2) pow 2 * y * y  /\ ~(y = &0)`;; でも行けるが．．．
let lemma06=REAL_RING `x = sqrt(&2) * y  /\ ~(y = &0) ==> x * x = sqrt(&2) pow 2 * y * y  /\ ~(y = &0)`;;
*)
let lemma07=MESON[REAL_POS; SQRT_POW_2]`sqrt(&2) pow 2 = &2`;;
(*
let lemma07=MESON[ARITH_RULE`&0<= &2`; SQRT_POW_2]
            `sqrt(&2) pow 2 = &2`;;
*)
let lemma08=CONV_RULE(REWRITE_CONV[lemma07])(IMP_TRANS lemma05 lemma06);;
(*
let lemma08=MESON[lemma05; lemma06; lemma07]`x / y = sqrt(&2) ==> x * x = &2 * y * y`;;
*)

g`~(?x y. &x / &y = sqrt (&2) )`;;
e(REPEAT STRIP_TAC);;
e(FIRST_X_ASSUM(MP_TAC o (MATCH_MP lemma08)) THEN SIMP_TAC[REAL_MUL; REAL_INJ]);;
e(MESON_TAC[thm20120110_2]);;
let thm20120112=top_thm();;