Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.



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]: http://afp.sourceforge.net/browser_info/current/HOL/Simpl/Vcg.html
  [2]: 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 MHonArc.