1 (* Title: HOL/IMPP/Hoare.thy |
1 (* Title: HOL/IMPP/Hoare.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David von Oheimb |
3 Author: David von Oheimb |
4 Copyright 1999 TUM |
4 Copyright 1999 TUM |
5 |
|
6 Inductive definition of Hoare logic for partial correctness |
|
7 Completeness is taken relative to completeness of the underlying logic |
|
8 Two versions of completeness proof: |
|
9 nested single recursion vs. simultaneous recursion in call rule |
|
10 *) |
5 *) |
11 |
6 |
12 Hoare = Natural + |
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 *} |
13 |
19 |
14 types 'a assn = "'a => state => bool" |
20 types 'a assn = "'a => state => bool" |
15 translations |
21 translations |
16 "a assn" <= (type)"a => state => bool" |
22 "a assn" <= (type)"a => state => bool" |
17 |
23 |
18 constdefs |
24 constdefs |
19 state_not_singleton :: bool |
25 state_not_singleton :: bool |
20 "state_not_singleton == ? s t::state. s ~= t" (* at least two elements *) |
26 "state_not_singleton == \<exists>s t::state. s ~= t" (* at least two elements *) |
21 |
27 |
22 peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35) |
28 peek_and :: "'a assn => (state => bool) => 'a assn" (infixr "&>" 35) |
23 "peek_and P p == %Z s. P Z s & p s" |
29 "peek_and P p == %Z s. P Z s & p s" |
24 |
30 |
25 datatype 'a triple = |
31 datatype 'a triple = |
26 triple ('a assn) com ('a assn) ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58) |
32 triple "'a assn" com "'a assn" ("{(1_)}./ (_)/ .{(1_)}" [3,60,3] 58) |
27 |
33 |
28 consts |
34 consts |
29 triple_valid :: nat => 'a triple => bool ( "|=_:_" [0 , 58] 57) |
35 triple_valid :: "nat => 'a triple => bool" ( "|=_:_" [0 , 58] 57) |
30 hoare_valids :: 'a triple set => 'a triple set => bool ("_||=_" [58, 58] 57) |
36 hoare_valids :: "'a triple set => 'a triple set => bool" ("_||=_" [58, 58] 57) |
31 hoare_derivs ::"('a triple set * 'a triple set) set" |
37 hoare_derivs :: "('a triple set * 'a triple set) set" |
32 syntax |
38 syntax |
33 triples_valid:: nat => 'a triple set => bool ("||=_:_" [0 , 58] 57) |
39 triples_valid:: "nat => 'a triple set => bool" ("||=_:_" [0 , 58] 57) |
34 hoare_valid :: 'a triple set => 'a triple => bool ("_|=_" [58, 58] 57) |
40 hoare_valid :: "'a triple set => 'a triple => bool" ("_|=_" [58, 58] 57) |
35 "@hoare_derivs":: 'a triple set => 'a triple set => bool ("_||-_" [58, 58] 57) |
41 "@hoare_derivs":: "'a triple set => 'a triple set => bool" ("_||-_" [58, 58] 57) |
36 "@hoare_deriv" :: 'a triple set => 'a triple => bool ("_|-_" [58, 58] 57) |
42 "@hoare_deriv" :: "'a triple set => 'a triple => bool" ("_|-_" [58, 58] 57) |
37 |
43 |
38 defs triple_valid_def "|=n:t == case t of {P}.c.{Q} => |
44 defs triple_valid_def: "|=n:t == case t of {P}.c.{Q} => |
39 !Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s')" |
45 !Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s')" |
40 translations "||=n:G" == "Ball G (triple_valid n)" |
46 translations "||=n:G" == "Ball G (triple_valid n)" |
41 defs hoare_valids_def"G||=ts == !n. ||=n:G --> ||=n:ts" |
47 defs hoare_valids_def: "G||=ts == !n. ||=n:G --> ||=n:ts" |
42 translations "G |=t " == " G||={t}" |
48 translations "G |=t " == " G||={t}" |
43 "G||-ts" == "(G,ts) : hoare_derivs" |
49 "G||-ts" == "(G,ts) : hoare_derivs" |
44 "G |-t" == " G||-{t}" |
50 "G |-t" == " G||-{t}" |
45 |
51 |
46 (* Most General Triples *) |
52 (* Most General Triples *) |
47 constdefs MGT :: com => state triple ("{=}._.{->}" [60] 58) |
53 constdefs MGT :: "com => state triple" ("{=}._.{->}" [60] 58) |
48 "{=}.c.{->} == {%Z s0. Z = s0}. c .{%Z s1. <c,Z> -c-> s1}" |
54 "{=}.c.{->} == {%Z s0. Z = s0}. c .{%Z s1. <c,Z> -c-> s1}" |
49 |
55 |
50 inductive hoare_derivs intrs |
56 inductive hoare_derivs intros |
51 |
|
52 empty "G||-{}" |
|
53 insert"[| G |-t; G||-ts |] |
|
54 ==> G||-insert t ts" |
|
55 |
57 |
56 asm "ts <= G ==> |
58 empty: "G||-{}" |
57 G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *) |
59 insert: "[| G |-t; G||-ts |] |
|
60 ==> G||-insert t ts" |
58 |
61 |
59 cut "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *) |
62 asm: "ts <= G ==> |
|
63 G||-ts" (* {P}.BODY pn.{Q} instead of (general) t for SkipD_lemma *) |
60 |
64 |
61 weaken"[| G||-ts' ; ts <= ts' |] ==> G||-ts" |
65 cut: "[| G'||-ts; G||-G' |] ==> G||-ts" (* for convenience and efficiency *) |
62 |
66 |
63 conseq"!Z s. P Z s --> (? P' Q'. G|-{P'}.c.{Q'} & |
67 weaken: "[| G||-ts' ; ts <= ts' |] ==> G||-ts" |
64 (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s')) |
68 |
65 ==> G|-{P}.c.{Q}" |
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}" |
66 |
72 |
67 |
73 |
68 Skip "G|-{P}. SKIP .{P}" |
74 Skip: "G|-{P}. SKIP .{P}" |
69 |
75 |
70 Ass "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}" |
76 Ass: "G|-{%Z s. P Z (s[X::=a s])}. X:==a .{P}" |
71 |
77 |
72 Local "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])} |
78 Local: "G|-{P}. c .{%Z s. Q Z (s[Loc X::=s'<X>])} |
73 ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}" |
79 ==> G|-{%Z s. s'=s & P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}" |
74 |
80 |
75 Comp "[| G|-{P}.c.{Q}; |
81 Comp: "[| G|-{P}.c.{Q}; |
76 G|-{Q}.d.{R} |] |
82 G|-{Q}.d.{R} |] |
77 ==> G|-{P}. (c;;d) .{R}" |
83 ==> G|-{P}. (c;;d) .{R}" |
78 |
84 |
79 If "[| G|-{P &> b }.c.{Q}; |
85 If: "[| G|-{P &> b }.c.{Q}; |
80 G|-{P &> (Not o b)}.d.{Q} |] |
86 G|-{P &> (Not o b)}.d.{Q} |] |
81 ==> G|-{P}. IF b THEN c ELSE d .{Q}" |
87 ==> G|-{P}. IF b THEN c ELSE d .{Q}" |
82 |
88 |
83 Loop "G|-{P &> b}.c.{P} ==> |
89 Loop: "G|-{P &> b}.c.{P} ==> |
84 G|-{P}. WHILE b DO c .{P &> (Not o b)}" |
90 G|-{P}. WHILE b DO c .{P &> (Not o b)}" |
85 |
91 |
86 (* |
92 (* |
87 BodyN "(insert ({P}. BODY pn .{Q}) G) |
93 BodyN: "(insert ({P}. BODY pn .{Q}) G) |
88 |-{P}. the (body pn) .{Q} ==> |
94 |-{P}. the (body pn) .{Q} ==> |
89 G|-{P}. BODY pn .{Q}" |
95 G|-{P}. BODY pn .{Q}" |
90 *) |
96 *) |
91 Body "[| G Un (%p. {P p}. BODY p .{Q p})`Procs |
97 Body: "[| G Un (%p. {P p}. BODY p .{Q p})`Procs |
92 ||-(%p. {P p}. the (body p) .{Q p})`Procs |] |
98 ||-(%p. {P p}. the (body p) .{Q p})`Procs |] |
93 ==> G||-(%p. {P p}. BODY p .{Q p})`Procs" |
99 ==> G||-(%p. {P p}. BODY p .{Q p})`Procs" |
94 |
100 |
95 Call "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} |
101 Call: "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} |
96 ==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}. |
102 ==> G|-{%Z s. s'=s & P Z (setlocs s newlocs[Loc Arg::=a s])}. |
97 X:=CALL pn(a) .{Q}" |
103 X:=CALL pn(a) .{Q}" |
|
104 |
|
105 ML {* use_legacy_bindings (the_context ()) *} |
98 |
106 |
99 end |
107 end |