Попытка рассматривать классы и подтипы типов как наборы и подмножества

Question

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

Ниже, когда я использую обозначение фигурных скобок {0,0}, он не представляет нормальные скобки HOL, и 0 представляет пустой набор.

Некоторые файлы, если вы хотите их

• A_i130424a.thy - ASCII дружественный THY.
• i130424a.thy - не ASCII дружественный THY.
• i130424a_DOC.pdf - PDF с номерами строк.
• MFZ_DOC.pdf - Основной проект, с которым это связано.
• Папка GitHub для этого вопроса и папка MFZ GitHub.

Предварительный разговор

Я описываю, что я делаю в THY (который я включаю внизу), и затем я в основном спрашиваю: "Есть ли что-то, что я могу сделать здесь, чтобы исправить это, чтобы я мог использовать классы типов?"

Как и в вопросе SO, связанном с выше, я пытаюсь связать в Groups.thy semigroup_add, Что я делаю, это создаю подтип моего типа sT с помощью typedef, а затем я пытаюсь поднять некоторые из моих основных функций констант и операторов в новый тип, такой как мой оператор объединения geUмой пустой набор emSмоя неупорядоченная пара наборов paSи предикат моего членства inP,

Это не работает, потому что я пытаюсь рассматривать новый тип как подмножество. В частности, мой новый тип должен представлять множество { {0,0} }, которая предназначена быть частью тривиальной полугруппы, полугруппы только с одним элементом.

Проблема состоит в том, что аксиома неупорядоченной пары утверждает, что если установлено x существует, затем установите (paS x x) существует, и аксиома объединения утверждает, что если установлено x существует, затем установите (geU x) существует. Итак, когда я пытаюсь поднять моего оператора объединения в мой новый тип, испытатель волшебным образом знает, что мне нужно доказать (geU{0,0} = {0,0}), что не соответствует действительности, но есть только один элемент {0,0} в моем новом типе, так что это должно быть так.

Вопрос

Можно это исправить? На мой взгляд, я сравниваю наборы и подмножества с типами и подтипами, где я знаю, что они не совпадают. Назовите мой основной тип sT и мой подтип subT, Что мне нужно для всех моих операторов, которые были определены с типом sTтакие типы как sT => sT, чтобы работать для типа subT когда subT рассматривается как тип sT, Новые операторы и константы, которые были определены с использованием типа subT, например, функция типа subT => subT, это как-то сработало бы так, как будто вещи магически должны работать с этими вещами.

Опубликовать вопрос

Здесь я указываю, что происходит по номеру строки в THY. Номера строк будут отображаться в PDF и на сайте GitHub.

В строках с 21 по 71 есть четыре раздела, в которых я объединил связанные константы, обозначения и аксиому.

1. Тип sTпредикат членства inP/PInи аксиома равенства (от 21 до 33).
2. Пустой набор emS/SEm и пустая аксиома набора (от 37 до 45).
3. Неупорядоченная константа пары paS/SPa и неупорядоченная парная аксиома (от 49 до 58).
4. Союз постоянный geU/UGe и аксиома объединения (от 62 до 71).

Начиная со строки 75, я создаю новый тип с typedef а затем создать экземпляр класса semigroup_add,

Нет проблем, пока я не попытаюсь поднять функцию неупорядоченной пары {.x,y.}, строка 108, и моя функция объединения (geU x)линия 114.

Ниже команд Isar я показываю вывод, который говорит мне, что мне нужно доказать, что определенные наборы равны {0,0}Факт, который не может быть доказан.

Вот дружественный ASCII источник, где я удалил некоторые комментарии и строки из THY, связанные с выше:

theory A_i130424a
imports Complex_Main 
begin  

--"AXIOM (sT type, inP predicate, and the equality axiom)"
typedecl sT ("sT")

consts PIn :: "sT => sT => bool"

notation
  PIn  ("in'_P") and
  PIn  (infix "inP" 51) and
  PIn  (infix "inP" 51)

axiomatization where
  Ax_x: "(! x. x inP r <-> x inP s) <-> (r = s)"
--"[END]"



--"AXIOM (emS and the empty set axiom)"
consts SEm :: "sT" ("emS")

notation (input)
  SEm ("emS")

axiomatization where
  Ax_em [simp]: "(x niP emS)"
--"[END]"



--"AXIOM (paS and the axiom of unordered pairs)"
consts SPa :: "sT => sT => sT"

notation
  SPa ("paS") and
  SPa ("({.(_),(_).})")

axiomatization  where
  Ax_pa [simp]: "(x inP {.r,s.}) <-> (x = r | x = s)"
--"[END]"



--"AXIOM (geU and the axiom of unions)"
consts UGe :: "sT => sT"

notation
  UGe ("geU") and
  UGe ("geU")

axiomatization where
  Ax_un: "x inP geU r = (? u. x inP u & u inP r)"
--"[END]"



--"EXAMPLE (A typedef type cannot be treated as a set of type sT)"
typedef tdLift = "{x::sT. x = {.emS,emS.}}"
  by(simp)

setup_lifting type_definition_tdLift

instantiation tdLift :: semigroup_add
begin
  lift_definition plus_tdLift:: "tdLift => tdLift => tdLift"
    is "% x y. {.emS,emS.}" by(simp)
  instance
  proof
    fix n m q :: tdLift
    show "(n + m) + q = n + (m + q)"
    by(transfer,simp)
  qed
end

theorem
  "((n::tdLift) + m) + q = n + (m + q)"
  by(transfer,simp)

class tdClass =
  fixes emSc :: "'a"                 ("emSk")
  fixes inPc :: "'a => 'a => bool"   (infix "∈k" 51)
  fixes paSc :: "'a => 'a => 'a"     ("({.(_),(_).}k)")
  fixes geUc :: "'a => 'a"           ("⋃k")

instantiation tdLift :: tdClass
begin
  lift_definition inPc_tdLift:: "tdLift => tdLift => bool"
    is "% x y. x inP y" 
    by(simp)
  lift_definition paSc_tdLift:: "tdLift => tdLift => tdLift"
    is "% x y. {.x,y.}"
    --"OUTPUT: 1. (!! (sT1 sT2). ([|(sT1 = emS); (sT2 = emS)|] ==> ({.sT1,sT2.} = emS)))"
    apply(auto)
    --"OUTPUT: 1. ({.emS.} = emS)"
    oops
  lift_definition geUc_tdLift:: "tdLift => tdLift"
    is "% x. geU x"
    --"OUTPUT: 1. (!! sT. ((sT = {.emS,emS.}) ==> ((geU  sT) = {.emS,emS.})))"
    apply(auto)
    --"OUTPUT: 1. ((geU  {.emS,emS.}) = {.emS,emS.})"
    oops  
  lift_definition emSc_tdLift:: "tdLift"
    is "emS" 
    --"OUTPUT: 
       exception THM 1 raised (line 333 of drule.ML):
       RSN: no unifiers
       (?t = ?t) [name HOL.refl]
       ((emS = {.emS,emS.}) ==> (Lifting.invariant (% x. (x = {.emS,emS.})) emS emS))"
    oops
  instance ..
end
--"[END]"


end

Answer 1

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

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

(ОБНОВЛЕНИЕ: вероятным решением для моего использования классов типов будет комбинация идей, частью решения которых является приведение типов, как объяснено в ответе на мой вопрос SO: Что такое подтип Isabelle/HOL? Какие команды Isar создают подтипы?

Если использование локалей в Groups.thy является для меня способом, то соответствующие классы типов для этих локалей, вероятно, также будут работать. Я могу создать такой класс, как semigroup_add использовать lift_definition определить plus оператор, и даже поднять мои операторы, которые возвращают bool в тип. Операторы, которые не могут быть перенесены в новый тип, в любом случае несколько бессмысленны в контексте нового типа, в котором приведение типов может вступить в игру, чтобы понять их для таких вещей, как объединения множеств. Дьявол кроется в деталях.)

С тем, что я сказал, что я хочу из типов и подтипов, я понял, что я получаю форму этого с typedef форма является функцией Rep а также Abs с которым я немного поработал.

Как описано в isar-ref.pdf pg. 242,

Для typedef t = A вновь введенный тип t сопровождается парой морфизмов, чтобы связать его с представляющим множеством по старому типу. По умолчанию инъекция из типа в набор называется Rep t, а ее обратная абс...

Ниже я использую Rep а также Abs в небольшом примере, чтобы продемонстрировать, что я могу связать свой основной тип, sT, с новым типом, который я определяю с typedef, который является типом tsA,

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

1. могу ли я связать с локалями Groups.thy,
2. где это более широко касается использования типов для ограничения домена и совместной области бинарных операторов моих полугрупп, групп и т. д.

Например, в Groups.thy есть

locale semigroup =
  fixes f :: "'a => 'a => 'a" (infixl "*" 70)
  assumes assoc [ac_simps]: "a * b * c = a * (b * c)"

Если я не использую подтипы, я думаю, что мне придется сделать что-то вроде этого, где inP мой \<in> (Я только начинаю с локалей):

locale sgA =
  fixes G :: sT
  fixes f :: "sT => sT => sT" (infixl "*" 70)
  assumes closed:
    "(a inP G) & (b inP G) --> (a * b) inP G"
  assumes assoc:
    "(a inP G) & (b inP G) & (c inP G) --> (a * b) * c = a * (b * c)"

Часть ответа в возможности использовать Groups.semigroup может быть использование Rep а также Abs; Я использую оператор типа tsA => tsA => tsA по типу tsA, но когда элементы типа tsA должны рассматриваться как элементы типа sT тогда я использую Rep на них, чтобы сопоставить их, чтобы напечатать sT,

Я не продумал все это или не экспериментировал достаточно, чтобы знать, что будет работать лучше, но я дал этот частичный ответ, чтобы попытаться объяснить больше того, что у меня на уме. Там может быть кто-то еще с некоторой хорошей информацией, чтобы добавить.

Подтипный подход не может быть полностью положительным, как показано ниже двумя последними theorem Команды в примере кода. Левая сторона последствий необходима, потому что я не использую силу типов, аналогичную closed а также assoc выше в locale sgA, Однако, несмотря на это, это не проблема для моего simp правила, тогда как теоремы, которые используют Rep а также Abs требуют metis для доказательства, и это может потребовать много уродливых накладных расходов, чтобы заставить вещи работать более гладко.

Ниже я включаю файл A_iSemigroup_xp.thy. Это версия ASCII iSemigroup_xp.thy. Для этого требуется импортировать MFZ.thy, где эти 3 файла находятся в этой папке GitHub.

theory A_iSemigroup_xp
imports MFZ
begin
--"[END]"

--"EXAMPLE (Possible subtype for a trivial semigroup)"
typedef tsA = "{x::sT. x = emS}"
  by(simp)

theorem "(Rep_tsA x) inP {.Rep_tsA x.}"
  by(metis 
    SSi_exists)

theorem "! x::tsA. x = (Abs_tsA emS)"
  by(metis (lifting, full_types) 
    Abs_tsA_cases 
    mem_Collect_eq)

theorem "! x. x inP {.emS.} --> x = emS"
  by(simp)

theorem "! x. x inP {.z inP {.emS.} ¦ z = emS.} --> x = emS"
  by(simp)
--"[END]"

--"ISAR (Theory end)"
end