:: Mizar Analysis of Algorithms: Preliminaries
:: by Grzegorz Bancerek
::
:: Received July 9, 2007
:: Copyright (c) 2007 Association of Mizar Users

:: AOFA_000 semantic presentation

notation
let x, y be set ;
antonym x nin y for x in y;
end;

theorem Th1: :: AOFA_000:1
for f, g, h being Function
for A being set st A c= dom f & A c= dom g & rng h c= A & ( for x being set st x in A holds
f . x = g . x ) holds
f * h = g * h
proof end;

registration
let x, y be non empty set ;
cluster <*x,y*> -> non-empty ;
coherence
<*x,y*> is non-empty
proof end;
end;

registration
let p, q be non-empty FinSequence;
cluster p ^ q -> non-empty ;
coherence
p ^ q is non-empty
proof end;
end;

definition
let f be homogeneous Function;
let x be set ;
pred x is_a_unity_wrt f means :Def1: :: AOFA_000:def 1
for y, z being set st ( <*y,z*> in dom f or <*z,y*> in dom f ) holds
( <*x,y*> in dom f & f . <*x,y*> = y & <*y,x*> in dom f & f . <*y,x*> = y );
end;

:: deftheorem Def1 defines is_a_unity_wrt AOFA_000:def 1 :
for f being homogeneous Function
for x being set holds
( x is_a_unity_wrt f iff for y, z being set st ( <*y,z*> in dom f or <*z,y*> in dom f ) holds
( <*x,y*> in dom f & f . <*x,y*> = y & <*y,x*> in dom f & f . <*y,x*> = y ) );

definition
let f be homogeneous Function;
attr f is associative means :Def2: :: AOFA_000:def 2
for x, y, z being set st <*x,y*> in dom f & <*y,z*> in dom f & <*(f . <*x,y*>),z*> in dom f & <*x,(f . <*y,z*>)*> in dom f holds
f . <*(f . <*x,y*>),z*> = f . <*x,(f . <*y,z*>)*>;
attr f is unital means :Def3: :: AOFA_000:def 3
 ex x being set st x is_a_unity_wrt f;
end;

:: deftheorem Def2 defines associative AOFA_000:def 2 :
for f being homogeneous Function holds
( f is associative iff for x, y, z being set st <*x,y*> in dom f & <*y,z*> in dom f & <*(f . <*x,y*>),z*> in dom f & <*x,(f . <*y,z*>)*> in dom f holds
f . <*(f . <*x,y*>),z*> = f . <*x,(f . <*y,z*>)*> );

:: deftheorem Def3 defines unital AOFA_000:def 3 :
for f being homogeneous Function holds
( f is unital iff ex x being set st x is_a_unity_wrt f );

definition
let X be set ;
let Y be non empty set ;
let Z be FinSequenceSet of X;
let y be Element of Y;
:: original: -->
redefine func Z --> y -> PartFunc of X * ,Y;
coherence
Z --> y is PartFunc of X * ,Y
proof end;
end;

registration
let X be non empty set ;
let x be Element of X;
let n be Nat;
cluster (n -tuples_on X) --> x -> non empty homogeneous quasi_total PartFunc of X * ,X;
coherence
(n -tuples_on X) --> x is non empty homogeneous quasi_total PartFunc of X * ,X
proof end;
end;

theorem Th2: :: AOFA_000:2
for X being non empty set
for x being Element of X
for n being Nat holds arity ((n -tuples_on X) --> x) = n
proof end;

Lm1: now
let X be non empty set ; :: thesis: for x being Element of X holds
( (0 -tuples_on X) --> x is nullary & (1 -tuples_on X) --> x is unary & (2 -tuples_on X) --> x is binary & (3 -tuples_on X) --> x is ternary )
let x be Element of X; :: thesis: ( (0 -tuples_on X) --> x is nullary & (1 -tuples_on X) --> x is unary & (2 -tuples_on X) --> x is binary & (3 -tuples_on X) --> x is ternary )
thus (0 -tuples_on X) --> x is nullary :: thesis: ( (1 -tuples_on X) --> x is unary & (2 -tuples_on X) --> x is binary & (3 -tuples_on X) --> x is ternary )
proof
thus arity ((0 -tuples_on X) --> x) = 0 by Th2; :: according to COMPUT_1:def 24 :: thesis: verum
end;
thus (1 -tuples_on X) --> x is unary :: thesis: ( (2 -tuples_on X) --> x is binary & (3 -tuples_on X) --> x is ternary )
proof
thus arity ((1 -tuples_on X) --> x) = 1 by Th2; :: according to COMPUT_1:def 25 :: thesis: verum
end;
thus (2 -tuples_on X) --> x is binary :: thesis: (3 -tuples_on X) --> x is ternary
proof
thus arity ((2 -tuples_on X) --> x) = 2 by Th2; :: according to COMPUT_1:def 26 :: thesis: verum
end;
thus (3 -tuples_on X) --> x is ternary :: thesis: verum
proof
thus arity ((3 -tuples_on X) --> x) = 3 by Th2; :: according to COMPUT_1:def 27 :: thesis: verum
end;
end;

registration
let X be non empty set ;
let x be Element of X;
cluster (0 -tuples_on X) --> x -> homogeneous nullary homogeneous PartFunc of X * ,X;
coherence
(0 -tuples_on X) --> x is homogeneous nullary PartFunc of X * ,X by Lm1;
cluster (1 -tuples_on X) --> x -> homogeneous unary homogeneous PartFunc of X * ,X;
coherence
(1 -tuples_on X) --> x is homogeneous unary PartFunc of X * ,X by Lm1;
cluster (2 -tuples_on X) --> x -> homogeneous binary homogeneous PartFunc of X * ,X;
coherence
(2 -tuples_on X) --> x is homogeneous binary PartFunc of X * ,X by Lm1;
cluster (3 -tuples_on X) --> x -> homogeneous ternary homogeneous PartFunc of X * ,X;
coherence
(3 -tuples_on X) --> x is homogeneous ternary PartFunc of X * ,X by Lm1;
end;

registration
let X be non empty set ;
cluster non empty homogeneous quasi_total binary associative unital Relation of X * ,X;
existence
ex b1 being non empty homogeneous quasi_total PartFunc of X * ,X st
( b1 is binary & b1 is associative & b1 is unital )
proof end;
cluster non empty homogeneous quasi_total nullary Relation of X * ,X;
existence
ex b1 being non empty homogeneous quasi_total PartFunc of X * ,X st b1 is nullary
proof end;
cluster non empty homogeneous quasi_total ternary Relation of X * ,X;
existence
ex b1 being non empty homogeneous quasi_total PartFunc of X * ,X st b1 is ternary
proof end;
end;

theorem Th3: :: AOFA_000:3
for X being non empty set
for p being FinSequence of FinTrees X
for x, t being set st t in rng p holds
t <> x -tree p
proof end;

definition
let f, g be Function;
let X be set ;
func f,X +* g -> Function equals :: AOFA_000:def 4
g +* (f | X);
coherence
g +* (f | X) is Function ;
end;

:: deftheorem defines +* AOFA_000:def 4 :
for f, g being Function
for X being set holds f,X +* g = g +* (f | X);

theorem Th4: :: AOFA_000:4
for f, g being Function
for x, X being set st x in X & X c= dom f holds
(f,X +* g) . x = f . x
proof end;

theorem Th5: :: AOFA_000:5
for f, g being Function
for x, X being set st x nin X & x in dom g holds
(f,X +* g) . x = g . x
proof end;

definition
let X, Y be non empty set ;
let f, g be Element of Funcs X,Y;
let A be set ;
:: original: +*
redefine func f,A +* g -> Element of Funcs X,Y;
coherence
f,A +* g is Element of Funcs X,Y
proof end;
end;

definition
let X, Y, Z be non empty set ;
let f be Element of Funcs X,Y;
let g be Element of Funcs Y,Z;
:: original: *
redefine func g * f -> Element of Funcs X,Z;
coherence
f * g is Element of Funcs X,Z
proof end;
end;

definition
let f be Function;
let x be set ;
func f orbit x -> set equals :: AOFA_000:def 5
{ ((iter f,n) . x) where n is Element of NAT : x in dom (iter f,n) } ;
coherence
{ ((iter f,n) . x) where n is Element of NAT : x in dom (iter f,n) } is set ;
end;

:: deftheorem defines orbit AOFA_000:def 5 :
for f being Function
for x being set holds f orbit x = { ((iter f,n) . x) where n is Element of NAT : x in dom (iter f,n) } ;

theorem Th6: :: AOFA_000:6
for f being Function
for x being set st x in dom f holds
x in f orbit x
proof end;

theorem :: AOFA_000:7
for f being Function
for x, y being set st rng f c= dom f & y in f orbit x holds
f . y in f orbit x
proof end;

theorem :: AOFA_000:8
for f being Function
for x being set st x in dom f holds
f . x in f orbit x
proof end;

theorem Th9: :: AOFA_000:9
for f being Function
for x being set st x in dom f & f . x in dom f holds
f orbit (f . x) c= f orbit x
proof end;

definition
let f be Function;
assume A1: rng f c= dom f ;
let A, x be set ;
defpred S1[ Nat] means for a being set st a in dom f holds
a in dom (iter f,$1);
A2: (dom f) \/ (rng f) = dom f by A1, XBOOLE_1:12;
then iter f,0 = id (dom f) by FUNCT_7:70;
then A3: S1[ 0 ] by FUNCT_1:34;
A4: now
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume A5: S1[i] ; :: thesis: S1[i + 1]
thus S1[i + 1] :: thesis: verum
proof
let a be set ; :: thesis: ( a in dom f implies a in dom (iter f,(i + 1)) )
assume a in dom f ; :: thesis: a in dom (iter f,(i + 1))
then A6: a in dom (iter f,i) by A5;
then A7: ( (iter f,i) . a in rng (iter f,i) & rng (iter f,i) c= dom f ) by A2, FUNCT_1:def 5, FUNCT_7:74;
iter f,(i + 1) = f * (iter f,i) by FUNCT_7:73;
hence a in dom (iter f,(i + 1)) by A6, A7, FUNCT_1:21; :: thesis: verum
end;
end;
A8: for i being Element of NAT holds S1[i] from NAT_1:sch 1(A3, A4);
func A,x iter f -> Function means :: AOFA_000:def 6
( dom it = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies it . a = x ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
it . a = (iter f,n) . a ) ) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . a = x ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
b1 . a = (iter f,n) . a ) ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . a = x ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
b1 . a = (iter f,n) . a ) ) ) & dom b2 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b2 . a = x ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
b2 . a = (iter f,n) . a ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines iter AOFA_000:def 6 :
for f being Function st rng f c= dom f holds
for A, x being set
for b4 being Function holds
( b4 = A,x iter f iff ( dom b4 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b4 . a = x ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
b4 . a = (iter f,n) . a ) ) ) ) );

definition
let f be Function;
assume A1: rng f c= dom f ;
let A be set ;
let g be Function;
defpred S1[ Nat] means for a being set st a in dom f holds
a in dom (iter f,$1);
A2: (dom f) \/ (rng f) = dom f by A1, XBOOLE_1:12;
then iter f,0 = id (dom f) by FUNCT_7:70;
then A3: S1[ 0 ] by FUNCT_1:34;
A4: now
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume A5: S1[i] ; :: thesis: S1[i + 1]
thus S1[i + 1] :: thesis: verum
proof
let a be set ; :: thesis: ( a in dom f implies a in dom (iter f,(i + 1)) )
assume a in dom f ; :: thesis: a in dom (iter f,(i + 1))
then A6: a in dom (iter f,i) by A5;
then A7: ( (iter f,i) . a in rng (iter f,i) & rng (iter f,i) c= dom f ) by A2, FUNCT_1:def 5, FUNCT_7:74;
iter f,(i + 1) = f * (iter f,i) by FUNCT_7:73;
hence a in dom (iter f,(i + 1)) by A6, A7, FUNCT_1:21; :: thesis: verum
end;
end;
A8: for i being Element of NAT holds S1[i] from NAT_1:sch 1(A3, A4);
func A,g iter f -> Function means :Def7: :: AOFA_000:def 7
( dom it = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies it . a = g . a ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
it . a = (iter f,n) . a ) ) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . a = g . a ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
b1 . a = (iter f,n) . a ) ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . a = g . a ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
b1 . a = (iter f,n) . a ) ) ) & dom b2 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b2 . a = g . a ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
b2 . a = (iter f,n) . a ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines iter AOFA_000:def 7 :
for f being Function st rng f c= dom f holds
for A being set
for g, b4 being Function holds
( b4 = A,g iter f iff ( dom b4 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b4 . a = g . a ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
b4 . a = (iter f,n) . a ) ) ) ) );

theorem Th10: :: AOFA_000:10
for f, g being Function
for a, A being set st rng f c= dom f & a in dom f & not f orbit a c= A holds
ex n being Nat st
( (A,g iter f) . a = (iter f,n) . a & (iter f,