Email Gateway (Feb 17 2025 at 09:17): Email Gateway (Feb 17 2025 at 09:17):From: Gunnar Teege <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle developers,
when defining a quotient type for a record I get an unexpected warning
about a missing mapper function. A minimized example is as follows:
record 'a myrec = c1 :: "'a"
setup_lifting type_definition_myrec_ext
copy_bnf ('a, 'm) myrec_ext
term map_myrec_ext
quotient_type 'a myrec_quot =
"'a myrec" / "λ(r1::'a myrec) (r2::'a myrec). c1 r1 = c1 r2"
by (simp add: equivp_def) metis
Here the quotient_type command signals the warning
"No map function defined for Test_Mapper.myrec.myrec_ext. This will
cause problems later on."
For my understanding the mapper should have been defined by the copy_bnf
command as map_myrec_ext, it is displayed by the subsequent term command.
If I omit the copy_bnf the record scheme is not registered as BNF and
the quotient_type command signals the additional warning about the
missing relator. So I don't see why after copy_bnf it finds the relator
but not the mapper.
It is not really a problem, because it is only a warning, but I would
like to understand it. Also it is not new for the 2025 RC2, it also
occurs at least in Isabelle 2023. But the 2025 release may be a good
opportunity to check and possibly resolve it.
I attach a theory file with a slightly extended example with two type
parameters where the quotient_type is nontrivial, it reproduces the same
warning.
Regards
Gunnar Teege
Email Gateway (Feb 17 2025 at 10:29):From: Gunnar Teege <cl-isabelle-users@lists.cam.ac.uk>
Ok, I have an answer to my question.
It seems that copy_bnf does not register the mapper in the functor
structure. When adding
functor map_myrec_ext
using myrec_ext.map_comp apply fastforce
apply (simp add: myrec_ext.map_id0)
done
after copy_bnf the warning disappears.
Thanks to Peter Gammie for figuring that out.
Maybe it would be useful to extend copy_bnf (and supposedly lift_bnf)
accordingly.
Regards
Gunnar Teege
when defining a quotient type for a record I get an unexpected warning
about a missing mapper function. A minimized example is as follows:
record 'a myrec = c1 :: "'a"
setup_lifting type_definition_myrec_ext
copy_bnf ('a, 'm) myrec_ext
term map_myrec_ext
quotient_type 'a myrec_quot =
"'a myrec" / "λ(r1::'a myrec) (r2::'a myrec). c1 r1 = c1 r2"
by (simp add: equivp_def) metis
Here the quotient_type command signals the warning
"No map function defined for Test_Mapper.myrec.myrec_ext. This will
cause problems later on."
Last updated: Mar 09 2025 at 12:28 UTC