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