10

次のような構造のイザベル証明があります。

proof (cases "n = 0")
  case True
  (* lots of stuff here *)
  show ?thesis sorry
next
  case False
  (* lots of stuff here too *)
  show ?thesis sorry
qed

最初のケースは実際には数ページの長さなので、2 番目のケースを読むと、カジュアルな読者には、私自身でさえ、何をFalse指しているのかが明確ではなくなります。(まあ、実際には ですが、読み取りからではなく、インタラクティブな環境でのみです。たとえば、Isabelle/jEdit でカーソルを の後に置くと、[出力] パネルの "this" の下にcase False表示されます。)n ≠ 0

「False」ケースの仮定を明示的にすることを可能にする構文があるので、読者は IDE とやり取りしたり、proofキーワードまでスクロールしたりする必要はありませんが、仮定を適切な場所で見ることができますか?

4

3 に答える 3

6

この場合、各ケースの仮定を明示的に述べると、証明がより読みやすくなります。

proof cases
  assume "n = 0"
  show ?thesis sorry
next
  assume "n ≠ 0"
  show ?thesis sorry
qed
于 2013-05-18T23:16:36.183 に答える
2

Isar では、同じテーマでさまざまなバリエーションを使用できます。元のアウトラインを維持しながら、次のように中間事実​​を明示できます。

proof (cases "n = 0")
  case True
  (* lots of stuff here *)
  from `n = 0` show ?thesis sorry
next
  case False
  (* lots of stuff here too *)
  from `n ≠ 0` show ?thesis sorry
qed

これは、元の証明のアウトラインを保守的に拡張したものです。つまり、チェック、統一、検索などのポリシーに変更を加えていません。

一般的に、フォーム

note `prop`

と同等です

have "prop" by fact
于 2013-10-09T19:39:32.310 に答える