0

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 つのセットが交差する場合、交差をカバーする近傍が存在する必要があります)。

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

class topspace =
    fixes X :: "'a set"
    fixes T :: "('a set) set"
    assumes A1: "p∈X ≡ ∃N∈T. p∈N"
    assumes A2: "U∈T ∧ V∈T ∧ x∈(U∩V) ⟹ ∃N∈T. x∈N ∧ N⊆(U∩V)"
begin 
  (* ... *)
end

ここまでは順調ですね。さまざまな定義を追加し、仮想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 による高度な数学への架け橋

4

2 に答える 2

0

私はここでいくつかの進歩を遂げました: aclassは の特別なタイプですがlocale、この種の使用法には必要ありませんlocale。キーワードを直接使用すると、状況が少し単純化されます。すべてのロケールには、それをインスタンス化するために使用できる関連付けられた定理があります。

locale topspace =
    fixes X :: "'a set"
    fixes T :: "('a set) set"
    assumes A1 [simp]: "x∈X ≡ ∃N∈T. x∈N"
    assumes A2 [simp]: "U∈T ∧ V∈T ∧ x∈(U∩V) ⟹ ∃N∈T. x∈N ∧ N⊆(U∩V)"

theorem
  assumes "X⇩A={1,2,3::int}" and "T⇩A={{}, {1,2,3::int}}"
  shows "topspace X⇩A T⇩A"
  proof
    show "⋀U V x. U∈T⇩A ∧ V∈T⇩A ∧ x∈U∩V ⟹ ∃N∈T⇩A. x∈N ∧ N⊆U∩V"
     and "⋀x. x∈X⇩A ≡ ∃N∈T⇩A. x∈N" using assms by auto
  qed

宣言に使用したい場合definition、証明の目標はもう少し複雑になり、unfoldingキーワードを使用する必要があります。(isabelle に付属の locales.pdf はこれをカバーしていますが、まだ自分の言葉で説明できるかどうかはわかりません)。とにかく、これは動作します：

experiment
begin

  definition X⇩B where "X⇩B={1,2,3::int}"
  definition T⇩B where "T⇩B={{}, {1,2,3::int}}"

  lemma istop0: "topspace X⇩B T⇩B" proof 
    show "⋀U V x. U∈T⇩B ∧ V∈T⇩B ∧ x∈U∩V ⟹ ∃N∈T⇩B. x∈N ∧ N⊆U∩V" 
     and "⋀x. x∈X⇩B ≡ ∃N∈T⇩B. x∈N" unfolding X⇩B_def T⇩B_def by auto
  qed

end

このすべての作業をサブロケール内で行うことも可能であり、おそらく望ましいと思いますが、そのための構文はまだ完全には解明されていません。

于 2018-07-10T02:49:43.547 に答える