:: An inference system of an extension of Floyd-Hoare logic for partial
:: predicates
::  by Ievgen Ivanov , Artur Korni{\l}owicz and Mykola Nikitchenko
::
:: Received June 29, 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 NOMIN_1, NUMBERS, SUBSET_1, XBOOLE_0, RELAT_1, FUNCT_1, FINSEQ_1,
      XXREAL_0, NAT_1, ARYTM_3, CARD_1, XBOOLEAN, TARSKI, CARD_3, ARYTM_1,
      FUNCT_7, PARTFUN1, NOMIN_3, NOMIN_2, PARTPR_1, PARTPR_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, MARGREL1, RELAT_1,
      RELSET_1, FUNCT_1, PARTFUN1, PARTFUN2, FINSEQ_1, BINOP_1, XXREAL_0,
      XCMPLX_0, CARD_3, FUNCT_7, NOMIN_1, PARTPR_1, PARTPR_2, NOMIN_2;
 constructors MIDSP_3, RELSET_1, MULTOP_1, NOMIN_2, PARTFUN2;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, FUNCT_7,
      RELSET_1, INT_1, NOMIN_1, NOMIN_2;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


begin

reserve v,x for object;
reserve D,V,A for set;
reserve n for Nat;
reserve p,q for PartialPredicate of D;
reserve f,g for BinominativeFunction of D;

definition
  let D,f,p;
  pred f coincides_with p means
:: NOMIN_3:def 1
  for d being Element of D st d in dom p holds f.d in dom p;
end;

definition
  let D,f,g,p,q;
  pred f,g coincide_with p,q means
:: NOMIN_3:def 2
  for d being Element of D st d in rng f & g.d in dom q holds d in dom p;
end;

theorem :: NOMIN_3:1
  f coincides_with PP_BottomPred(D);

theorem :: NOMIN_3:2
  PPid(D) coincides_with p;

definition
  let D,p,q;
  pred p ||= q means
:: NOMIN_3:def 3
  for d being Element of D holds
   d in dom p & p.d = TRUE implies d in dom q & q.d = TRUE;
  reflexivity;
end;

reserve D for non empty set;
reserve d for Element of D;
reserve f,g for BinominativeFunction of D;
reserve p,q,r,s for PartialPredicate of D;

theorem :: NOMIN_3:3
  p ||= r implies PP_and(p,q) ||= r;

theorem :: NOMIN_3:4
  PP_and(p,q) ||= p;

theorem :: NOMIN_3:5
  p ||= q & r ||= s implies PP_and(p,r) ||= PP_and(q,s);

theorem :: NOMIN_3:6
  PP_or(p,q) ||= r implies p ||= r;

theorem :: NOMIN_3:7
  p ||= PP_or(q,r) implies
  for d st d in dom p & p.d = TRUE holds
   d in dom q & q.d = TRUE or d in dom r & r.d = TRUE;

theorem :: NOMIN_3:8
  PP_or(p,p) ||= p;

theorem :: NOMIN_3:9
  p ||= q & r ||= s implies PP_or(p,r) ||= PP_or(q,s);

theorem :: NOMIN_3:10
  PP_or(p,q) ||= r implies PP_and(p,q) ||= r;

definition
  let D;
  func SemanticFloydHoareTriples(D) -> set equals
:: NOMIN_3:def 4
  { <*p,f,q*> where p,q is PartialPredicate of D,
                    f is BinominativeFunction of D :
   for d being Element of D holds
    d in dom p & p.d = TRUE & d in dom f & f.d in dom q implies
     q.(f.d) = TRUE };
end;

notation
  let D;
  synonym SFHTs(D) for SemanticFloydHoareTriples(D);
end;

theorem :: NOMIN_3:11
  <*p,f,q*> in SFHTs(D) implies
  for d holds d in dom p & p.d = TRUE & d in dom f & f.d in dom q implies
   q.(f.d) = TRUE;

theorem :: NOMIN_3:12
  <*{},f,p*> in SFHTs(D);

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

definition
  let D;
  mode SemanticFloydHoareTriple of D
    is Element of SemanticFloydHoareTriples(D);
  mode SFHT of D is Element of SFHTs(D);
end;

theorem :: NOMIN_3:13
  <*p,id dom p,p*> is SFHT of D;

theorem :: NOMIN_3:14
  <*p,id field f,p*> is SFHT of D;

::$N CONS_1 rule
theorem :: NOMIN_3:15
  <*p,f,q*> is SFHT of D & r ||= p implies <*r,f,q*> is SFHT of D;

::$N CONS_2 rule
theorem :: NOMIN_3:16
  <*p,f,q*> is SFHT of D & q ||= r & dom r c= dom q
  implies <*p,f,r*> is SFHT of D;

::$N skip rule
theorem :: NOMIN_3:17
  <*p,PPid(D),p*> is SFHT of D;

theorem :: NOMIN_3:18
  <*PP_False(D),f,p*> is SFHT of D;

::$N inversion rule
theorem :: NOMIN_3:19
  p is total implies <*PP_inversion(p),f,q*> is SFHT of D;

::$N composition rule
theorem :: NOMIN_3:20
  <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & f,g coincide_with q,r
  implies <*p,PP_composition(f,g),r*> is SFHT of D;

::$N IF rule
theorem :: NOMIN_3:21
  <*PP_and(r,p),f,q*> is SFHT of D &
  <*PP_and(PP_not(r),p),g,q*> is SFHT of D implies
  <*p,PP_IF(r,f,g),q*> is SFHT of D;

theorem :: NOMIN_3:22
  f coincides_with p & <*p,f,p*> is SFHT of D implies
  <*p,iter(f,n),p*> is SFHT of D;

::$N while rule
theorem :: NOMIN_3:23
  f coincides_with p & dom p c= dom f &
  <*PP_and(r,p),f,p*> is SFHT of D implies
  <*p,PP_while(r,f),PP_and(PP_not(r),p)*> is SFHT of D;

::$N unconditional composition rule (USEQ)
theorem :: NOMIN_3:24
  <*p,f,q*> is SFHT of D &
  <*q,g,r*> is SFHT of D & <*PP_inversion(q),g,s*> is SFHT of D
  implies <*p,PP_composition(f,g),PP_or(r,s)*> is SFHT of D;

::$N unconditional composition rule (USEQ)
theorem :: NOMIN_3:25
  <*p,f,q*> is SFHT of D &
  <*q,g,r*> is SFHT of D & <*PP_inversion(q),g,r*> is SFHT of D
  implies <*p,PP_composition(f,g),r*> is SFHT of D;

::$N unconditional while rule (UWH)
theorem :: NOMIN_3:26
  <*PP_and(r,p),f,p*> is SFHT of D &
  <*PP_and(r,PP_inversion(p)),f,p*> is SFHT of D implies
  <*p,PP_while(r,f),PP_and(PP_not(r),p)*> is SFHT of D;

::$N DP rule
theorem :: NOMIN_3:27
  <*p,f,r*> is SFHT of D & <*q,f,r*> is SFHT of D implies
  <*PP_or(p,q),f,r*> is SFHT of D;

reserve p,q for SCPartialNominativePredicate of V,A;
reserve f,g for SCBinominativeFunction of V,A;
reserve E for (V,A)-FPrg-yielding FinSequence;
reserve e for Element of product E;
reserve d for TypeSCNominativeData of V,A;

theorem :: NOMIN_3:28
  (for d being TypeSCNominativeData of V,A holds
   d in dom p & p.d = TRUE & d in dom f & f.d in dom q implies q.(f.d) = TRUE)
  implies
  <*p,f,q*> is SFHT of ND(V,A);

::$N assignment rule
theorem :: NOMIN_3:29
  <*SC_Psuperpos(p,f,v),SC_assignment(f,v),p*> is SFHT of ND(V,A);

::$N SFID_1 rule
theorem :: NOMIN_3:30
  <*SC_Psuperpos(p,f,v),SC_Fsuperpos(PPid(ND(V,A)),f,v),p*> is SFHT of ND(V,A);

::$N SFID rule
theorem :: NOMIN_3:31
  product E <> {} implies
  <*SC_Psuperpos(p,e,E),SC_Fsuperpos(PPid(ND(V,A)),e,E),p*> is SFHT of ND(V,A);

::$N SF_1 rule
theorem :: NOMIN_3:32
  <*p, PP_composition(SC_Fsuperpos(PPid(ND(V,A)),g,v),f), q*>
   is SFHT of ND(V,A)
  implies
  <*p,SC_Fsuperpos(f,g,v),q*> is SFHT of ND(V,A);

::$N SF rule
theorem :: NOMIN_3:33
  product E <> {} &
  <*p, PP_composition(SC_Fsuperpos(PPid(ND(V,A)),e,E),f), q*>
    is SFHT of ND(V,A)
  implies
  <*p,SC_Fsuperpos(f,e,E),q*> is SFHT of ND(V,A);