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

definition

let D be set ;
let f be BinominativeFunction of D;
let p be PartialPredicate of D;

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;

:: deftheorem defines coincides_with NOMIN_3:def 1 :
for D being set
for f being BinominativeFunction of D
for p being PartialPredicate of D holds
( f coincides_with p iff for d being Element of D st d in dom p holds
f . d in dom p );

definition

let D be set ;
let f, g be BinominativeFunction of D;
let p, q be PartialPredicate of D;

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;

:: deftheorem defines coincide_with NOMIN_3:def 2 :
for D being set
for f, g being BinominativeFunction of D
for p, q being PartialPredicate of D holds
( f,g coincide_with p,q iff for d being Element of D st d in rng f & g . d in dom q holds
d in dom p );

theorem :: NOMIN_3:1

for D being set
for f being BinominativeFunction of D holds f coincides_with PP_BottomPred D ;

theorem :: NOMIN_3:2

for D being set
for p being PartialPredicate of D holds PPid D coincides_with p ;

definition

let D be set ;
let p, q be PartialPredicate of D;

pred p ||= q means :: NOMIN_3:def 3
for d being Element of D st d in dom p & p . d = TRUE holds
( d in dom q & q . d = TRUE );

reflexivity
for p being PartialPredicate of D
for d being Element of D st d in dom p & p . d = TRUE holds
( d in dom p & p . d = TRUE ) ;

end;

:: deftheorem defines ||= NOMIN_3:def 3 :
for D being set
for p, q being PartialPredicate of D holds
( p ||= q iff for d being Element of D st d in dom p & p . d = TRUE holds
( d in dom q & q . d = TRUE ) );

theorem Th3: :: NOMIN_3:3

for D being non empty set
for p, q, r being PartialPredicate of D st p ||= r holds
PP_and (p,q) ||= r

proof end;

theorem :: NOMIN_3:4

for D being non empty set
for p, q being PartialPredicate of D holds PP_and (p,q) ||= p by Th3;

theorem :: NOMIN_3:5

for D being non empty set
for p, q, r, s being PartialPredicate of D st p ||= q & r ||= s holds
PP_and (p,r) ||= PP_and (q,s)

proof end;

theorem Th6: :: NOMIN_3:6

for D being non empty set
for p, q, r being PartialPredicate of D st PP_or (p,q) ||= r holds
p ||= r

proof end;

theorem :: NOMIN_3:7

for D being non empty set
for p, q, r being PartialPredicate of D st p ||= PP_or (q,r) holds
for d being Element of D st d in dom p & p . d = TRUE & not ( d in dom q & q . d = TRUE ) holds
( d in dom r & r . d = TRUE )

proof end;

theorem :: NOMIN_3:8

for D being non empty set
for p being PartialPredicate of D holds PP_or (p,p) ||= p ;

theorem :: NOMIN_3:9

for D being non empty set
for p, q, r, s being PartialPredicate of D st p ||= q & r ||= s holds
PP_or (p,r) ||= PP_or (q,s)

proof end;

theorem :: NOMIN_3:10

for D being non empty set
for p, q, r being PartialPredicate of D st PP_or (p,q) ||= r holds
PP_and (p,q) ||= r by Th6, Th3;

definition

let D be non empty set ;

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 st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE } ;

coherence
{ <*p,f,q*> where p, q is PartialPredicate of D, f is BinominativeFunction of D : for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE } is set ;

end;

:: deftheorem defines SemanticFloydHoareTriples NOMIN_3:def 4 :
for D being non empty set holds SemanticFloydHoareTriples D = { <*p,f,q*> where p, q is PartialPredicate of D, f is BinominativeFunction of D : for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE } ;

notation

let D be non empty set ;
synonym SFHTs D for SemanticFloydHoareTriples D;

end;

theorem Th11: :: NOMIN_3:11

for D being non empty set
for f being BinominativeFunction of D
for p, q being PartialPredicate of D st <*p,f,q*> in SFHTs D holds
for d being Element of D st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE

proof end;

theorem Th12: :: NOMIN_3:12

for D being non empty set
for f being BinominativeFunction of D
for p being PartialPredicate of D holds <*{},f,p*> in SFHTs D

proof end;

registration

let D be non empty set ;

cluster SemanticFloydHoareTriples D -> non empty ;

coherence
not SFHTs D is empty by Th12;

end;

definition

let D be non empty set ;
mode SemanticFloydHoareTriple of D is Element of SemanticFloydHoareTriples D;
mode SFHT of D is Element of SFHTs D;

end;

theorem :: NOMIN_3:13

for D being non empty set
for p being PartialPredicate of D holds <*p,(id (dom p)),p*> is SFHT of D

proof end;

theorem Th14: :: NOMIN_3:14

for D being non empty set
for f being BinominativeFunction of D
for p being PartialPredicate of D holds <*p,(id (field f)),p*> is SFHT of D

proof end;

:: CONS_1 rule

theorem Th15: :: NOMIN_3:15

for D being non empty set
for f being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & r ||= p holds
<*r,f,q*> is SFHT of D

proof end;

:: CONS_2 rule

theorem :: NOMIN_3:16

for D being non empty set
for f being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & q ||= r & dom r c= dom q holds
<*p,f,r*> is SFHT of D

proof end;

:: skip rule

theorem :: NOMIN_3:17

for D being non empty set
for p being PartialPredicate of D holds <*p,(PPid D),p*> is SFHT of D

proof end;

theorem Th18: :: NOMIN_3:18

for D being non empty set
for f being BinominativeFunction of D
for p being PartialPredicate of D holds <*(PP_False D),f,p*> is SFHT of D

proof end;

:: inversion rule

theorem :: NOMIN_3:19

for D being non empty set
for f being BinominativeFunction of D
for p, q being PartialPredicate of D st p is total holds
<*(PP_inversion p),f,q*> is SFHT of D

proof end;

:: composition rule

theorem :: NOMIN_3:20

for D being non empty set
for f, g being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & f,g coincide_with q,r holds
<*p,(PP_composition (f,g)),r*> is SFHT of D

proof end;

:: IF rule

theorem :: NOMIN_3:21

for D being non empty set
for f, g being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*(PP_and (r,p)),f,q*> is SFHT of D & <*(PP_and ((PP_not r),p)),g,q*> is SFHT of D holds
<*p,(PP_IF (r,f,g)),q*> is SFHT of D

proof end;

theorem :: NOMIN_3:22

for n being Nat
for D being non empty set
for f being BinominativeFunction of D
for p being PartialPredicate of D st f coincides_with p & <*p,f,p*> is SFHT of D holds
<*p,(iter (f,n)),p*> is SFHT of D

proof end;

:: while rule

theorem :: NOMIN_3:23

for D being non empty set
for f being BinominativeFunction of D
for p, r being PartialPredicate of D st f coincides_with p & dom p c= dom f & <*(PP_and (r,p)),f,p*> is SFHT of D holds
<*p,(PP_while (r,f)),(PP_and ((PP_not r),p))*> is SFHT of D

proof end;

:: unconditional composition rule (USEQ)

theorem Th24: :: NOMIN_3:24

for D being non empty set
for f, g being BinominativeFunction of D
for p, q, r, s being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,s*> is SFHT of D holds
<*p,(PP_composition (f,g)),(PP_or (r,s))*> is SFHT of D

proof end;

:: unconditional composition rule (USEQ)

theorem :: NOMIN_3:25

for D being non empty set
for f, g being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*p,f,q*> is SFHT of D & <*q,g,r*> is SFHT of D & <*(PP_inversion q),g,r*> is SFHT of D holds
<*p,(PP_composition (f,g)),r*> is SFHT of D

proof end;

:: unconditional while rule (UWH)

theorem :: NOMIN_3:26

for D being non empty set
for f being BinominativeFunction of D
for p, r being PartialPredicate of D st <*(PP_and (r,p)),f,p*> is SFHT of D & <*(PP_and (r,(PP_inversion p))),f,p*> is SFHT of D holds
<*p,(PP_while (r,f)),(PP_and ((PP_not r),p))*> is SFHT of D

proof end;

:: DP rule

theorem :: NOMIN_3:27

for D being non empty set
for f being BinominativeFunction of D
for p, q, r being PartialPredicate of D st <*p,f,r*> is SFHT of D & <*q,f,r*> is SFHT of D holds
<*(PP_or (p,q)),f,r*> is SFHT of D

proof end;

theorem Th27: :: NOMIN_3:28

for V, A being set
for p, q being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A st ( for d being TypeSCNominativeData of V,A st d in dom p & p . d = TRUE & d in dom f & f . d in dom q holds
q . (f . d) = TRUE ) holds
<*p,f,q*> is SFHT of (ND (V,A))

proof end;

:: assignment rule

theorem :: NOMIN_3:29

for v being object
for V, A being set
for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds <*(SC_Psuperpos (p,f,v)),(SC_assignment (f,v)),p*> is SFHT of (ND (V,A))

proof end;

:: SFID_1 rule

theorem :: NOMIN_3:30

for v being object
for V, A being set
for p being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A holds <*(SC_Psuperpos (p,f,v)),(SC_Fsuperpos ((PPid (ND (V,A))),f,v)),p*> is SFHT of (ND (V,A))

proof end;

:: SFID rule

theorem :: NOMIN_3:31

for V, A being set
for p being SCPartialNominativePredicate of V,A
for E being b₁,b₂ -FPrg-yielding FinSequence
for e being Element of product E st product E <> {} holds
<*(SC_Psuperpos (p,e,E)),(SC_Fsuperpos ((PPid (ND (V,A))),e,E)),p*> is SFHT of (ND (V,A))

proof end;

:: SF_1 rule

theorem :: NOMIN_3:32

for v being object
for V, A being set
for p, q being SCPartialNominativePredicate of V,A
for f, g being SCBinominativeFunction of V,A st <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),g,v)),f)),q*> is SFHT of (ND (V,A)) holds
<*p,(SC_Fsuperpos (f,g,v)),q*> is SFHT of (ND (V,A))

proof end;

:: SF rule

theorem :: NOMIN_3:33

for V, A being set
for p, q being SCPartialNominativePredicate of V,A
for f being SCBinominativeFunction of V,A
for E being b₁,b₂ -FPrg-yielding FinSequence
for e being Element of product E st product E <> {} & <*p,(PP_composition ((SC_Fsuperpos ((PPid (ND (V,A))),e,E)),f)),q*> is SFHT of (ND (V,A)) holds
<*p,(SC_Fsuperpos (f,e,E)),q*> is SFHT of (ND (V,A))

proof end;