let thm20120112=prove (`~(?x y. &x / &y = sqrt (&2) )`, REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o (MATCH_MP lemma08)) THEN SIMP_TAC[REAL_MUL; REAL_INJ] THEN MESON_TAC[thm20120110_2]);; 0..0..1..solved at 4 val thm20120112 : thm = |- ~(?…

let lemma05=MATCH_MP lemma03 lemma04;; 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[REA…

さらに計算系の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 = …