Re: "mode Element of ...", some questions...

On Tue, 20 Oct 2009, Ozyavas, Adem wrote:

> Dear All,
>
> I would like to ask a question but before that please let me present the following Mizar fragment:
>
>
> definition
>  func setA -> set equals
>    {k where k is Element of NAT: k < 15};
>  correctness;
> end;
>
> definition
>  let e be Element of setA;
>  func f(e) -> Element of setA means
>    ...
> end;
>
> f(1) = ...;
> ::>*103  (Unknown Functor)
>
>
> 1 is Element of setA;
> ::>                         *4 (This inference is not accepted)
>
>
> My questions are
> (1) how to make Mizar accept "1 is Element of setA"? I checked the MML for "mode Element of ..." examples and could not find anything that could help me.

As '1' is a numeral and not a 'regular' functor, you cannot redefine it, 
or register new attributes for it.

> (2) This relates to the Question (1). How can I make sure that 1 is known to be an Element of setA so that 103 error does not occur?

But you can always use a 'permissive' definition of f(), so that it 
accepts all 'Element of NAT', but is meaningful only for these in 'setA', 
e.g.

definition
  let e be Element of NAT;
  assume e in setA;
:: or e < 15
   func f(e) -> Element of setA means
   ...
end;

Then f(1) is a perfectly legal expression;

Best,
Adam Naumowicz

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================