Как мне написать алгебраический c cpos в качестве локали Изабель

Question

Я пытаюсь доказать известный факт, что существует стандартный способ построения algebriac_cpo из частичного порядка. Моя проблема в том, что я продолжаю получать сообщение об ошибке

Не удалось объединить тип: Нет заданного типа арности :: частичное_приказ

, и я не могу понять, что это значит.

Я думаю, что у меня есть отследил мою проблему до определения cpo. Определение работает, и я доказал различные результаты для него, но рабочая интерпретация part_order терпит неудачу с cpo.

   theory LocaleProblem imports  "HOL-Lattice.Bounds" 
begin
definition directed:: "'a::partial_order set ⇒ bool" where
 " directed a  ≡ 
    ¬a={} ∧ ( ∀ a1 a2. a1∈a∧ a2∈a ⟶ (∃ ub . (is_Sup {a1,a2} ub))) " 
class cpo = partial_order +
  fixes bot :: "'a::partial_order" ("⊥")
  assumes bottom: " ∀ x::'a. ⊥ ⊑ x "  
  assumes dlub:  "directed (d::'a::partial_order set)  ⟶ (∃ lub . is_Inf  d lub) "

print_locale cpo 

interpretation "idl" : partial_order
   "(⊆)::( ('b set) ⇒ ('b set) ⇒ bool) " 
  by (unfold_locales , auto) (* works *)

interpretation "idl" : cpo
   "(⊆)::( ('b set) ⇒ ('b set) ⇒ bool) " 
   "{}" (* gives error 
Type unification failed: No type arity set :: partial_order

Failed to meet type constraint:

Term:  (⊆) :: 'b set ⇒ 'b set ⇒ bool
Type:  ??'a ⇒ ??'a ⇒ bool *)

Любая помощь высоко ценится. Дэвид

Вы предложили два решения. Следуя работе Hennessy в Algebrai c Теория процессов "Я пытаюсь доказать (где I (A) - идеал, являющийся множествами)" Если is_apart_order, то I (A) является algebraic_cpo ", тогда я захочу чтобы применить результат к ряду семантик, дайте в виде наборов. Доза, которую ваш комментарий означает, что второе решение не является хорошей идеей?

Изначально у меня была проверенная лемма, которая началась

lemma directed_ran: "directed (d::('a::partial_order×'b::partial_order) set) ⟹   directed (Range d)"
proof (unfold directed_def) 

Первое решение хорошо началось:

context partial_order begin (* type 'a  is now a partial_order *)   
definition
  is_Sup :: "'a set ⇒ 'a ⇒ bool" where
  "is_Sup A sup = ((∀x ∈ A. x ⊑ sup) ∧ (∀z. (∀x ∈ A. x ⊑ z) ⟶ sup ⊑ z))"

definition directed:: "'a  set ⇒ bool" where
 " directed a  ≡ 
    ¬a={} ∧ ( ∀ a1 a2. a1∈a∧ a2∈a ⟶ (∃ ub . (is_Sup {a1,a2} ub))) " 

lemma directed_ran: "directed (d::('c::partial_order×'b::partial_order) set) ⟹   directed (Range d)"
proof - assume a:"directed d" 
  from a local.directed_def[of "d"]  (* Fail with message below *)

  show "directed (Range d)"

Увы, рабочая лемма теперь не работает: я переписал доказательства (развернуть local.directed_def), поэтому я исследовал и обнаружил, что хотя факт существования local.directed_def не может быть unified

Failed to meet type constraint:

Term:  d :: ('c × 'b) set
Type:  'a set

Я успешно изменил тип в утверждении леммы, но теперь не могу найти способ развернуть определение в доказательстве. Есть ли способ сделать это?

Второе решение снова начинается хорошо:

instantiation  set:: (type)  partial_order
begin
definition setpoDef: "a⊑(b:: 'a set) = subset_eq a  b"
instance proof 
   fix x::"'a set"     show " x ⊑ x" by (auto simp: setpoDef) 
  fix x y z::"'a set" show  "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z" by(auto simp: setpoDef)
  fix x y::"'a set" show "x ⊑ y ⟹ y ⊑ x ⟹ x = y"   by (auto simp: setpoDef)
qed     
end

, но следующий шаг не удался

instance proof 
  fix d show "directed d ⟶ (∃lub. is_Sup d (lub::'a set))"
  proof assume "directed d " with directed_def[of "d"]  show "∃lub. is_Sup d lub" 
      by (metis Sup_least Sup_upper is_SupI setpoDef)
  qed
next   
  from class.cpo_axioms_def[of "bot"]  show  "∀x . ⊥  ⊑ x " (* Fails *)
qed
end

первый подцель доказан, но показывает "∀x. ⊑ ⊑ x "хотя вырезать вставку из субгаля в выводе не совпадает с подцелью. Обычно на этом этапе необходимо добавить ограничения типа. Но я не могу найти ни одной этой работы. Знаете ли вы, что идет не так? Знаете ли вы если я смогу заставить Output показать информацию о типе в sugoal.

Answer 1

Команда interpretation действует на язык, который неявно объявляет определение класса типа. В частности, он не регистрирует конструктор типа как экземпляр класса типа. Вот для чего хороша команда instantiation. Поэтому во втором interpretation Изабель жалуется на то, что set не зарегистрирован как экземпляр partial_order.

, поскольку directed требует упорядочения только для одного экземпляра типа (а именно 'a) ), Я рекомендую переместить определение направленного в контекст языкового класса класса partial_order и удалить ограничение сортировки для 'a:

context partial_order begin
definition directed:: "'a set ⇒ bool" where 
  "directed a ≡ ¬a={} ∧ ( ∀ a1 a2. a1∈a∧ a2∈a ⟶ (∃ ub . (is_Sup {a1,a2} ub))) " 
end

(Это работает, только если is_Sup также определяется в контексте локали. Если нет, я рекомендую заменить условие is_Sup на a1 <= ub и a2 <= ub.)

Тогда вам не нужно ограничивать 'a в cpo определение класса типа, либо:

class cpo = partial_order +
  fixes bot :: "'a" ("⊥")
  assumes bottom: " ∀ x::'a. ⊥ ⊑ x "  
  assumes dlub:  "directed (d::'a set)  ⟶ (∃ lub . is_Inf  d lub)"

И, следовательно, ваша интерпретация не должна завершиться ошибкой из-за ограничений сортировки.

В качестве альтернативы, вы можете объявить set как экземпляр partial_order вместо того, чтобы интерпретировать класс типа. Преимущество состоит в том, что вы также можете использовать константы и теоремы, которым нужно partial_order в качестве ограничения сортировки, т. Е. Которые не были определены или доказаны в контексте языкового стандарта partial_order. Недостатком является то, что вам придется определять операцию класса типа внутри блока instantiation. Поэтому нельзя просто сказать, что следует использовать отношение подмножества; это должна быть новая константа. В зависимости от того, что вы собираетесь делать с экземпляром, это может не иметь значения или быть очень раздражающим.