:: 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-2019 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 while rule (UWH)
theorem :: NOMIN_3:25
<*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:26
<*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:27
(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:28
<*SC_Psuperpos(p,f,v),SC_assignment(f,v),p*> is SFHT of ND(V,A);
::$N SFID_1 rule
theorem :: NOMIN_3:29
<*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:30
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:31
<*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:32
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);