Re: [mizar] Strong Mizar wish: linking to consider

[Markus Wenzel <wenzelm@informatik.tu-muenchen.de>]

On Fri, 8 Mar 2002, Freek Wiedijk wrote:

> Currently it's not possible to say something like:
>
>   consider x such that
>  A1: P x and
>  A2: Q x by ...;
>   then R x by ...;
>
> because the "then" is not allowed.  I would very much
> like this to be allowed.  It would save me many labels.
>
> It might not seem clear what the "then" should link to.
> There are four possibilities:
>
>   1. "ex x st P x"
>   2. "P x & Q x"
>   3. "P x"
>   4. "Q x"

Just note that in Isabelle/Isar this would look as follows:

  obtain x where a1: P x and x2: Q x <proof>
  then have R x <proof>

Due to the way the Isar language works, especially derived concepts like
this "obtain", there was never a question that "then" would pick up *all*
of the previously established facts simultaneously (as a list of local
theorems).  Only afterwards I realized that Mizar treats this differently.

As I understand it, Mizar only has singleton facts.  So probably your
proposal number 2 would probably come close to the most desirable
behaviour.  Note that number 1 does not make too much sense from the
user's perspective, since the existential statement is just an internal
auxiliary thing to justify that consider/obtain in the first place.


	Markus

--------------------------------------------------------------------
Institut für Informatik, TU München, http://www4.in.tum.de/~wenzelm/
--- <>< ------------------------------------------------------------