[isabelle-dev] NEWS: structured Isar goal statements

[Johannes Hölzl]

Am Montag, den 15.06.2015, 20:30 +0200 schrieb Makarius:
> On Mon, 15 Jun 2015, Lars Noschinski wrote:
>    * 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.

Hm, maybe with parenthesis:
  assume ("integrable (M i) (f i)" if "i : I" for i)
But yeah, this does not look very canonical...

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

At least if premises share sub-premises, for example:

lemma nn_integral_setsum:
  assumes "finite I"
  assumes ("!!x. 0 <= f i x" and "f i : borel_measurable M"
             if "i : I" for i)
  show "(INT x. SUM i : I. f i x d M) = (SUM i : I. INT x. f i x d M)"
...

E.g. in measure theory I often have the case to assume that for a
indexed-familiy all elements are non-negative & measurable or similar.

>    * 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev