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?

Tobias





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