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.

Larry Paulson

On 10 Dec 2013, at 22:37, David Greenaway <David.Greenaway at> 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 [1], our own tactics (for example, bundled with
> [2]), 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
> :(
> Cheers,
> David
>  [1]:
>  [2]:
> ________________________________
> 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 MHonArc.