Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to: Sublocales in Isabelle/ML

Email Gateway (Jul 05 2022 at 20:19):

From: Gebistorf Cedric <gecedric@student.ethz.ch>
Hello everyone,

I am currently trying to automate some Isabelle/HOL theories using Isabelle/ML. These theories use the 'sublocale’-Command at some point. Unfortunately, I am stuck (and I have been that for a while now) on how to generate a sublocale in Isabelle/ML.

Obviously I looked at the Isar-sublocale command and from there learned about the 'val sublocale_cmd: Expression.expression -> string defines -> local_theory -> Proof.state' command in the interpretation.ML file. Unfortunately, I am unable to correctly generate the first two arguments so that it would work.

Therefore my question: Could anyone give me a hint on how to generate a sublocale only in Isabelle/ML? Is the 'Interpretation.sublocale_cmd' the right approach or are there other functions that one should use?

More concretely, using an example from https://isabelle.in.tum.de/doc/locales.pdf): How would one generate the sublocale
'sublocale total_order ⊆ lattice
<Proof>'
using Isabelle/ML?

Cheers and thanks for your help,
Cedric

Email Gateway (Jul 06 2022 at 11:55):

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

a few hints what might help:

a) Note that the //⊆// is short for

context sub
begin

sublocale sup <proof>

end

b) The corresponding Isabelle/ML structure is roughly

setup ‹
Named_Target.init [] \<^locale>‹sub›
#> Interpretation.sublocale ([(\<^locale>‹sup›, (("", false),
(Expression.Positional [], [])))], []) []
#> Proof.global_skip_proof true
#> Local_Theory.exit_global
›

I am at a loss to explain what has to be inserted in the
»Proof.global_skip_proof true hole«, but maybe the documentation or the
ML source code is helpful.

c) Aside: The _cmd-Interfaces are extern in the sense that they are
parametrized with fragments from raw Isar source (roughly speaking).
Always use the proper interfaces when programming Isabelle/ML directly.

d) It is often helpful to present the bigger context where a problem is
encountered – then a change of perspective can often eliminate the
source of the problem entirely.

Hope this helps,
Florian
OpenPGP_signature

Last updated: Jan 04 2025 at 20:18 UTC