[isabelle-dev] [isabelle] the sound of a sledgehammer

[Peter Lammich]

On Do, 2013-02-14 at 17:22 +0000, Lawrence Paulson wrote:
> In a dream scenario, one might imagine opening a document containing a number of occurrences of "sorry", and each one of these occurrences would be given to counterexample finders and to sledgehammer, without any specific user intervention. Then somehow any counterexamples or proofs that were found would be noted somehow, and the user could inspect these.
> 
> I recognise this idea isn't even half baked. But I know that you want to look at these problems differently from just saying, "how did it work in Proof General"? And the idea of having a whole bunch of gaps checked (as it were) simultaneously is very appealing.
> 

But both in jEdit and PG, there is one "gap" that the user is currently
interested in most, and that's the proof he's currently editing viz. the
lemma he has just typed. Unlike the document model of Isabelle/jEdit,
the user that develops a theory file only works at one place in the file
at the same time, and pays special interest to this place.
As a user who just typed in/altered a lemma, I'm interested in a
counter-example for that lemma --- without needing to type quickcheck,
sledgehammer, or sorry first (I usually want to type proof, by, or apply
there). 


--
  Peter