Создание класса из конкретного объекта? - PullRequest
Новая
       66

Создание класса из конкретного объекта?

0 голосов
/ 06 июля 2018

Я пытаюсь формализовать серию доказательств о топологии из книги [1] в Изабель.

Я хочу закодировать идею, что топологическое пространство (X, T) состоит из набора X «точек» (элементов некоторого произвольного типа 'a) и набора подмножеств X, называемых T, таких, что :

  • A1. если элемент p находится в X, то существует по крайней мере один набор N в T, который также содержит p.
  • A2. если множества U и V находятся в T, и если p∈ (U∩V), то они должны существовать в множестве N в T, где 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 случаях.

Но как мне создать его? Если только я неправильно истолковываю вещи, примеры, которые я до сих пор видел для ключевых слов instance и instantiate, похоже, были посвящены объявлению того, что один конкретный абстрактный класс (или тип, или локаль) является экземпляром другого.

Как мне сказать Изабель, что конкретная пара наборов (например, X={1::int, 2, 3}, T={X,{}}) образует topspace?

Аналогично, как я могу использовать свое определение, чтобы доказать, что X={1::int, 2, 3}, T={} не соответствует требованиям?

Наконец, когда я показываю, что конкретный конкретный объект X соответствует определению topspace, как я могу сказать Изабель, чтобы теперь использовать все определения и теоремы, которые я доказал о topspace, при доказательстве X

Кстати, я использую class, потому что я не знаю ничего лучше. Если это не подходящий инструмент для работы, я с удовольствием сделаю что-нибудь еще.

[1]: Мост к углубленной математике Деннис Сентильес

Ответы [ 2 ]

0 голосов
/ 21 октября 2018

Хотя локали реализованы в самом исчислении и, следовательно, их предикаты могут использоваться в любом регулярном предложении, это обычно не рекомендуется.Вместо этого вам следует создавать экземпляры локалей, используя, например, интерпретацию, как в следующем примере. 

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

Подходит ли этот шаблон для ваших нужд, зависит от вашего приложения;если вы просто хотите иметь предикат, лучше определить его напрямую, без использования языкового стандарта.

Примечание: действительно нужно Pure равенство »≡«;предпочесть равенство HOL »=« или его синтаксический вариант »⟷«.

0 голосов
/ 10 июля 2018

Я добился здесь некоторого прогресса: class - это особый тип 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. (Locales.pdf, поставляемый с isabelle, покрывает это, но я не уверен, что пока не могу объяснить это своими словами). Во всяком случае, это работает: 

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

Я полагаю, что также возможно и, возможно, предпочтительнее выполнять всю эту работу внутри подобласти, но я не совсем определил синтаксис для этого.

...