Example (20.1)

　先のものでは

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 t) THEN MP_TAC t)) THEN
  EVERY_ASSUM (MP_TAC o (MATCH_MP SQRT_POS_LE)) THEN
  MAP_EVERY ABBREV_TAC sqrt THEN
  REPEAT (FIRST_X_ASSUM (MP_TAC o (MATCH_MP SQRT_POW_2))) THEN
  ASM_SIMP_TAC[] THEN
  CONV_TAC REAL_SOS);;
let SQRT_SOS_TAC = CONV_TAC o SQRT_SOS;;

　これなら

# SQRT_SOS[`a=sqrt x`]`&0 < x ==> (x = sqrt x <=> x = &1)`;;
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Translating proof certificate to HOL
val it : thm = |- &0 < x ==> (x = sqrt x <=> x = &1)

となります．