Isabelle の証明には 2 つのスタイルがあります。
apply (this method)
apply (that method)
ステートメント、および新しい「構造化された」Isar スタイル。私自身、どちらも役に立つと思います。「apply」スタイルはより簡潔なので、興味のない技術的な補題には便利ですが、「構造化」スタイルは主要な定理に便利です。
あるスタイルから別のスタイルに切り替えるのが好きな場合もあります。「適用」スタイルから「構造化」スタイルへの切り替えは簡単です。
proof -
私の適用チェーンで。私の質問は、「構造化」スタイルから「適用」スタイルに戻すにはどうすればよいですか?
より具体的な例を挙げると、5 つのサブゴールがあるとします。最初の 2 つのサブゴールをディスパッチするために、いくつかの「適用」命令を発行します。次に、構造化された証明を開始して、3 番目の証明を省きます。サブゴールが 2 つ残っています。これらのスタイルを「適用」するにはどうすればよいですか?