isabelle - 定理に複数の名前を定義できますか?

Question

次の定理があるとします。

theorem non_ASCII_thm_name:
  "True"
  by simp

コマンドnon_ASCII_thm_nameのようなものでASCII名を定義したい。notationたとえば、次のようにします。

notation non_ASCII_thm_name ("ASCII_thm_name")

Isar コマンドはnotation、abbreviation定数でのみ使用できます。これを可能にする Isar コマンドはありますか?

できれば、Isar コマンドで提供したいのはシノニムだけです。たとえば、 を使用する場合、追加の事実 を使用しない定理sledgehammerが 1 つだけ存在することが望ましいでしょう。non_ASCII_thm_namesledgehammerASCII_thm_name

Answer 1

部分的な解決策は、次のコマンドを使用することです。

lemmas ASCII_thm_name = non_ASCII_thm_name

ASCII_thm_nameこれは、 と同じである と呼ばれる新しい定理を定義しますnon_ASCII_thm_name。

残念ながら、 などのツールがfind_theorems新しい名前を使用するという保証はありませんが、代わりに独自のヒューリスティックを使用して、ユーザーに出力する「最適な」名前を決定します。

の別の同義語はlemmasistheoremsですが、前者の方がより標準的なアプローチであると考えられています。