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

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

  •  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=,或其语法变体·。