[isabelle] Finite Datatype



Hi,

is there a simple way to proof the following statement?
I have a proof but it contains a case-disinction over all elements in the datatype. This is inacceptable for the actual dataype which contains several thousands of elements; the proof would require to much time.

theory Test imports Main begin
datatype A = A0 | A1
datatype Label = B0 A A
instance Label :: "finite"
oops
end

Regards,
Sven






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