Isabelle/Isar（その21）

　0とは限らない自然数からの帰納法は，Nat.thyのdec_inductという定理となっています．

print_statement dec_induct

theorem dec_induct:
fixes i :: "nat"
and j :: "nat"
and P :: "nat ⇒ bool"
assumes "i ≤ j"
and "P i"
and "⋀n. i ≤ n ⟹ P n ⟹ P (Suc n)"
shows "P j"

thm dec_induct

?i ≤ ?j ⟹ ?P ?i ⟹ (⋀n. ?i ≤ n ⟹ ?P n ⟹ ?P (Suc n)) ⟹ ?P ?j

これをinductionのルールとして指定すれば

fun X :: "nat => real" where
  "X n  = (if 11 <= n then 2 * X (n - 1) + 1 else 0)"

に対して，直ちに

lemma "10 <= n ==> X n = 2 ^ n / 2 ^ 10 - 1"
  by (induction n rule: dec_induct, simp_all)

が通ります．