Re: [isabelle] Large theories



On 06/06/16 20:44, ÐÑÐÐÐÑÐÐÐ ÐÐÐÐÐÐÐÑÐÐÐÑ ÐÐÐÑÐÐÐ wrote:

> 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.

These numbers are not that big, but if you go through surface syntax of
Isabelle (the logical language, the theory and proof language, maybe
even just ML source language) it is likely to choke.

Note that the canonical way to import big things into an LCF-style
prover like Isabelle is to write some ML functions that do that, and
construct terms and proofs by internal means. Never ever generate source
that is then fed into the system.


Examples for reading external material can be seen in src/HOL/SPARK.

In such applications it is important to recall that surface syntax (for
input and output of end-user material) is really just the surface and
not the real system. E.g. the SPARK importer turned out incredible slow,
until someone pointed out that there is redundant output of intermediate
statements.


	Makarius





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