(* Title: HOL/IMPP/Hoare.thy ID: $Id: Hoare.thy,v 1.3 2005/09/17 18:14:30 wenzelm Exp $ Author: David von Oheimb Copyright 1999 TUM *) header {* Inductive definition of Hoare logic for partial correctness *} theory Hoare imports Natural begin text {* Completeness is taken relative to completeness of the underlying logic. Two versions of completeness proof: nested single recursion vs. simultaneous recursion in call rule *} types 'a assn = "'a => state => bool" translations "a assn" <= (type)"a => state => bool" constdefs state_not_singleton :: bool "state_not_singleton == ∃s t::state. s ~= t" (* at least two elements *) 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 *) constdefs MGT :: "com => state triple" ("{=}._.{->}" [60] 58) "{=}.c.{->} == {%Z s0. Z = s0}. c .{%Z s1. <c,Z> -c-> s1}" inductive hoare_derivs intros empty: "G||-{}" insert: "[| G |-t; G||-ts |] ==> G||-insert t ts" 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}" 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}" Loop: "G|-{P &> b}.c.{P} ==> G|-{P}. WHILE b DO c .{P &> (Not o b)}" (* BodyN: "(insert ({P}. BODY pn .{Q}) G) |-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}" *) Body: "[| G Un (%p. {P p}. BODY p .{Q p})`Procs ||-(%p. {P p}. the (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}" ML {* use_legacy_bindings (the_context ()) *} end
theorem single_stateE:
state_not_singleton ==> ∀t. (∀s. s = t) --> False
theorem triple_valid_def2:
|=n:{P}. c .{Q} = (∀Z s. P Z s --> (∀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}. the (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'}; ∀Z s. P Z s --> (∀s'. (∀Z'. P' Z' s --> Q' Z' s') --> Q Z s') |] ==> G|-{P}. c .{Q}
theorem conseq1:
[| G|-{P'}. c .{Q}; ∀Z s. P Z s --> P' Z s |] ==> G|-{P}. c .{Q}
theorem conseq2:
[| G|-{P}. c .{Q'}; ∀Z s. Q' Z s --> Q Z s |] ==> G|-{P}. c .{Q}
theorem Body1:
[| G ∪ (%p. {P p}. BODY p .{Q p}) ` Procs||-(%p. {P p}. the (body p) .{Q p}) ` Procs; pn ∈ Procs |] ==> G|-{P pn}. BODY pn .{Q pn}
theorem BodyN:
insert ({P}. BODY pn .{Q}) G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}
theorem escape:
∀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}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}
theorem derivs_insertD:
G||-insert t ts ==> G|-t ∧ G||-ts
theorem finite_pointwise:
[| finite U; ∀p. G|-{P' p}. c0.0 p .{Q' p} --> G|-{P p}. c0.0 p .{Q p}; G||-(%p. {P' p}. c0.0 p .{Q' p}) ` U |] ==> G||-(%p. {P p}. c0.0 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 ∪ (%pn. {P pn}. BODY pn .{Q pn}) ` Procs||=(%pn. {P pn}. the (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|-{=}.c.{->} ==> G|-{%Z s0. ∀s1. <c,s0> -c-> s1 --> Z = s1}. c .{op =}
theorem MGT_alternD:
[| state_not_singleton; G|-{%Z s0. ∀s1. <c,s0> -c-> s1 --> Z = s1}. c .{op =} |] ==> G|-{=}.c.{->}
theorem MGF_complete:
[| {}|-{=}.c.{->}; {}|={P}. c .{Q} |] ==> {}|-{P}. c .{Q}
theorem MGF_lemma1:
[| state_not_singleton; ∀pn∈dom body. G|-{=}.BODY pn.{->}; WT c |] ==> G|-{=}.c.{->}
theorem nesting_lemma:
[| !!G ts. ts ⊆ G ==> P G ts; !!G pn. P (insert (mgt_call pn) G) {mgt (the (body pn))} ==> P G {mgt_call pn}; !!G c. [| wt c; ∀pn∈U. P G {mgt_call pn} |] ==> P G {mgt c}; !!pn. pn ∈ U ==> wt (the (body pn)); finite U; uG = mgt_call ` U; G ⊆ uG; n ≤ card uG; card G = card uG - n; wt c |] ==> P G {mgt c}
theorem MGT_BodyN:
insert ({=}.BODY pn.{->}) G|-{=}.the (body pn).{->} ==> G|-{=}.BODY pn.{->}
theorem MGF:
[| state_not_singleton; WT_bodies; WT c |] ==> {}|-{=}.c.{->}
theorem MGT_Body:
[| G ∪ (%pn. {=}.BODY pn.{->}) ` Procs||-(%pn. {=}.the (body pn).{->}) ` Procs; finite Procs |] ==> G||-(%pn. {=}.BODY pn.{->}) ` Procs
theorem MGF_lemma2_simult:
[| state_not_singleton; WT_bodies; F ⊆ (%pn. {=}.the (body pn).{->}) ` dom body |] ==> (%pn. {=}.BODY pn.{->}) ` dom body||-F
theorem MGF':
[| state_not_singleton; WT_bodies; WT c |] ==> {}|-{=}.c.{->}
theorem hoare_complete:
[| state_not_singleton; WT_bodies; WT c; {}|={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:
∀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 weak_Local:
[| G|-{P}. c .{Q}; ∀k Z s. Q Z s --> Q Z (s[Loc Y::=k]) |] ==> G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{Q}