Re: [isabelle] Stuck with Isabelle type instantiation



Dear Wenda,


Am 14.03.2013 um 21:35 schrieb "W. Li" <wl302 at 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

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 = ...



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