問題タブ [isabelle]

イザベルでは、サブゴールが重複しているシナリオにたまに到達します。たとえば、次の証明スクリプトを想像してみてください。

目標を持って：

重複するサブゴールをインプレースで排除する方法はありますか？そのため、証明を繰り返す必要はありませんか？

私は次のイザベルの目標を持っています：

非常に単純であるにもかかわらず、戦術、、、、、などのいずれも目標を達成することはできませsimpん。fastclarsimpblastfastforce

なぜIsabelleはif、「a≠a」と「b≠b」の両方がになるように構成の本体を単純化してFalse、目標を解決しないのですか？

Isabelle で Scala コードを生成しています。Scala ファイルのヘッダーを指定するにはどうすればよいですか? たとえば、次のようなものが欲しいです。

使用するパッケージを指定するにはどうすればよいですか? たとえば、パッケージを使用するGENERATEDには、ファイルは単語で始まる必要がありますpackage GENERATED。

これまでに得た最良のアイデアは、code_include2 番目のパラメーターが空のコマンド ( "") です。より長い 2 番目のパラメーターを選択すると、Efficient_Nat理論は最初にそのコードを発行します。ただし、ファイルの先頭に書き込む必要があります。

この解決策はどれほど悪いですか？それほど悪くない場合、現在の日付、現在のあなたのファイル、および発生した行などをどのように追加できますexport_codeか。エクスポートしたコード方程式を追加することはできますが、それらの品位は追加できませんか?

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

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

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

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

補題があり、たとえばmylem: foo ?a = bar ?aが 2 回出現するゴールにそれを適用する必要があるとしますが、これらの位置の 1 つだけです。複雑な式になる可能性のある, ...をすべて書き出す必要なく、それを行う 2 つの方法を知っています。foobaz (foo (f p q)) (foo (g r s))pq

• 適切な数 (ここでは 0 または 1) のコマンドapply (subst mylem)が続きます。back
• を使用します。apply (subst mylem[where a = 'foo x y', standard])ここで、xおよびyはバインドされていない名前です。

ここでの使用はsubstデモンストレーションのためだけです。私は本当に補題を変更したいと思っています。たとえば、ruleこの方法で曖昧さをなくしたい複数の可能な一致がある場合に使用します。

どちらのアプローチも、私には悪いスタイルに見えます。それを達成するためのより良い方法はありますか？

コードジェネレーターを試しています。私の理論には、不変式をエンコードするデータ型が含まれています。

のコードをエクスポートしたいと思いますis_one。まず、コード ジェネレーターのデータ型を次のように設定する必要があるようです。

そして今is_one、抽象化に違反しないためのコード方程式を定義することができます:

質問 1:の定義をsmall_oneから引き出さないようにすることはできますis_oneか?

これで、小さなアイテムの複合値が得られました。

その形式では、それを使用してコードをエクスポートできません (「コード式 foo の抽象化違反...」)。

質問 2:[code abstract]そのような値のレンマを定義するにはどうすればよいですか? コード ジェネレーターは、形式の補題を受け入れないようmap to_nat foo = ...です。