[isabelle-dev] Explorer.thy [was: performance problems]
florian.haftmann at informatik.tu-muenchen.de
Tue Sep 18 21:04:55 CEST 2018
Am 12.09.2018 um 11:12 schrieb Lawrence Paulson:
> I regard it as indispensable. But it does need better pretty printing.
> Also I greatly prefer the if/for format to assume/fix.
Am 12.09.2018 um 12:12 schrieb Mathias Fleury:
> I have my own version of explore
> (https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy), which
> does not have better pretty printing, but has two variants that I find
> indispensable: explore_have produces "have … if … for …"
> and explore_lemma produces "lemma fixes … assumes … shows …". There is
> even an option for cartouches.
proper pretty printing should not be to difficult; maybe
Sledgehammer_Isar_Proof can be reused or a common base extracted from that.
explore_have should maybe just be the standard variant.
I would suggest a further variant
explore <method expr>
would actually be the same as
apply <method expr>
but, given a proof goal ‹!!ys. Qs ==> D›, for remaining goals ‹!!xs1.
Ps1 ==> C1› … ‹!!xsn. Psn ==> Cn› after method application suggest a
have C1 if Ps1 for xs1
moreover have C2 if Ps2 for xs2
moreover have Cn if Psn for xsn
ultimately show D
qed <method expr>
and hence provide a way to quickly get to the essence of a proof after
initial »explore auto«.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev