:: Recursive Definitions. {P}art {II}
:: by Artur Korni{\l}owicz
::
:: Received February 10, 2004
:: Copyright (c) 2004-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ZFMISC_1, XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4,
TARSKI, CARD_1, ARYTM_3, MCART_1, NAT_1, ARYTM_1, XXREAL_0, FUNCT_7,
RECDEF_2, XTUPLE_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, DOMAIN_1,
ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_4, FUNCT_7, XXREAL_0;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, INT_1, BINARITH, FUNCT_7,
NAT_D, RELSET_1, XTUPLE_0;
registrations SUBSET_1, ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, XTUPLE_0;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin
reserve a,b,c,d,e,z for object, A,B,C,D,E for set;
:: Projections
definition
let x be triple object;
redefine func x`1_3 means
:: RECDEF_2:def 1
for y1,y2,y3 being object holds x = [y1,y2,y3] implies
it = y1;
redefine func x`2_3 means
:: RECDEF_2:def 2
for y1,y2,y3 being object holds x = [y1,y2,y3] implies
it = y2;
redefine func x`3_3 means
:: RECDEF_2:def 3
for y1,y2,y3 being object holds x = [y1,y2,y3] implies
it = y3;
end;
::$CT
theorem :: RECDEF_2:2
z in [:A,B,C:] implies z`1_3 in A & z`2_3 in B & z`3_3 in C;
theorem :: RECDEF_2:3
z in [:A,B,C:] implies z = [ z`1_3, z`2_3, z`3_3 ];
definition
let x be quadruple object;
redefine func x`1_4 means
:: RECDEF_2:def 4
for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
implies it = y1;
redefine func x`2_4 means
:: RECDEF_2:def 5
for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
implies it = y2;
redefine func x`3_4 means
:: RECDEF_2:def 6
for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
implies it = y3;
redefine func x`4_4 means
:: RECDEF_2:def 7
for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
implies it = y4;
end;
::$CT
theorem :: RECDEF_2:5
z in [:A,B,C,D:] implies z`1_4 in A & z`2_4 in B & z`3_4 in C & z`4_4 in D;
theorem :: RECDEF_2:6
z in [:A,B,C,D:] implies z = [ z`1_4, z`2_4, z`3_4, z`4_4 ];
definition
::$CD 5
end;
::$CT 3
:: Conditional schemes
scheme :: RECDEF_2:sch 1
ExFunc3Cond { C() -> set, P,Q,R[object], F,G,H(object) -> object }:
ex f being
Function st dom f = C() & for c being set st c in C() holds (P[c] implies f.c =
F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))
provided
for c being set st c in C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (Q[c] implies not R[c]) and
for c being set st c in C() holds P[c] or Q[c] or R[c];
scheme :: RECDEF_2:sch 2
ExFunc4Cond { C() -> set, P,Q,R,S[object], F,G,H,I(object) -> object }:
ex f being
Function st dom f = C() & for c being set st c in C() holds (P[c] implies f.c =
F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)) & (S[c] implies f
.c = I(c))
provided
for c being set st c in C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (P[c] implies not S[c]) & (Q[c] implies not R[c]) & (Q[c]
implies not S[c]) & (R[c] implies not S[c]) and
for c being set st c in C() holds P[c] or Q[c] or R[c] or S[c];
:: 1 step
scheme :: RECDEF_2:sch 3
DoubleChoiceRec { A, B() -> non empty set, A0() -> Element of
A(), B0() -> Element of B(), P[object,object,object,object,object] }:
ex f
being sequence of A(), g being sequence of B() st f.0 = A0() & g.0 =
B0() & for n being Nat holds P[n,f.n,g.n,f.(n+1),g.(n+1)] provided
for n being Nat, x being Element of A(), y being Element of B()
ex x1 being Element of A(), y1 being Element of B() st
P[n,x,y,x1,y1];
:: 2 steps
scheme :: RECDEF_2:sch 4
LambdaRec2Ex { A,B() -> set, F(object,object,object) -> object }:
ex f being Function st
dom f = NAT & f.0 = A() & f.1 = B() & for n being Nat holds f.(n+2)
= F(n,f.n,f.(n+1));
scheme :: RECDEF_2:sch 5
LambdaRec2ExD { X() -> non empty set, A,B() -> Element of X(),
F(object,object,object) -> Element of X() }:
ex f being sequence of X() st f.0 = A() & f.1 = B()
& for n being Nat holds f.(n+2) = F(n,f.n,f.(n+1));
scheme :: RECDEF_2:sch 6
LambdaRec2Un { A,B() -> object, F,G() -> Function,
F(object,object,object) -> object }:
F() = G()
provided
dom F() = NAT and
F().0 = A() & F().1 = B() and
for n being Nat holds F().(n+2) = F(n,F().n,F().(n+1)) and
dom G() = NAT and
G().0 = A() & G().1 = B() and
for n being Nat holds G().(n+2) = F(n,G().n,G().(n+1));
scheme :: RECDEF_2:sch 7
LambdaRec2UnD { X() -> non empty set, A,B() -> Element of X(), F,G() ->
sequence of X(), F(object,object,object) -> Element of X() }: F() = G()
provided
F().0 = A() & F().1 = B() and
for n being Nat holds F().(n+2) = F(n,F().n,F().(n+1)) and
G().0 = A() & G().1 = B() and
for n being Nat holds G().(n+2) = F(n,G().n,G().(n+1));
:: 3 steps
scheme :: RECDEF_2:sch 8
LambdaRec3Ex { A,B,C() -> set, F(object,object,object,object) -> object }:
ex f being
Function st dom f = NAT & f.0 = A() & f.1 = B() & f.2 = C() & for n being
Nat holds f.(n+3) = F(n,f.n,f.(n+1),f.(n+2));
scheme :: RECDEF_2:sch 9
LambdaRec3ExD { X() -> non empty set, A,B,C() -> Element of X(),
F(object,object,object,object) -> Element of X() }:
ex f being sequence of X() st f.0 = A() & f.1 = B() & f.2 = C() &
for n being Nat holds f.(n+3) = F(n,f.n,f.(n+1),f.(n+2));
scheme :: RECDEF_2:sch 10
LambdaRec3Un { A,B,C() -> object, F,G() -> Function,
F(object,object,object,object) -> object }: F() = G()
provided
dom F() = NAT and
F().0 = A() & F().1 = B() & F().2 = C() and
for n being Nat holds F().(n+3) = F(n,F().n,F().(n+1),F()
.(n+2)) and
dom G() = NAT and
G().0 = A() & G().1 = B() & G().2 = C() and
for n being Nat holds G().(n+3) = F(n,G().n,G().(n+1),G()
.(n+2));
scheme :: RECDEF_2:sch 11
LambdaRec3UnD { X() -> non empty set, A,B,C() -> Element of X(), F,G() ->
sequence of X(), F(object,object,object,object) -> Element of X() }:
F() = G()
provided
F().0 = A() & F().1 = B() & F().2 = C() and
for n being Nat holds F().(n+3) = F(n,F().n,F().(n+1),F()
.(n+2)) and
G().0 = A() & G().1 = B() & G().2 = C() and
for n being Nat holds G().(n+3) = F(n,G().n,G().(n+1),G()
.(n+2));
:: 4 steps
scheme :: RECDEF_2:sch 12
LambdaRec4Un { A,B,C,D() -> object, F,G() -> Function,
F(object,object,object,object,object) -> object }: F() = G()
provided
dom F() = NAT and
F().0 = A() & F().1 = B() & F().2 = C() & F().3 = D() and
for n being Nat holds F().(n+4) = F(n,F().n,F().(n+1),F()
.(n+2),F().(n+3)) and
dom G() = NAT and
G().0 = A() & G().1 = B() & G().2 = C() & G().3 = D() and
for n being Nat holds G().(n+4) = F(n,G().n,G().(n+1),G()
.(n+2),G().(n+3));
scheme :: RECDEF_2:sch 13
LambdaRec4UnD { X() -> non empty set, A,B,C,D() -> Element of X(), F,G() ->
sequence of X(), F(object,object,object,object,object) -> Element of X() }:
F() = G()
provided
F().0 = A() & F().1 = B() & F().2 = C() & F().3 = D() and
for n being Nat holds F().(n+4) = F(n,F().n,F().(n+1),F()
.(n+2),F().(n+3)) and
G().0 = A() & G().1 = B() & G().2 = C() & G().3 = D() and
for n being Nat holds G().(n+4) = F(n,G().n,G().(n+1),G()
.(n+2),G().(n+3));
begin :: Addenda
:: 2010.05.120, A.T.
theorem :: RECDEF_2:10
for x,y,X,Y,Z being set
st x`1_3 = y`1_3 & x`2_3 = y`2_3 & x`3_3 = y`3_3 &
y in [:X,Y,Z:] & x in [:X,Y,Z:]
holds x = y;