inc_induct, exn2n

　それでは，次に，後ろ向きの帰納法を

find_theorems name: induct "?P (Suc ?n) ==> ?P ?n"

のように探してみると

searched for:
name: "induct"
"?P (Suc ?n) ⟹ ?P ?n"

found 4 theorem(s):

Nat.inc_induct:
?i ≤ ?j ⟹ ?P ?j ⟹ (⋀i. i < ?j ⟹ ?P (Suc i) ⟹ ?P i) ⟹ ?P ?i
Nat.strict_inc_induct:
?i < ?j ⟹
(⋀i. ?j = Suc i ⟹ ?P i) ⟹
(⋀i. i < ?j ⟹ ?P (Suc i) ⟹ ?P i) ⟹ ?P ?i
Nat.zero_induct: ?P ?k ⟹ (⋀n. ?P (Suc n) ⟹ ?P n) ⟹ ?P 0
Nat.zero_induct_lemma: ?P ?k ⟹ (⋀n. ?P (Suc n) ⟹ ?P n) ⟹ ?P (?k - ?i)

のようなものがあるので，ここではinc_inductを ?i = n, ?j = 2 ^ n として使います（incという名はP iを示すのにP (Suc i)を用いるからでしょう）．

　ということで補題として

lemma exn2n:
  "n <= 2 ^ n"

を設けます．これに近い定理はof_nat_less_two_powerなどが既にありますが，普通の帰納法ですので

proof (induct n)
  case 0 show ?case by simp
next
  case (Suc m)
  hence "Suc m <= 2 ^ m + 1" by simp
  also have "... <= 2 ^ Suc m" by simp
  finally show ?case .
qed

と片付けましょう．

　参考までにof_nat_less_two_powerと同じ内容のone line proofも書いておきます．

lemma "n <= 2 ^ n"
 by (induct n, simp, subgoal_tac "1 <= 2 ^ n", drule add_le_mono, auto)