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

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

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

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

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

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

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

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

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

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

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

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

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

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

:: WP: SFID rule
theorem :: NOMIN_3:31
for V, A being set
for p being SCPartialNominativePredicate of V,A
for E being b1,b2 -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;

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

:: WP: 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 b1,b2 -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;