Isabelle/HOLの基本 その3

まず、全ての命題に名前を付ける必要があるのは不便だろう。直前に示した命題は this という名前で参照できる。 上の最初の部分は

  assume "surj f"
  from this have ...

と書き換えられる。

そしてthisを用いて

• then = from this

• thus = then show

• hence = then have

と定められているので、上の証明は次のように簡単に書ける。

  proof
    assume "surj f"
    hence "∀A. ∃a. A = f a" by (simp add: surj_def)
    hence "∃a. {x. x ∉ f x} = f a" by blast
    thus False by blast
  qed

また、 from のように使用する定理を前置するのではなく後置する方法もある。

• 'have' prop 'using' fact = 'from' fact 'have' prop

• 'have' prop 'with' fact = 'from' fact this 'have' prop

証明だけではなく補題ももう少し構造化された方法で宣言できる。

  lemma
    fixes f :: "'a => 'a set"
    assumes s: "surj f"
    shows False

• fixes は変数を固定し、型を宣言するために使う。通常省略することも多い。

• assumes/shows は仮定と結論を述べるために使う。仮定が複数ある場合はandで繋ぐ。

[| A; B; C |] ==> D を assumes A and B and C / shows D とかけるようになるということを覚えておけばよい。

ゴールが複数ある場合、proofのセクションをnextで区切って書く:

  lemma P
  proof
    ...
    show P1
  next
    ...
    show P2
  next
    ...
    show P3
  qed

existを使った定理から一時的に変数を束縛して使用するためにobtainを使う。

  have p: "∃x. P(x)" ...

  obtain x where k: "P (x)" using p by auto

obtain…where… それ自体命題の宣言なのでこれにも証明が必要なことに注意。 obtain以降の行では束縛したxが変数として使えるようになる。

宣言する命題の部分に is を用いて名前を付けることができる。(名前は ? から始める必要がある)

  show "form1 <--> form2" (is "?L <--> ?R")

このように名前をつけると、showの中のproof…qedセクションではform1の代わりに ?L などと書けるようになる。 このisはパターンマッチを行い、無視したい(利用しない)パターンはアンダーバーで潰すことができる。

また、showおよびlemmaの中では宣言した命題全体を ?thesis で参照できる。 つまり上の例では ?thesis は form1 <--> form2 のことである。

haveなどで示した命題は、名前をつけていなくてもクオートで囲むことで参照できる。

  have "x > 0"
  ...
  from `x > 0` ...

thenなどにより直前の命題は参照できるがそれ以前の命題は参照できない。 moreover/ultimatelyというキーワードを使うと、それまでに示された全ての命題を仮定に追加して証明ができる。

  have P1 ...
  moreover have P2 ...
  moreover
  ...
  moreover have Pn ...
  ultimatery have ..  (* ここで、P1 .. Pnの全ての命題が仮定に追加される *)

証明のスコープを明示するのに {} で囲むことができる。

  proof-
    { fix k
      assume ...
      ...
      have ... }
    then show ...　(* ここのthenでは直前のproof block {}部分全体を参照する *)

複数のゴールを示す際にnextで区切る代わりにproof blockを並べることもできる。

場合分けを行う場合、casesコマンドを用いてコンストラクタごとにゴールを分離する。 このときIsar proofでもcaseというキーワードで場合分けを使った証明を書くことができる。

  proof (cases xs)
    case Nil
    ...
  next
    case (Cons y ys)
    ...
  qed

これは帰納法を使った時も同じことが出来る。