8177

1 
(* Title: HOL/IMPP/Hoare.thy


2 
ID: $Id$


3 
Author: David von Oheimb


4 
Copyright 1999 TUM


5 
*)


6 

17477

7 
header {* Inductive definition of Hoare logic for partial correctness *}


8 


9 
theory Hoare


10 
imports Natural


11 
begin


12 


13 
text {*


14 
Completeness is taken relative to completeness of the underlying logic.


15 


16 
Two versions of completeness proof: nested single recursion


17 
vs. simultaneous recursion in call rule


18 
*}

8177

19 


20 
types 'a assn = "'a => state => bool"


21 
translations

17477

22 
"a assn" <= (type)"a => state => bool"

8177

23 


24 
constdefs


25 
state_not_singleton :: bool

17477

26 
"state_not_singleton == \<exists>s t::state. s ~= t" (* at least two elements *)

8177

27 


28 
peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35)

17477

29 
"peek_and P p == %Z s. P Z s & p s"

8177

30 


31 
datatype 'a triple =

17477

32 
triple "'a assn" com "'a assn" ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58)


33 

8177

34 
consts

17477

35 
triple_valid :: "nat => 'a triple => bool" ( "=_:_" [0 , 58] 57)


36 
hoare_valids :: "'a triple set => 'a triple set => bool" ("_=_" [58, 58] 57)


37 
hoare_derivs :: "('a triple set * 'a triple set) set"

8177

38 
syntax

17477

39 
triples_valid:: "nat => 'a triple set => bool" ("=_:_" [0 , 58] 57)


40 
hoare_valid :: "'a triple set => 'a triple => bool" ("_=_" [58, 58] 57)


41 
"@hoare_derivs":: "'a triple set => 'a triple set => bool" ("__" [58, 58] 57)


42 
"@hoare_deriv" :: "'a triple set => 'a triple => bool" ("__" [58, 58] 57)

8177

43 

17477

44 
defs triple_valid_def: "=n:t == case t of {P}.c.{Q} =>


45 
!Z s. P Z s > (!s'. <c,s> n> s' > Q Z s')"

8177

46 
translations "=n:G" == "Ball G (triple_valid n)"

17477

47 
defs hoare_valids_def: "G=ts == !n. =n:G > =n:ts"

8177

48 
translations "G =t " == " G={t}"


49 
"Gts" == "(G,ts) : hoare_derivs"


50 
"G t" == " G{t}"


51 


52 
(* Most General Triples *)

17477

53 
constdefs MGT :: "com => state triple" ("{=}._.{>}" [60] 58)

8177

54 
"{=}.c.{>} == {%Z s0. Z = s0}. c .{%Z s1. <c,Z> c> s1}"


55 

17477

56 
inductive hoare_derivs intros


57 


58 
empty: "G{}"


59 
insert: "[ G t; Gts ]


60 
==> Ginsert t ts"

8177

61 

17477

62 
asm: "ts <= G ==>


63 
Gts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *)

8177

64 

17477

65 
cut: "[ G'ts; GG' ] ==> Gts" (* for convenience and efficiency *)

8177

66 

17477

67 
weaken: "[ Gts' ; ts <= ts' ] ==> Gts"

8177

68 

17477

69 
conseq: "!Z s. P Z s > (? P' Q'. G{P'}.c.{Q'} &


70 
(!s'. (!Z'. P' Z' s > Q' Z' s') > Q Z s'))


71 
==> G{P}.c.{Q}"

8177

72 


73 

17477

74 
Skip: "G{P}. SKIP .{P}"

8177

75 

17477

76 
Ass: "G{%Z s. P Z (s[X::=a s])}. X:==a .{P}"

8177

77 

17477

78 
Local: "G{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])}


79 
==> G{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}"

8177

80 

17477

81 
Comp: "[ G{P}.c.{Q};


82 
G{Q}.d.{R} ]


83 
==> G{P}. (c;;d) .{R}"

8177

84 

17477

85 
If: "[ G{P &> b }.c.{Q};


86 
G{P &> (Not o b)}.d.{Q} ]


87 
==> G{P}. IF b THEN c ELSE d .{Q}"

8177

88 

17477

89 
Loop: "G{P &> b}.c.{P} ==>


90 
G{P}. WHILE b DO c .{P &> (Not o b)}"

8177

91 


92 
(*

17477

93 
BodyN: "(insert ({P}. BODY pn .{Q}) G)


94 
{P}. the (body pn) .{Q} ==>


95 
G{P}. BODY pn .{Q}"

8177

96 
*)

17477

97 
Body: "[ G Un (%p. {P p}. BODY p .{Q p})`Procs


98 
(%p. {P p}. the (body p) .{Q p})`Procs ]


99 
==> G(%p. {P p}. BODY p .{Q p})`Procs"

8177

100 

17477

101 
Call: "G{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])}


102 
==> G{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}.


103 
X:=CALL pn(a) .{Q}"


104 


105 
ML {* use_legacy_bindings (the_context ()) *}

8177

106 


107 
end
