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

[Ozyavas, Adem]

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.
(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?


Thank you all and I always appreciate the group's help.
Regards,

Adem Ozyavas
Texas Tech University

[Artur Kornilowicz]

Hi Adem,

there is a couple of solutions to your problem:

first, at global level (e.g. theorems) you can write

theorem
   for x being Element of setA st x = 1 holds f(x) ...;

Inside proofs you can write

reconsider j = 1 as Element of setA;
f(j) = ...;

You can't use 'j' in theorems formulations because local constants can't
be imported to the library.

Another solution is to use

definition
   let x, y be set;
   assume x in y;
   func In (x, y) -> Element of y equals
:: FUNCT_7:def 1
   x;
end;

Having this, Mizar automatically knows that
In(1,setA) is Element of setA;

So you can formulate facts as

f(In(1,setA)) = ...;


I believe it helps.

Best regards
Artur




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. (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?
>
>
> Thank you all and I always appreciate the group's help.
> Regards,
>
> Adem Ozyavas
> Texas Tech University

==========================================================================

Artur Kornilowicz                          e-mail: arturk@...

Dept. of Programming and Formal Methods    http://math.uwb.edu.pl/~arturk/
Institute of Computer Science              tel. [phone]
University of Bialystok                    fax. [phone]
Sosnowa 64, 15-887 Bialystok, Poland

[Adam Naumowicz]

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: [phone]
Institute of Informatics                 Tel: [phone] (office)
University of Bialystok                  E-mail: adamn@...
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================