Isabelle/Isar（その28)

　次は

thm nat_less_induct

(⋀n∷nat. ∀m

を用いる例．任意の自然数は0か，2の自然数冪と奇数との積かの何れかであるという性質です．

lemma
  fixes n :: "nat"
  shows "n = 0 | (EX d m. n = 2 ^ d * m & odd m)"
proof (induction n rule: nat_less_induct)
  case (1 n)
  moreover
  have "odd n ==> (n = 2 ^ 0 * n & odd n)" by auto
  moreover
  have "even n ==> n = 0 | (EX k. n = 2 * k & k < n)"
    by presburger
  ultimately show ?case
    by (metis mult_assoc power_Suc mult_0_right)
qed

　caseの名前が1であることは，イニシャルプルーフのあと

print_cases

cases:
1:
fix n_
let "?case∷bool" =
"(n_∷nat) = (0∷nat) ∨ (∃(d∷nat) m∷nat. n_ = (2∷nat) ^ d * m ∧ odd m)"
assume
1.IH: "∀m

のように確認できます．

　そして，presburgerはその名の通り自然数についてのプルーバー，また

thm mult_assoc power_Suc mult_0_right

(?a∷?'a) * (?b∷?'a) * (?c∷?'a) = ?a * (?b * ?c)
(?a∷?'a) ^ Suc (?n∷nat) = ?a * ?a ^ ?n
(?m∷nat) * (0∷nat) = (0∷nat)

は帰納法の下請けの結果を元に戻した際に必要な計算規則です．

　なお，odd n | even n が不要なのは odd が ~even の別名であること(Parity.thy)をシステムが知っているからです．

　さらに，odd n の場合の結論は

thm power_0 nat_mult_1

(?a∷?'a) ^ (0∷nat) = (1∷?'a)
(1∷nat) * (?n∷nat) = ?n

から構成できるので

proof (induction n rule: nat_less_induct)
  case (1 n)
  moreover
  have "even n ==> n = 0 | (EX k. n = 2 * k & k < n)"
    by presburger
  ultimately show ?case
    by (metis mult_assoc power_Suc mult_0_right power_0 nat_mult_1)
qed

のようにmetisに任せても構いません．

　参考までに．．．HOL Lightでは

# EVEN_ODD_DECOMPOSITION;;
val it : thm = |- !n. (?k m. ODD m /\ n = 2 EXP k * m) <=> ~(n = 0)

のように実装されています．