先のものでは SQRT_SOS[`a=sqrt x`]`&0 < x ==> (x = sqrt x <=> x = &1)`;;などが処理できないので，少し手を入れました． let SQRT_SOS sqrt tm = prove (tm, REPEAT STRIP_TAC THEN REPEAT (FIRST_X_ASSUM (fun t -> ASSUME_TAC (MATCH_MP REAL_LT_IMP_LE…

前回の平方根の消去をconversionにしてみました． let SQRT_SOS sqrt tm = prove (tm, REPEAT STRIP_TAC THEN REPEAT (FIRST_X_ASSUM (ASSUME_TAC o (MATCH_MP REAL_LT_IMP_LE))) THEN EVERY_ASSUM (MP_TAC o (MATCH_MP SQRT_POS_LE)) THEN MAP_EVERY ABBREV…

今回は平方根を含む不等式の変形です． g`!x y :real. &0 <= x ==> ( y <= sqrt x <=> y < &0 \/ (&0 <= y /\ y pow 2 <= x) )`;; e(REPEAT STRIP_TAC);; e(MP_TAC((UNDISCH o SPEC_ALL)SQRT_POS_LE));; e(ABBREV_TAC`z = sqrt x`);; e(ONCE_ASM_REWRITE_TAC…