Email Gateway (Aug 23 2022 at 08:45): Email Gateway (Aug 23 2022 at 08:45):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
The reference manual says in Subsection 11.9.2, “The Lifting package
works with all four kinds of type abstraction: type copies, subtypes,
total quotients and partial quotients.” Also, the documentation of
lift_definition further down in this subsection mentions type copies.
However, when I try to use lift_definition with a subtype, Isabelle
tells me that lifting has failed and the reason is that no quotient type
with the name of my subtype can be found. Why is this?
Here’s a simplified version of the code in question:
typedef surjective_function = "{f :: nat ⇒ nat. surj f}"
using surj_id
by blast
lift_definition
surjective_function_composition :: "
surjective_function ⇒
surjective_function ⇒
surjective_function"
(infixl "∘" 55)
is comp
All the best,
Wolfgang
Email Gateway (Aug 23 2022 at 08:45):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
By looking at the code of HOL-Library.Comparator, I found a solution,
which I guess is the recommended one: add the line
setup_lifting type_definition_surjective_function
after the subtype definition.
Interestingly, my memories are telling me that this is not necessary for
quotient types. Is this the case? If yes, what is the reason for this
mismatch?
Also I’d like to suggest to change the error message you get without the
setup_lifting line, since it referring to quotient types is
misleading.
All the best,
Wolfgang
Email Gateway (Aug 23 2022 at 08:45):From: Frédéric Boulanger <frederic.boulanger@lri.fr>
I think you need:
setup_lifting type_definition_surjective_function
before being able to use lift_definition.
Best regards,
Frédéric Boulanger
CentraleSupélec - Département Informatique Laboratoire de Recherche en Informatique
3 rue Joliot-Curie, 91192 Gif-sur-Yvette cedex Bât. 650 - 1 rue Raimond Castaing, 91190 Gif-sur-Yvette
+33 [0]1 69 85 14 84
Last updated: Apr 24 2024 at 04:17 UTC