defining sets recursively

[Ozyavas, Adem]

Dear All,

Is there a way to define sets recursively in Mizar? I have searched tens of files in the MML and have not seen an example.
To give an example, I am trying to define the following set:

let S be set which is defined as follows:

(i) real numbers are in S, and
(ii) Assume A1, A2, ..., An are members of S, then <*A1,A2,...,An*> is a member of S. (Here <*...*> is the finite sequence notation from Mizar.)

With recursively defined sets (if possible) I want to define a finite sequence whose range is a subset of S, given below. For example, with the above recursively defined S such a finite sequence in Mizar of range subset of S would be:
   let fs be FinSequence of S;

the finite sequence <* 1, 4, <* 3, 12 *>,<*<*7,23*>, 34*>, 22*> is an example of fs as well as <*3,4,1*>. That is every finite sequence of arbitrarily nested finite sequences are examples of fs.

I appreciate your help in advance.

Sincerely,
Adem Ozyavas  

[trybulec]

Ozyavas, Adem wrote:

>Dear All,
>
>Is there a way to define sets recursively in Mizar? I have searched tens of files in the MML and have not seen an example.
>To give an example, I am trying to define the following set:
>
>let S be set which is defined as follows:
>
>(i) real numbers are in S, and
>(ii) Assume A1, A2, ..., An are members of S, then <*A1,A2,...,An*> is a member of S. (Here <*...*> is the finite sequence notation from Mizar.)
>
>  
>

Probably the simplest way to do it is to use the NAT_1:sch 11 scheme:

  deffunc F(set,set) = $2 \/ $2*;
  consider f being Function such that dom f = NAT &
  f.0 = REAL & for n being Nat holds f.(n+1) = F(n,f.n)
                   from NAT_1:sch 11;

then  your set S is
    Union f
'Union' is the union of the range: CARD_3:def 4

If you want to make it to a definition:

definition let A be set;
  func ??? A means
    ex  f  being Function st it = Union f & dom f = NAT &
     f.0 = A & for n being Nat holds f.(n+1) = F(n,f.n);
 existence
 proof
   :: use the scheme NAT_1:sch 11
 end;
 uniqueness;
end;

I believe it  is better to define the general concept, not just for REAL


Regards,
Andrzej Trybulec