Isabelle/Isar（その27) - ATPとCASのこと

　Isabelleのマニュアルを斜め読みしていると，帰納法の例として，リストの形によるものが丁寧に書かれていますが，普通の数学の例は数列の和，しかもnat上での甘いものくらいなので，少し補います（リストも項数が有限の列と見ればよいのでしょうが）．

　複数個の仮定をとる（ように見える）タイプ．まず，数列xを定義します．

fun x :: "nat => real" where
  "x 0 = 0" | "x (Suc 0) = 2" | "x (Suc (Suc 0)) = 6" |
  "x (Suc (Suc (Suc n))) = 3 * x (Suc (Suc n)) - 3 * x (Suc n) + x n"

あとは，これまでと同じくx.inductを参照させれば．．．

lemma
  fixes n :: "nat"
  shows "x n = n * (n + 1)"
  by (induction n rule: x.induct, simp_all)

Outputは

Failed to finish proof:
goal (1 subgoal):
x n = real (n * (n + (1∷nat)))
1. ⋀n∷nat.
x (Suc (Suc n)) =
real (Suc (Suc (Suc (Suc (Suc (Suc (n + (n + (n + (n + (n + n * n))))))))))) ⟹
x (Suc n) = real (Suc (Suc (n + (n + (n + n * n))))) ⟹
x n = real n + real n * real n ⟹
(3∷real) *
real (Suc (Suc (Suc (Suc (Suc (Suc (n + (n + (n + (n + (n + n * n))))))))))) -
(3∷real) * real (Suc (Suc (n + (n + (n + n * n))))) +
(real n + real n * real n) =
real (Suc (Suc (Suc (Suc (Suc (Suc (Suc
(Suc (Suc (Suc (Suc (Suc (n + (n + (n + (n + (n + (n + (n + n * n)))))))))))))))))))
variables:
n :: nat

となります（笑）．これを見ると最後のreal (Suc ...の等式までは来ているので，HOL LightでのREAL，!n. &(SUC n) = &n + &1にあたる

thm real_of_nat_Suc

real (Suc (?n&#8759;nat)) = real ?n + (1&#8759;real)

を参照させれば

lemma x_n:
  fixes n :: "nat"
  shows "x n = n * (n + 1)"
  by (induction n rule: x.induct, simp_all add: real_of_nat_Suc)

print_statement x_n

Outputは

theorem x_n:
fixes n :: "nat"
shows "x (n∷nat) = real (n * (n + (1∷nat)))"

となります．