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



On 12 Dec 2013, at 1:22 am, Lars Noschinski <noschinl at in.tum.de> wrote:

> On 11.12.2013 14:58, Makarius wrote:
>> From this I guess that your change Isabelle/93a84eb6c522 from 02-Jan-1998
>> no longer conforms to what you would do today.  Although it is hard to
>> tell precisely, since flex-flex pair are extremely rare, and defining an
>> intended meaning operates almost at 0 entropy.
>
> I guess the rarity of flex-flex pairs depends on the kind of proofs you
> do. I recently wrote a VCG for program refinement, consisting mainly of
> a large set of introduction rules. I remember seeing flex-flex pairs
> quite often for the intermediate results (although the usually would
> disappear when the VCG successfully completed).

Yes, that’s very similar to the kinds of proofs we have.

flex-flex pairs are still rare in our proofs, but they do pop up occasionally.

Cheers,
Gerwin

________________________________

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.