# [isabelle] Stuck with Isabelle type instantiation

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

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*