問題タブ [isar]

Isabelle の書籍 [1] からトポロジーに関する一連の証明を形式化しようとしています。

位相空間 (X,T) は、「点」(任意の型 'a の要素) の集合 X と、T と呼ばれる X のサブセットの集合で構成されるという考えをエンコードしたいと思います。

• A1. 要素 p が X にある場合、T にも p を含む集合 N が少なくとも 1 つ存在します。
• A2. 集合 U と V が T 内にあり、p∈(U∩V) の場合、T 内の集合 N に N⊆(U∩V) と x∈N が存在する必要があります。(2 つのセットが交差する場合、交差をカバーする近傍が存在する必要があります)。

現在、私は次の定義を持っています：

ここまでは順調ですね。さまざまな定義を追加し、仮想topspaceインスタンスに関するさまざまな補題や定理を証明することができます。

しかし、実際に作成するにはどうすればよいでしょうか。誤解していない限り、これまで見てきたinstanceandinstantiateキーワードの例はすべて、ある特定の抽象クラス (または型またはロケール) が別の抽象クラスのインスタンスであることを宣言することに関するものだったようです。

セットの特定のペア (たとえばX={1::int, 2, 3}、T={X,{}}) が を形成することを Isabelle に伝えるにはどうすればよいtopspaceですか?

同様に、自分の定義を使用してX={1::int, 2, 3}, T={}、要件に適合しないことを証明するにはどうすればよいですか?

最後に、特定の具体的なオブジェクト X が a の定義を満たすことを示したら、X について証明するときに、topspace私が証明したすべての定義と定理を使用するようイザベルに指示するにはどうすればよいtopspaceでしょうか?

ところで、私はclassそれ以上よくわからないので使用しています。それが仕事に適したツールでない場合は、別のことを喜んで行います。

[1]: Dennis Sentilles による高度な数学への架け橋

ロケールの解釈に必要な証明で、構造体のいくつかのプロパティを使用したいと考えています。

例として、述語 P を定義し、述語を満たす要素に対する操作についていくつかの補題 (addは閉二項操作であり、結合的であり、中立要素addが存在する) を証明したとします。zeroaddP

次に、要素のセットを、ロケールを満たす構造として解釈したいと思います。monoid

しかし、私の証明の目標では、すべての要素が実際に述語を満たしていることを得ることができず、セット内の要素について既に証明したPような一般的な目標が残されています。add zero a = a

すべての要素が predicate を満たすことを目標に強制するにはどうすればよいPですか?

ロケールのパラメーターに何らかの定義があり、ロケールの仮定を書きやすく、読みやすく、理解しやすくする場合 (関数が非常に複雑であるため、仮定のステートメントまたはその名前が単純化されるため)仮定を読みやすく理解しやすくします)、その関数を定義する最良の方法は何ですか?

人為的な例として、関数を仮定のステートメントに組み込みたいとしfgます (もちろん、ここでは実際には役に立ちません)。

使用することを考えるかもしれませんdefines:

しかし、 locales.pdf ドキュメントは、それが非推奨であることを示唆しているようです(しかし、私にはわかりません):

下位互換性のために提供されているコンテキスト要素constrainsと を除いて、文法は完全です。defines

fgロケールのレンマにCtrl キーを押しながらホバリングすると、 defined_afteras という名前になりますconstant "local.fg"が、 in defined_duringit isfixed fg\nfree variableです。defined_after_defしかし、それは等しいことを達成しdefined_during_defます (つまり、後者には追加のパラメーターや仮定はありません)、3 番目のオプションはそうではありません:

ロケールと同じfgように、補題にも同じ Ctrl-hover テキストがあります。defined_during

Web サイトの PDF の 1 つまたは NEWS ファイルに何か記載されているのかもしれませんが、明らかなものは見つかりません。isar-ref.pdf は次のようにコメントしています。

assumes要素と要素の両方definesがロケール仕様に貢献します。パラメーターから派生した操作を定義する場合、definition通常は (§5.4) の方が適切です。

しかし、私はこの情報をどのように使用するかわかりません。おそらく、私が求めていることを実行してもあまり利益が得られない場合は、ロケールのように続行する必要があると言っているのでしょうdefined_after(引用符がdefinitionロケール定義内で使用できることを意味しない限り)。これは私が望んでいるものではありません。（余談ですが、この引用の最初の文はdefines、追加のパラメーターと仮定を導入する3番目のオプションと何らかの形で同等であることを私に示唆していたでしょうが、そうではありません。 it-appears-Isabelle-jargon 「ロケール仕様」とは、最初のオプションと 2 番目のオプションで Ctrl-hover テキストが異なる原因を説明することを意味しますが、私にはわかりません。)