reductions in Mizar

Hello,

in Mizar version 7.12.02, which will be issued officially soon,
a new mechanism, called reductions, has been implemented.

Reductions are an attempt to increase power of the Mizar checker.

Syntax is:

registration
   let x_1,...,x_n;
   reduce term1(x_1,...,x_n) to term2(x_1,...,x_n);
   reducibility
   proof
     thus term1(x_1,...,x_n) = term2(x_1,...,x_n);
   end;
end;

where term2 has to be a _subterm_ of term1. This restriction is a result 
of a Mizar principle, that the system does not generate new terms itself 
(with very few exceptions).

Correctness condition to be proved is "reducibility".

Examples of reductions are:

reduce X \/ {} to X

reduce union {} to {}


Reductions are treated by equalizer. Whenever system finds a term which 
can be matched to the 'term1', equivalence classes of 'term1' and its 
subterm 'term2' are joined.


An important restriction of usage reductions is that 'term1' has to occur 
explicitly in an equality. For example, having a reduction

registration
   let X be set;
   reduce X \/ {} to X;
   reducibility;
end;

a reasoning

now
   let X be set;
   X \/ {} = X;
end;

is accepted without any reference, while

now
   let X be set;
   set A = {};
   X \/ A = X;
             *4
end;

not.

The reason is that reductions are applied at the very beginning stage of 
building of the congruence closure performed by the equalizer.


Reductions are imported to a Mizar article through environment directive
"registrations".

Best regards
Artur