Isabelle/Isar（その29）

　Isarの証明は対話的，つまりシステムが生成するサブゴールを次の目標とするのが基本ですが，過信は禁物です．例えば

lemma
  fixes a b :: "real"
  assumes "a + b = 0"
  shows "a < 0 | b <= 0"
proof

に対するOutputは

proof (state): step 1

goal (1 subgoal):
1. a < (0∷real)
variables:
a, b :: real

となり，確かに十分条件ではありますが，無理な相談です．これはproofによるイニシャルプルーフが(rule disjI1)となることが原因なので，人間が方針を決めねばなりません．

　まずは，プルーバーに任せてみましょう．

lemma
  fixes a b :: "real"
  assumes "a + b = 0"
  shows "a < 0 | b <= 0"
using assms by arith

通りました．simpには無理ですが，auto，forceなどでも通ります．

　次に，aについて場合を分けて見ます．つまり，a<0がTrue，Falseで分ける訳です．

lemma
  fixes a b :: "real"
  assumes "a + b = 0"
  shows "a < 0 | b <= 0"
proof (cases "a < 0")
  case True
  thus ?thesis ..
next
  case False
  hence "0 <= a" by simp
  with assms have "b <= 0" by simp
  thus ?thesis ..
qed

?thesisはシステムが結論に付ける別名で，caseの名前はprint_casesとすれば見られます．

　今度は，背理法です．

lemma
  fixes a b :: "real"
  assumes "a + b = 0"
  shows "a < 0 | b <= 0"
proof (rule ccontr)
  assume "~?thesis"
  hence "0 <= a & 0 < b" by simp
  hence "0 < a + b" by simp
  thus False using assms by simp
qed

　３つの場合を敢えて場合分けで処理するなら

lemma
  fixes a b c :: "real"
  assumes "a + b + c = 0"
  shows "a < 0 | b < 0 | c <= 0"
proof (cases "a < 0")
  case True thus ?thesis ..
next
  case False note na = this thus ?thesis
  proof (cases "b < 0")
    case True thus ?thesis
      by (intro disj_assoc disjI1 disjI2)
  next
    case False
    with na assms have "c <= 0" by arith
    thus ?thesis
      by (intro disj_assoc disjI2)
  qed
qed

２つ目，３つ目の?thesisの証明は勿論by simpでも構いません．