[isabelle] Isabelle/ML - Theorem and Local Theories · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle/ML - Theorem and Local Theories

Email Gateway (Oct 16 2024 at 13:46):

From: "\"Marmsoler, Diego\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Makarius,

Thank you very much for your answer. It clarifies a lot.

I do have a follow up question, and I was wondering if someone could help me with that.

I am currently using the following function to retrieve the morphism:

fun get_morphism source target thy =
let
val dep = List.filter (fn x => #source x = source andalso #target x = target) (Locale.dest_dependencies [@{theory Main}] thy);
in
if (length dep) <> 1 then
error "Wrong number of dependencies"
else
#morphism (hd dep) |> Morphism.set_context thy
End

Basically, I use Locale.dest_dependencies to obtain all morphisms which are available in my theory (minus the once available in Main) and then I filter the one out with the correct source and destination.

This works for my purpose, but it does not feel like it is the correct way to do it, so I was wondering if there is a better way to do this?

In particular, I was wondering if there is an exposed function which does something like: "give me the morphism (dependency) of locale x for source y".

If there is no such function available, I was wondering if it could be useful to add one in the future?

Thanks for your help.

All the best,

Diego

-----Original Message-----
From: Makarius <makarius@sketis.net>
Sent: 12 August 2024 09:46
To: Marmsoler, Diego <D.Marmsoler@exeter.ac.uk>; isabelle-
users@cl.cam.ac.uk
Subject: Re: [isabelle] Isabelle/ML - Theorem and Local Theories

CAUTION: This email originated from outside of the organisation. Do not click
links or open attachments unless you recognise the sender and know the
content is safe.

On 09/08/2024 10:56, "Marmsoler, Diego" (via cl-isabelle-users Mailing List)
wrote:

I think I found what I was looking for in my previous question.

I was looking for the dependency morphism stored in the dependencies
field of a locale.

Morphisms are indeed the proper approach. How to get them is a different
question, though. My guess from a distance is that some of the locale
interpretation operations will do the job abstractly and robustly.

I guess it is often the case that a package generates some terms and
theorems and uses them later on to create some new terms and theorems.

From my limited experience with Isabelle/ML I can see at least the
following approaches to do so:

I can keep references to the terms and theorems and use morphisms to
later
transfer them into my current context.

#1 sounds fine, but where did the original types/terms/theorems come from?
Was that the original user input? If so, it often helps to maintain private
Theory_Data/Generic_Data for the package.

I can use Proof_Context.read_term_abbrev / Proof_Context.get_thm to
obtain
a reference by name.

#2 is very bad: it leads to fragile implementations. A proper value is a constant,
not some source text (or name) whose interpretation depends a lot on the
context.

At least for terms I can construct them manually using term constructors
(Const / Free / …)

#3 is ok in principle, but the proper way is to use ML antiquotations to produce
constants for types and terms, see also §2.2 in the "implementation"
manual with examples at the end of that section. There are also older forms of
direct use of Const with the "const_name" antiquotation: one day that might
become legacy.

A more ambitious form is the "instantiate" antiquotation (for
types/terms/props, certified types/terms/props, and thms). I did not find that
in the documentation on the spot, so the NEWS entry from Isabelle2022-1
needs to suffice:

"""
* ML antiquotation "instantiate" allows to instantiate formal entities (types,
terms, theorems) with values given ML. This works uniformly for "typ", "term",
"prop", "ctyp", "cterm", "cprop", "lemma" --- given as a keyword after the
instantiation.

(etc. including a few examples)
"""

Also for terms I could use Syntax.read_term to obtain a reference.

#4 is as bad like #2. Read/check operations are only valid for user input in the
application context.

Makarius

Email Gateway (Oct 16 2024 at 15:29):

From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Dear Diego,

One standard use case that works out of the box can be thought of as viewing the problem from "inside out”. Where by “inside” I mean inside of the locale.

You enter the locale you are interested in. There you operate and think relative to the “fixes” and “assumes” of that locale (including all ancestors).
Within that locale you write our Isabelle/ML code, which on the Isar toplevel could be via commands like “declaration” or for example “simproc_setup”. Those commands expect your Isabelle/ML code do be a function depending on a morphism “phi". Whenever you want to refer to some abstract entity of the locale, e.g. the fixes and assumes (or theorems) you can and usually should make use of “phi" to transform them from the abstract version to the concrete interpretation. E.g. if you have an assumption (or theorem) named foo in your locale you can transform it by "Morphism.thm phi @{thm foo}”. Note that as you are within the locale you can use the antiquotation mechanisms like @{thm …} to have static checks that you actually refer to what you mean.
Whenever the locale is interpreted (e.g. by “sublocale", “interpretation", new locales that have this locale as ancestor, …), the locale infrastructure of Isabelle automatically activates all the declarations (and simprocs) by supplying the proper “phi" to your declaration, simproc… So in case of the simproc there may be a lot of instances of the same simproc active at the same moment with different phi. That’s why it is important that you transform all abstract entities in step 2 by using Morphism.thm, Morphism.term etc.

So when your use case fits into this model of thinking, there is no need to worry about where to get the phi from. Generating all the necessary phi’s and applying them to all the “declarations” is done by the infrastructure. In this context a simproc is just a special kind of declaration. The more general “declaration” can also be used to work with custom Theory_Data / Generic_Data, as Makarius has pointed out. The core idea here is that in step 2 above you also use the phi at hand to transform that custom data.

Here is a small example from the AFP that illustrates this approach:

https://www.isa-afp.org/sessions/autocorres2_test/#Match_Cterm_Ex.html

Regards,
Norbert

Norbert Schirmer (nschirmer@apple.com)
 SEG Formal Verification

On 16. Oct 2024, at 11:54, Marmsoler, Diego (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:

Hi Makarius,

Thank you very much for your answer. It clarifies a lot.

I do have a follow up question, and I was wondering if someone could help me with that.

I am currently using the following function to retrieve the morphism:

fun get_morphism source target thy =
let
val dep = List.filter (fn x => #source x = source andalso #target x = target) (Locale.dest_dependencies [@{theory Main}] thy);
in
if (length dep) <> 1 then
error "Wrong number of dependencies"
else
#morphism (hd dep) |> Morphism.set_context thy
End

Basically, I use Locale.dest_dependencies to obtain all morphisms which are available in my theory (minus the once available in Main) and then I filter the one out with the correct source and destination.

This works for my purpose, but it does not feel like it is the correct way to do it, so I was wondering if there is a better way to do this?

In particular, I was wondering if there is an exposed function which does something like: "give me the morphism (dependency) of locale x for source y".

If there is no such function available, I was wondering if it could be useful to add one in the future?

Thanks for your help.

All the best,

Diego

-----Original Message-----
From: Makarius <makarius@sketis.net>
Sent: 12 August 2024 09:46
To: Marmsoler, Diego <D.Marmsoler@exeter.ac.uk>; isabelle-
users@cl.cam.ac.uk
Subject: Re: [isabelle] Isabelle/ML - Theorem and Local Theories

CAUTION: This email originated from outside of the organisation. Do not click
links or open attachments unless you recognise the sender and know the
content is safe.

On 09/08/2024 10:56, "Marmsoler, Diego" (via cl-isabelle-users Mailing List)
wrote:

I think I found what I was looking for in my previous question.

I was looking for the dependency morphism stored in the dependencies
field of a locale.

Morphisms are indeed the proper approach. How to get them is a different
question, though. My guess from a distance is that some of the locale
interpretation operations will do the job abstractly and robustly.

I guess it is often the case that a package generates some terms and
theorems and uses them later on to create some new terms and theorems.

From my limited experience with Isabelle/ML I can see at least the
following approaches to do so:

I can keep references to the terms and theorems and use morphisms to
later
transfer them into my current context.

#1 sounds fine, but where did the original types/terms/theorems come from?
Was that the original user input? If so, it often helps to maintain private
Theory_Data/Generic_Data for the package.

I can use Proof_Context.read_term_abbrev / Proof_Context.get_thm to
obtain
a reference by name.

#2 is very bad: it leads to fragile implementations. A proper value is a constant,
not some source text (or name) whose interpretation depends a lot on the
context.

At least for terms I can construct them manually using term constructors
(Const / Free / …)

#3 is ok in principle, but the proper way is to use ML antiquotations to produce
constants for types and terms, see also §2.2 in the "implementation"
manual with examples at the end of that section. There are also older forms of
direct use of Const with the "const_name" antiquotation: one day that might
become legacy.

A more ambitious form is the "instantiate" antiquotation (for
types/terms/props, certified types/terms/props, and thms). I did not find that
in the documentation on the spot, so the NEWS entry from Isabelle2022-1
needs to suffice:

"""
* ML antiquotation "instantiate" allows to instantiate formal entities (types,
terms, theorems) with values given ML. This works uniformly for "typ", "term",
"prop", "ctyp", "cterm", "cprop", "lemma" --- given as a keyword after the
instantiation.

(etc. including a few examples)
"""

Also for terms I could use Syntax.read_term to obtain a reference.

#4 is as bad like #2. Read/check operations are only valid for user input in the
application context.

Makarius

Email Gateway (Oct 16 2024 at 21:09):

From: "\"Marmsoler, Diego\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Norbert,

Thank you very much for your detailed answer.
I was just wondering if this use case also works if the locale is generated in Isabelle/ML using Expression.add_locale.

To be more precise, in my case the flow is roughly as follows:

* Proof a theorem using Goal.prove. This returns a reference to the proven theorem thm.
* Create a new locale using Expression.add_locale
* Use the original theorem reference thm to proof a new theorem within the context of the locale

When I tried this first, the proof in step 3 did not work but I got it to work by using the dependency morphism to transfer the original thm theorem into the context of the newly created locale.

All the best,

Diego

From: Norbert Schirmer <nschirmer@apple.com>
Sent: 16 October 2024 16:22
To: Marmsoler, Diego <D.Marmsoler@exeter.ac.uk>
Cc: isabelle-users@cl.cam.ac.uk
Subject: Re: [isabelle] Isabelle/ML - Theorem and Local Theories

CAUTION: This email originated from outside of the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe.

Dear Diego,

One standard use case that works out of the box can be thought of as viewing the problem from "inside out”. Where by “inside” I mean inside of the locale.

You enter the locale you are interested in. There you operate and think relative to the “fixes” and “assumes” of that locale (including all ancestors).
Within that locale you write our Isabelle/ML code, which on the Isar toplevel could be via commands like “declaration” or for example “simproc_setup”. Those commands expect your Isabelle/ML code do be a function depending on a morphism “phi". Whenever you want to refer to some abstract entity of the locale, e.g. the fixes and assumes (or theorems) you can and usually should make use of “phi" to transform them from the abstract version to the concrete interpretation. E.g. if you have an assumption (or theorem) named foo in your locale you can transform it by "Morphism.thm phi @{thm foo}”. Note that as you are within the locale you can use the antiquotation mechanisms like @{thm …} to have static checks that you actually refer to what you mean.
Whenever the locale is interpreted (e.g. by “sublocale", “interpretation", new locales that have this locale as ancestor, …), the locale infrastructure of Isabelle automatically activates all the declarations (and simprocs) by supplying the proper “phi" to your declaration, simproc… So in case of the simproc there may be a lot of instances of the same simproc active at the same moment with different phi. That’s why it is important that you transform all abstract entities in step 2 by using Morphism.thm, Morphism.term etc.

Here is a small example from the AFP that illustrates this approach:

https://www.isa-afp.org/sessions/autocorres2_test/#Match_Cterm_Ex.html

Regards,
Norbert

Norbert Schirmer (nschirmer@apple.com<mailto:nschirmer@apple.com>)
 SEG Formal Verification

On 16. Oct 2024, at 11:54, Marmsoler, Diego (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk>> wrote:

Hi Makarius,

Thank you very much for your answer. It clarifies a lot.

I do have a follow up question, and I was wondering if someone could help me with that.

I am currently using the following function to retrieve the morphism:

This works for my purpose, but it does not feel like it is the correct way to do it, so I was wondering if there is a better way to do this?

In particular, I was wondering if there is an exposed function which does something like: "give me the morphism (dependency) of locale x for source y".

If there is no such function available, I was wondering if it could be useful to add one in the future?

Thanks for your help.

All the best,

Diego

-----Original Message-----
From: Makarius <makarius@sketis.net<mailto:makarius@sketis.net>>
Sent: 12 August 2024 09:46
To: Marmsoler, Diego <D.Marmsoler@exeter.ac.uk<mailto:D.Marmsoler@exeter.ac.uk>>; isabelle-
users@cl.cam.ac.uk<mailto:users@cl.cam.ac.uk>
Subject: Re: [isabelle] Isabelle/ML - Theorem and Local Theories

CAUTION: This email originated from outside of the organisation. Do not click
links or open attachments unless you recognise the sender and know the
content is safe.

On 09/08/2024 10:56, "Marmsoler, Diego" (via cl-isabelle-users Mailing List)
wrote:

I think I found what I was looking for in my previous question.

I was looking for the dependency morphism stored in the dependencies
field of a locale.

Morphisms are indeed the proper approach. How to get them is a different
question, though. My guess from a distance is that some of the locale
interpretation operations will do the job abstractly and robustly.

I guess it is often the case that a package generates some terms and
theorems and uses them later on to create some new terms and theorems.

From my limited experience with Isabelle/ML I can see at least the
following approaches to do so:

I can keep references to the terms and theorems and use morphisms to
later

transfer them into my current context.

#1 sounds fine, but where did the original types/terms/theorems come from?
Was that the original user input? If so, it often helps to maintain private
Theory_Data/Generic_Data for the package.

I can use Proof_Context.read_term_abbrev / Proof_Context.get_thm to
obtain

a reference by name.

#2 is very bad: it leads to fragile implementations. A proper value is a constant,
not some source text (or name) whose interpretation depends a lot on the
context.

At least for terms I can construct them manually using term constructors
(Const / Free / …)

#3 is ok in principle, but the proper way is to use ML antiquotations to produce
constants for types and terms, see also §2.2 in the "implementation"
manual with examples at the end of that section. There are also older forms of
direct use of Const with the "const_name" antiquotation: one day that might
become legacy.

A more ambitious form is the "instantiate" antiquotation (for
types/terms/props, certified types/terms/props, and thms). I did not find that
in the documentation on the spot, so the NEWS entry from Isabelle2022-1
needs to suffice:

"""

ML antiquotation "instantiate" allows to instantiate formal entities (types,
terms, theorems) with values given ML. This works uniformly for "typ", "term",
"prop", "ctyp", "cterm", "cprop", "lemma" --- given as a keyword after the
instantiation.

(etc. including a few examples)
"""

Also for terms I could use Syntax.read_term to obtain a reference.

#4 is as bad like #2. Read/check operations are only valid for user input in the
application context.

Makarius

Email Gateway (Oct 17 2024 at 08:22):

From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Hi Diego,

I see. Indeed, in case the locale is not yet there in your Isar theory, it is not obvious how to put Isabelle/ML text within that locale. So you loose the convenience of antiquotations to refer to locale content at that point.

But the scenario you describe seems to be different. One central question is in which context “ctxt” do you make the Goal.prove.Is this also a locale context?
Note that the theorem you get out of Goal.prove lives within that ctxt that you supplied. So it depends very much on the ctxt to know where you can immediately use it. When you want to use that theorem in another context ctxt1 (like the locale you generate in step 2) the idea is that you first export the theorem from ctxt to the theory level and then import it to ctxt1. For the export there is Proof_Context.export but for the import there is no obvious Isabelle/ML API (as far as I know). My understanding of the current state of Isabelle is that the “import” is something that should be implicitly handled by the locale infrastructure. So here some ideas how to use what is there to do the import. One way I usually think about this is to think about how I would write down an example in the Isar top-level and then think about what happens in the background.

Here some sketch:

context some_locale_one
begin
…
lemma foo: ...
end

locale my_new_locale
begin

… here I want to use foo
end

You cannot directly use theorem foo in my_new_locale. What technically is available is the theory-level version some_locale_one.foo, which is a generalised version of foo with respect to the fixes / assumes of some_locale_one. So you can use that one, but then you have to discharge the assumptions by yourself.

The canonical way to access foo in my_new_locale is to do some kind of interpretation (or sublocale, …) command of some_locale_one inside my_new_locale. As a result you can access the interpreted version of foo potentially with a qualified name that you supplied with the interpretation. So this interpretation is the kind of automatic import of the theorem foo that the infrastructure provides.

Note that one important ingredient in the background is that the lemma foo above is not just a Goal.prove but more importantly it “notes” the theorem to the local theory, via a derivative of Local_Theory.note. This Local_Theory.note is one kind of “declaration” that I referred to in my last mail. Everything that is noted will then also be subject to interpretation and be automatically imported.

I routinely use the following idiom for such things in Isabelle/ML where I use named theorems and attributes to store the theorems.

named_theorems my_collection

context some_locale_one
begin
…
lemma foo[my_collection]: ...
end

locale my_new_locale
begin

… here I want to use foo
So I interprete some_locale_one and then use

Named_Theorems.get ctxt @{named_theorems my_collection}
end

Instead of the theorem name I use the more robust named theorems (via antiquotation named_theorems) to access the theorems in Isabelle/ML. You can also directly supply attributes like my_collection to Local_Theory.note.

This illustrates the general principle with the existing ingredients like named theorems and attributes.
For more ambitious and custom use cases there is the Local_Thoery.declaration which is more general than Local_Theory.note. With it you can implement your own approach to “store” and “retrieve” data. There are various applications of this technique in the AFP entry of AutoCorres2.

Regards,
Norbert

Norbert Schirmer (nschirmer@apple.com)
 SEG Formal Verification

On 16. Oct 2024, at 23:08, Marmsoler, Diego <D.Marmsoler@exeter.ac.uk> wrote:

Hi Norbert,

Thank you very much for your detailed answer.
I was just wondering if this use case also works if the locale is generated in Isabelle/ML using Expression.add_locale.

To be more precise, in my case the flow is roughly as follows:
Proof a theorem using Goal.prove. This returns a reference to the proven theorem thm.
Create a new locale using Expression.add_locale
Use the original theorem reference thm to proof a new theorem within the context of the locale

When I tried this first, the proof in step 3 did not work but I got it to work by using the dependency morphism to transfer the original thm theorem into the context of the newly created locale.

All the best,

Diego

From: Norbert Schirmer <nschirmer@apple.com <mailto:nschirmer@apple.com>>
Sent: 16 October 2024 16:22
To: Marmsoler, Diego <D.Marmsoler@exeter.ac.uk <mailto:D.Marmsoler@exeter.ac.uk>>
Cc: isabelle-users@cl.cam.ac.uk <mailto:isabelle-users@cl.cam.ac.uk>
Subject: Re: [isabelle] Isabelle/ML - Theorem and Local Theories

CAUTION: This email originated from outside of the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe.

Dear Diego,

One standard use case that works out of the box can be thought of as viewing the problem from "inside out”. Where by “inside” I mean inside of the locale.
1. You enter the locale you are interested in. There you operate and think relative to the “fixes” and “assumes” of that locale (including all ancestors).
2. Within that locale you write our Isabelle/ML code, which on the Isar toplevel could be via commands like “declaration” or for example “simproc_setup”. Those commands expect your Isabelle/ML code do be a function depending on a morphism “phi". Whenever you want to refer to some abstract entity of the locale, e.g. the fixes and assumes (or theorems) you can and usually should make use of “phi" to transform them from the abstract version to the concrete interpretation. E.g. if you have an assumption (or theorem) named foo in your locale you can transform it by "Morphism.thm phi @{thm foo}”. Note that as you are within the locale you can use the antiquotation mechanisms like @{thm …} to have static checks that you actually refer to what you mean.
3. Whenever the locale is interpreted (e.g. by “sublocale", “interpretation", new locales that have this locale as ancestor, …), the locale infrastructure of Isabelle automatically activates all the declarations (and simprocs) by supplying the proper “phi" to your declaration, simproc… So in case of the simproc there may be a lot of instances of the same simproc active at the same moment with different phi. That’s why it is important that you transform all abstract entities in step 2 by using Morphism.thm, Morphism.term etc.

So when your use case fits into this model of thinking, there is no need to worry about where to get the phi from. Generating all the necessary phi’s and applying them to all the “declarations” is done by the infrastructure. In this context a simproc is just a special kind of declaration. The more general “declaration” can also be used to work with custom Theory_Data / Generic_Data, as Makarius has pointed out. The core idea here is that in step 2 above you also use the phi at hand to transform that custom data.

Here is a small example from the AFP that illustrates this approach:

https://www.isa-afp.org/sessions/autocorres2_test/#Match_Cterm_Ex.html

Regards,
Norbert

--

Norbert Schirmer (nschirmer@apple.com <mailto:nschirmer@apple.com>)
 SEG Formal Verification

On 16. Oct 2024, at 11:54, Marmsoler, Diego (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk <mailto:cl-isabelle-users@lists.cam.ac.uk>> wrote:

Hi Makarius,

Thank you very much for your answer. It clarifies a lot.

I do have a follow up question, and I was wondering if someone could help me with that.

I am currently using the following function to retrieve the morphism:

fun get_morphism source target thy =
let
val dep = List.filter (fn x => #source x = source andalso #target x = target) (Locale.dest_dependencies [@{theory Main}] thy);
in
if (length dep) <> 1 then
error "Wrong number of dependencies"
else
#morphism (hd dep) |> Morphism.set_context thy
End

Basically, I use Locale.dest_dependencies to obtain all morphisms which are available in my theory (minus the once available in Main) and then I filter the one out with the correct source and destination.

This works for my purpose, but it does not feel like it is the correct way to do it, so I was wondering if there is a better way to do this?

In particular, I was wondering if there is an exposed function which does something like: "give me the morphism (dependency) of locale x for source y".

If there is no such function available, I was wondering if it could be useful to add one in the future?

Thanks for your help.

All the best,

Diego

-----Original Message-----
From: Makarius <makarius@sketis.net <mailto:makarius@sketis.net>>
Sent: 12 August 2024 09:46
To: Marmsoler, Diego <D.Marmsoler@exeter.ac.uk <mailto:D.Marmsoler@exeter.ac.uk>>; isabelle-
users@cl.cam.ac.uk <mailto:users@cl.cam.ac.uk>
Subject: Re: [isabelle] Isabelle/ML - Theorem and Local Theories

CAUTION: This email originated from outside of the organisation. Do not click
links or open attachments unless you recognise the sender and know the
content is safe.

On 09/08/2024 10:56, "Marmsoler, Diego" (via cl-isabelle-users Mailing List)
wrote:

I think I found what I was looking for in my previous question.

I was looking for the dependency morphism stored in the dependencies
field of a locale.

Morphisms are indeed the proper approach. How to get them is a different
question, though. My guess from a distance is that some of the locale
interpretation operations will do the job abstractly and robustly.

I guess it is often the case that a package generates some terms
[message truncated]

Email Gateway (Oct 17 2024 at 21:56):

From: "\"Marmsoler, Diego\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Norbert,

Ok, that is very useful, and indeed a solution to my problem (my situation is similar as you described just that my_new_locale actually imports some_locale_one which, however, should not make a big different here).

My solution so far is more in the direction of your first description: importing the theorem in my_new_locale using the dependency morphism from some_locale_one to my_new_locale (which in my case is possible since my_new_locale imports some_locale_one and thus there is a corresponding dependency morphism).
Now, the reason why I did it this way is that both, Goal.prove as well as Local_Theory.note, return the proven theorem which I then wanted to use as the reference for the theorem (instead of the name ecc).

However, if I understand your comments correctly, you suggest not to do this, but rather use the name (theorem name or, for more robust solution, Named_Theorem).
Is this correct?

Thanks again for all your comments!

All the best,

Diego

From: Norbert Schirmer <nschirmer@apple.com>
Sent: 17 October 2024 09:22
To: Marmsoler, Diego <D.Marmsoler@exeter.ac.uk>
Cc: isabelle-users@cl.cam.ac.uk
Subject: Re: [isabelle] Isabelle/ML - Theorem and Local Theories

CAUTION: This email originated from outside of the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe.

Hi Diego,

Here some sketch:

context some_locale_one
begin
…
lemma foo: ...
end

locale my_new_locale
begin

… here I want to use foo
end

I routinely use the following idiom for such things in Isabelle/ML where I use named theorems and attributes to store the theorems.

named_theorems my_collection

context some_locale_one
begin
…
lemma foo[my_collection]: ...
end

locale my_new_locale
begin

… here I want to use foo
So I interprete some_locale_one and then use

Named_Theorems.get ctxt @{named_theorems my_collection}
end

Regards,
Norbert

Norbert Schirmer (nschirmer@apple.com<mailto:nschirmer@apple.com>)
 SEG Formal Verification

On 16. Oct 2024, at 23:08, Marmsoler, Diego <D.Marmsoler@exeter.ac.uk<mailto:D.Marmsoler@exeter.ac.uk>> wrote:

Hi Norbert,

Thank you very much for your detailed answer.
I was just wondering if this use case also works if the locale is generated in Isabelle/ML using Expression.add_locale.

To be more precise, in my case the flow is roughly as follows:

When I tried this first, the proof in step 3 did not work but I got it to work by using the dependency morphism to transfer the original thm theorem into the context of the newly created locale.

All the best,

Diego

From: Norbert Schirmer <nschirmer@apple.com<mailto:nschirmer@apple.com>>
Sent: 16 October 2024 16:22
To: Marmsoler, Diego <D.Marmsoler@exeter.ac.uk<mailto:D.Marmsoler@exeter.ac.uk>>
Cc: isabelle-users@cl.cam.ac.uk<mailto:isabelle-users@cl.cam.ac.uk>
Subject: Re: [isabelle] Isabelle/ML - Theorem and Local Theories

CAUTION: This email originated from outside of the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe.

Dear Diego,

One standard use case that works out of the box can be thought of as viewing the problem from "inside out”. Where by “inside” I mean inside of the locale.

You enter the locale you are interested in. There you operate and think relative to the “fixes” and “assumes” of that locale (including all ancestors).
Within that locale you write our Isabelle/ML code, which on the Isar toplevel could be via commands like “declaration” or for example “simproc_setup”. Those commands expect your Isabelle/ML code do be a function depending on a morphism “phi". Whenever you want to refer to some abstract entity of the locale, e.g. the fixes and assumes (or theorems) you can and usually should make use of “phi" to transform them from the abstract version to the concrete interpretation. E.g. if you have an assumption (or theorem) named foo in your locale you can transform it by "Morphism.thm phi @{thm foo}”. Note that as you are within the locale you can use the antiquotation mechanisms like @{thm …} to have static checks that you actually refer to what you mean.
Whenever the locale is interpreted (e.g. by “sublocale", “interpretation", new locales that have this locale as ancestor, …), the locale infrastructure of Isabelle automatically activates all the declarations (and simprocs) by supplying the proper “phi" to your declaration, simproc… So in case of the simproc there may be a lot of instances of the same simproc active at the same moment with different phi. That’s why it is important that you transform all abstract entities in step 2 by using Morphism.thm, Morphism.term etc.

Here is a small example from the AFP that illustrates this approach:

https://www.isa-afp.org/sessions/autocorres2_test/#Match_Cterm_Ex.html

Regards,
Norbert

Norbert Schirmer (nschirmer@apple.com<mailto:nschirmer@apple.com>)
 SEG Formal Verification

On 16. Oct 2024, at 11:54, Marmsoler, Diego (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk>> wrote:

Hi Makarius,

Thank you very much for your answer. It clarifies a lot.

I do have a follow up question, and I was wondering if someone could help me with that.

I am currently using the following function to retrieve the morphism:

This works for my purpose, but it does not feel like it is the correct way to do it, so I was wondering if
[message truncated]

Email Gateway (Oct 18 2024 at 07:48):

From: Norbert Schirmer <cl-isabelle-users@lists.cam.ac.uk>
Hi Diego,

On 17. Oct 2024, at 23:56, Marmsoler, Diego (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:

However, if I understand your comments correctly, you suggest not to do this, but rather use the name (theorem name or, for more robust solution, Named_Theorem).
Is this correct?

This is the way that I figured out to by quite robust. My rational here being that this is how the Isar-Toplevel works so it should be a well established roundtrip. However, I fully understand your point that it is somehow feels quite indirect. You already have a theorem as ML value at hand and then kind of fall back to names or named theorems to refetch the “same” theorem but in another context.

My impression is that the Isabelle/ML API of this portion of Isabelle is very much motivated and tailored towards the Isar top-level. So everything that you need for that is well established and available. Other use cases might just not (yet) be equally well supported by Isabelle/ML. In your case you achieved to retrieve the Morphism phi you were interested in from some low level data, but as you have written it does not feel to be the intended way. So I agree that there seems to be some opportunities for more Isabelle/ML API at that point.

One further side remark from my experiences with working with those Morphisms. It can be quite costly to apply those morphisms. So when writing Isabelle/ML one should make deliberate choices when to apply them and avoid repeated applications. So when you already have an interpretation at hand (like in case of your locale) it might indeed be “cheaper” to just refetch it from the context via its (name / named theorems) as to apply the Morphism by hand.

Regards,
Norbert

Norbert Schirmer (nschirmer@apple.com)
 SEG Formal Verification

Email Gateway (Oct 18 2024 at 21:59):

From: "\"Marmsoler, Diego\"" <cl-isabelle-users@lists.cam.ac.uk>
Hi Norbert,

You already have a theorem as ML value at hand and then kind of fall back to names or named theorems to refetch the “same” theorem but in another context.

Indeed, this was my main concern, but your answer now clarified a lot.

In general, all your comments were very helpful and much appreciated!

Thanks, and all the best,

Diego

From: Norbert Schirmer <nschirmer@apple.com>
Sent: 18 October 2024 08:48
To: Marmsoler, Diego <D.Marmsoler@exeter.ac.uk>
Cc: isabelle-users@cl.cam.ac.uk
Subject: Re: [isabelle] Isabelle/ML - Theorem and Local Theories

CAUTION: This email originated from outside of the organisation. Do not click links or open attachments unless you recognise the sender and know the content is safe.

Hi Diego,

On 17. Oct 2024, at 23:56, Marmsoler, Diego (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk<mailto:cl-isabelle-users@lists.cam.ac.uk>> wrote:

However, if I understand your comments correctly, you suggest not to do this, but rather use the name (theorem name or, for more robust solution, Named_Theorem).
Is this correct?

Regards,
Norbert

Norbert Schirmer (nschirmer@apple.com<mailto:nschirmer@apple.com>)
 SEG Formal Verification

Last updated: Mar 09 2025 at 12:28 UTC