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