*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Large theories*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 7 Jun 2016 15:07:46 +0200*In-reply-to*: <CAFMZHLq6qvcQv2mghe1Qx9KTKtvj=vTNf9YKHeOghLOSHsFRsg@mail.gmail.com>*References*: <CAFMZHLq6qvcQv2mghe1Qx9KTKtvj=vTNf9YKHeOghLOSHsFRsg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.1.1

Dear Stanislav,

http://www.isa-afp.org/browser_info/current/AFP/Flyspeck-Tame/Arch.html

http://www.isa-afp.org/browser_info/current/AFP/Flyspeck-Tame/ArchComp.html

Best Tobias On 06/06/2016 20:44, ÐÑÐÐÐÑÐÐÐ ÐÐÐÐÐÐÐÑÐÐÐÑ ÐÐÐÑÐÐÐ wrote:

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.

**Attachment:
smime.p7s**

**References**:**[isabelle] Large theories***From:*ÐÑÐÐÐÑÐÐÐ ÐÐÐÐÐÐÐÑÐÐÐÑ ÐÐÐÑÐÐÐ

- Previous by Date: Re: [isabelle] Turnstile
- Next by Date: Re: [isabelle] Large theories
- Previous by Thread: [isabelle] Large theories
- Next by Thread: Re: [isabelle] Large theories
- Cl-isabelle-users June 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list