Email Gateway (Aug 22 2022 at 15:29): Email Gateway (Aug 22 2022 at 15:29):From: Lars Hupel <hupel@in.tum.de>
Dear list,
consider the following class:
class "term" =
fixes
"consts" :: "'a ⇒ string set"
assumes
"consts t ⊆ {}"
(this is a stripped-down example, obviously)
I thought I could write a trivial instance proof:
instantiation unit :: "term" begin
instance proof (standard, goal_cases)
case (1 t)
show ?case sorry
qed
end
But "show ?case" prints:
Failed to refine any pending goal
I'm at a loss for an explanation. It happens in Isabelle/82add6bf8a42 too.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:29):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Lars,
I thought I could write a trivial instance proof:
Why did you think that? The class specifies a constant and makes an assumption on that constant. If you add a definition, e.g.,
definition "consts_unit = (λu :: unit. UNIV::string set)"
then it all works out.
Also, I presume by "consts t ⊆ {}" you meant "{} ⊆ consts t", but again Isabelle just won't let you continue, apparently because you haven't defined a constant that must be defined in all type classes.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 15:29):From: Lars Hupel <hupel@in.tum.de>
I feel stupid now – thanks for clearing that up. I was under the
impression that I could leave constants unspecified. Somehow I didn't
make the connection that this could be the cause for the error.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:29):From: Manuel Eberl <eberlm@in.tum.de>
To be fair, Lars had me take a look at it, too, and I didn't spot the
problem either, although, in retrospect, it is of course completely obvious.
That may indicate that the error message is not ideal in this case.
Manuel
Email Gateway (Aug 22 2022 at 15:29):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
you can leave constants unspecified in type class instantiations. The problem only
arises when you want to do the type class instantiation proof in Isar. It all works out in
apply-style:
class "term" = fixes "consts" :: "'a ⇒ string set"
assumes "{} ⊆ consts t"
instantiation unit :: "term" begin
instance apply intro_classes apply simp done
end
Best,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC