Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Stuck with Isabelle type instantiation


view this post on Zulip Email Gateway (Aug 19 2022 at 10:47):

From: "W. Li" <wl302@cam.ac.uk>
Hello,

Could anyone be kind enough to help me with a type instantiation problem?

I defined a simple data type 'kon_nodes' with four constructors (i.e. 'a',
'b', 'c' and 'd'), and I want to show that 'kon_nodes' is of class 'enum'.
However, I cannot finish the instance proof. The code is as follows:
datatype kon_nodes = a|b|c|d instantiation kon_nodes :: enum begin
definition "enum =[a,b,c,d]" definition "enum_all P <-> P a ∧ P b ∧ P c
∧ P d" definition "enum_ex P <-> P a ∨ P b ∨ P c ∨ P d" instance sorry
end

Actually, there is a very similar proof in the theory of 'enum' in the
library. I copy and paste the exact code to my Isabelle 2013, but,
surprisingly, Isabelle does not accept the proof either. The proof from the
theory of 'enum' is as follows: datatype finite_4 = a⇣1 | a⇣2 | a⇣3 |
a⇣4

notation (output) a⇣1 ("a⇣1")
notation (output) a⇣2 ("a⇣2")
notation (output) a⇣3 ("a⇣3")
notation (output) a⇣4 ("a⇣4")

lemma UNIV_finite_4:
"UNIV = {a⇣1, a⇣2, a⇣3, a⇣4}"
by (auto intro: finite_4.exhaust)

instantiation finite_4 :: enum
begin

definition
"enum = [a⇣1, a⇣2, a⇣3, a⇣4]"

definition
"enum_all P <-> P a⇣1 ∧ P a⇣2 ∧ P a⇣3 ∧ P a⇣4"

definition
"enum_ex P <-> P a⇣1 ∨ P a⇣2 ∨ P a⇣3 ∨ P a⇣4"

instance proof qed (simp_all only: enum_finite_4_def enum_all_finite_4_def
enum_ex_finite_4_def UNIV_finite_4, simp_all) end

I feel confused. Any help would be greatly appreciated.
Wenda Li

view this post on Zulip Email Gateway (Aug 19 2022 at 10:47):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Wenda,

In Enum.thy, unqualified access to the enum constant is disabled at the
end. Therefore, your definition "enum = [a, b, c, d]" does not define
the overloaded type class parameter, but introduces a new constant enum.
This also holds for enum_ex and enum_all. Try it with qualified access:

definition "enum_class.enum = [a, b, c, d]"

Best,
Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 10:47):

From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Wenda,

as far as I see, your proof can easily be repaired by using the postfix _kon_nodes in your definitions.
Then all results are easily proven.

datatype kon_nodes = a|b|c|d

instantiation kon_nodes :: enum

begin
definition [simp]: "enum_kon_nodes =[a,b,c,d]"
definition [simp]: "enum_all_kon_nodes P <-> P a ∧ P b ∧ P c ∧ P d"
definition [simp]: "enum_ex_kon_nodes P <-> P a ∨ P b ∨ P c ∨ P d" instance

proof
qed (auto, (case_tac x, auto)+)
end

I hope, this was useful,
René

PS: usually type names are not plural, so I would call it datatype kon_node = ...


Last updated: Mar 28 2024 at 20:16 UTC