[isabelle-dev] NEWS: structured Isar goal statements

Makarius makarius at sketis.net
Mon Jun 15 20:30:39 CEST 2015

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 

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

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


More information about the isabelle-dev mailing list