Isabelle/Isar（その21）

　さて，これまでは数列を定理の中で，言わば局所的に定義しましたが，セッション全体を通して大域的に定義すると，システムが証明に便利な定理を自動的に用意してくれます．

　まず，数列Xを次のように定義します．

fun X :: "nat => real" where
  "X 0 = 0" | "X (Suc n) = 2 * X n + 1"

１行目は見ての通り写像としてのタイプそして，２行目で帰納的定義を与えている訳ですが，ここでも，メタレベルの全称量化が略された（もしくはパターンマッチングを想定した開いた）式を用いる点が特徴で，その為，連言ではなく選言になっています（!! n. が全体に掛かっている）．

　このように定義すると，IsarはこのXに従う４つの定理を作成します．名前で検索すると．．．

find_theorems name: "X."

Outputは

searched for:
name: "X."

found 4 theorem(s):

Scratch.X.cases: (?x = 0 ⟹ ?P) ⟹ (⋀n. ?x = Suc n ⟹ ?P) ⟹ ?P
Scratch.X.induct: ?P 0 ⟹ (⋀n. ?P n ⟹ ?P (Suc n)) ⟹ ?P ?a0.0
Scratch.X.simps(1): X 0 = 0
Scratch.X.simps(2): X (Suc ?n) = 2 * X ?n + 1

これらはsimpで参照される属性を与えられているので，直ちに

lemma "X n = 2 ^ n - 1"
  by (induct n, simp_all)

が通ります．

　また，if then elseを用いて

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

のように定義することも出来，この場合の定理は

searched for:
name: "X."

found 3 theorem(s):

Scratch.X.cases: (⋀n. ?x = n ⟹ ?P) ⟹ ?P
Scratch.X.induct: (⋀n. (n ≠ 0 ⟹ ?P (n - 1)) ⟹ ?P n) ⟹ ?P ?a0.0
Scratch.X.simps: X ?n = (if ?n = 0 then 0 else 2 * X (?n - 1) + 1)

となりますが，上記のlemmaの証明はそのまま通ります．