代码之家 › 专栏 › 技术社区 › tangentstorm

从一个具体的对象实例化一个类?

isar isabelle

0

tangentstorm · 技术社区 · 6 年前

我试图将伊莎贝尔[1]一书中关于拓扑学的一系列证明形式化。

我想对拓扑空间(X,T)的概念进行编码,即拓扑空间(X,T)由一组X的“点”(某些任意类型的“a”元素)和一组X的子集(称为T)组成,这样:

A1。如果元素p在X中,那么T中至少有一个集合N也包含p。
A2。如果集合U和V在T中,如果p(UV)在T中,那么在集合N中必须存在N(UV)和xN。(如果两个集合相交,则必须有一个覆盖该相交的邻域。)。

目前我有以下定义:

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 实例。

但我如何真正创造一个呢?除非我误解了一些事情,否则我迄今为止看到的例子 instance 和 instantiate 关键字似乎都是关于声明一个特定的抽象类(或类型或区域设置)是另一个的实例。

我该怎么告诉伊莎贝尔 特指的 两套(例如。 X={1::int, 2, 3} , T={X,{}} )表格a 顶部空间 ?

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

最后,一旦我证明一个特定的具体对象X符合a的定义 顶部空间 ,我该如何告诉伊莎贝尔现在利用我已经证明的所有定义和定理 顶部空间 当证明X的事情时?

顺便说一句,我正在使用 class 因为我再也不知道了。如果这不是适合这份工作的工具,我很乐意做其他事情。

[1]: A Bridge to Advanced Mathematics 丹尼斯·森蒂利斯著

2 回复 | 直到 6 年前

1

0

tangentstorm 6 年前

我在这里取得了一些进展:a class 是一种特殊的 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

我相信在一个子区域内完成所有这些工作也是可能的,而且可能更可取,但我还没有完全弄清楚它的语法。

2

0

Florian Haftmann 6 年前

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

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

这种模式是否真的适合你的需要取决于你的应用;如果您只想拥有一个谓词,最好直接定义它,而不使用locale。

注:真正需要的是纯粹的平等;更喜欢HOL equality=,或其语法变体·。