:: Helly property for subtrees
::  by Jessica Enright and Piotr Rudnicki
::
:: Received January 10, 2008
:: Copyright (c) 2008-2021 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, XBOOLE_0, FINSEQ_1, FUNCT_1, GRAPH_2, ARYTM_3, NAT_1,
      XXREAL_0, SUBSET_1, TREES_1, TARSKI, CARD_1, ORDINAL1, FINSET_1,
      MEMBERED, RELAT_1, ORDINAL4, GLIB_000, GLIB_001, ABIAN, ZFMISC_1,
      ARYTM_1, GRAPH_1, RCOMP_1, SETFAM_1, HELLY;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FINSET_1, CARD_1, NUMBERS,
      XCMPLX_0, XXREAL_0, SETFAM_1, FUNCT_1, FINSEQ_1, MEMBERED, NAT_1,
      TREES_1, XXREAL_2, ABIAN, GRAPH_2, GLIB_000, GLIB_001, GLIB_002,
      FINSEQ_6;
 constructors DOMAIN_1, SETFAM_1, NAT_1, GRAPH_2, GLIB_001, GLIB_002, XXREAL_2,
      RELSET_1, RAT_1, FINSEQ_6;
 registrations FINSET_1, XREAL_0, XXREAL_0, NAT_1, INT_1, RELAT_1, FINSEQ_1,
      ABIAN, MEMBERED, GLIB_000, GLIB_001, GLIB_002, XXREAL_2, CARD_1, FUNCT_1,
      XBOOLE_0, ORDINAL1;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;


begin :: General preliminaries

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

definition
  let p, q be FinSequence;
  func maxPrefix(p,q) -> FinSequence means
:: 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;
  commutativity;
end;

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

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

theorem :: HELLY:4
  for p being non empty FinSequence holds <*p.1*> is_a_prefix_of p;

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

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

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

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

theorem :: 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)
;

begin :: Graph preliminaries

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

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

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

registration
  let G be _Graph;
  cluster -> non empty for Walk of G;
end;

theorem :: 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();

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();

theorem :: HELLY:15
  for G being _Graph for W1, W2 being Walk of G holds W1
  is_a_prefix_of W1.append(W2);

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

theorem :: 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;

theorem :: 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;

theorem :: 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 Path-like;

theorem :: 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;

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;

theorem :: 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;

theorem :: 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;

theorem :: 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);

begin :: Trees

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;
end;

theorem :: HELLY:25
  for T being _Tree for P being Path of T st P is non trivial holds P is open;

registration
  let T be _Tree;
  cluster non trivial -> open for Path of T;
end;

theorem :: HELLY:26  :: Only for _Tree as it is not true for cyclic paths
  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;

theorem :: 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;

definition
  let T be _Tree;
  let a, b be Vertex of T;
  func T.pathBetween(a,b) -> Path of T means
:: HELLY:def 2

  it is_Walk_from a, b;
end;

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

:: more theorems about pathBetween ?

theorem :: HELLY:29
  for T being _Tree, a, b being Vertex of T holds a in T
  .pathBetween(a,b).vertices() & b in T.pathBetween(a,b).vertices();

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

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

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

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

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

theorem :: 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);

theorem :: 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;

theorem :: 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);

theorem :: 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));

theorem :: 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);

theorem :: 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;

theorem :: 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};

theorem :: 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};

definition
  let T be _Tree, a, b, c be Vertex of T;
  func MiddleVertex(a, b, c) -> Vertex of T means
:: HELLY:def 3

  T.pathBetween(a,b)
.vertices() /\ T.pathBetween(b,c).vertices() /\ T.pathBetween(c,a).vertices() =
  { it };
end;

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

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

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

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

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

theorem :: 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;

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

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

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

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

theorem :: HELLY:51
  for T being _Tree for P1, P2 be 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);

theorem :: HELLY:52 :: PMV302:
  for T being _Tree for P1, P2, P3, P4 be 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);

theorem :: 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 <> {};

begin :: The Helly property

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;

:: 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, X being finite set st for x being set st x in X ex
  t being _Subtree of T st x = the_Vertices_of t holds X is with_Helly_property
;