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

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: [email protected]

Dept. of Programming and Formal Methods    http://math.uwb.edu.pl/~arturk/
Institute of Computer Science              tel. +48 (85) 745-7662
University of Bialystok                    fax. +48 (85) 745-7662
Sosnowa 64, 15-887 Bialystok, Poland