[isabelle-dev] Explorer.thy [was: performance problems]

[Florian Haftmann]

Hi all,

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
proof skeleton

	proof -
          fix ys
          assume Qs
          have C1 if Ps1 for xs1
          moreover have C2 if Ps2 for xs2
          …
	  moreover have Cn if Psn for xsn
          ultimately show D
            by
        qed <method expr>

and hence provide a way to quickly get to the essence of a proof after
initial »explore auto«.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180918/9518e27a/attachment.sig>