Email Gateway (Oct 18 2023 at 22:19): Email Gateway (Oct 18 2023 at 22:19):From: Guilherme Silva <guilhermegfsilva@gmail.com>
Hello,
I found several examples online of how to use the instantiation command to
define an enumeration for a type defined using datatype, such as this post:
https://stackoverflow.com/questions/54879738/how-to-generate-code-for-the-existential-quantifier
or in these theories for Enum:
https://isabelle.in.tum.de/library/HOL/HOL/Enum.html
https://www.isa-afp.org/browser_info/Isabelle2009-1/HOL/FinFun/Enum.html
My question is if it would be possible to define an instantiation for a
type defined using typedecl instead, since due to the nature of typedecl we
know nothing about the type itself at its definition. I've been trying to
do it by defining a few constants to serve as the enumeration, but all I
have so far is this, which isn't working.
typedecl type1
consts A :: type1
consts B :: type1
consts C :: type1
instantiation type1 :: enum
begin
definition "Enum.enum = [G,H,I]"
definition "Enum.enum_all P = list_all P [G,H,I]"
definition "Enum.enum_ex P = list_ex P [G,H,I]"
instance proof (* this is where I'm required to write the instance proof,
but I'm not sure if it's possible based on what I know about type1. *)
end
Could there be another way to do this? I'm required to use typedecl for the
project I'm working on.
Guilherme Silva
Email Gateway (Oct 18 2023 at 23:26):From: Jan van Brügge <jan@vanbruegge.de>
No this cannot work. As you said yourself, you know nothing about the type, so you also don't know if it is enumerable.
The only "solution" would be to add an axiom that the type is enumerable, but you should never add new axioms to the theory in your proofs.
Cheers,
Jan
Oct 18, 2023 11:19:34 PM Guilherme Silva <guilhermegfsilva@gmail.com>:
Last updated: Apr 28 2024 at 20:16 UTC