HOL Light上で関数を定義する道具としては，new_definition(: term -> thm = )は既に述べましたが，例えば # let fib = new_definition `fib n = if n = 0 \/ n = 1 then 1 else fib(n - 1) + fib(n - 2)`;; Exception: Failure "new_definition: term not c…

m:numから始まる帰納法の原理numm_INDUCTIONを証明し，それを適用するtactic，INDUCTm_TACを定義しましょう． まずは肩慣らしに，1から始まるものを証明して見ます． g ( `!P. P 1 /\ (!n. 1 P n ==> P (SUC n) ) ==> (!n. 1 P n)` );; e ( STRIP_TAC THEN S…