Re: [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"
I don't think there is an easy way. If your datatype as more than 100
constructors, you will anyway find that it can take a very long time to
even define such a datatype, never mind any proofs based on it. If the
large number of elements comes from the fact that there is a hierarchy
of datatypes, like above, you should be able to prove finiteness in
layers, and each layer should stay manageable.
Since this is in essence a finite problem, Tjark Weber's SAT-solver link
may be able to prove this automatically. Tjark?
This archive was generated by a fusion of
Pipermail (Mailman edition) and