[isabelle] Importing classes into a locale in Isabelle and other related questions



Dear All,

Approximately a week ago I posted a question on stack overflow with regard
to a possibility to import Isabelle classes into a locale. However, the
question has not been answered yet. Furthermore, the question received no
comments from the users of stack overflow. The question can be accessed via
the following link:
https://stackoverflow.com/questions/50085849/importing-classes-into-a-locale-in-isabelle-and-other-related-questions
.

Please find a copy of the statement of the question below:
*Question*

   - I would like to understand if there exists a simple method for
   importing classes into locales.
   - Alternatively, I would like to understand if there is a simple method
   that would enable me to use multiple types within the assumptions in
   classes.

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
<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-August/msg00237.html>
-
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

*Proposed solution*

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.

   - Also, please let me know if any of the information that is stated in
   the definition of the question is incorrect: I am new to Isabelle.

------------------------------
*General comments that are not directly related to the question*

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 why all four theories co-exist in HOL and the relationship
between these theories is not always clearly indicated.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.