0

我正在尝试从 Isabelle 的一本书 [1] 中形式化一系列关于拓扑的证明。

我想编码拓扑空间（X，T）由一组“点”（某种任意类型'a的元素）和一组X的子集（称为T）组成的想法，使得：

  • A1。如果元素 p 在 X 中，则在 T 中至少存在一个集合 N 也包含 p。
  • A2。如果集合 U 和 V 在 T 中，并且如果 p∈(U∩V)，则在 T 中一定存在集合 N，其中 N⊆(U∩V) 和 x∈N。（如果两个集合相交，则必须有一个邻域覆盖该相交。）。

目前我有以下定义：

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关键字的示例似乎都是关于声明一个特定的抽象类（或类型或语言环境）是另一个抽象类的实例。

我如何告诉 Isabelle 一对特定的集合（例如X={1::int, 2, 3}, T={X,{}}）形成一个topspace？

同样，我如何使用我的定义来证明X={1::int, 2, 3}, T={}不符合要求？

最后，一旦我证明一个特定的具体对象 X 符合 a 的定义，topspace我如何告诉 Isabelle 现在topspace在证明关于 X 的事情时使用我已经证明的所有定义和定理？

顺便说一句，我正在使用，class因为我不知道更好。如果它不是适合这项工作的工具，我很乐意做其他事情。

[1]：Dennis Sentilles通往高等数学的桥梁

4

2 回答 2

0

尽管语言环境是在微积分本身中实现的，因此它们的谓词可以用于任何常规命题，但通常不建议这样做。相反，您应该使用例如解释来实例化语言环境，如下例所示。

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)"

context
  fixes X⇩A T⇩A
  assumes X⇩A_eq: "X⇩A = {1, 2, 3 :: int}"
    and T⇩A_eq: "T⇩A = {{}, {1, 2, 3 :: int}}"
begin

interpretation example: topspace X⇩A T⇩A
  by standard (auto simp add: X⇩A_eq T⇩A_eq)

lemmas facts = example.A1 example.A2

end

thm facts

这种模式是否真正适合您的需求取决于您的应用程序；如果您只想拥有一个谓词，最好直接定义它而不使用语言环境。

注意：确实需要纯等式»≡«；更喜欢 HOL 等式 »=«，或其语法变体 »⟷«。

于 2018-10-21T15:55:00.153 回答
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 回答