[isabelle] Large theories



Hello,

I'm working on a verification of properties of a large set containing
approximately 2 million objects. Each object is relatively simple.
These objects were constructed by a computer program; now I want to prove
that the result of the program is correct.
My plan is
  1. to define 2 million objects.
  2. to prove properties of every object (that is I need 2 million lemmas).
Each lemma has <=500 steps, each step is relatively simple. That is, I need
approx. 500*2mln = 1billion simple steps.
I'm going to generate the proofs for all that lemmas by another computer
programs.

Has anybody worked with specifications of this size?
Is it practical to conduct a proof of this size in Isabelle/HOL? If yes,
can you recommend how to organize the proof? If no, can you suggest other
verification tools?

My experiments show that it is impractical to define a set of 2 million
objects in Isabelle/HOL (Isabelle allocates a lot of memory and the
computation time is large).
I found that many small-size definitions are easier to handle than one
large definition. E.g. I was able to define 20 000 sets a1,...,a20000
containing 100 elements and then define 200 sets b1,...,b200 (each being a
union of 100 sets a_{100*i+1},...,a_{100*i+200}), and finally define a set
C as a union of b1,...,b200. But for aesthetic reasons I don't like it.
Moreover, given the speed of Isabelle, I'm not sure that proofs of 2
million lemmas can be conducted in a reasonable time (say, less than two
months).

Any ideas?

Stanislav.



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