問題タブ [isabelle]

時々、私が適用スタイルの証明を書いているとき、私は証明方法 fooを次のように変更する方法を望んでいました

foo最初の目標を試してください。それが目標を解決するなら、良いです。それでも解決しない場合は、元の状態に戻して失敗します。

これは次のコードで発生しました：

さらに上に変更を加えると、への呼び出しsimpは目標を完全に解決できなくなり、ループします。私が次のようなものを指定できたら

または（代替案のsynatx）

または（おそらくさらに良い構文）

このスクリプトでは解決できなかった最初の目標で停止していました。

isabelle_afp多くの理論が保存されているディレクトリがあるとしましょう。このディレクトリはライブラリであり、その中のファイルを変更する予定はありません。Isabelle/jEdit の起動時間を短縮したい (デフォルトではisabelle_afp、現在の理論が依存しているすべての理論が新たに処理される)。

このステップをスキップするにはどうすればよいですか? システム マニュアルには、 persistent heap imageを構築するように指示されています。そうする最も簡単な方法は何ですか？

また、Isabelle/jEdit にこのヒープ イメージをロードするように指示するにはどうすればよいでしょうか?

l :: 'a list述語に一致する要素を一致させて削除したいP :: ('a => bool)

そのようなタスクを達成するための最良の方法は何ですか？役立つ可能性のある既存の機能をどのように見つけることができますか？

タプルを引数とする定義を作成したいと思います。

ただし、これは受け入れられません。エラーメッセージは

fun作品の代わりに使用しdefinitionていますが、これは私が望むものではありません。次の表記も機能しますが、やや醜いです。

タプルを引数として使用する最良の方法は何definitionですか？

次の補題を示したいとしましょう

私は目標を達成します

ただし、必要ありませんB。どうすれば私の目標を次のようなものに移すことができますか

元のステートメントを変更したくはありませんlemma。適用スタイルの現在の目標だけを変更します。

inductive内に実行可能ファイルを作成したいlocale。localeすべてが正常に動作しなければ:

ただし、 alocaleで同じことを試しても機能しません。

code_predロケールの行は次のエラーを返します。

codegenのドキュメント セクション「7.3 ロケールと解釈」によると、ロケールからのコードのエクスポートは少しトリッキーですが、実現可能です。次の例は正常に機能します。

複数のパラメーターを持つロケールのコードをエクスポートするにはどうすればよいですか? 以下を考えるとlocale：

私はそれを解釈することができます

しかし、この解釈を定義に使用することはできません

で失敗します

locale解釈せずに、定義から直接コードを生成したいと思っています。例：

インスタンス化する仮定MyTestは実行可能であり、それらのコードを生成できます

isInL任意の の定義を実行する関数を定義できますMyTest。

ただし、コードのエクスポートは失敗します。

なぜ私はそのようなことをしたいのですか？私は、eg hereに似ているが有限localeのコンテキストで a を使用しています。グラフが有効かどうかのテストは簡単です。ここで、グラフ アルゴリズムのコードを Scala にエクスポートしたいと考えています。もちろん、コードは任意の有効なグラフで実行する必要があります。valid_graph

次のような Scala の例えを考えています。

次のロケール定義を検討してください。

Isarでは、fまたはの見出語の定義を操作しようとするf_posと、ロケールの仮定と固定変数が表示されなくなります。たとえば、次をthm f_def f_pos返します。

予想通り。

ただし、MLでこれらの用語について推論しようとすると、「隠された」固定変数が突然公開されます。ML {* @{thm f_def} |> prop_of *}たとえば、次を返します。

ここで、固定変数aは関数のパラメーターになりますf。

MLのロケール内で作業して、そのようなロケール変数にさらされないようにする方法はありますか？

最近、適用スタイルの証明で不要な前提を削除する方法を学んだので、不要な変数を削除する方法を知りたいと思っています。つまり、私が目標を持っているとします

whereは、またはyには現れません。次のように変換するにはどうすればよいですか？ABC