isabelle - イザベルのケース分析

Question

Isabelle でケース分析を適用するにはどうすればよいですか? apply (induct x)（誘導に使用される）に似たものを探していました。

Answer 1

ケース分析は通常、メソッドを使用して実行されます（Isabelle2014のIsabelle / Isarリファレンスマニュアルcasesのインデックスの「ケース（メソッド）」も参照してください）。初心者の方は、Isabelle/HOLでのプログラミングと証明のチュートリアルをお勧めします。

Isabelle 2014以降、ドキュメントはドキュメントパネルのIsabelle /jEditIDEでも利用できることに注意してください。