sorry to bother again :(

[Ozyavas, Adem]

Dear All,

Sorry to bother again with some details. I have the following introduction and question.

Let A be the following set (it is not exactly the Mizar syntax:)):

::starts here

    defpred P[Element of NAT,Element of NAT] means ...

    setA = {[a,b] where a is Element of NAT, b is Element of NAT: P[a,b]}

   theorem setA is non empty
   proof
     ex a,b being Element of NAT st [a,b] in setA
     proof
        take 1 , 2 ;
        P[1,2] proof ... end;
        hence [1,2] in setA;
::>                                #4  
     end;
     then consider a,b being Element of NAT such that L1: [a,b] in setA;
     thus thesis by L1;  ::BOOLE is in the requirements
  end;

::ends here


After proving that property P holds for particular objects (1 and 2 in this case), that is, P[1,2];
what other conditions Mizar expects for the "[1,2] in setA" to hold?

I have found the solution for finite sets in the ENUMSET1.miz article  but not for this case where
set's elements are those that satisfy a property.

Thank you again and sorry my troubles...

Adem Ozyavas
Texas Tech University

[Artur Kornilowicz]

Hi Adem,

first, please check is Mizar understands that

1 is Element of NAT

in your environment.

setA consist of pairs of such elements.

I guess you need

constructors SUBSET_1, NUMBERS;
requirements SUBSET, NUMERALS;

in your environment.

If it does not work, feel free to ask again.

Best,
Artur


On Mon, 26 Oct 2009, Ozyavas, Adem wrote:

> Dear All,
>
> Sorry to bother again with some details. I have the following introduction and question.
>
> Let A be the following set (it is not exactly the Mizar syntax:)):
>
> ::starts here
>
>    defpred P[Element of NAT,Element of NAT] means ...
>
>    setA = {[a,b] where a is Element of NAT, b is Element of NAT: P[a,b]}
>
>   theorem setA is non empty
>   proof
>     ex a,b being Element of NAT st [a,b] in setA
>     proof
>        take 1 , 2 ;
>        P[1,2] proof ... end;
>        hence [1,2] in setA;
> ::>                                #4
>     end;
>     then consider a,b being Element of NAT such that L1: [a,b] in setA;
>     thus thesis by L1;  ::BOOLE is in the requirements
>  end;
>
> ::ends here
>
>
> After proving that property P holds for particular objects (1 and 2 in this case), that is, P[1,2];
> what other conditions Mizar expects for the "[1,2] in setA" to hold?
>
> I have found the solution for finite sets in the ENUMSET1.miz article  but not for this case where
> set's elements are those that satisfy a property.
>
> Thank you again and sorry my troubles...
>
> 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