Re: [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 

would actually be the same as

apply 

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 

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



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Mathias Fleury]

Hi all,


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.



Mathias


> On 12. Sep 2018, at 11:12, Lawrence Paulson  wrote:
> 
> Signed PGP part
> I regard it as indispensable. But it does need better pretty printing. Also I 
> greatly prefer the if/for format to assume/fix.
> 
> Larry
> 
>> On 12 Sep 2018, at 07:23, Florian Haftmann 
>>  wrote:
>> 
 On 7 Sep 2018, at 19:18, Makarius  wrote:
 
 I can't try it out, since theory "Explorer" is missing.
>>> 
>>> Attached. A very cool thing.
>> 
>> Nice to see that old draft from 5 years ago.
>> 
>> I would still agree that such a tool would be tremendously useful, but
>> before going into the distro it would need technical improvement, i.e.
>> more civilized approach toward Isar proof text generation, similar to
>> Sledgehammer_Isar_Proof.
>> 
>> Any opinions on that?
>> 
>> Cheers,
>>  Florian
>> 
>> --
>> 
>> PGP available:
>> http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>> 
> 
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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.

Larry

> On 12 Sep 2018, at 07:23, Florian Haftmann 
>  wrote:
> 
>>> On 7 Sep 2018, at 19:18, Makarius  wrote:
>>> 
>>> I can't try it out, since theory "Explorer" is missing.
>> 
>> Attached. A very cool thing.
> 
> Nice to see that old draft from 5 years ago.
> 
> I would still agree that such a tool would be tremendously useful, but
> before going into the distro it would need technical improvement, i.e.
> more civilized approach toward Isar proof text generation, similar to
> Sledgehammer_Isar_Proof.
> 
> Any opinions on that?
> 
> Cheers,
>   Florian
> 
> --
> 
> PGP available:
> http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 



signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Florian Haftmann]

>> On 7 Sep 2018, at 19:18, Makarius  wrote:
>>
>> I can't try it out, since theory "Explorer" is missing.
> 
> Attached. A very cool thing. 

Nice to see that old draft from 5 years ago.

I would still agree that such a tool would be tremendously useful, but
before going into the distro it would need technical improvement, i.e.
more civilized approach toward Isar proof text generation, similar to
Sledgehammer_Isar_Proof.

Any opinions on that?

Cheers,
Florian

-- 

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



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev