Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] OFCLASS and locale.class

Email Gateway (Aug 19 2022 at 17:20):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,

I have the following setup:

• I have tactic which can derive locale-interpretations, e.g. "linorder less_eq_mytype less_mytype"
• I now want to conclude from this the "OFCLASS(mytype,linorder)" statement.

In Isar, I would easily do this by

lemma "OFCLASS(mytype,linorder)"
proof -
interpret linorder less_eq_mytype less_mytype by my_tactic
show ?thesis by (intro_classes, auto)
qed

However, perhaps there might be a smarter way of doing this which does not require the "interpret" command.

And my real question is, if the interpret is necessary, how to perform the above proof on the Isabelle/ML-level,
i.e., especially the "interpret" command.

Any help is appreciated.

Best regards,
René

Email Gateway (Aug 19 2022 at 17:21):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Rene,

• I have tactic which can derive locale-interpretations, e.g.
  "linorder less_eq_mytype less_mytype"
• I now want to conclude from this the "OFCLASS(mytype,linorder)" statement.

In Isar, I would easily do this by

lemma "OFCLASS(mytype,linorder)"
proof -
interpret linorder less_eq_mytype less_mytype by my_tactic
show ?thesis by (intro_classes, auto)
qed

However, perhaps there might be a smarter way of doing this which does not require the "interpret" command.

no, this is quite canonical. The »subclass« command does the same:

• Establish a proof obligation for an interpretation and give it to the
  user.

• From this, establish the subclass relation on the axclass level.

• Then establish the subclass dependency on the locale level.

And my real question is, if the interpret is necessary, how to perform the above proof on the Isabelle/ML-level,
i.e., especially the "interpret" command.

It is maybe best for setup a Isar proof goal from ML and then use
Expression.interpret.

You can also do this on a more fundamental level using something like
(Context.proof_map ooo Locale.add_registration) in a proof context, but
then you have to manually deal with all the subtle constracts of the
locale machinery. I would not recommend this in a first step.

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 17:21):

From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear Florian,

thanks for the hints, they are definitely helpful pointers to get started.
I'll try the Expression.interpret approach first. Still, it seems that I first
have to study the material in src/Pure/Isar/... and the Isabelle/Isar implementation
manual in more detail to understand what is going on there, and what are the important
methods for my purpose.

Enjoy the weekend,
René

Last updated: Nov 21 2024 at 12:39 UTC