Isabelle/Isar（その19）

　premsを参照する例として

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"

の証明を考えます．これは自然数の成り立ちからすれば途中から始まる帰納法なので，やや面倒です．

　まず，assumesとshowsにメタの含意記号 ==>，assumesにメタの全称記号 !! がありますが，これらうちshowsを対象レベルの論理記号を用いて

  shows "1 <= n --> a n = 2 ^ n - 1"

とすると，premsに分解されず，対象レベルの含意全体が結論に設定されますので，例えば

proof (rule impI, induction n)

などとして，帰納法の適用以前にメタレベルの含意にする必要が生じます．assumesの方は

assumes "a 1 = 1" and "ALL n. 1 <= n --> a (Suc n) = 2 * a n + 1"

で構わないのですが，showsとの整合性からメタで書いています．

　では，先と同じく

proof (induction n)

と入力しましょう．するとサブゴールは

proof (state): step 1

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

となり，print_casesで場合分けの設定を見ると

cases:
0:
let "?case" = "a 0 = 2 ^ 0 - 1"
assume 0.prems: "1 ≤ 0"
Suc:
fix n_
let "?case" = "a (Suc n_) = 2 ^ Suc n_ - 1"
assume Suc.IH: "1 ≤ n_ ⟹ a n_ = 2 ^ n_ - 1" and Suc.prems: "1 ≤ Suc n_"

のように0.prems，Suc.premsが確認できます．

　そこで，１つ目のサブゴールに対して

  case 0

と入力すれば

proof (state): step 2

this:
1 ≤ 0

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

のように成り立たない1 ≤ 0が仮定なので，含意は成り立ち，そのまま

  thus "?case"
    by simp

とすれば

show a 0 = 2 ^ 0 - 1
Successful attempt to solve goal by exported rule:
(1 ≤ 0) ⟹ a 0 = 2 ^ 0 - 1

となります．なお，thusによりthisとして参照せず，fromなどを用いて0.premsを明示的に参照するには

  from "0.prems" show "?case"

のように " " が入用です．