I would like to reuse theorems that are associated with certain pre-defined classes in the library HOL for the development of my own locales. However, it seems to me that, at the moment, there are no standard methods that would allow me to achieve this (e.g. see this question - clause 5).
Unfortunately, my problem will require the definition of structures (i.e. locales or classes) with the assumptions that use multiple types. Thus, I would prefer to use locales. However, I would also like to avoid code duplication and reuse the structures that already exist in the library HOL as much as I can.
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
At the moment I am thinking about redefining the minimal amount of axioms in my own locales that is sufficient to establish the equivalence between my locales and the corresponding classes in HOL. However, this approach results in a certain amount of code duplication:
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
Is the approach that I intend to follow considered to be an acceptable style for the development of a library in Isabelle? Unfortunately, I have not seen this approach being used within the context of the development of HOL. However, I am still not familiar with a large part of the library.
Lastly, as a side note, I have noticed that there may be a certain amount of partial code duplication in HOL. In particular, it seems to me that the theories in HOL/Lattice/, HOL/Algebra/Order-HOL/Algebra/Lattice and HOL/Library/Boolean_Algebra resemble the theory in HOL/Orderings-HOL/Lattices. However, I am not certain if the equivalence between these theories was established through the sublocale/subclass relationship (e.g. see class_deps) to a sufficient extent. Of course, I understand that the theories use distinct axiomatisation and the theories in HOL/Algebra/ and HOL/Library/Boolean_Algebra are based on locales. Furthermore, the theories in HOL/Algebra/ contain a certain amount of information that has not been formalised in other theories. However, I would still like to gain a better understanding of why all four theories co-exist in HOL and the relationship between these theories is not always clearly indicated.
A solution to the problem was proposed on the mailing list of Isabelle by Akihisa Yamada and is available at the following hyperlink: link. A copy of the solution (with minor changes to formatting) is also provided below for a reference with the permission of the author.
It should be noted that the proposed solution has also been used in the context of the development of HOL.
let me comment to your technical questions as I also tackled the same goal as you. I'll be happy if there's a better solution, though.
lemma (in my_locale) property_locale: "⟦ x ≤ y; y ≤ z ⟧ ⟹ x ≤ z"
by nitpick
Interpreting a class as a locale doesn't seem to import notations, so here "≤" refers to the global one for "ord", which assumes nothing (you can check by ctrl+hover on x etc.).
My solution is to define a locale for syntax and interpret it (sublocale is somehow slow) whenever you want to use the syntax.
locale ord_syntax = ord
begin
notation less_eq (infix "⊑" 50)
notation less (infix "⊏" 50)
abbreviation greater_eq_syntax (infix "⊒" 50) where
"greater_eq_syntax ≡ ord.greater_eq less_eq"
abbreviation greater_syntax (infix "⊐" 50) where
"greater_syntax ≡ ord.greater less"
end
context my_locale begin
interpretation ord_syntax.
lemma property_locale: "⟦ x ⊑ y; y ⊑ z ⟧ ⟹ x ⊑ z" using less_eq.order_trans.
end