普通の数学ならTaylorの定理が簡単ですが，HOL Lightで書いてみると予想外に長くなりましたので，MVTを二重に使う方針にしました． (* f(x)<=f(p)+(x-p)*f'(p) *) let ass = ASM_SIMP_TAC[] THEN STRIP_TAC;; g`!a b:real f f' f'':real->real. a<b /\ (!x. a<=x /\ x<=b ==> (f diffl f</b>…

今回は私がHOL Lightで証明を書く際の環境？をご紹介します． OSはWindows，エディターは秀丸，OcamlはDOS窓内です． 秀丸はシェアウエアですが，軽快な作動と柔軟なカスタマイズ性，Cライクなマクロが特徴で，私は例えば，カーソルのある論理行をクリップボ…