:: Helly property for subtrees
:: by Jessica Enright and Piotr Rudnicki
::
:: Received January 10, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem :: HELLY:1
for p being non empty FinSequence holds <*(p . 1)*> ^' p = p
proof end;

definition
let p, q be FinSequence;
func maxPrefix (p,q) -> FinSequence means :Def1: :: HELLY:def 1
( it is_a_prefix_of p & it is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds
r is_a_prefix_of it ) );
existence
ex b1 being FinSequence st
( b1 is_a_prefix_of p & b1 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds
r is_a_prefix_of b1 ) )
proof end;
uniqueness
for b1, b2 being FinSequence st b1 is_a_prefix_of p & b1 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds
r is_a_prefix_of b1 ) & b2 is_a_prefix_of p & b2 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds
r is_a_prefix_of b2 ) holds
b1 = b2
proof end;
commutativity
for b1, p, q being FinSequence st b1 is_a_prefix_of p & b1 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds
r is_a_prefix_of b1 ) holds
( b1 is_a_prefix_of q & b1 is_a_prefix_of p & ( for r being FinSequence st r is_a_prefix_of q & r is_a_prefix_of p holds
r is_a_prefix_of b1 ) )
;
end;

:: deftheorem Def1 defines maxPrefix HELLY:def 1 :
for p, q, b3 being FinSequence holds
( b3 = maxPrefix (p,q) iff ( b3 is_a_prefix_of p & b3 is_a_prefix_of q & ( for r being FinSequence st r is_a_prefix_of p & r is_a_prefix_of q holds
r is_a_prefix_of b3 ) ) );

theorem :: HELLY:2
for p, q being FinSequence holds
( p is_a_prefix_of q iff maxPrefix (p,q) = p )
proof end;

theorem Th3: :: HELLY:3
for p, q being FinSequence holds len (maxPrefix (p,q)) <= len p
proof end;

theorem Th4: :: HELLY:4
for p being non empty FinSequence holds <*(p . 1)*> is_a_prefix_of p
proof end;

theorem Th5: :: HELLY:5
for p, q being non empty FinSequence st p . 1 = q . 1 holds
1 <= len (maxPrefix (p,q))
proof end;

theorem Th6: :: HELLY:6
for p, q being FinSequence
for j being Nat st j <= len (maxPrefix (p,q)) holds
(maxPrefix (p,q)) . j = p . j
proof end;

theorem Th7: :: HELLY:7
for p, q being FinSequence
for j being Nat st j <= len (maxPrefix (p,q)) holds
p . j = q . j
proof end;

theorem Th8: :: HELLY:8
for p, q being FinSequence holds
( not p is_a_prefix_of q iff len (maxPrefix (p,q)) < len p )
proof end;

theorem Th9: :: HELLY:9
for p, q being FinSequence st not p is_a_prefix_of q & not q is_a_prefix_of p holds
p . ((len (maxPrefix (p,q))) + 1) <> q . ((len (maxPrefix (p,q))) + 1)
proof end;

begin

theorem Th10: :: HELLY:10
for G being _Graph
for W being Walk of G
for m, n being Nat holds len (W .cut (m,n)) <= len W
proof end;

theorem :: HELLY:11
for G being _Graph
for W being Walk of G
for m, n being Nat st not W .cut (m,n) is trivial holds
not W is trivial
proof end;

theorem Th12: :: HELLY:12
for G being _Graph
for W being Walk of G
for m, n, i being odd Nat st m <= n & n <= len W & i <= len (W .cut (m,n)) holds
ex j being odd Nat st
( (W .cut (m,n)) . i = W . j & j = (m + i) - 1 & j <= len W )
proof end;

registration
let G be _Graph;
cluster -> non empty for Walk of G;
correctness
coherence
for b1 being Walk of G holds not b1 is empty
;
by CARD_1:27;
end;

theorem Th13: :: HELLY:13
for G being _Graph
for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds
W1 .vertices() c= W2 .vertices()
proof end;

theorem :: HELLY:14
for G being _Graph
for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds
W1 .edges() c= W2 .edges()
proof end;

theorem Th15: :: HELLY:15
for G being _Graph
for W1, W2 being Walk of G holds W1 is_a_prefix_of W1 .append W2
proof end;

theorem Th16: :: HELLY:16
for G being _Graph
for W1, W2 being Walk of G st W1 is trivial & W1 .last() = W2 .first() holds
W1 .append W2 = W2
proof end;

theorem Th17: :: HELLY:17
for G being _Graph
for W1, W2 being Trail of G st W1 .last() = W2 .first() & W1 .edges() misses W2 .edges() holds
W1 .append W2 is Trail-like
proof end;

theorem Th18: :: HELLY:18
for G being _Graph
for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & ( P1 .first() in P2 .vertices() implies P1 .first() = P2 .last() ) & (P1 .vertices()) /\ (P2 .vertices()) c= {(P1 .first()),(P1 .last())} holds
P1 .append P2 is Path-like
proof end;

theorem Th19: :: HELLY:19
for G being _Graph
for P1, P2 being Path of G st P1 .last() = P2 .first() & P1 is open & P2 is open & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds
( P1 .append P2 is open & P1 .append P2 is Path-like )
proof end;

theorem Th20: :: HELLY:20
for G being _Graph
for P1, P2 being Path of G st P1 .last() = P2 .first() & P2 .last() = P1 .first() & P1 is open & P2 is open & P1 .edges() misses P2 .edges() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last()),(P1 .first())} holds
P1 .append P2 is Cycle-like
proof end;

theorem :: HELLY:21
for G being simple _Graph
for W1, W2 being Walk of G
for k being odd Nat st k <= len W1 & k <= len W2 & ( for j being odd Nat st j <= k holds
W1 . j = W2 . j ) holds
for j being Nat st 1 <= j & j <= k holds
W1 . j = W2 . j
proof end;

theorem Th22: :: HELLY:22
for G being _Graph
for W1, W2 being Walk of G st W1 .first() = W2 .first() holds
len (maxPrefix (W1,W2)) is odd
proof end;

theorem Th23: :: HELLY:23
for G being _Graph
for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 holds
(len (maxPrefix (W1,W2))) + 2 <= len W1
proof end;

theorem Th24: :: HELLY:24
for G being non-multi _Graph
for W1, W2 being Walk of G st W1 .first() = W2 .first() & not W1 is_a_prefix_of W2 & not W2 is_a_prefix_of W1 holds
W1 . ((len (maxPrefix (W1,W2))) + 2) <> W2 . ((len (maxPrefix (W1,W2))) + 2)
proof end;

begin

definition
mode _Tree is Tree-like _Graph;
let G be _Graph;
mode _Subtree of G is Tree-like Subgraph of G;
end;

registration
let T be _Tree;
cluster Trail-like -> Path-like for Walk of T;
correctness
coherence
for b1 being Walk of T st b1 is Trail-like holds
b1 is Path-like
;
proof end;
end;

theorem Th25: :: HELLY:25
for T being _Tree
for P being Path of T st not P is trivial holds
P is open
proof end;

registration
let T be _Tree;
cluster non trivial Path-like -> open for Walk of T;
correctness
coherence
for b1 being Path of T st not b1 is trivial holds
b1 is open
;
by Th25;
end;

theorem Th26: :: HELLY:26
for T being _Tree
for P being Path of T
for i, j being odd Nat st i < j & j <= len P holds
P . i <> P . j
proof end;

theorem Th27: :: HELLY:27
for T being _Tree
for a, b being Vertex of T
for P1, P2 being Path of T st P1 is_Walk_from a,b & P2 is_Walk_from a,b holds
P1 = P2
proof end;

definition
let T be _Tree;
let a, b be Vertex of T;
func T .pathBetween (a,b) -> Path of T means :Def2: :: HELLY:def 2
it is_Walk_from a,b;
existence
ex b1 being Path of T st b1 is_Walk_from a,b
proof end;
uniqueness
for b1, b2 being Path of T st b1 is_Walk_from a,b & b2 is_Walk_from a,b holds
b1 = b2
by Th27;
end;

:: deftheorem Def2 defines .pathBetween HELLY:def 2 :
for T being _Tree
for a, b being Vertex of T
for b4 being Path of T holds
( b4 = T .pathBetween (a,b) iff b4 is_Walk_from a,b );

theorem Th28: :: HELLY:28
for T being _Tree
for a, b being Vertex of T holds
( (T .pathBetween (a,b)) .first() = a & (T .pathBetween (a,b)) .last() = b )
proof end;

:: more theorems about pathBetween ?
theorem Th29: :: HELLY:29
for T being _Tree
for a, b being Vertex of T holds
( a in (T .pathBetween (a,b)) .vertices() & b in (T .pathBetween (a,b)) .vertices() )
proof end;

registration
let T be _Tree;
let a be Vertex of T;
cluster T .pathBetween (a,a) -> closed ;
correctness
coherence
T .pathBetween (a,a) is closed
;
proof end;
end;

registration
let T be _Tree;
let a be Vertex of T;
cluster T .pathBetween (a,a) -> trivial ;
correctness
coherence
T .pathBetween (a,a) is trivial
;
;
end;

theorem Th30: :: HELLY:30
for T being _Tree
for a being Vertex of T holds (T .pathBetween (a,a)) .vertices() = {a}
proof end;

theorem Th31: :: HELLY:31
for T being _Tree
for a, b being Vertex of T holds (T .pathBetween (a,b)) .reverse() = T .pathBetween (b,a)
proof end;

theorem Th32: :: HELLY:32
for T being _Tree
for a, b being Vertex of T holds (T .pathBetween (a,b)) .vertices() = (T .pathBetween (b,a)) .vertices()
proof end;

theorem Th33: :: HELLY:33
for T being _Tree
for a, b being Vertex of T
for t being _Subtree of T
for a9, b9 being Vertex of t st a = a9 & b = b9 holds
T .pathBetween (a,b) = t .pathBetween (a9,b9)
proof end;

theorem Th34: :: HELLY:34
for T being _Tree
for a, b being Vertex of T
for t being _Subtree of T st a in the_Vertices_of t & b in the_Vertices_of t holds
(T .pathBetween (a,b)) .vertices() c= the_Vertices_of t
proof end;

theorem Th35: :: HELLY:35
for T being _Tree
for P being Path of T
for a, b being Vertex of T
for i, j being odd Nat st i <= j & j <= len P & P . i = a & P . j = b holds
T .pathBetween (a,b) = P .cut (i,j)
proof end;

theorem Th36: :: HELLY:36
for T being _Tree
for a, b, c being Vertex of T holds
( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,b) = (T .pathBetween (a,c)) .append (T .pathBetween (c,b)) )
proof end;

theorem Th37: :: HELLY:37
for T being _Tree
for a, b, c being Vertex of T holds
( c in (T .pathBetween (a,b)) .vertices() iff T .pathBetween (a,c) is_a_prefix_of T .pathBetween (a,b) )
proof end;

theorem Th38: :: HELLY:38
for T being _Tree
for P1, P2 being Path of T st P1 .last() = P2 .first() & (P1 .vertices()) /\ (P2 .vertices()) = {(P1 .last())} holds
P1 .append P2 is Path-like
proof end;

theorem Th39: :: HELLY:39
for T being _Tree
for a, b, c being Vertex of T holds
( c in (T .pathBetween (a,b)) .vertices() iff ((T .pathBetween (a,c)) .vertices()) /\ ((T .pathBetween (c,b)) .vertices()) = {c} )
proof end;

theorem Th40: :: HELLY:40
for T being _Tree
for a, b, c, d being Vertex of T
for P1, P2 being Path of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not P1 is_a_prefix_of P2 & not P2 is_a_prefix_of P1 & d = P1 . (len (maxPrefix (P1,P2))) holds
((T .pathBetween (d,b)) .vertices()) /\ ((T .pathBetween (d,c)) .vertices()) = {d}
proof end;

Lm1: for T being _Tree
for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds
(((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {c}

proof end;

Lm2: for T being _Tree
for a, b, c being Vertex of T
for P1, P4 being Path of T st P1 = T .pathBetween (a,b) & P4 = T .pathBetween (a,c) & not P1 c= P4 & not P4 c= P1 holds
((P1 .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {(P1 . (len (maxPrefix (P1,P4))))}

proof end;

definition
let T be _Tree;
let a, b, c be Vertex of T;
func MiddleVertex (a,b,c) -> Vertex of T means :Def3: :: HELLY:def 3
(((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {it};
existence
ex b1 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1}
proof end;
uniqueness
for b1, b2 being Vertex of T st (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b1} & (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b2} holds
b1 = b2
by ZFMISC_1:3;
end;

:: deftheorem Def3 defines MiddleVertex HELLY:def 3 :
for T being _Tree
for a, b, c, b5 being Vertex of T holds
( b5 = MiddleVertex (a,b,c) iff (((T .pathBetween (a,b)) .vertices()) /\ ((T .pathBetween (b,c)) .vertices())) /\ ((T .pathBetween (c,a)) .vertices()) = {b5} );

theorem Th41: :: HELLY:41
for T being _Tree
for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (a,c,b)
proof end;

theorem Th42: :: HELLY:42
for T being _Tree
for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (b,a,c)
proof end;

theorem :: HELLY:43
for T being _Tree
for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (b,c,a)
proof end;

theorem Th44: :: HELLY:44
for T being _Tree
for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (c,a,b)
proof end;

theorem :: HELLY:45
for T being _Tree
for a, b, c being Vertex of T holds MiddleVertex (a,b,c) = MiddleVertex (c,b,a)
proof end;

theorem Th46: :: HELLY:46
for T being _Tree
for a, b, c being Vertex of T st c in (T .pathBetween (a,b)) .vertices() holds
MiddleVertex (a,b,c) = c
proof end;

theorem :: HELLY:47
for T being _Tree
for a being Vertex of T holds MiddleVertex (a,a,a) = a
proof end;

theorem Th48: :: HELLY:48
for T being _Tree
for a, b being Vertex of T holds MiddleVertex (a,a,b) = a
proof end;

theorem Th49: :: HELLY:49
for T being _Tree
for a, b being Vertex of T holds MiddleVertex (a,b,a) = a
proof end;

theorem :: HELLY:50
for T being _Tree
for a, b being Vertex of T holds MiddleVertex (a,b,b) = b
proof end;

theorem Th51: :: HELLY:51
for T being _Tree
for P1, P2 being Path of T
for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & not b in P2 .vertices() & not c in P1 .vertices() holds
MiddleVertex (a,b,c) = P1 . (len (maxPrefix (P1,P2)))
proof end;

theorem :: HELLY:52
for T being _Tree
for P1, P2, P3, P4 being Path of T
for a, b, c being Vertex of T st P1 = T .pathBetween (a,b) & P2 = T .pathBetween (a,c) & P3 = T .pathBetween (b,a) & P4 = T .pathBetween (b,c) & not b in P2 .vertices() & not c in P1 .vertices() & not a in P4 .vertices() holds
P1 . (len (maxPrefix (P1,P2))) = P3 . (len (maxPrefix (P3,P4)))
proof end;

theorem Th53: :: HELLY:53
for T being _Tree
for a, b, c being Vertex of T
for S being non empty set st ( for s being set st s in S holds
( ex t being _Subtree of T st s = the_Vertices_of t & ( ( a in s & b in s ) or ( a in s & c in s ) or ( b in s & c in s ) ) ) ) holds
meet S <> {}
proof end;

begin

definition
let F be set ;
attr F is with_Helly_property means :: HELLY:def 4
for H being non empty set st H c= F & ( for x, y being set st x in H & y in H holds
x meets y ) holds
meet H <> {} ;
end;

:: deftheorem defines with_Helly_property HELLY:def 4 :
for F being set holds
( F is with_Helly_property iff for H being non empty set st H c= F & ( for x, y being set st x in H & y in H holds
x meets y ) holds
meet H <> {} );

:: At some point one would like to define allSubtrees of a Tree
:: The claim below does not hold when T is infinite and we consider
:: infinite families of subtrees. Example: half-line tree with
:: subtrees T_i = {j >= i}.
:: main Prop4p7:
theorem :: HELLY:54
for T being _Tree
for X being finite set st ( for x being set st x in X holds
ex t being _Subtree of T st x = the_Vertices_of t ) holds
X is with_Helly_property
proof end;