isabelle - ケース分析によって生成された変数に名前を付けることができますか?

Question

場合分けや帰納法で生成される変数に自分の名前を付けることはできますか?

Answer 1

proof構造化された証明（キーワードで始まる）を使用している場合は、 casekeywoardを使用して、証明するケースを選択し、ケース分析/誘導によって作成された変数に名前を付けることができます。

lemma "length (rev xs) = length xs"
proof (induct xs)
  case Nil
  then show ?case ...
next
  case (Cons x xs)
  then show ?case ...
qed

ここcase (Cons x xs)で、リストが開始要素と残りのリストで構成されている場合（つまり、帰納法のステップ）を証明し、変数に名前を付けたいことをIsabelleに伝えxますxs。

プルーフブロックでは、コマンドでケースのリストを見ることができますprint_cases。

一方、apply-styleを使用している場合、これらの変数に直接名前を付ける方法はありません（また、この場合、自由変数の代わりに束縛変数を処理する必要があるため、case_tacの代わりに必要になる可能性があります）。最も外側のメタ定量化された変数の名前を変更するために使用できるcases方法があります。rename_tac

ほとんどのプロジェクト（L4.verifiedプロジェクトのようなプログラム検証の注目すべき例外を除く）では、一般的な証明スタイルは、ほとんど構造化された証明を使用することです。非構造化証明は探索に使用され、変数の名前を変更する必要があるほど複雑になることはめったにありません。