[isabelle] finite maps and lifting · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] finite maps and lifting

Email Gateway (Mar 23 2026 at 22:06):

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

Dear Isabelle Mailing List,

I have a question about using the lifting package together with finite maps (HOL-Library.Finite_Map). I am trying to define a copy of a simple fmap type as follows:

typedef myfmap =
"UNIV::((nat, nat) fmap) set"
..

However, when I attempt to set up the lifting package with

setup_lifting type_definition_myfmap

I encounter the following error:

exception THM 1 raised (line 2157 of "thm.ML"):
dest_state
Quotient (fmrel (=)) (fmmap id) (fmmap id) (fmrel (=))

If anyone has any insight into what I may be doing wrong, I would greatly appreciate your help.

Thanks and all the best,

Diego

Email Gateway (Mar 24 2026 at 16:18):

From: Alex Shkotin <alex.shkotin@gmail.com>

Hi Diego,

Meanwhile, have a look
https://chat.qwen.ai/s/t_056fc366-7d43-4103-9c8a-0436d8c1f96b?fev=0.2.16

Alex

вт, 24 мар. 2026 г. в 01:03, "Marmsoler, Diego" <
cl-isabelle-users@lists.cam.ac.uk>:

Dear Isabelle Mailing List,

I have a question about using the lifting package together with finite
maps (HOL-Library.Finite_Map). I am trying to define a copy of a simple
fmap type as follows:

typedef myfmap =
"UNIV::((nat, nat) fmap) set"
..

However, when I attempt to set up the lifting package with

setup_lifting type_definition_myfmap

I encounter the following error:

exception THM 1 raised (line 2157 of "thm.ML"):
dest_state
Quotient (fmrel (=)) (fmmap id) (fmmap id) (fmrel (=))

If anyone has any insight into what I may be doing wrong, I would greatly
appreciate your help.

Thanks and all the best,

Diego

Email Gateway (Mar 24 2026 at 16:58):

From: Makarius <makarius@sketis.net>

On 24/03/2026 17:18, Alex Shkotin wrote:

Meanwhile, have a look https://chat.qwen.ai/s/
t_056fc366-7d43-4103-9c8a-0436d8c1f96b?fev=0.2.16

Can someone who understands the issue please comment on the quality of the
machine-generated result?

Looking myself superficially, I am worried about two marginal details:

- "Updating to the latest Isabelle release." We did agree on this mailing
list recently that "latest" is very inaccurate and often misleading. Why is
there this interjection anyway?

- Double quotes everywhere to mark inner syntax. It is the traditional way
and still the majority style, but one happy day it will be discontinued to
have proper cartouches everywhere. Then double-quotes will also be free for
use inside HOL for string literals. Will that happy day be a sad day for tons
of machine-digested text?

Makarius

Email Gateway (Mar 24 2026 at 18:33):

From: Makarius <makarius@sketis.net>

On 24/03/2026 19:17, Lawrence Paulson wrote:

Most people are still using double quotes, but fortunately a simple regular expression substitution takes care of them.

I wasn't aware that they were deprecated. If it really is our intention then it needs to be made public.

On 24 Mar 2026, at 16:55, Makarius <makarius@sketis.net> wrote:

Will that happy day be a sad day for tons of machine-digested text?

Replacing the double-quotes properly is not so easy. For formally checked-text
it can be done reliably, based on authentic PIDE markup produced by
Isabelle/ML at the point where inner syntax is recognized. That will also work
for arbitrary nesting of embedded formal languages, e.g. in antiquotations.
That won't work for informal use of the same, because the markup is missing.

The traditional double-quoting of inner-syntax is not deprecated yet, just a
bit old-fashioned: I use it myself routinely, but not universally.

A few very elite users have switched their formal live to Isabelle cartouches
already some years ago. It looks better and is more robust. Disadvantage: It
is not immediately clear how to input it, despite the Isabelle/jEdit
completion on the " character. The German and French keyboards should also
have a standard mapping for it that I never know.

Makarius

Email Gateway (Mar 24 2026 at 20:06):

From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>

Hi Makarius and Diego,

On 24 Mar 2026, at 17.55, Makarius <makarius@sketis.net> wrote:

Can someone who understands the issue please comment on the quality of the machine-generated result?

I took this as a challenge. The answer by QWEN was mostly nonsense — of course setup_lifting should work with type copies via type definition. Mainly any chatbot used on the internet lacks access to the Isabelle sources and the ability to search them and try things out. Below is the transcript with better local setup using OpenCode+GPT 5.4 via Github Copilot and AWS’s Isabelle/Q (MCP interface)—thanks @Kevin Kappelmann for recommending this setup.

After some back and forth and some nudges into the right direction, the model found a working workaround for the issue. At the end the LLM also suggested writing a reply to the mailing list, which I replicate below. I think this reply might be the weakest point in the overall conversation (next to the moment when the model tried reading my emails on this topic, which is actually a smart thing to do), although I do like the fact that it signed with Diego. Otherwise, I am astonished by the models' ability to orient itself in Isabelle/ML and understand things based on the “induction on the sources” it is performing. (I haven’t seen it looking up Mercurial history yet, but this could be a future instruction.)

As for the workaround itself: I don’t have a good intuition why Quotient_fmap_bnf_2prem has the right shape for this to work. But also I am also not very familiar with setup_lifting internals. The various other declarations make sense (the uniqueness/totality lemmas could be more general, i.e., not involving the equality constants). In many cases, a lifting plugin derives those automatically for BNFs, but I believe the scope of the plugin is restricted to BNFs without dead variables (whereas in finite maps the domain is dead).

Best wishes,
Dmitriy

https://opncd.ai/share/FzaMm9I7

Dear Diego,
I was able to reproduce the problem in a small theory, and it looks like a bug or at least a missing registration in the interaction between setup_lifting and Finite_Map.
What happens is that setup_lifting turns your typedef into an internal Quotient theorem and then tries to generate a parametrized correspondence relation for the raw type fmap. For that, it consults the registered quot_map theorem for fmap. The existing one from Finite_Map is not in the shape that this part of Lifting expects for a type copy of fmap, which causes the low-level dest_state exception.
A working workaround is to locally override the quot_map theorem for fmap with a two-premise version, and additionally register the relator facts that setup_lifting needs:
theory Scratch
imports "HOL-Library.Finite_Map"
begin
typedef myfmap =
"UNIV :: ((nat, nat) fmap) set"
..
lemma Quotient_fmap_bnf_2prem[quot_map]:
assumes "Quotient (=) (id :: 'a => 'a) id (=)"
assumes "Quotient R Abs Rep T"
shows "Quotient (fmrel R)
(fmmap Abs :: ('a, 'b) fmap => ('a, 'c) fmap)
(fmmap Rep :: ('a, 'c) fmap => ('a, 'b) fmap)
(fmrel T)"
using assms Quotient_fmap_bnf
by (simp add: Quotient_alt_def)
declare fmap.rel_eq[relator_eq]
declare fmap.rel_mono[relator_mono]
declare fmap.rel_compp[symmetric, relator_distr]
lemma left_total_fmrel_eq[transfer_rule]: "left_total (fmrel (=))"
by (simp add: fmap.rel_eq left_total_eq)
lemma bi_total_fmrel_eq[transfer_rule]: "bi_total (fmrel (=))"
by (simp add: fmap.rel_eq bi_total_eq)
lemma left_unique_fmrel_eq[transfer_rule]: "left_unique (fmrel (=))"
by (simp add: fmap.rel_eq left_unique_eq)
lemma right_unique_fmrel_eq[transfer_rule]: "right_unique (fmrel (=))"
by (simp add: fmap.rel_eq right_unique_eq)
lemma bi_unique_fmrel_eq[transfer_rule]: "bi_unique (fmrel (=))"
by (simp add: fmap.rel_eq bi_unique_eq)
lemma right_total_fmrel_eq[transfer_rule]: "right_total (fmrel (=))"
by (simp add: fmap.rel_eq right_total_eq)
setup_lifting type_definition_myfmap
end
With these declarations in place, setup_lifting type_definition_myfmap succeeds cleanly.
So in short:

your original typedef is fine;
the failure is caused by how Lifting reuses the registered fmap quotient-map information;
the workaround above makes the registrations explicit enough for this case.
This seems worth reporting upstream, since Finite_Map already has the relevant BNF facts, but not in a form that setup_lifting can directly use here.
Best,
Diego

Email Gateway (Mar 24 2026 at 20:15):

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

Hi Alex,

thanks for the pointer but the proposed solutions do not seem to work.

In particular,

the first suggestion gives the same error message:

exception THM 1 raised (line 2157 of "thm.ML"):
dest_state
Quotient (fmrel (=)) (fmmap id) (fmmap id) (fmrel (=))

for the second suggestion, lemma myfmap_quotient gives a typing error.

Also the explanations do not seem very convincing.
For example "setup_lifting requires a quotient theorem, not just a typedef." is not true (at least not in the general case).

Best,

Diego

From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Makarius <makarius@sketis.net>
Sent: 24 March 2026 16:55
To: Alex Shkotin <alex.shkotin@gmail.com>; Marmsoler, Diego <D.Marmsoler@exeter.ac.uk>; isabelle-users@cl.cam.ac.uk <isabelle-users@cl.cam.ac.uk>
Subject: Re: [isabelle] finite maps and lifting

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 24/03/2026 17:18, Alex Shkotin wrote:

Meanwhile, have a look https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fchat.qwen.ai%2Fs%2F&data=05%7C02%7Cd.marmsoler%40exeter.ac.uk%7C011f89e046664d72d79708de89c622d1%7C912a5d77fb984eeeaf321334d8f04a53%7C0%7C0%7C639099681255414191%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=S3CqVwmWSvPjFxyEbBnTFNH81UgK2X5akHvJmwR7YFI%3D&reserved=0<https://chat.qwen.ai/s/>
t_056fc366-7d43-4103-9c8a-0436d8c1f96b?fev=0.2.16

Can someone who understands the issue please comment on the quality of the
machine-generated result?

Looking myself superficially, I am worried about two marginal details:

- "Updating to the latest Isabelle release." We did agree on this mailing
list recently that "latest" is very inaccurate and often misleading. Why is
there this interjection anyway?

Makarius

Email Gateway (Mar 25 2026 at 13:06):

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

Hi Dmitriy,

Thanks for your help.

I am not sure I completely understand why the Quotient_fmap_bnf_2prem is required but it seems to work.

Thanks again,

Diego

From: Dmitriy Traytel <traytel@di.ku.dk>
Sent: 24 March 2026 20:05
To: Makarius <makarius@sketis.net>
Cc: Alex Shkotin <alex.shkotin@gmail.com>; Marmsoler, Diego <D.Marmsoler@exeter.ac.uk>; isabelle-users@cl.cam.ac.uk <isabelle-users@cl.cam.ac.uk>
Subject: Re: [isabelle] finite maps and lifting

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 Makarius and Diego,

On 24 Mar 2026, at 17.55, Makarius <makarius@sketis.net> wrote:

Can someone who understands the issue please comment on the quality of the machine-generated result?

Best wishes,
Dmitriy

https://opncd.ai/share/FzaMm9I7

your original typedef is fine;
the failure is caused by how Lifting reuses the registered fmap quotient-map information;
the workaround above makes the registrations explicit enough for this case.
This seems worth reporting upstream, since Finite_Map already has the relevant BNF facts, but not in a form that setup_lifting can directly use here.
Best,
Diego

Email Gateway (Mar 26 2026 at 10:57):

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

Hi Dmitriy (all),

thanks again for your help with my typedef question.
I now have a follow-up question. In particular I tried to add a type parameter to myfmap which then causes again problems with the setup-lifting command.

My definition now looks like this:

typedef 'a myfmap =
"UNIV :: (('a, nat) fmap) set"
..

The setup you (or your LLM) proposed now leads to the following error:

exception THM 1 raised (line 2626 of "thm.ML"):
RSN: no unifiers
Quotient R Abs Rep T [Quotient R Abs Rep T]
Quotient (=) id id (=) ⟹ Quotient ?R ?Abs ?Rep ?T ⟹ Quotient (fmrel ?R) (fmmap ?Abs) (fmmap ?Rep) (fmrel ?T)

Any ideas how to adapt the format of the lemma would be very much appreciated.

Thanks and all the best,

Diego

From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of "Marmsoler, Diego" <cl-isabelle-users@lists.cam.ac.uk>
Sent: 25 March 2026 13:06
To: Dmitriy Traytel <traytel@di.ku.dk>
Cc: isabelle-users@cl.cam.ac.uk <isabelle-users@cl.cam.ac.uk>
Subject: Re: [isabelle] finite maps and lifting

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 Dmitriy,

Thanks for your help.

I am not sure I completely understand why the Quotient_fmap_bnf_2prem is required but it seems to work.

Thanks again,

Diego

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 Makarius and Diego,

On 24 Mar 2026, at 17.55, Makarius <makarius@sketis.net> wrote:

Can someone who understands the issue please comment on the quality of the machine-generated result?

Best wishes,
Dmitriy

https://opncd.ai/share/FzaMm9I7

your original typedef is fine;
the failure is caused by how Lifting reuses the registered fmap quotient-map information;
the workaround above makes the registrations explicit enough for this case.
This seems worth reporting upstream, since Finite_Map already has the relevant BNF facts, but not in a form that setup_lifting can directly use here.
Best,
Diego

Email Gateway (Mar 26 2026 at 13:48):

From: Lars Hupel <lars@hupel.info>

Hi Diego,

Quotient_fmap_bnf_2prem[quot_map]:
assumes "Quotient (=) (id :: 'a => 'a) id (=)"

this assumption looks fishy since it contains no variables.

I suspect you could just delete it. Does that work?

However, the subsequent declarations (left_total) may also have to be generalised. I’ll check later.

Cheers
Lars

Email Gateway (Mar 26 2026 at 14:39):

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

Hi Lars,

thanks for the hint.

Indeed the assumption is suspicious and the proof of lemma Quotient_fmap_bnf_2prem also works without this assumption.
However, without the assumption the setup_lifting command complaints (even for the version of myfmap without type parameters):

exception THM 1 raised (line 2157 of "thm.ML"):
dest_state
Quotient (fmrel (=)) (fmmap id) (fmmap id) (fmrel (=))

It looks like the lifting package somehow expects two assumptions for the quot_map lemma (even for the case without type parameters).

Diego

From: Lars Hupel <lars@hupel.info>
Sent: 26 March 2026 13:48
To: Marmsoler, Diego <D.Marmsoler@exeter.ac.uk>
Cc: Dmitriy Traytel <traytel@di.ku.dk>; isabelle-users@cl.cam.ac.uk <isabelle-users@cl.cam.ac.uk>; Marmsoler, Diego <D.Marmsoler@exeter.ac.uk>
Subject: Re: [isabelle] finite maps and lifting

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,

Quotient_fmap_bnf_2prem[quot_map]:
assumes "Quotient (=) (id :: 'a => 'a) id (=)"

this assumption looks fishy since it contains no variables.

I suspect you could just delete it. Does that work?

However, the subsequent declarations (left_total) may also have to be generalised. I’ll check later.

Cheers
Lars

Email Gateway (Mar 30 2026 at 17:48):

From: Lars Hupel <lars@hupel.info>

Hi Diego,

it's even weirder.

Indeed the assumption is suspicious and the proof of lemma
Quotient_fmap_bnf_2prem also works without this assumption.

This theorem is already in the Finite_Map theory as "Quotient_fmap_bnf";
indeed with only one premise.

I suspect that it was written by Ondrej himself, since he was still at
the chair when I committed the Finite_Map theory.

Regarding the error:

exception THM 1 raised (line 2157 of "thm.ML"):
dest_state
Quotient (fmrel (=)) (fmmap id) (fmmap id) (fmrel (=))

I could also reproduce it.

While these declarations:

declare fmap.rel_eq[relator_eq]
declare fmap.rel_mono[relator_mono]
declare fmap.rel_compp[symmetric, relator_distr]

are indeed missing, they don't appear to change anything (same for the
left_total etc.) [1].

Sadly, I couldn't find any examples in the AFP for how this could look
like in practice [2].

tl;dr I have no idea how to fix your issue.

Cheers
Lars

[1] Interesting side note: for fset, those declarations are made by the
"bnf" command. However, fmap is declared as a BNF using "lift_bnf",
which does not make these declarations. I am unsure whether this is an
oversight; Jasmin et al. probably now.

[2] Perhaps as a consolation,
"Probabilistic_System_Zoo.Nonempty_Bounded_Set" contains a relevant
snippet, but it is commented out, just below the line (* FIXME for ONDRA
*) ;)

Email Gateway (Mar 30 2026 at 19:08):

From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>

Hi both,

Both bnf and lift_bnf run the same lifting plugin that should do the registration in principle. The plugin however is not handling types with dead variables (such as fmap or bounded sets from the AFP). This was a design decision by Ondrej; I don’t think that I recall the reasoning.

I assume that the lifting infrastructure expects to see as many assumptions in the quotient theorem as there are type arguments in the type. Possibly also in the rel/map constants (which would explain the above—from BNFs you won’t get the contravariant map function for fmap or the binary relator—but one can define them manually of course). But I am unsure about the precise expected shape that the lifting infrastructure needs.

Best wishes,
Dmitriy

On 30 Mar 2026, at 19.48, Lars Hupel <lars@hupel.info> wrote:

[You don't often get email from lars@hupel.info. Learn why this is important at https://aka.ms/LearnAboutSenderIdentification ]

Hi Diego,

it's even weirder.

Indeed the assumption is suspicious and the proof of lemma
Quotient_fmap_bnf_2prem also works without this assumption.

This theorem is already in the Finite_Map theory as "Quotient_fmap_bnf";
indeed with only one premise.

I suspect that it was written by Ondrej himself, since he was still at
the chair when I committed the Finite_Map theory.

Regarding the error:

exception THM 1 raised (line 2157 of "thm.ML"):
dest_state
Quotient (fmrel (=)) (fmmap id) (fmmap id) (fmrel (=))

I could also reproduce it.

While these declarations:

declare fmap.rel_eq[relator_eq]
declare fmap.rel_mono[relator_mono]
declare fmap.rel_compp[symmetric, relator_distr]

are indeed missing, they don't appear to change anything (same for the
left_total etc.) [1].

Sadly, I couldn't find any examples in the AFP for how this could look
like in practice [2].

tl;dr I have no idea how to fix your issue.

Cheers
Lars

[1] Interesting side note: for fset, those declarations are made by the
"bnf" command. However, fmap is declared as a BNF using "lift_bnf",
which does not make these declarations. I am unsure whether this is an
oversight; Jasmin et al. probably now.

[2] Perhaps as a consolation,
"Probabilistic_System_Zoo.Nonempty_Bounded_Set" contains a relevant
snippet, but it is commented out, just below the line (* FIXME for ONDRA
*) ;)

Email Gateway (Mar 30 2026 at 22:19):

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

Hi Lars,
Hi Dmitriy,

thanks a lot for your help!

Indeed, it seems that the BNF command does not create contravariant versions of the relator and mapper functions which, however, seems to be required in this case.

Thus, based on your suggestions I tried the following:

*
I defined contravariant versions of relator and mapper functions for fmap.
*
Using these I defined a new version of the quot_map theorem which is as follows:
assumes "Quotient R1 abs1 rep1 T1" and "Quotient R2 abs2 rep2 T2"
shows "Quotient (rel_fmap R1 R2) (map_fmap rep1 abs2) (map_fmap abs1 rep2) (rel_fmap T1 T2)"
*
I updated the left_total ecc. lemmas accordingly.

This seems to work now except that I get the following warning:

Generation of a parametric transfer rule for the abs. or the rep. function failed.
A non-parametric version will be used.
Reason:
Rewriting (merging) of this term has failed:
rel_fmap T (=) OO rel_fmap (=) (=)

I guess this results in weaker support for transfer.
Do you have any suggestions how to address this warning?

Thanks and all the best,

Diego

From: Dmitriy Traytel <traytel@di.ku.dk>
Sent: 30 March 2026 20:08
To: Lars Hupel <lars@hupel.info>; Marmsoler, Diego <D.Marmsoler@exeter.ac.uk>
Cc: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] finite maps and lifting

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 both,

Best wishes,
Dmitriy

On 30 Mar 2026, at 19.48, Lars Hupel <lars@hupel.info> wrote:

[You don't often get email from lars@hupel.info. Learn why this is important at https://aka.ms/LearnAboutSenderIdentification ]

Hi Diego,

it's even weirder.

Indeed the assumption is suspicious and the proof of lemma
Quotient_fmap_bnf_2prem also works without this assumption.

This theorem is already in the Finite_Map theory as "Quotient_fmap_bnf";
indeed with only one premise.

I suspect that it was written by Ondrej himself, since he was still at
the chair when I committed the Finite_Map theory.

Regarding the error:

exception THM 1 raised (line 2157 of "thm.ML"):
dest_state
Quotient (fmrel (=)) (fmmap id) (fmmap id) (fmrel (=))

I could also reproduce it.

While these declarations:

declare fmap.rel_eq[relator_eq]
declare fmap.rel_mono[relator_mono]
declare fmap.rel_compp[symmetric, relator_distr]

are indeed missing, they don't appear to change anything (same for the
left_total etc.) [1].

Sadly, I couldn't find any examples in the AFP for how this could look
like in practice [2].

tl;dr I have no idea how to fix your issue.

Cheers
Lars

[1] Interesting side note: for fset, those declarations are made by the
"bnf" command. However, fmap is declared as a BNF using "lift_bnf",
which does not make these declarations. I am unsure whether this is an
oversight; Jasmin et al. probably now.

[2] Perhaps as a consolation,
"Probabilistic_System_Zoo.Nonempty_Bounded_Set" contains a relevant
snippet, but it is commented out, just below the line (* FIXME for ONDRA
*) ;)

Email Gateway (Mar 31 2026 at 15:10):

From: Lars Hupel <lars@hupel.info>

Hi Diego,

I admire your tenacity!

Thus, based on your suggestions I tried the following:

*
I defined contravariant versions of relator and mapper functions for
fmap.
*
Using these I defined a new version of the quot_map theorem which is
as follows:
assumes "Quotient R1 abs1 rep1 T1" and "Quotient R2 abs2 rep2 T2"
shows "Quotient (rel_fmap R1 R2) (map_fmap rep1 abs2) (map_fmap abs1
rep2) (rel_fmap T1 T2)"
*
I updated the left_total ecc. lemmas accordingly.

Would you be willing to post a patch on the mailing list? I might
consider updating the material in HOL-Library. It seems to me that the
lifting setup we have today is simply wrong, and your approach is the
correct one (or at least more correct ...)

Generation of a parametric transfer rule for the abs. or the rep.
function failed.
A non-parametric version will be used.
Reason:
Rewriting (merging) of this term has failed:
rel_fmap T (=) OO rel_fmap (=) (=)

I remember liberally sprinkling invocations of "parametric_constant" all
over the theory, e.g.:

parametric_constant map_add_transfer[transfer_rule]: map_add_def
parametric_constant map_of_transfer[transfer_rule]: map_of_def

Perhaps it will help if you add those for "rel_fmap", "map_fmap" etc.?

If you used "lift_definition" to define them, also refer to this example
from the library:

lift_definition fmdom :: "('a, 'b) fmap ⇒ 'a fset"
is dom
parametric dom_transfer
.

I hope that a combination of these will enable you to progress with your
definitions.

Cheers
Lars

Email Gateway (Apr 01 2026 at 14:22):

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

Hi Lars,

I remember liberally sprinkling invocations of "parametric_constant" all
over the theory, e.g.:

parametric_constant map_add_transfer[transfer_rule]: map_add_def
parametric_constant map_of_transfer[transfer_rule]: map_of_def

Perhaps it will help if you add those for "rel_fmap", "map_fmap" etc.?

I like the "sprinkling over the theory" approach but unfortunately it did not solve the problem for me (;
What did help, however, is to add some missing lemmas as [relator_eq], [relator_mono], and [relator_distr], respectively.

This resulted now in a setup_lifting without any warnings.
I also tested it by lifting some simple definitions and lemmas from finite_map and it seems to work.

Would you be willing to post a patch on the mailing list? I might
consider updating the material in HOL-Library. It seems to me that the
lifting setup we have today is simply wrong, and your approach is the
correct one (or at least more correct ...)

Sure, I still need to finish the proofs for some of the lemmas, then I can share a patch.
I would not go as far as calling my approach the correct one but at least it seems to work (;

On a related matter, I was thinking if it would make sense to integrate some parts of Finite_Map_Extras into Finite_Maps.
Maybe there is a reason not to integrate them but I use the two almost always together.

Thanks a lot for your help!

All the best,

Diego

From: Lars Hupel <lars@hupel.info>
Sent: 31 March 2026 16:09
To: cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Cc: Marmsoler, Diego <D.Marmsoler@exeter.ac.uk>
Subject: Re: [isabelle] finite maps and lifting

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,

I admire your tenacity!

Thus, based on your suggestions I tried the following:

*
I defined contravariant versions of relator and mapper functions for
fmap.
*
Using these I defined a new version of the quot_map theorem which is
as follows:
assumes "Quotient R1 abs1 rep1 T1" and "Quotient R2 abs2 rep2 T2"
shows "Quotient (rel_fmap R1 R2) (map_fmap rep1 abs2) (map_fmap abs1
rep2) (rel_fmap T1 T2)"
*
I updated the left_total ecc. lemmas accordingly.

Generation of a parametric transfer rule for the abs. or the rep.
function failed.
A non-parametric version will be used.
Reason:
Rewriting (merging) of this term has failed:
rel_fmap T (=) OO rel_fmap (=) (=)

I remember liberally sprinkling invocations of "parametric_constant" all
over the theory, e.g.:

parametric_constant map_add_transfer[transfer_rule]: map_add_def
parametric_constant map_of_transfer[transfer_rule]: map_of_def

Perhaps it will help if you add those for "rel_fmap", "map_fmap" etc.?

If you used "lift_definition" to define them, also refer to this example
from the library:

lift_definition fmdom :: "('a, 'b) fmap ⇒ 'a fset"
is dom
parametric dom_transfer
.

I hope that a combination of these will enable you to progress with your
definitions.

Cheers
Lars

Email Gateway (Apr 08 2026 at 13:45):

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

Hi Lars (all),

I did spend some more time on this but run into a problem for which I would need some input from a Transfer/Lifting expert.

My original idea was to define contravariant versions of the relator and mapper by lifting corresponding definitions from maps:

definition rel_map :: "('a ⇒ 'c ⇒ bool) ⇒ ('b ⇒ 'd ⇒ bool) ⇒ ('a ⇀ 'b) ⇒ ('c ⇀ 'd) ⇒ bool" where
"rel_map R f ≡ (R ===> rel_option f)"

definition map_map :: "('c ⇒ 'a) ⇒ ('b ⇒ 'd) ⇒ ('a ⇀ 'b) ⇒ ('c ⇀ 'd)" where
"map_map f g ≡ f ---> map_option g"

lift_definition rel_fmap :: "('a ⇒ 'c ⇒ bool) ⇒ ('b ⇒ 'd ⇒ bool) ⇒ ('a, 'b) fmap ⇒ ('c, 'd) fmap ⇒ bool"
is rel_map
parametric rel_map_transfer
done

lift_definition map_fmap :: "('c ⇒ 'a) ⇒ ('b ⇒ 'd) ⇒ ('a, 'b) fmap ⇒ ('c, 'd) fmap"
is map_map
parametric map_map_transfer
sorry

and then to prove the following quot_map theorem:

lemma fmap_quotient[quot_map]:
assumes 1: "Quotient R1 abs1 rep1 T1"
assumes 2: "Quotient R2 abs2 rep2 T2"
shows "Quotient (rel_fmap R1 R2) (map_fmap rep1 abs2) (map_fmap abs1 rep2) (rel_fmap T1 T2)"

This seems to fix the problem with setup_lifting but I do have two issues when trying to finish the proofs.

The first issue is that the goal for lifting map_fmap seems to be not provable.
In particular it requires to prove that
"finite (dom fun3) ==> finite (dom (map_map fun1 fun2 fun3))"
which does not seem to be provable in general.
This is an issue because the lifted definition is required to prove the quotient theorem.

The second problem is that the rel_fmap definition is not left/right total, in general.
It can be shown that it is left/right_total w.r.t. equality but not for general left/righ_unique left/right_total relations.
This problem seems to be less critical since lifting still works on my examples but it leads to warnings in setup_lifting.

Now I was wondering if the above approach seems like a reasonable approach and if so if someone has any ideas how to solve the above issues.

Thanks and all the best,

Diego

From: cl-isabelle-users-request@lists.cam.ac.uk <cl-isabelle-users-request@lists.cam.ac.uk> on behalf of "Marmsoler, Diego" <cl-isabelle-users@lists.cam.ac.uk>
Sent: 01 April 2026 15:22
To: Lars Hupel <lars@hupel.info>; cl-isabelle-users@lists.cam.ac.uk <cl-isabelle-users@lists.cam.ac.uk>
Subject: Re: [isabelle] finite maps and lifting

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 Lars,

I remember liberally sprinkling invocations of "parametric_constant" all
over the theory, e.g.:

parametric_constant map_add_transfer[transfer_rule]: map_add_def
parametric_constant map_of_transfer[transfer_rule]: map_of_def

Perhaps it will help if you add those for "rel_fmap", "map_fmap" etc.?

This resulted now in a setup_lifting without any warnings.
I also tested it by lifting some simple definitions and lemmas from finite_map and it seems to work.

Would you be willing to post a patch on the mailing list? I might
consider updating the material in HOL-Library. It seems to me that the
lifting setup we have today is simply wrong, and your approach is the
correct one (or at least more correct ...)

Sure, I still need to finish the proofs for some of the lemmas, then I can share a patch.
I would not go as far as calling my approach the correct one but at least it seems to work (;

Thanks a lot for your help!

All the best,

Diego

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,

I admire your tenacity!

Thus, based on your suggestions I tried the following:

*
I defined contravariant versions of relator and mapper functions for
fmap.
*
Using these I defined a new version of the quot_map theorem which is
as follows:
assumes "Quotient R1 abs1 rep1 T1" and "Quotient R2 abs2 rep2 T2"
shows "Quotient (rel_fmap R1 R2) (map_fmap rep1 abs2) (map_fmap abs1
rep2) (rel_fmap T1 T2)"
*
I updated the left_total ecc. lemmas accordingly.

Generation of a parametric transfer rule for the abs. or the rep.
function failed.
A non-parametric version will be used.
Reason:
Rewriting (merging) of this term has failed:
rel_fmap T (=) OO rel_fmap (=) (=)

I remember liberally sprinkling invocations of "parametric_constant" all
over the theory, e.g.:

parametric_constant map_add_transfer[transfer_rule]: map_add_def
parametric_constant map_of_transfer[transfer_rule]: map_of_def

Perhaps it will help if you add those for "rel_fmap", "map_fmap" etc.?

If you used "lift_definition" to define them, also refer to this example
from the library:

lift_definition fmdom :: "('a, 'b) fmap ⇒ 'a fset"
is dom
parametric dom_transfer
.

I hope that a combination of these will enable you to progress with your
definitions.

Cheers
Lars

Last updated: Apr 12 2026 at 02:50 UTC