[isabelle-dev] NEWS: structured Isar goal statements

[Makarius]

On Mon, 15 Jun 2015, Lars Noschinski wrote:

> I wonder whether this syntax would be useful for other situations, e.g. 
> assume and assumes, too?

Something like that is in the MKM 2008 paper "Logic-free reasoning in 
Isabelle/Isar", see 
http://www4.in.tum.de/~wenzelm/papers/isar-reasoning.pdf


I was thinking about this again when brushing up the internal Isar 
structures, but did not make any moves in that direction yet, due to the 
following open questions:

   * What is the meaning of this anyway?

       assume "B x" if "A x" for x

     Is it:

       assume "!!x. A x ==> B x"

     or is it:

       fix x assume "A x" assume "B x"

     Since if/for in have/show is explicit notation for the eigen-context,
     the second one is conceptually more obvious, but probably not to the
     user.

   * What are convicing applications where spelling out !! and ==>
     connectives in assumptions, or extra fix/assume context elements is
     too awkward?

   * Implementation complexity: if/for for assume and presume would demand
     the same for "theorem fixes / assumes / shows / obtains", probably
     also for 'obtain' and 'consider' etc.


 	Makarius