Re: [mizar] Re: Mizar 7.8.04 MML 4.80.962

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Freek,

On Sun, 25 Mar 2007, Freek Wiedijk wrote:

> > Anyway, I agree that readability is one of Mizar's
> > strengths, and we should try to preserve it.
>
> I very much agree.  (That's why I never liked the change that
> you need to use "deffunc" and "defpred" now if you want to
> use a scheme.  The proofs are much less readable that way.)

For some complicated schemes it may be the opposite: it may be hard for 
human readers to find the right instantiation if the search space is 
sufficiently large. But I guess it would not be difficult to have 
hide/show of for-scheme-only deffuncs and defpreds in html.

> > > but the "identify" construction wasn't available those days.
>
> I don't think I know what this is.  Can you clarify on the
> list, or point to a description somewhere?

http://mizar.uwb.edu.pl/forum/archive/0303/msg00017.html

however instead of "assume", "when" is now used:

Identify-Registration =
   "identify" Functor-Pattern "with" Functor-Pattern
    [ "when" Variable-Identifier "=" Variable-Identifier
             { "," Variable-Identifier "=" Variable-Identifier }  ] ";"
   Correctness-Conditions .

I think the construct is still quite experimental, and its current 
implementation is something like having multiple "equals" 
(i.e. expanded) (re)definitions of a functor available at the same time.

Josef