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