:: Kleene Algebra of Partial Predicates
::  by Artur Korni{\l}owicz , Ievgen Ivanov and Mykola Nikitchenko
:: 
:: Received March 27, 2018
:: Copyright (c) 2018-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 PARTPR_1, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1,
      MARGREL1, XBOOLEAN, TARSKI, MONOID_0, FUNCOP_1, ZFMISC_1, BINOP_1,
      LATTICES, EQREL_1, XXREAL_2, ROBBINS1, PBOOLE, STRUCT_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MARGREL1, RELAT_1, RELSET_1,
      FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, STRUCT_0, MONOID_0,
      LATTICES, ROBBINS1;
 constructors RFUNCT_3, RELSET_1, MARGREL1, LATTICES, MONOID_0, ROBBINS1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1, RELSET_1, NAT_1,
      MONOID_0, LATTICES, ROBBINS1;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Partial predicates

reserve x for object;
reserve D for set;

definition
  let D;
  func Pr(D) -> set equals
:: PARTPR_1:def 1
  PFuncs(D,BOOLEAN);
end;

registration
  let D;
  cluster Pr(D) -> non empty functional;
end;

definition
  let D;
  mode PartialPredicate of D is PartFunc of D,BOOLEAN;
end;

reserve p for PartialPredicate of D;

theorem :: PARTPR_1:1
  x in Pr(D) implies x is PartialPredicate of D;

theorem :: PARTPR_1:2
  p in Pr(D);

theorem :: PARTPR_1:3
  x in dom p implies p.x = TRUE or p.x = FALSE;

definition
  let D;
  func PPnegation(D) -> Function of Pr(D),Pr(D) means
:: PARTPR_1:def 2
  for p being PartialPredicate of D holds
   dom(it.p) = dom p &
   for d being object holds
    (d in dom p & p.d = TRUE implies it.p.d = FALSE) &
    (d in dom p & p.d = FALSE implies it.p.d = TRUE);
end;

definition
  let D,p;
  func PP_not(p) -> PartialPredicate of D equals
:: PARTPR_1:def 3
  PPnegation(D).p;
  involutiveness;
end;

theorem :: PARTPR_1:4
  x in dom p & PP_not(p).x = FALSE implies p.x = TRUE;

theorem :: PARTPR_1:5
  x in dom p & PP_not(p).x = TRUE implies p.x = FALSE;

theorem :: PARTPR_1:6
  x in dom PP_not(p) & PP_not(p).x = FALSE implies x in dom p & p.x = TRUE;

theorem :: PARTPR_1:7
  x in dom PP_not(p) & PP_not(p).x = TRUE implies x in dom p & p.x = FALSE;

reserve D for non empty set;
reserve p,q,r for PartialPredicate of D;

definition
  let D;
  func PPdisjunction(D) -> Function of [:Pr(D),Pr(D):],Pr(D) means
:: PARTPR_1:def 4

  for p,q being PartialPredicate of D holds
   dom(it.(p,q)) = {d where d is Element of D:
                    d in dom p & p.d = TRUE or d in dom q & q.d = TRUE
                    or d in dom p & p.d = FALSE & d in dom q & q.d = FALSE} &
  for d being object holds
   (d in dom p & p.d = TRUE or d in dom q & q.d = TRUE implies
      it.(p,q).d = TRUE) &
   (d in dom p & p.d = FALSE & d in dom q & q.d = FALSE implies
      it.(p,q).d = FALSE);
end;

definition
  let D,p,q;
  func PP_or(p,q) -> PartialPredicate of D equals
:: PARTPR_1:def 5
  PPdisjunction(D).(p,q);
  commutativity;
  idempotence;
end;

theorem :: PARTPR_1:8
  x in dom(PP_or(p,q)) implies
   x in dom p & p.x = TRUE or x in dom q & q.x = TRUE
   or x in dom p & p.x = FALSE & x in dom q & q.x = FALSE;

theorem :: PARTPR_1:9
  x in dom p & x in dom q & PP_or(p,q).x = TRUE implies
   p.x = TRUE or q.x = TRUE;

theorem :: PARTPR_1:10
  x in dom PP_or(p,q) & PP_or(p,q).x = TRUE implies
   x in dom p & p.x = TRUE or x in dom q & q.x = TRUE;

theorem :: PARTPR_1:11
  x in dom p & PP_or(p,q).x = FALSE implies p.x = FALSE;

theorem :: PARTPR_1:12
  x in dom q & PP_or(p,q).x = FALSE implies q.x = FALSE;

theorem :: PARTPR_1:13
  x in dom PP_or(p,q) & PP_or(p,q).x = FALSE implies
   x in dom p & p.x = FALSE & x in dom q & q.x = FALSE;

::$N Associativity law
theorem :: PARTPR_1:14
  PP_or(p,PP_or(q,r)) = PP_or(PP_or(p,q),r);

theorem :: PARTPR_1:15
  PP_or(PP_or(p,q),PP_or(p,r)) = PP_or(PP_or(p,q),r);

definition
  let D,p,q;
  func PP_and(p,q) -> PartialPredicate of D equals
:: PARTPR_1:def 6
  PP_not PP_or(PP_not(p),PP_not(q));
  commutativity;
  idempotence;
  func PP_imp(p,q) -> PartialPredicate of D equals
:: PARTPR_1:def 7
  PP_or(PP_not(p),q);
end;

theorem :: PARTPR_1:16
  dom(PP_and(p,q)) =
    {d where d is Element of D:
             d in dom p & p.d = FALSE or d in dom q & q.d = FALSE
          or d in dom p & p.d = TRUE & d in dom q & q.d = TRUE};

theorem :: PARTPR_1:17
  x in dom(PP_and(p,q)) implies
   x in dom p & p.x = FALSE or x in dom q & q.x = FALSE
    or x in dom p & p.x = TRUE & x in dom q & q.x = TRUE;

theorem :: PARTPR_1:18
  x in dom p & p.x = TRUE & x in dom q & q.x = TRUE implies
   PP_and(p,q).x = TRUE;

theorem :: PARTPR_1:19
  x in dom p & p.x = FALSE implies PP_and(p,q).x = FALSE;

theorem :: PARTPR_1:20
  x in dom q & q.x = FALSE implies PP_and(p,q).x = FALSE;

theorem :: PARTPR_1:21
  x in dom p & PP_and(p,q).x = TRUE implies p.x = TRUE;

theorem :: PARTPR_1:22
  x in dom q & PP_and(p,q).x = TRUE implies q.x = TRUE;

theorem :: PARTPR_1:23
  x in dom PP_and(p,q) & PP_and(p,q).x = TRUE implies
   x in dom p & p.x = TRUE & x in dom q & q.x = TRUE;

theorem :: PARTPR_1:24
  x in dom p & x in dom q & PP_and(p,q).x = FALSE implies
   p.x = FALSE or q.x = FALSE;

theorem :: PARTPR_1:25
  x in dom PP_and(p,q) & PP_and(p,q).x = FALSE implies
   x in dom p & p.x = FALSE or x in dom q & q.x = FALSE;

::$N Associativity law
theorem :: PARTPR_1:26
  PP_and(p,PP_and(q,r)) = PP_and(PP_and(p,q),r);

theorem :: PARTPR_1:27
  PP_and(PP_and(p,q),PP_and(p,r)) = PP_and(PP_and(p,q),r);

::$N Meet-absorbing law
theorem :: PARTPR_1:28
  PP_or(PP_and(p,q),q) = q;

::$N Join-absorbing law
theorem :: PARTPR_1:29
  PP_and(p,PP_or(p,q)) = p;

::$N Distributivity law
theorem :: PARTPR_1:30
  PP_and(p,PP_or(q,r)) = PP_or(PP_and(p,q),PP_and(p,r));

theorem :: PARTPR_1:31
  dom(PP_imp(p,q)) =
    {d where d is Element of D:
             d in dom p & p.d = FALSE or d in dom q & q.d = TRUE
          or d in dom p & p.d = TRUE & d in dom q & q.d = FALSE};

theorem :: PARTPR_1:32
  x in dom(PP_imp(p,q)) implies
   x in dom p & p.x = FALSE or x in dom q & q.x = TRUE
   or x in dom p & p.x = TRUE & x in dom q & q.x = FALSE;

theorem :: PARTPR_1:33
  x in dom p & p.x = FALSE implies PP_imp(p,q).x = TRUE;

theorem :: PARTPR_1:34
  x in dom q & q.x = TRUE implies PP_imp(p,q).x = TRUE;

theorem :: PARTPR_1:35
  x in dom p & p.x = TRUE & x in dom q & q.x = FALSE implies
   PP_imp(p,q).x = FALSE;

theorem :: PARTPR_1:36
  x in dom p & x in dom q & PP_imp(p,q).x = TRUE implies
   p.x = FALSE or q.x = TRUE;

theorem :: PARTPR_1:37
  x in dom p & PP_imp(p,q).x = FALSE implies p.x = TRUE;

theorem :: PARTPR_1:38
  x in dom q & PP_imp(p,q).x = FALSE implies q.x = FALSE;

theorem :: PARTPR_1:39
  x in dom PP_imp(p,q) & PP_imp(p,q).x = FALSE implies
   x in dom p & p.x = TRUE & x in dom q & q.x = FALSE;

theorem :: PARTPR_1:40
  x in dom PP_imp(p,q) & PP_imp(p,q).x = TRUE implies
   x in dom p & p.x = FALSE or x in dom q & q.x = TRUE;

theorem :: PARTPR_1:41
  PP_and(PP_imp(p,r),PP_imp(q,r)) = PP_imp(PP_or(p,q),r);

theorem :: PARTPR_1:42
  PP_or(PP_imp(p,r),PP_imp(q,r)) = PP_imp(PP_and(p,q),r);

::$N True constant predicate
definition
  let D be set;
  func PP_True(D) -> PartialPredicate of D equals
:: PARTPR_1:def 8
  D --> TRUE;
end;

::$N False constant predicate
definition
  let D be set;
  func PP_False(D) -> PartialPredicate of D equals
:: PARTPR_1:def 9
  D --> FALSE;
end;

theorem :: PARTPR_1:43
  for D being set holds PP_not(PP_False(D)) = PP_True(D);

theorem :: PARTPR_1:44
  for D being set holds PP_not(PP_True(D)) = PP_False(D);

theorem :: PARTPR_1:45
  PP_or(p,PP_True(D)) = PP_True(D);

theorem :: PARTPR_1:46
  PP_or(PP_True(D),p) = PP_True(D);

theorem :: PARTPR_1:47
  PP_and(p,PP_False(D)) = PP_False(D);

theorem :: PARTPR_1:48
  PP_and(PP_False(D),p) = PP_False(D);

theorem :: PARTPR_1:49
  PP_or(p,PP_not(p)) = PP_True(D) | dom p;

theorem :: PARTPR_1:50
  PP_or(PP_not(p),p) = PP_True(D) | dom p;

theorem :: PARTPR_1:51
  PP_and(p,PP_not(p)) = PP_False(D) | dom p;

theorem :: PARTPR_1:52
  PP_and(PP_not(p),p) = PP_False(D) | dom p;

theorem :: PARTPR_1:53
  PP_imp(PP_False(D),p) = PP_True(D);

theorem :: PARTPR_1:54
  PP_imp(p,PP_True(D)) = PP_True(D);

theorem :: PARTPR_1:55
  PP_or(PP_False(D)|dom p,PP_True(D)|dom q) = PP_True(D) | dom q;

::$N Empty predicate
definition
  let D be set;
  func PP_BottomPred(D) -> PartialPredicate of D equals
:: PARTPR_1:def 10
  {};
end;

theorem :: PARTPR_1:56
  for D being set holds PP_not(PP_BottomPred(D)) = PP_BottomPred(D);

theorem :: PARTPR_1:57
  PP_or(PP_BottomPred(D),PP_True(D)) = PP_True(D);

theorem :: PARTPR_1:58
  PP_and(PP_BottomPred(D),PP_False(D)) = PP_False(D);

theorem :: PARTPR_1:59
  PP_imp(PP_BottomPred(D),PP_True(D)) = PP_True(D);

begin :: Algebra of partial connectives with (strong) Kleene logical connectives

definition
  let D;
  func PartialPredConnectivesMeet(D) -> BinOp of Pr(D) means
:: PARTPR_1:def 11
  for p,q being PartialPredicate of D holds it.(p,q) = PP_and(p,q);
  func PartialPredConnectivesJoin(D) -> BinOp of Pr(D) means
:: PARTPR_1:def 12
  for p,q being PartialPredicate of D holds it.(p,q) = PP_or(p,q);
  func PartialPredConnectivesCompl(D) -> UnOp of Pr(D) means
:: PARTPR_1:def 13
  for p being PartialPredicate of D holds it.p = PP_not(p);
end;

definition
  let D;
  func PartialPredConnectivesLatt(D) -> strict OrthoLattStr equals
:: PARTPR_1:def 14
   OrthoLattStr(# Pr(D) , PartialPredConnectivesJoin(D) ,
                            PartialPredConnectivesMeet(D) ,
                            PartialPredConnectivesCompl(D) #);
end;

registration
  let D be non empty set;
  let f,g be BinOp of D;
  let h be UnOp of D;
  cluster OrthoLattStr(#D,f,g,h#) -> non empty;
end;

registration
  let D;
  cluster PartialPredConnectivesLatt(D) ->
          non empty constituted-Functions;
end;

registration
  cluster non empty constituted-Functions for LattStr;
end;

registration
  cluster strict non empty constituted-Functions for OrthoLattStr;
end;

registration
  let D;
  cluster PartialPredConnectivesLatt(D) -> Lattice-like;
  cluster PartialPredConnectivesLatt(D) -> bounded;
  cluster PartialPredConnectivesLatt(D) ->
     de_Morgan join-idempotent with_idempotent_element;
end;

theorem :: PARTPR_1:60
  Top PartialPredConnectivesLatt(D) = PP_True(D);

theorem :: PARTPR_1:61
  Bottom PartialPredConnectivesLatt(D) = PP_False(D);

definition
  let L be non empty constituted-Functions LattStr, a, b be Element of L;
  pred a is_a_partial_complement_of b means
:: PARTPR_1:def 15
  a"\/"b = Top L | dom b & b"\/"a = Top L | dom b &
  a"/\"b = Bottom L | dom b & b"/\"a = Bottom L | dom b;
end;

definition
  let L be non empty constituted-Functions LattStr;
  attr L is partially_complemented means
:: PARTPR_1:def 16
  for b being Element of L
   ex a being Element of L st a is_a_partial_complement_of b;
end;

definition
  let IT be constituted-Functions non empty LattStr;
  attr IT is partially_Boolean means
:: PARTPR_1:def 17
  IT is bounded partially_complemented distributive;
end;

registration
  cluster partially_Boolean -> bounded partially_complemented distributive
      for constituted-Functions non empty LattStr;
  cluster bounded partially_complemented distributive -> partially_Boolean
      for constituted-Functions non empty LattStr;
end;

theorem :: PARTPR_1:62
  for a,b being Element of PartialPredConnectivesLatt(D)
   st a = p & b = PP_not(p) holds b is_a_partial_complement_of a;

registration
  let D;
  cluster PartialPredConnectivesLatt(D) -> partially_Boolean;
end;

::$N Distributivity law
theorem :: PARTPR_1:63
  PP_or(p,PP_and(q,r)) = PP_and(PP_or(p,q),PP_or(p,r));

definition
  let L be non empty OrthoLattStr;
  attr L is Kleene means
:: PARTPR_1:def 18
  for x,y being Element of L holds x"/\"x` [= y"\/"y`;
end;

registration
  cluster Boolean well-complemented -> Kleene for
    meet-absorbing join-absorbing meet-commutative non empty OrthoLattStr;
end;

registration
  let D;
  cluster PartialPredConnectivesLatt(D) -> Kleene;
end;

registration
  cluster partially_Boolean join-idempotent Lattice-like
          for non empty constituted-Functions LattStr;
end;

registration
  cluster Kleene de_Morgan join-idempotent with_idempotent_element
          Lattice-like strict
          for non empty OrthoLattStr;
end;

registration
  cluster partially_Boolean Kleene de_Morgan
          join-idempotent with_idempotent_element Lattice-like strict
          for non empty constituted-Functions OrthoLattStr;
end;