Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.
This is a very unfortunate situation to be in. But I guess it’s no different from other kinds of legacy nightmare code.
You’ll probably have to bite the bullet and redo some of these proofs. I assume they are very lengthy apply-chains rather than structured proofs. The irony is that it might have been easier to write structured proofs in the first place.
On 10 Dec 2013, at 22:37, David Greenaway <David.Greenaway at nicta.com.au> wrote:
> On 11/12/13 08:42, Lawrence Paulson wrote:
>> You shouldn’t have to redo the proofs. If you are lucky, doing the
>> proof in Isabelle2013 may give you a clue as to how the variables are
>> being instantiated, so that you can add a constraint somewhere. And
>> flex-flex constraints are very rare.
> Again, these tend to pop up in very large proofs which I have very
> little understanding or context of. Add in a few moving parts, such as
> Schirmer's SIMPL VCG , our own tactics (for example, bundled with
> ), and ugly proofs done on a deadline, it all becomes a bit much.
> Tracking down the original problem involved carefully comparing
> line-by-line the proof output between Isabelle2013 and Isabelle2013-1
> and seeing where they diverged.
> I am certainly not advocating this proof style, merely trying to cope
> with it.
>> Do you really have 400k lines of Isabelle proof scripts? All of the
>> Isabelle/HOL theories (including examples and libraries) are barely
>> more than that.
> ~/l4.verified # rm -rf isabelle
> ~/l4.verified # wc -l **/*.thy | tail -1
> 536136 total
> : http://afp.sourceforge.net/browser_info/current/HOL/Simpl/Vcg.html
> : http://ssrg.nicta.com.au/projects/TS/autocorres/
> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
This archive was generated by a fusion of
Pipermail (Mailman edition) and