Email Gateway (Aug 19 2022 at 09:44): Email Gateway (Aug 19 2022 at 09:44):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Dear all,
based on the examples in "src/HOL/Enum.thy" I was trying to prove the
following instance (where the "[]" should be replaced by a suitable
representation of the universe of the intended type), still in Isabelle2012:
instantiation bit0 :: (finite) enum
begin
definition "enum = []"
definition "enum_all P = (filter P enum = enum)"
definition "enum_ex P = (filter P enum ≠ [])"
instance
proof (default)
show "UNIV = set enum"
Whatever goal I try to state with "show" after the "proof (default)"
command, I always get an error
"Local statement will fail to solve any pending goal"
I can neither refer to definitions "enum_bit0_def",
"enum_all_bit0_def", "enum_ex_bit0_def" in the "instance" proof.
What am I doing wrong? Have I missed some type annotations, or should
I do the definitions names explicit?
Thanks for any ideas,
Jesus
Email Gateway (Aug 19 2022 at 09:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Jesus,
This looks like type inference gives you too generic types. Try to
explicitly restrict the type like this, for both definitions and goal
statements.
definition "(enum :: bit0 list) = []"
show "(UNIV :: bit0 set) = set enum"
Hope this helps
Andreas
Email Gateway (Aug 19 2022 at 09:44):From: Jesus Aransay <jesus-maria.aransay@unirioja.es>
Hi Andreas,
thanks for your hint; I tried to be as exhaustive as I could with type
annotations, but the problem still persists;
instantiation bit0 :: (finite) enum
begin
definition "(enum::'a bit0 list) = ([]::'a bit0 list)"
definition "enum_all P = (filter P ([]::'a bit0 list) = [])"
definition "enum_ex P = (filter P enum ≠ [])"
thm enum_def (*This theorem refers to a constant named "local.enum"; I
guess this should not be the case*)
thm enum_bit0_def (*This theorem does not even exist in the context;
the same happens with enum_all and enum_ex*)
instance
proof (default)
show "(UNIV::'a bit0 set) = set enum" (*This show fails because enum
makes reference to "local.enum"*)
Thanks for any other suggestions,
Jesus
Email Gateway (Aug 19 2022 at 09:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jesus,
you are right, type inference is not the main problem here. The issue is
that at the end of Enum.thy, unqualified access for enum, enum_all and
enum_ex is disabled. So you have to use the names enum_class.enum, etc.;
for the declarations in Enum.thy, the short names naturally work.
definition "enum_class.enum = ([] :: 'a bit0 list)"
definition "enum_class.enum_all P = (filter P ([]::'a bit0 list) = [])"
definition "enum_class.enum_ex P = (filter P enum_class.enum ≠ ([] :: 'a
bit0 list))"
Best,
Andreas
Last updated: Apr 16 2024 at 01:05 UTC