Isabelle/Isar（その20）

　次に帰納法の２つ目のサブゴールに移ります．

next
  case (Suc m)

と入力すると，Outputは

proof (state): step 7

this:
1 ≤ m ⟹ a m = 2 ^ m - 1
1 ≤ Suc m

goal (1 subgoal):
1. ⋀n. (1 ≤ n ⟹ a n = 2 ^ n - 1) ⟹ 1 ≤ Suc n ⟹ a (Suc n) = 2 ^ Suc n - 1

さらに使えるfactsをprint_factsで確認すると

facts:
:
a 1 = 1
1 ≤ Suc m
1 ≤ m ⟹ a m = 2 ^ m - 1
∀n. 1 ≤ n ⟹ a (Suc n) = 2 * a n + 1
Suc:
1 ≤ m ⟹ a m = 2 ^ m - 1
1 ≤ Suc m
Suc.IH: 1 ≤ m ⟹ a m = 2 ^ m - 1
Suc.prems: 1 ≤ Suc m
assms:
a 1 = 1
∀n. 1 ≤ n ⟹ a (Suc n) = 2 * a n + 1
this:
1 ≤ m ⟹ a m = 2 ^ m - 1
1 ≤ Suc m

となっています．これらから

show "?case"

すなわち

proof (prove): step 8

goal (1 subgoal):
1. a (Suc m) = 2 ^ Suc m - 1

を導く訳ですが，mについてはSuc.premsという当たり前のことしか判らず，Suc.IHを直ちに用いることはできませんので，mが0の場合と，1以上つまりSuc kと表せる場合とに分けて証明します．

　それには，上記の?caseに対して，自然数の変数mが0か否かで場合を分けるという方法を

proof (cases m "?case")

のように適用して，print_casesにより得られた場合を確認すると

cases:
  0:
    let "?case" = "a (Suc m) = 2 ^ Suc m - 1"
    assume "m = 0"
  Suc:
    fix nat_
    let "?case" = "a (Suc m) = 2 ^ Suc m - 1"
    assume "m = Suc nat_"

となっていますので

    case 0

と入力すれば，m = 0 がthisになるので

    thus "?case"
      using assms(1)

と入力すれば

proof (prove): step 12

using this:
  m = 0
  a 1 = 1

goal (1 subgoal):
 1. a (Suc m) = 2 ^ Suc m - 1

なので，そのまま

      by simp

と処理できます（これが事実上の帰納法のベースステップ）．引き続き

  next
    case (Suc k)
    thus "?case"
      using Suc.IH assms(2)

と入力すればOutputは

proof (prove): step 17

using this:
m = Suc k
1 ≤ ?n ⟹ a (Suc ?n) = 2 * a ?n + 1
1 ≤ m ⟹ a m = 2 ^ m - 1

goal (1 subgoal):
1. a (Suc m) = 2 ^ Suc m - 1

ですから，?nにSuc kつまり1以上であるmがマッチすることはsimpにも判り

      by simp
  qed

とすれば

show a (Suc m) = 2 ^ Suc m - 1
Successful attempt to solve goal by exported rule:
(1 ≤ ?m2 ⟹ a ?m2 = 2 ^ ?m2 - 1) ⟹
(1 ≤ Suc ?m2) ⟹ a (Suc ?m2) = 2 ^ Suc ?m2 - 1
proof (state): step 18

this:
a (Suc m) = 2 ^ Suc m - 1

goal:
No subgoals!

のように帰納法の２つ目のサブゴールが消えて

qed

とすれば証明が完成します．

　以上をまとめれば

lemma
  fixes "a" :: "nat => real" and "n" :: "nat"
  assumes "a 1 = 1" and "!!n. 1 <= n ==> a (Suc n) = 2 * a n + 1"
  shows "1 <= n ==> a n = 2 ^ n - 1"
proof (induction n)
  case 0
  thus "?case"
    by simp
next
  case (Suc m)
  show "?case"
  proof (cases m "?case")
    case 0
    thus "?case"
      using assms(1)
      by simp
  next
    case (Suc k)
    thus "?case"
      using assms(2) Suc.IH
      by simp
  qed
qed

となります．

　なお，単にa 1 = 1にするのが目的なら

lemma
"(a::nat=>real) 1 = 1 & (ALL n. a (Suc n) = 2 * a n + 1) --> a n = 2 ^ n - 1"
  by (induction n, auto)

あるいは

lemma
  fixes "a" :: "nat => real" and "n" :: "nat"
  assumes "a 0 = 0" and "ALL n. a (Suc n) = 2 * a n + 1"
  shows "a n = 2 ^ n - 1"
proof (induction n)
  case 0
  show "?case"
    using assms(1) by simp
next
  case (Suc m)
  thus "?case"
    using assms(2) by simp
qed

のようにすれば充分です．