:: Fix-points in complete lattices
::  by Piotr Rudnicki and Andrzej Trybulec
::
:: Received September 16, 1996
:: Copyright (c) 1996-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 FUNCT_1, XBOOLE_0, RELAT_1, FUNCT_4, SUBSET_1, NUMBERS, ABIAN,
      FUNCT_7, ARYTM_3, COHSP_1, TARSKI, FUNCOP_1, ZFMISC_1, SETFAM_1, FUNCT_2,
      LATTICES, STRUCT_0, ORDINAL1, ORDINAL2, EQREL_1, CARD_1, BINOP_1,
      LATTICE3, PBOOLE, FILTER_0, FILTER_1, WELLORD1, RELAT_2, ORDERS_1,
      ORDERS_2, XXREAL_0, REWRITE1, XXREAL_2, SEQM_3, KNASTER, NAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
      XCMPLX_0, NAT_1, RELAT_1, RELAT_2, ORDERS_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, BINOP_1, FUNCOP_1, SETFAM_1, FUNCT_4, WELLORD1, ORDINAL2,
      STRUCT_0, COHSP_1, LATTICES, LATTICE3, QUANTAL1, ORDERS_2, ABIAN;
 constructors WELLORD1, WELLORD2, BINOP_1, DOMAIN_1, ORDINAL2, NAT_1, ABIAN,
      BOOLEALG, QUANTAL1, COHSP_1, RELSET_1, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, CARD_1,
      STRUCT_0, LATTICES, LATTICE3, QUANTAL1;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Preliminaries

reserve f, g, h for Function;

theorem :: KNASTER:1
  h = f \/ g & dom f misses dom g implies (h is one-to-one iff f is
  one-to-one & g is one-to-one & rng f misses rng g);

begin :: Fix points in general

reserve x, y, z, u, X for set,
  A for non empty set,
  n for Element of NAT,
  f for Function of X, X;

theorem :: KNASTER:2
  x is_a_fixpoint_of iter(f,n) implies f.x is_a_fixpoint_of iter(f, n);

theorem :: KNASTER:3
  (ex n st x is_a_fixpoint_of iter(f,n) & for y st y is_a_fixpoint_of
  iter(f,n) holds x = y) implies x is_a_fixpoint_of f;

definition
  let A, B be non empty set, f be Function of A, B;

  redefine attr f is c=-monotone means
:: KNASTER:def 1

  for x, y being Element of A st x c= y holds f.x c= f.y;
end;

registration
  let A be set, B be non empty set;
  cluster c=-monotone for Function of A, B;
end;

definition
  let X be set;
  let f be c=-monotone Function of bool X, bool X;
  func lfp (X, f) -> Subset of X equals
:: KNASTER:def 2
  meet {h where h is Subset of X : f.h c= h};
  func gfp (X, f) -> Subset of X equals
:: KNASTER:def 3
  union {h where h is Subset of X : h c= f.h };
end;

reserve f for c=-monotone Function of bool X, bool X,
  S for Subset of X;

theorem :: KNASTER:4
  lfp(X, f) is_a_fixpoint_of f;

theorem :: KNASTER:5
  gfp(X, f) is_a_fixpoint_of f;

theorem :: KNASTER:6
  f.S c= S implies lfp(X,f) c= S;

theorem :: KNASTER:7
  S c= f.S implies S c= gfp(X,f);

theorem :: KNASTER:8
  S is_a_fixpoint_of f implies lfp(X,f) c= S & S c= gfp(X,f);

::$N Knaster Theorem
scheme :: KNASTER:sch 1
  Knaster{A() -> set, F(object) -> set}:
ex D being set st F(D) = D & D c= A()
provided
 for X, Y being set st X c= Y holds F(X) c= F(Y) and
 F(A()) c= A();

reserve X, Y for non empty set,
  f for Function of X, Y,
  g for Function of Y, X;

:: Banach decomposition

theorem :: KNASTER:9
  ex Xa, Xb, Ya, Yb being set st Xa misses Xb & Ya misses Yb & Xa
  \/ Xb = X & Ya \/ Yb = Y & f.:Xa = Ya & g.:Yb = Xb;

::$N Schroeder Bernstein theorem
theorem :: KNASTER:10
  for X, Y being non empty set,
      f being Function of X, Y,
      g being Function of Y, X st
    f is one-to-one & g is one-to-one holds
   ex h being Function of X,Y st h is bijective;

theorem :: KNASTER:11  ::: EULER_1:12
  f is bijective implies X,Y are_equipotent;

theorem :: KNASTER:12
  f is one-to-one & g is one-to-one implies X,Y are_equipotent;

begin :: The lattice of a lattice subset

definition
  let L be Lattice, f be Function of the carrier of L, the carrier of L, x be
  Element of L, O be Ordinal;
  func (f, O)+.x -> set means
:: KNASTER:def 4

  ex L0 being Sequence st it = last L0 & dom L0
= succ O & L0.0 = x & (for C being Ordinal st succ C in succ O holds L0.succ C
= f.(L0.C)) & for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal
  holds L0.C = "\/"(rng(L0|C), L);
  func (f, O)-.x -> set means
:: KNASTER:def 5

  ex L0 being Sequence st it = last L0 & dom L0
= succ O & L0.0 = x & (for C being Ordinal st succ C in succ O holds L0.succ C
= f.(L0.C)) & for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal
  holds L0.C = "/\"(rng(L0|C) , L);
end;

reserve L for Lattice,
  f for Function of the carrier of L, the carrier of L,
  x for Element of L,
  O, O1, O2, O3, O4 for Ordinal,
  T for Sequence;

theorem :: KNASTER:13
  (f, 0)+.x = x;

theorem :: KNASTER:14
  (f, 0)-.x = x;

theorem :: KNASTER:15
  (f, succ O)+.x = f.(f, O)+.x;

theorem :: KNASTER:16
  (f, succ O)-.x = f.(f, O)-.x;

theorem :: KNASTER:17
  O <> 0 & O is limit_ordinal & dom T = O & (for A being Ordinal
  st A in O holds T.A = (f, A)+.x) implies (f, O)+.x = "\/"(rng T, L);

theorem :: KNASTER:18
  O <> 0 & O is limit_ordinal & dom T = O & (for A being Ordinal
  st A in O holds T.A = (f, A)-.x) implies (f, O)-.x = "/\"(rng T, L);

theorem :: KNASTER:19
  iter(f, n).x = (f, n)+.x;

theorem :: KNASTER:20
  iter(f, n).x = (f, n)-.x;

definition
  let L be Lattice, f be (UnOp of the carrier of L), a be Element of L, O be
  Ordinal;
  redefine func (f, O)+.a -> Element of L;
end;

definition
  let L be Lattice, f be (UnOp of the carrier of L), a be Element of L, O be
  Ordinal;
  redefine func (f, O)-.a -> Element of L;
end;

definition
  let L be non empty LattStr, P be Subset of L;
  attr P is with_suprema means
:: KNASTER:def 6

  for x,y being Element of L st x in P & y
in P ex z being Element of L st z in P & x [= z & y [= z & for z9 being Element
  of L st z9 in P & x [= z9 & y [= z9 holds z [= z9;
  attr P is with_infima means
:: KNASTER:def 7

  for x,y being Element of L st x in P & y
in P ex z being Element of L st z in P & z [= x & z [= y & for z9 being Element
  of L st z9 in P & z9 [= x & z9 [= y holds z9 [= z;
end;

registration
  let L be Lattice;
  cluster non empty with_suprema with_infima for Subset of L;
end;

definition
  let L be Lattice, P be non empty with_suprema with_infima Subset of L;
  func latt P -> strict Lattice means
:: KNASTER:def 8

  the carrier of it = P & for x, y
  being Element of it ex x9, y9 being Element of L st x = x9 & y = y9 & (x [= y
  iff x9 [= y9);
end;

begin :: Complete lattices

registration
  cluster complete -> bounded for Lattice;
end;

reserve L for complete Lattice,
  f for monotone UnOp of L,
  a, b for Element of L;

theorem :: KNASTER:21
  ex a st a is_a_fixpoint_of f;

theorem :: KNASTER:22
  for a st a [= f.a for O holds a [= (f, O)+.a;

theorem :: KNASTER:23
  for a st f.a [= a for O holds (f, O)-.a [= a;

theorem :: KNASTER:24
  for a st a [= f.a for O1, O2 st O1 c= O2 holds (f, O1)+.a [= (f, O2)+.a;

theorem :: KNASTER:25
  for a st f.a [= a for O1, O2 st O1 c= O2 holds (f, O2)-.a [= (f, O1)-.a;

theorem :: KNASTER:26
  for a st a [= f.a for O1, O2 st O1 c< O2 & not (f, O2)+.a
  is_a_fixpoint_of f holds (f, O1)+.a <> (f, O2)+.a;

theorem :: KNASTER:27
  for a st f.a [= a for O1, O2 st O1 c< O2 & not (f, O2)-.a
  is_a_fixpoint_of f holds (f, O1)-.a <> (f, O2)-.a;

theorem :: KNASTER:28
  a [= f.a & (f, O1)+.a is_a_fixpoint_of f implies for O2 st O1 c=
  O2 holds (f, O1)+.a = (f, O2)+.a;

theorem :: KNASTER:29
  f.a [= a & (f, O1)-.a is_a_fixpoint_of f implies for O2 st O1 c=
  O2 holds (f, O1)-.a = (f, O2)-.a;

theorem :: KNASTER:30
  for a st a [= f.a ex O st card O c= card the carrier of L & (f,
  O)+.a is_a_fixpoint_of f;

theorem :: KNASTER:31
  for a st f.a [= a ex O st card O c= card the carrier of L & (f,
  O)-.a is_a_fixpoint_of f;

theorem :: KNASTER:32
  for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f ex O st
card O c= card the carrier of L & (f, O)+.(a"\/"b) is_a_fixpoint_of f & a [= (f
  , O)+.(a"\/"b) & b [= (f, O)+.(a"\/"b);

theorem :: KNASTER:33
  for a, b st a is_a_fixpoint_of f & b is_a_fixpoint_of f ex O st
card O c= card the carrier of L & (f, O)-.(a"/\"b) is_a_fixpoint_of f & (f, O)
  -.(a"/\"b) [= a & (f, O)-.(a"/\"b) [= b;

theorem :: KNASTER:34
  a [= b & b is_a_fixpoint_of f implies for O2 holds (f, O2)+.a [= b;

theorem :: KNASTER:35
  b [= a & b is_a_fixpoint_of f implies for O2 holds b [= (f, O2) -.a;

definition
  let L be complete Lattice, f be UnOp of L such that
 f is monotone;
  func FixPoints f -> strict Lattice means
:: KNASTER:def 9

  ex P being non empty
  with_suprema with_infima Subset of L st P = {x where x is Element of L: x
  is_a_fixpoint_of f} & it = latt P;
end;

theorem :: KNASTER:36
  the carrier of FixPoints f = {x where x is Element of L: x
  is_a_fixpoint_of f};

theorem :: KNASTER:37
  the carrier of FixPoints f c= the carrier of L;

theorem :: KNASTER:38
  a in the carrier of FixPoints f iff a is_a_fixpoint_of f;

theorem :: KNASTER:39
  for x, y being Element of FixPoints f, a, b st x = a & y = b
  holds (x [= y iff a [= b);

theorem :: KNASTER:40
  FixPoints f is complete;

definition
  let L, f;
  func lfp f -> Element of L equals
:: KNASTER:def 10
  (f, nextcard the carrier of L)+.Bottom L;
  func gfp f -> Element of L equals
:: KNASTER:def 11
  (f, nextcard the carrier of L)-.Top L;
end;

theorem :: KNASTER:41
  lfp f is_a_fixpoint_of f & ex O st card O c= card the carrier of
  L & (f, O)+.Bottom L = lfp f;

theorem :: KNASTER:42
  gfp f is_a_fixpoint_of f & ex O st card O c= card the carrier of
  L & (f, O)-.Top L = gfp f;

theorem :: KNASTER:43
  a is_a_fixpoint_of f implies lfp f [= a & a [= gfp f;

theorem :: KNASTER:44
  f.a [= a implies lfp f [= a;

theorem :: KNASTER:45
  a [= f.a implies a [= gfp f;

begin :: Boolean Lattices

reserve f for monotone UnOp of BooleLatt A;

theorem :: KNASTER:46
  for f being UnOp of BooleLatt A holds f is monotone iff f is c=-monotone;

theorem :: KNASTER:47
  ex g being c=-monotone Function of bool A, bool A st lfp (A, g) = lfp f;

theorem :: KNASTER:48
  ex g being c=-monotone Function of bool A, bool A st gfp (A, g) = gfp f;