[isabelle] Finite Datatype
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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and