The abstract of the Mizar article:

Recursive Definitions

by

Krzysztof Hryniewiecki

Received September 4, 1989

MML identifier: RECDEF_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, FUNCT_1, RELAT_1, PARTFUN1, TARSKI, ARYTM_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, REAL_1,
      NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCT_2, DOMAIN_1;
 constructors REAL_1, NAT_1, FINSEQ_1, FUNCT_2, DOMAIN_1, XREAL_0, MEMBERED,
      XBOOLE_0;
 clusters FUNCT_1, RELSET_1, FINSEQ_1, SUBSET_1, ARYTM_3, MEMBERED, ZFMISC_1,
      XBOOLE_0, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve n,m,k for Nat,
        D for non empty set,
        Z,x,y,z,y1,y2 for set,
        p,q for FinSequence;

definition let D be set, p be PartFunc of D,NAT; let n be Element of D;
 redefine func p.n -> Nat;
end;

::::::::::::::::::::::::::::::::::::::::
::       Schemes of existence         ::
::::::::::::::::::::::::::::::::::::::::

scheme RecEx{A() -> set,P[set,set,set]}:
   ex f being Function st dom f = NAT & f.0 = A() &
     for n being Element of NAT holds P[n,f.n,f.(n+1)]
 provided
   for n being Nat for x being set
       ex y being set st P[n,x,y] and
   for n being Nat for x,y1,y2 being set
         st P[n,x,y1] & P[n,x,y2] holds y1=y2;

scheme RecExD{D()->non empty set,A() -> Element of D(),
                  P[set,set,set]}:
   ex f being Function of NAT,D() st
     f.0 = A() &
     for n being Element of NAT holds P[n,f.n,f.(n+1)]
 provided
   for n being Nat for x being Element of D()
       ex y being Element of D() st P[n,x,y];

scheme LambdaRecEx{A() -> set,G(set,set) -> set}:
  ex f being Function st dom f = NAT &
      f.0 = A() & for n being Element of NAT holds f.(n+1) = G(n,f.n);

scheme LambdaRecExD{D() -> non empty set, A() -> Element of D(),
                 G(set,set) -> Element of D()}:
  ex f being Function of NAT,D() st
      f.0 = A() & for n being Element of NAT holds f.(n+1) = G(n,f.n);

scheme FinRecEx{A() -> set,N() -> Nat,P[set,set,set]}:
  ex p being FinSequence st len p = N() & (p.1 = A() or N() = 0) &
    for n st 1 <= n & n < N() holds P[n,p.n,p.(n+1)]
 provided
    for n being Nat st 1 <= n & n < N()
          for x being set ex y being set st P[n,x,y] and
    for n being Nat st 1 <= n & n < N()
         for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2;

scheme FinRecExD{D() -> non empty set,A() -> Element of D(),
                  N() -> Nat, P[set,set,set]}:
 ex p being FinSequence of D() st len p = N() & (p.1 = A() or N() = 0) &
    for n st 1 <= n & n < N() holds P[n,p.n,p.(n+1)]
provided
 for n being Nat st 1 <= n & n < N() holds for x being Element of D()
      ex y being Element of D() st P[n,x,y];

scheme SeqBinOpEx{S() -> FinSequence,P[set,set,set]}:
  ex x st ex p being FinSequence st x = p.(len p) & len p = len S() &
     p.1 = S().1 & for k st 1 <= k & k < len S() holds
         P[S().(k+1),p.k,p.(k+1)]
provided
 for k,x st 1 <= k & k < len S() ex y st P[S().(k+1),x,y] and
 for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) &
      P[z,x,y1] & P[z,x,y2] holds y1 = y2;

scheme LambdaSeqBinOpEx{S() -> FinSequence,F(set,set) -> set}:
  ex x st ex p being FinSequence st x = p.(len p) & len p = len S() &
   p.1 = S().1 & for k st 1 <= k & k < len S()
     holds p.(k+1) = F(S().(k+1),p.k);

::::::::::::::::::::::::::::::::::::::
::     Schemes of uniqueness        ::
::::::::::::::::::::::::::::::::::::::

scheme RecUn{A() -> set, F, G() -> Function, P[set,set,set]}:
  F() = G()
provided
 dom F() = NAT & F().0 = A() & for n holds P[n,F().n,F().(n+1)] and
 dom G() = NAT & G().0 = A() & for n holds P[n,G().n,G().(n+1)] and
 for n for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2;

scheme RecUnD{D() -> non empty set,A() -> Element of D(),
        P[set,set,set], F, G() -> Function of NAT,D()} : F() = G()
 provided
   F().0 = A() & (for n holds P[n,F().n,F().(n+1)]) and
   G().0 = A() & (for n holds P[n,G().n,G().(n+1)]) and
   for n being Nat,x,y1,y2 being Element of D()
         st P[n,x,y1] & P[n,x,y2] holds y1=y2;

scheme LambdaRecUn{A() -> set, RecFun(set,set) -> set,
        F, G() -> Function}:
  F() = G()
  provided
   dom F() = NAT & F().0 = A() &
        for n holds F().(n+1) = RecFun(n,F().n) and
   dom G() = NAT & G().0 = A() &
        for n holds G().(n+1) = RecFun(n,G().n);

scheme LambdaRecUnD{D() -> non empty set,A() -> Element of D(),
         RecFun(set,set) -> Element of D(),
        F, G() -> Function of NAT,D()}:
  F() = G()
  provided
   F().0 = A() & for n holds F().(n+1) = RecFun(n,F().n) and
   G().0 = A() & for n holds G().(n+1) = RecFun(n,G().n);

scheme LambdaRecUnR{A() -> Real, RecFun(set,set) -> set,
   F, G() -> Function of NAT,REAL}:
 F() = G()
 provided
 F().0 = A() & for n holds F().(n+1) = RecFun(n,F().n) and
 G().0 = A() & for n holds G().(n+1) = RecFun(n,G().n);

scheme FinRecUn{A() -> set,N() -> Nat,
       F, G() -> FinSequence, P[set,set,set]}:
  F() = G()
provided
 for n st 1 <= n & n < N()
       for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2 and
 len F() = N() & (F().1 = A() or N() = 0) &
    for n st 1 <= n & n < N() holds P[n,F().n,F().(n+1)] and
 len G() = N() & (G().1 = A() or N() = 0) &
    for n st 1 <= n & n < N() holds P[n,G().n,G().(n+1)];

scheme FinRecUnD{D() -> non empty set, A() -> Element of D(), N() -> Nat,
    F, G() -> FinSequence of D(), P[set,set,set]}:
  F() = G()
provided
 for n st 1 <= n & n < N()
       for x,y1,y2 being Element of D()
         st P[n,x,y1] & P[n,x,y2] holds y1 = y2 and
 len F() = N() & (F().1 = A() or N() = 0) &
    for n st 1 <= n & n < N() holds P[n,F().n,F().(n+1)] and
 len G() = N() & (G().1 = A() or N() = 0) &
    for n st 1 <= n & n < N() holds P[n,G().n,G().(n+1)];

scheme SeqBinOpUn{S() -> FinSequence,P[set,set,set],x, y() -> set}:
  x() = y()
provided
 for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) &
        P[z,x,y1] & P[z,x,y2] holds y1 = y2 and
 ex p being FinSequence st x() = p.(len p) & len p = len S() & p.1 = S().1 &
      for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] and
 ex p being FinSequence st y() = p.(len p) & len p = len S() & p.1 = S().1 &
      for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)];

scheme LambdaSeqBinOpUn{S() -> FinSequence, F(set,set) -> set,
                          x, y() -> set}:
  x() = y()
provided
 ex p being FinSequence st x() = p.(len p) & len p = len S() & p.1 = S().1 &
    for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k)
  and
 ex p being FinSequence st y() = p.(len p) & len p = len S() & p.1 = S().1 &
    for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k);
           :::::::::::::::::::::::::::::::
::   Schemes of definitness  ::
:::::::::::::::::::::::::::::::

scheme DefRec{A() -> set,n() -> Nat,P[set,set,set]}:
   (ex y being set st ex f being Function st
     y = f.n() & dom f = NAT & f.0 = A() &
       for n holds P[n,f.n,f.(n+1)]) &
     for y1,y2 being set st
        (ex f being Function st
     y1 = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) &
        (ex f being Function st
     y2 = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)])
    holds y1 = y2
provided

 for n,x ex y st P[n,x,y] and
 for n,x,y1,y2 st P[n,x,y1] & P[n,x,y2] holds y1 = y2;

scheme LambdaDefRec{A() -> set,n() -> Nat,RecFun(set,set) -> set}:
   (ex y being set st ex f being Function st
     y = f.n() & dom f = NAT & f.0 = A() &
       for n holds f.(n+1) = RecFun(n,f.n)) &
     for y1,y2 being set st
     (ex f being Function st
     y1 = f.n() & dom f = NAT & f.0 = A() &
       for n holds f.(n+1) = RecFun(n,f.n)) &
     (ex f being Function st
     y2 = f.n() & dom f = NAT & f.0 = A() &
       for n holds f.(n+1) = RecFun(n,f.n))
    holds y1 = y2;

scheme DefRecD{D() -> non empty set,A() -> (Element of D()),
           n() -> Nat,P[set,set,set]}:
   (ex y being Element of D() st ex f being Function of NAT,D() st
     y = f.n() & f.0 = A() &
       for n holds P[n,f.n,f.(n+1)]) &
     for y1,y2 being Element of D() st
        (ex f being Function of NAT,D() st
     y1 = f.n() & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) &
        (ex f being Function of NAT,D() st
     y2 = f.n() & f.0 = A() & for n holds P[n,f.n,f.(n+1)])
    holds y1 = y2
provided
 for n being Nat,x being Element of D()
      ex y being Element of D() st P[n,x,y] and
 for n being Nat, x,y1,y2 being Element of D()
      st P[n,x,y1] & P[n,x,y2] holds y1 = y2;

scheme LambdaDefRecD{D() -> non empty set, A() -> Element of D(),
       n() -> Nat, RecFun(set,set) -> Element of D()}:
   (ex y being Element of D() st ex f being Function of NAT,D() st
     y = f.n() & f.0 = A() &
       for n being Nat holds f.(n+1) = RecFun(n,f.n)) &
     for y1,y2 being Element of D() st
     (ex f being Function of NAT,D() st
     y1 = f.n() & f.0 = A() &
       for n being Nat holds f.(n+1) = RecFun(n,f.n)) &
     (ex f being Function of NAT,D() st
     y2 = f.n() & f.0 = A() &
       for n being Nat holds f.(n+1) = RecFun(n,f.n))
    holds y1 = y2;

scheme SeqBinOpDef{S() -> FinSequence,P[set,set,set]}:
  (ex x st ex p being FinSequence st x = p.(len p) & len p = len S() &
     p.1 = S().1 & for k st 1 <= k & k < len S() holds
        P[S().(k+1),p.k,p.(k+1)]) &
  for x,y st
     (ex p being FinSequence st x = p.(len p) & len p = len S() &
     p.1 = S().1 & for k st 1 <= k & k < len S() holds
        P[S().(k+1),p.k,p.(k+1)]) &
     (ex p being FinSequence st y = p.(len p) & len p = len S() &
     p.1 = S().1 & for k st 1 <= k & k < len S() holds
        P[S().(k+1),p.k,p.(k+1)])
   holds x = y
provided
 for k,y st 1 <= k & k < len S() ex z st P[S().(k+1),y,z] and
 for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) &
          P[z,x,y1] & P[z,x,y2] holds y1 = y2;

scheme LambdaSeqBinOpDef{S() -> FinSequence,F(set,set) -> set}:
  (ex x st ex p being FinSequence st x = p.(len p) & len p = len S() &
    p.1 = S().1 & for k st 1 <= k & k < len S()
      holds p.(k+1) = F(S().(k+1),p.k)) &
  for x,y st
    (ex p being FinSequence st x = p.(len p) & len p = len S() &
    p.1 = S().1 & for k st 1 <= k & k < len S()
        holds p.(k+1) = F(S().(k+1),p.k)) &
    (ex p being FinSequence st y = p.(len p) & len p = len S() &
    p.1 = S().1 & for k st 1 <= k & k < len S()
       holds p.(k+1) = F(S().(k+1),p.k))
   holds x = y;