Up to index of Isabelle/HOL/IMPP
theory Hoare = Natural(* Title: HOL/IMPP/Hoare.thy
ID: $Id: Hoare.thy,v 1.31 1999/11/24 13:48:19 oheimb Exp $
Author: originally Tobias Nipkow, completely new by David von Oheimb
Copyright 1995, 1999 TUM
Inductive definition of Hoare logic for partial correctness
Completeness is taken relative to completeness of the underlying logic
Two dimensions of completeness proof:
* induction on the term structure vs. rule induction wrt. the operat. semantics
* nested single recursion vs. simultaneous recursion in call rule
VerNS: nested single structural induction
VerSS: simultaneous structural induction
VerNR: rule induction with nested single call rule
VerSR: rule induction with simultaneous call rule (non-interesting)
*)
Hoare = Natural +
types 'a assn = "'a => state => bool"
translations
"a assn" <= (type)"a => state => bool"
constdefs
peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35)
"peek_and P p == %Z s. P Z s & p s"
datatype 'a triple =
triple ('a assn) com ('a assn) ("{(1_)}. (_) .{(1_)}" [3,60,3] 58)
consts
triple_valid :: nat => 'a triple => bool ( "|=_:_" [0 , 58] 57)
hoare_valids :: 'a triple set => 'a triple set => bool ("_||=_" [58, 58] 57)
hoare_derivs ::"('a triple set * 'a triple set) set"
syntax
triples_valid:: nat => 'a triple set => bool ("||=_:_" [0 , 58] 57)
hoare_valid :: 'a triple set => 'a triple => bool ("_|=_" [58, 58] 57)
"@hoare_derivs":: 'a triple set => 'a triple set => bool ("_||-_" [58, 58] 57)
"@hoare_deriv" :: 'a triple set => 'a triple => bool ("_|-_" [58, 58] 57)
defs triple_valid_def "|=n:t == case t of {P}.c.{Q} =>
!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s')"
translations "||=n:G" == "Ball G (triple_valid n)"
defs hoare_valids_def"G||=ts == !n. ||=n:G --> ||=n:ts"
translations "G |=t " == " G||={t}"
"G||-ts" == "(G,ts) : hoare_derivs"
"G |-t" == " G||-{t}"
(* Most General Triples *)
locale struct_ind =
fixes MGT :: com => state triple ("{=}._.{->}" [ 60 ] 58)
assumes
defines MGT_def "{=}.c.{->} == {%Z s0. Z=s0}.c.{%Z s1. <c,Z> -c-> s1}"
inductive hoare_derivs intrs
(*VerS_*)
empty "G||-{}"
insert"[| G |-t; G||-ts |]
==> G||-insert t ts"
(*Ver_S*)
asm "ts <= G ==>
G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *)
cut "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *)
weaken"[| G||-ts' ; ts <= ts' |] ==> G||-ts"
conseq"!Z s. P Z s --> (? P' Q'. G|-{P'}.c.{Q'} &
(!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s'))
==> G|-{P}.c.{Q}"
(*Ver_R*)
diverg"G|-{%Z s. ~(? s'. <c, s> -c-> s')}.c.{Q}"
Skip "G|-{P}. SKIP .{P}"
Ass "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}"
Local "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])}
==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}"
Comp "[| G|-{P}.c.{Q};
G|-{Q}.d.{R} |]
==> G|-{P}. (c;;d) .{R}"
If "[| G|-{P &> b }.c.{Q};
G|-{P &> (Not o b)}.d.{Q} |]
==> G|-{P}. IF b THEN c ELSE d .{Q}"
(*Ver_R*)
LoopT "[| G|-{P &> b}.c.{Q};
G|-{Q}. WHILE b DO c .{R} |]
==> G|-{P &> b}. WHILE b DO c .{R}"
Loop "G|-{P &> b}.c.{P} ==>
G|-{P}. WHILE b DO c .{P &> (Not o b)}"
(*VerN_
BodyN "(insert ({P}. BODY pn .{Q}) G)
|-{P}. body pn .{Q} ==>
G|-{P}. BODY pn .{Q}"
VerS_*)
Body "[| G Un (%p. {P p}. BODY p .{Q p})``Procs
||-(%p. {P p}. body p .{Q p})``Procs |]
==> G||-(%p. {P p}. BODY p .{Q p})``Procs"
Call "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}
==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.
X:=CALL pn(a) .{Q}"
end
theorem triple_valid_def2:
|=n:{P}. c .{Q} = (ALL Z s. P Z s --> (ALL s'. <c,s> -n-> s' --> Q Z s'))
theorem Body_triple_valid_0:
|=0:{P}. BODY pn .{Q} [!]
theorem Body_triple_valid_Suc:
|=n:{P}. body pn .{Q} = |=Suc n:{P}. BODY pn .{Q} [!]
theorem triple_valid_Suc:
|=Suc n:t ==> |=n:t
theorem triples_valid_Suc:
||=Suc n:ts ==> ||=n:ts
theorem conseq12:
[| G|-{P'}. c .{Q'};
ALL Z s. P Z s --> (ALL s'. (ALL Z'. P' Z' s --> Q' Z' s') --> Q Z s') |]
==> G|-{P}. c .{Q}
theorem conseq1:
[| G|-{P'}. c .{Q}; ALL Z s. P Z s --> P' Z s |] ==> G|-{P}. c .{Q}
theorem conseq2:
[| G|-{P}. c .{Q'}; ALL Z s. Q' Z s --> Q Z s |] ==> G|-{P}. c .{Q}
theorem Body1:
[| G Un
(%p. {P p}. BODY p .{Q p}) `` Procs||-(%p. {P p}. body p .{Q p}) `` Procs;
pn : Procs |]
==> G|-{P pn}. BODY pn .{Q pn}
theorem BodyN:
insert ({P}. BODY pn .{Q}) G|-{P}. body pn .{Q} ==> G|-{P}. BODY pn .{Q}
theorem escape:
ALL Z s. P Z s --> G|-{%Z s'. s' = s}. c .{%Z'. Q Z} ==> G|-{P}. c .{Q}
theorem constant:
(C ==> G|-{P}. c .{Q}) ==> G|-{%Z s. P Z s & C}. c .{Q}
theorem LoopF:
G|-{%Z s. P Z s & ¬ b s}. WHILE b DO c .{P}
theorem thin:
[| G'||-ts; G' <= G |] ==> G||-ts
theorem weak_Body:
G|-{P}. body pn .{Q} ==> G|-{P}. BODY pn .{Q}
theorem derivs_insertD:
G||-insert t ts ==> G|-t & G||-ts
theorem finite_pointwise:
[| finite U; ALL p. G|-{P' p}. c0 p .{Q' p} --> G|-{P p}. c0 p .{Q p};
G||-(%p. {P' p}. c0 p .{Q' p}) `` U |]
==> G||-(%p. {P p}. c0 p .{Q p}) `` U
theorem Loop_sound_lemma:
G|={P &> b}. c .{P} ==> G|={P}. WHILE b DO c .{P &> Not o b} [!]
theorem Body_sound_lemma:
G Un
(%pn. {P pn}. BODY pn .{Q pn}) ``
Procs||=(%pn. {P pn}. body pn .{Q pn}) `` Procs
==> G||=(%pn. {P pn}. BODY pn .{Q pn}) `` Procs
[!]
theorem hoare_sound:
G||-ts ==> G||=ts [!]
theorem MGT_alternI:
G|-MGT c ==> G|-{%Z s0. ALL s1. <c,s0> -c-> s1 --> Z = s1}. c .{op =}
[!!c. MGT c == {op =}. c .{%Z s1. <c,Z> -c-> s1}]
theorem MGT_alternD:
G|-{%Z s0. ALL s1. <c,s0> -c-> s1 --> Z = s1}. c .{op =} ==> G|-MGT c
[!!c. MGT c == {op =}. c .{%Z s1. <c,Z> -c-> s1}, !]
theorem MGF_complete:
[| {}|-MGT c; {}|={P}. c .{Q} |] ==> {}|-{P}. c .{Q}
[!!c. MGT c == {op =}. c .{%Z s1. <c,Z> -c-> s1}]
theorem MGF_lemma1:
ALL pn. G|-MGT (BODY pn) ==> G|-MGT c
[!!c. MGT c == {op =}. c .{%Z s1. <c,Z> -c-> s1}, !]
theorem nesting_lemma:
[| !!x ts. ts <= x ==> P x ts;
!!x pn. P (insert (mgt_call pn) x) {mgt (body pn)} ==> P x {mgt_call pn};
!!x xa. ALL pn:U. P x {mgt_call pn} ==> P x {mgt xa}; finite U;
uG = mgt_call `` U; G <= uG; n <= card uG; card G = card uG - n |]
==> P G {mgt c}
theorem MGT_BodyN:
insert (MGT (BODY pn)) G|-MGT (body pn) ==> G|-MGT (BODY pn)
[!!c. MGT c == {op =}. c .{%Z s1. <c,Z> -c-> s1}]
theorem MGF:
{}|-MGT c [!!c. MGT c == {op =}. c .{%Z s1. <c,Z> -c-> s1}, !]
theorem MGF_lemma2_simult:
[| finite F; F <= range (%pn. MGT (body pn)) |]
==> range (%pn. MGT (BODY pn))||-F
[!!c. MGT c == {op =}. c .{%Z s1. <c,Z> -c-> s1}, !]
theorem MGT_Body:
[| G Un (%pn. MGT (BODY pn)) `` Procs||-(%pn. MGT (body pn)) `` Procs;
finite Procs |]
==> G||-(%pn. MGT (BODY pn)) `` Procs
[!!c. MGT c == {op =}. c .{%Z s1. <c,Z> -c-> s1}]
theorem MGF:
{}|-MGT c [!!c. MGT c == {op =}. c .{%Z s1. <c,Z> -c-> s1}, !]
theorem hoare_complete:
{}|={P}. c .{Q} ==> {}|-{P}. c .{Q} [!]
theorem MGF2_complete:
[| ALL s0 s1. <c,s0> -c-> s1 --> {}|-{%Z s. s = s0}. c .{%Z s'. s' = s1};
{}|={P}. c .{Q} |]
==> {}|-{P}. c .{Q}
theorem const_eq:
G|-{%Z s'. s' = s & C s'}. c .{Q} = (C s --> G|-{%Z s'. s' = s}. c .{Q})
theorem MGF2:
ALL s0a s1a. <c,s0a> -c-> s1a --> {}|-{%Z s. s = s0a}. c .{%Z s'. s' = s1a} [!]
theorem hoare_complete:
{}|={P}. c .{Q} ==> {}|-{P}. c .{Q} [!]
theorem hoare_eq:
{}|-{P}. c .{Q} = {}|={P}. c .{Q} [!]
theorem falseE:
G|-{%Z s. False}. c .{Q}
theorem trueI:
G|-{P}. c .{%Z s. True}
theorem disj:
[| G|-{P}. c .{Q}; G|-{P'}. c .{Q'} |]
==> G|-{%Z s. P Z s | P' Z s}. c .{%Z s. Q Z s | Q' Z s}
theorem hoare_SkipI:
ALL Z s. P Z s --> Q Z s ==> G|-{P}. SKIP .{Q}
theorem single_asm:
{t}|-t
theorem export_s:
(!!s'. G|-{%Z s. s' = s & P Z s}. c .{Q}) ==> G|-{P}. c .{Q}
theorem getlocs_def2:
getlocs (st g l) = l
theorem update_Loc_idem2:
s[Loc X::=s<X>] = s
theorem update_overwrt:
s[X::=x][X::=y] = s[X::=y]
theorem getlocs_Loc_update:
s[Loc X::=k]<Y> = (if X = Y then k else s<Y>)
theorem classic_Local_valid:
ALL v. G|={%Z s. P Z (s[Loc X::=v]) &
s<X> = a (s[Loc X::=v])}. c .{%Z s. Q Z (s[Loc X::=v])}
==> G|={P}. LOCAL X:=a IN c .{Q}
[!]
theorem classic_Local:
ALL v. G|-{%Z s. P Z (s[Loc X::=v]) &
s<X> = a (s[Loc X::=v])}. c .{%Z s. Q Z (s[Loc X::=v])}
==> G|-{P}. LOCAL X:=a IN c .{Q}
theorem weak_Local:
[| G|-{P}. c .{Q}; ALL k Z s. Q Z s --> Q Z (s[Loc X::=k]) |]
==> G|-{%Z s. P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}
theorem getlocs_Glb_update:
getlocs (s[Glb X::=k]) = getlocs s
theorem getlocs_setlocs:
getlocs (setlocs s l) = l
theorem getlocs_setlocs_lemma:
getlocs (setlocs s (getlocs s')[X::=k]) = getlocs (s'[X::=k])
theorem Call_invariant:
G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}
==> G|-{%Z s. s' = s &
I Z (getlocs (s[X::=k Z])) &
P Z (setlocs s newlocs[Loc Arg::=
a s])}. X:=CALL pn(a) .{%Z s.
I Z (getlocs (s[X::=k Z])) & Q Z s}