Example (18.1)

　前回の結果をより簡明に表すなら

g`~(?x y:num. &x / &y = sqrt (&2) )`;;

let lemma01=MESON[real_div; REAL_INV_0; REAL_MUL_RZERO]`x / y = z /\ y = &0 ==> z = &0`;;
let lemma02=REAL_FIELD`x / y = z /\ ~(y = &0) ==> x = y * z`;;
let lemma012=MESON[lemma01; lemma02]`!x y z. ~(z = &0) ==> (x / y = z ==> x = y * z)`;;
let lemma03=MESON[ARITH_RULE`&0< &2`; SQRT_POS_LT; REAL_POS_NZ]`~(sqrt(&2) = &0)`;;
let lemma0123=MESON[lemma012; lemma03]`!x y. x / y = sqrt(&2) ==> x = y * sqrt(&2)`;;
let lemma04=REAL_RING`x=y*z:real==>x*x=(z*z)*y*y`;;
let lemma05=MESON[ARITH_RULE`&0<= &2`; SQRT_POW_2; POW_2]`sqrt(&2) * sqrt(&2) = &2`;;

e(MESON_TAC[
lemma0123; lemma04; lemma05; REAL_MUL; REAL_INJ;
lemma01; lemma03; thm20120110_2] );;

0..0..1..2..8..18..43..102..209..415..828..1522..2863..5177..9204..16018..29216.
.solved at 29476
val it : goalstack = No subgoals

となります．

　tacticsを使うまでもなくMESONでＯＫですが，流れは

# g`~(?x y:num. &x / &y = sqrt (&2) )`;;
val it : goalstack = 1 subgoal (1 total)

`~(?x y. &x / &y = sqrt (&2))`

# e(REPEAT STRIP_TAC);;
val it : goalstack = 1 subgoal (1 total)

0 [`&x / &y = sqrt (&2)`]

`F`

# e(MP_TAC (MESON[lemma0123; lemma04; lemma05]`&x / &y = sqrt(&2) ==> &x * &x =
&2 * &y * &y`) THEN ASM_SIMP_TAC[REAL_MUL; REAL_INJ]);;
0..0..1..2..6..11..19..29..39..50..solved at 79
val it : goalstack = 1 subgoal (1 total)

0 [`&x / &y = sqrt (&2)`]

`~(x * x = 2 * y * y)`

# e(ASM_MESON_TAC[lemma01; lemma03; thm20120110_2]);;
0..0..1..2..8..17..solved at 23
val it : goalstack = No subgoals

と書いたほうが見やすいでしょう．

　どちらにせよ，分母を払う処理に手間が掛かります．すなわち，HOL Lightは

# REAL_INV_0;;
val it : thm = |- inv (&0) = &0

のような体系なので，例えば

`!x y z:real. x / y = z ==> x = z * y`

はthmではない(x=&1,y=z=&0)ことに注意せねばなりません．