Re: defining sets recursively

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