Вопрос
- Я хотел бы понять, существует ли простой метод для импорта классов в локали.
- В качестве альтернативы я хотел бы понять, существует ли простой метод, который позволил бы мне использовать несколько типов в рамках предположений в классах.
Я хотел бы повторно использовать теоремы, которые связаны с определенными предопределенными классами в библиотеке HOL, для разработки моих собственных локалей. Тем не менее, мне кажется, что в настоящее время нет стандартных методов, которые позволили бы мне достичь этого (например, см. этот вопрос - пункт 5).
К сожалению, моя проблема потребует определения структур (то есть локалей или классов) с предположениями, которые используют несколько типов. Таким образом, я бы предпочел использовать локали. Однако я также хотел бы избежать дублирования кода и использовать структуры, которые уже существуют в библиотеке HOL, насколько это возможно.
theory my_theory
imports Complex_Main
begin
(*It is possible to import other classes, establish a subclass relationship and
use theorems from the super classes. However, if I understand correctly, it
is not trivial to ensure that multiple types can be used in the assumptions
that are associated with the subclass.*)
class my_class = order +
fixes f :: "'a ⇒ real"
begin
subclass order
proof
qed
end
lemma (in my_class) property_class: "⟦ x ≤ y; y ≤ z ⟧ ⟹ x ≤ z"
by auto
(*Multiple types can be used with ease. However, I am not sure how (if
it is possible) to ensure that the lemmas that are associated with the
imported class can be reused in the locale.*)
locale my_locale =
less_eq: order less_eq
for less_eq :: "'a ⇒ 'a ⇒ bool" +
fixes f :: "'a ⇒ 'b"
begin
sublocale order
proof
qed
end
sublocale my_locale ⊆ order
proof
qed
(*nitpick finds a counterexample, because, for example, less_eq is treated
as a free variable.*)
lemma (in my_locale) property_locale: "⟦ x ≤ y; y ≤ z ⟧ ⟹ x ≤ z"
by nitpick
end
Предлагаемое решение
В данный момент я думаю о переопределении минимального количества аксиом в моих собственных локалях, достаточного для установления эквивалентности между моими локалями и соответствующими классами в HOL. Однако такой подход приводит к некоторому дублированию кода:
theory my_plan
imports Complex_Main
begin
locale partial_order =
fixes less_eq :: "'a ⇒ 'a ⇒ bool" (infixl "≼" 50)
and less :: "'a ⇒ 'a ⇒ bool" (infixl "≺" 50)
assumes refl [intro, simp]: "x ≼ x"
and anti_sym [intro]: "⟦ x ≼ y; y ≼ x ⟧ ⟹ x = y"
and trans [trans]: "⟦ x ≼ y; y ≼ z ⟧ ⟹ x ≼ z"
and less_eq: "(x ≺ y) = (x ≼ y ∧ x ≠ y)"
begin
end
sublocale partial_order ⊆ order
proof
fix x y z
show "x ≼ x" by simp
show "x ≼ y ⟹ y ≼ z ⟹ x ≼ z" using local.trans by blast
show "x ≼ y ⟹ y ≼ x ⟹ x = y" by blast
show "(x ≺ y) = (x ≼ y ∧ ¬ y ≼ x)" using less_eq by auto
qed
sublocale order ⊆ partial_order
proof
fix x y z
show "x ≤ x" by simp
show "x ≤ y ⟹ y ≤ x ⟹ x = y" by simp
show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z" by simp
show "(x < y) = (x ≤ y ∧ x ≠ y)" by auto
qed
lemma (in partial_order) le_imp_less_or_eq: "x ≼ y ⟹ x ≺ y ∨ x = y"
by (simp add: le_imp_less_or_eq)
end
Считается ли подход, которому я собираюсь следовать, приемлемым стилем для развития библиотеки в Изабель? К сожалению, я не видел, чтобы этот подход использовался в контексте развития HOL. Тем не менее, я до сих пор не знаком с большой частью библиотеки.
- Также, пожалуйста, дайте мне знать, если какая-либо информация, указанная в определении вопроса, неверна: я новичок в Изабель.
Общие комментарии, не связанные напрямую с вопросом
Наконец, в качестве примечания я заметил, что в HOL может быть определенное количество частичного дублирования кода. В частности, мне кажется, что теории в HOL/Lattice/, HOL/Algebra/Order - HOL/Algebra/Lattice и HOL/Library/Boolean_Algebra напоминают теорию в HOL/Orderings - HOL/Lattices. Тем не менее, я не уверен, была ли эквивалентность между этими теориями установлена в рамках отношения субкласс / подкласс (например, см. class_deps) в достаточной степени. Конечно, я понимаю, что теории используют различные аксиоматизации и теории в HOL/Algebra/ и HOL/Library/Boolean_Algebra основаны на локалях. Кроме того, теории в HOL/Algebra/ содержат определенное количество информации, которая не была формализована в других теориях. Однако мне все же хотелось бы лучше понять, почему все четыре теории сосуществуют в HOL, и взаимосвязь между этими теориями не всегда четко обозначена.