Email Gateway (Aug 22 2022 at 17:13): Email Gateway (Aug 22 2022 at 17:13):From: xanonec xyz <xanonec@gmail.com>
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.
Email Gateway (Aug 22 2022 at 17:13):From: Akihisa Yamada <ayamada@trs.cm.is.nagoya-u.ac.jp>
Dear xanonec,
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
Best regards,
Akihisa
Email Gateway (Aug 22 2022 at 17:13):From: xanonec xyz <xanonec@gmail.com>
Dear Dr Akihisa Yamada,
Thank you for your reply. It seems that the solution that you have proposed
may be the best solution that is currently available because it was used in
HOL on several occasions. Anecdotally, it is possible that someone else has
struggled with the same problem - theory Dense_Linear_Order in the folder
HOL/Decision_Procs/ contains the following code:
locale linorder_stupid_syntax = linorder
begin
notation
less_eq ("op ⊑") and
less_eq ("(_/ ⊑ _)" [51, 51] 50) and
less ("op ⊏") and
less ("(_/ ⊏ _)" [51, 51] 50)
end
I have to admit that I thought that the problem is likely to be related to
notation before asking the question. However, I became slightly confused
after reading clause 5 in the following question:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-August/msg00237.html.
After reading clause 5 in the aforementioned question I thought that the
problem may not have a trivial solution and decided to postpone the
independent investigation until I receive a reply from the community.
If possible, I would like to provide a copy of your reply on stack
overflow. Please let me know if this is acceptable (of course, I will
provide a link to your original answer). Alternatively, please let me know
if you would prefer to provide an answer on stack overflow yourself or you
would prefer your answer not to be copied to stack overflow.
xanonec
Email Gateway (Aug 22 2022 at 17:16):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear xanonec,
to start with:
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 is a re-occuring topic on this mailing list, so let me quote from
an older post
(https://groups.google.com/forum/#!topic/fa.isabelle/kRHYNQ3uFCU/discussion):
as a rule of thumb, there are basically two algebraic hierarchy
developments in HOL:HOL-Main with type classes: * implicit use due to type inference * pragmatic and simple sharing between similar types * explicit definitions * directly executable
HOL-Algebra with locales: * explicit carrier – possibility to develop proper meta theory (*) * implicit definitions where possible * suitable for mathematics
(*) The meaning of »meta theory« in this context is roughly that you can
reason about algebraic structures, not only on properties of their
elements. For example, the classification of all simple groups would be
meta theory, whereas the statement »The integers form a group wrt. +, 0
and -« is not.
HOL/Library/Boolean_Algebra is somewhat special as it seems to be used
only in HOL-Word.
Concerning re-using classes in locales: classes carry only global
syntax: i.e. < always refers to the global constant less, but during
input / output occurences on local type 'a are replaces by the local
less (»user space type system«). Hence, when building a local upon a
class, syntax must be installed explicitly.
It might also be the case that you only want to take over some results
from an existing class; then it is usually better to formulate the
locale stand-alone and use a confined interpretation:
class c = …
locale l = … <operations, syntax, assumptions…>
begin
interpretation c: c … <proof>
lemma result1 = c.result1
lemma result2 = c.result2
…
end
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 17:17):From: xanonec xyz <xanonec@gmail.com>
Dear Dr Florian Haftmann,
Thank your comments.
The extracts from the post that is available on https://groups.google.com/
forum/#!topic/fa.isabelle/kRHYNQ3uFCU/discussion were helpful and provide
an explanation for the observation that I made in the concluding remarks of
my question.
Also, with the help of the previous answer and your comments, I believe I
have gained a certain level of understanding of the problem that is related
to the propagation of the notation/syntax from classes to locales. However,
I would also like to gain further understanding of the meaning and
significance of clause 5 in the post that is available on
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2014-August/msg00237.html
(I
could not find any comments on clause 5 within the post, although several
comments on other clauses were made):
Last updated: Nov 21 2024 at 12:39 UTC