Re: [isabelle] Isabelle2015-RC0 available for testing

Le 04/05/2015 09:56, Makarius a Ãcrit :
> On Mon, 4 May 2015, Jasmin Blanchette wrote:
>> I should perhaps add for clarification that Auto Sledgehammer, like
>> the other auto tools, works fine for top-level lemmas but not for
>> subgoals or intermediate steps in an Isar proof. This is something
>> that would require more work in Isabelle/jEdit.
> There is not so much going on there.  The PIDE print function for the
> auto tools merely has a hardwired policy for "theory_goal" commands,
> see also
> That may be understood as a relatively crude way to prevent the
> implicit mode from sucking up too many resources.  Even in that form
> it is already quite heavy.
> Nonetheless I think that implicit tools (with good scheduling
> policies) are better than funny command-lines or click-panels.  Too
> bad that we don't have 32 or 64 cores now as we should.  Damn market
> economy.
>> For starters, it would be nice if Isabelle/jEdit could notice
>> âsorryâs and attack them. I donât think Iâm the only one who
>> introduces them regularly as placeholders to prevent the interface
>> from showing errors.
> In recent Isabelle versions the idea is to eliminate the need for
> "sorry" proofs.  The document processing recovers at the next theory
> command.
What is exactly a theory command? As for now, I cannot get rid of them
in Isar proofs:

have XXX
hence YYY by t

seems to be processed as "have XXX by t".

Nor on the lemma level, for example:
lemma test: "f var"

lemma "f 1"
using testby auto

Contrary to previous case "lemma 'f 1'" is not skipped. But the lemma
"test" is not defined. While this was the goal of adding a lemma (under
my workflow at least): whenever I need another lemma, I put it before
and see if it can be useful.

So what do you mean exactly by "eliminating the need for 'sorry' proofs"?

(using Isabelle RC, which is a recent Isabelle version, I assume).


> Concerning auto tools: there could be some way to mark/unmark parts of
> the proof document that should be attacked implicitly.
>     Makarius

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.