Gedichte
Musik
Bilder
Quellcodebibliothek
Diashow
Normaldarstellung
Quellcodebibliothek
Statistik
Leitseite
products
/
Sources
/
formale Sprachen
/
Isabelle
/
Tools
/
VSCode
/
extension
/
media
/ (
Beweissystem Isabelle
Version 2025-1
©
) Datei vom 16.11.2025 mit Größe 417 B
Bilddatei
Hoare.thy
products/sources/formale Sprachen/Isabelle/HOL/Isar_Examples/Hoare.thy
(* Title: HOL/Isar_Examples/Hoare.thy Author: Makarius A formulation of Hoare logic suitable for Isar. *) section \
Hoare Logic\
theory Hoare imports "HOL-Hoare.Hoare_Tac" begin subsection \
Abstract syntax and semantics\
text \
The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\
WHILE\
programs closely follows the existing tradition in Isabelle/HOL of formalizing the presentation given in \<^cite>\
\
\S6\
in "Winskel:1993"\
. See also \<^dir>\
~~/src/HOL/Hoare\
and \<^cite>\
"Nipkow:1998:Winskel"\
. \
type_synonym 'a bexp = "'a set" type_synonym 'a assn = "'a set" type_synonym 'a var = "'a \
nat" datatype 'a com = Basic "'a \
'a" | Seq "'a com" "'a com" (\
(_;/ _)\
[60, 61] 60) | Cond "'a bexp" "'a com" "'a com" | While "'a bexp" "'a assn" "'a var" "'a com" abbreviation Skip (\
SKIP\
) where "SKIP \
Basic id" type_synonym 'a sem = "'a \
'a \
bool" primrec iter :: "nat \
'a bexp \
'a sem \
'a sem" where "iter 0 b S s s' \
s \
b \
s = s'" | "iter (Suc n) b S s s' \
s \
b \
(\
s''. S s s'' \
iter n b S s'' s')" primrec Sem :: "'a com \
'a sem" where "Sem (Basic f) s s' \
s' = f s" | "Sem (c1; c2) s s' \
(\
s''. Sem c1 s s'' \
Sem c2 s'' s')" | "Sem (Cond b c1 c2) s s' \
(if s \
b then Sem c1 s s' else Sem c2 s s')" | "Sem (While b x y c) s s' \
(\
n. iter n b (Sem c) s s')" definition Valid :: "'a bexp \
'a com \
'a bexp \
bool" (\
(3\
_/ (2_)/ _)\
[100, 55, 100] 50) where "\
P c Q \
(\
s s'. Sem c s s' \
s \
P \
s' \
Q)" lemma ValidI [intro?]: "(\
s s'. Sem c s s' \
s \
P \
s' \
Q) \
\
P c Q" by (simp add: Valid_def) lemma ValidD [dest?]: "\
P c Q \
Sem c s s' \
s \
P \
s' \
Q" by (simp add: Valid_def) subsection \
Primitive Hoare rules\
text \
From the semantics defined above, we derive the standard set of primitive Hoare rules; e.g.\ see \<^cite>\
\
\S6\
in "Winskel:1993"\
. Usually, variant forms of these rules are applied in actual proof, see also \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}. \<^medskip> The \
basic\
rule represents any kind of atomic access to the state space. This subsumes the common rules of \
skip\
and \
assign\
, as formulated in \S\ref{sec:hoare-isar}. \
theorem basic: "\
{s. f s \
P} (Basic f) P" proof fix s s' assume s: "s \
{s. f s \
P}" assume "Sem (Basic f) s s'" then have "s' = f s" by simp with s show "s' \
P" by simp qed text \
The rules for sequential commands and semantic consequences are established in a straight forward manner as follows. \
theorem seq: "\
P c1 Q \
\
Q c2 R \
\
P (c1; c2) R" proof assume cmd1: "\
P c1 Q" and cmd2: "\
Q c2 R" fix s s' assume s: "s \
P" assume "Sem (c1; c2) s s'" then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'" by auto from cmd1 sem1 s have "s'' \
Q" .. with cmd2 sem2 show "s' \
R" .. qed theorem conseq: "P' \
P \
\
P c Q \
Q \
Q' \
\
P' c Q'" proof assume P'P: "P' \
P" and QQ': "Q \
Q'" assume cmd: "\
P c Q" fix s s' :: 'a assume sem: "Sem c s s'" assume "s \
P'" with P'P have "s \
P" .. with cmd sem have "s' \
Q" .. with QQ' show "s' \
Q'" .. qed text \
The rule for conditional commands is directly reflected by the corresponding semantics; in the proof we just have to look closely which cases apply. \
theorem cond: assumes case_b: "\
(P \
b) c1 Q" and case_nb: "\
(P \
-b) c2 Q" shows "\
P (Cond b c1 c2) Q" proof fix s s' assume s: "s \
P" assume sem: "Sem (Cond b c1 c2) s s'" show "s' \
Q" proof cases assume b: "s \
b" from case_b show ?thesis proof from sem b show "Sem c1 s s'" by simp from s b show "s \
P \
b" by simp qed next assume nb: "s \
b" from case_nb show ?thesis proof from sem nb show "Sem c2 s s'" by simp from s nb show "s \
P \
-b" by simp qed qed qed text \
The \
while\
rule is slightly less trivial --- it is the only one based on recursion, which is expressed in the semantics by a Kleene-style least fixed-point construction. The auxiliary statement below, which is by induction on the number of iterations is the main point to be proven; the rest is by routine application of the semantics of \<^verbatim>\
WHILE\
. \
theorem while: assumes body: "\
(P \
b) c P" shows "\
P (While b X Y c) (P \
-b)" proof fix s s' assume s: "s \
P" assume "Sem (While b X Y c) s s'" then obtain n where "iter n b (Sem c) s s'" by auto from this and s show "s' \
P \
-b" proof (induct n arbitrary: s) case 0 then show ?case by auto next case (Suc n) then obtain s'' where b: "s \
b" and sem: "Sem c s s''" and iter: "iter n b (Sem c) s'' s'" by auto from Suc and b have "s \
P \
b" by simp with body sem have "s'' \
P" .. with iter show ?case by (rule Suc) qed qed subsection \
Concrete syntax for assertions\
text \
We now introduce concrete syntax for describing commands (with embedded expressions) and assertions. The basic technique is that of semantic ``quote-antiquote''. A \<^emph>\
quotation\
is a syntactic entity delimited by an implicit abstraction, say over the state space. An \<^emph>\
antiquotation\
is a marked expression within a quotation that refers the implicit argument; a typical antiquotation would select (or even update) components from the state. We will see some examples later in the concrete rules and applications. \<^medskip> The following specification of syntax and translations is for Isabelle experts only; feel free to ignore it. While the first part is still a somewhat intelligible specification of the concrete syntactic representation of our Hoare language, the actual ``ML drivers'' is quite involved. Just note that the we re-use the basic quote/antiquote translations as already defined in Isabelle/Pure (see \<^ML>\
Syntax_Trans.quote_tr\
, and \<^ML>\
Syntax_Trans.quote_tr'\
,). \
syntax "_quote" :: "'b \
('a \
'b)" "_antiquote" :: "('a \
'b) \
'b" (\
\
_\
[1000] 1000) "_Subst" :: "'a bexp \
'b \
idt \
'a bexp" (\
_[_'/\
_]\
[1000] 999) "_Assert" :: "'a \
'a set" (\
(\
_\
)\
[0] 1000) "_Assign" :: "idt \
'b \
'a com" (\
(\
_ :=/ _)\
[70, 65] 61) "_Cond" :: "'a bexp \
'a com \
'a com \
'a com" (\
(0IF _/ THEN _/ ELSE _/ FI)\
[0, 0, 0] 61) "_While_inv" :: "'a bexp \
'a assn \
'a com \
'a com" (\
(0WHILE _/ INV _ //DO _ /OD)\
[0, 0, 0] 61) "_While" :: "'a bexp \
'a com \
'a com" (\
(0WHILE _ //DO _ /OD)\
[0, 0] 61) translations "\
b\
" \
"CONST Collect (_quote b)" "B [a/\
x]" \
"\
\
(_update_name x (\
_. a)) \
B\
" "\
x := a" \
"CONST Basic (_quote (\
(_update_name x (\
_. a))))" "IF b THEN c1 ELSE c2 FI" \
"CONST Cond \
b\
c1 c2" "WHILE b INV i DO c OD" \
"CONST While \
b\
i (\
_. 0) c" "WHILE b DO c OD" \
"WHILE b INV CONST undefined DO c OD" parse_translation \
let fun quote_tr [t] = Syntax_Trans.quote_tr \<^syntax_const>\
_antiquote\
t | quote_tr ts = raise TERM ("quote_tr", ts); in [(\<^syntax_const>\
_quote\
, K quote_tr)] end \
text \
As usual in Isabelle syntax translations, the part for printing is more complicated --- we cannot express parts as macro rules as above. Don't look here, unless you have to do similar things for yourself. \
print_translation \
let fun quote_tr' f (t :: ts) = Term.list_comb (f $ Syntax_Trans.quote_tr' \<^syntax_const>\
_antiquote\
t, ts) | quote_tr' _ _ = raise Match; val assert_tr' = quote_tr' (Syntax.const \<^syntax_const>\
_Assert\
); fun bexp_tr' name ((Const (\<^const_syntax>\
Collect\
, _) $ t) :: ts) = quote_tr' (Syntax.const name) (t :: ts) | bexp_tr' _ _ = raise Match; fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = quote_tr' (Syntax.const \<^syntax_const>\
_Assign\
$ Syntax_Trans.update_name_tr' f) (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) | assign_tr' _ = raise Match; in [(\<^const_syntax>\
Collect\
, K assert_tr'), (\<^const_syntax>\
Basic\
, K assign_tr'), (\<^const_syntax>\
Cond\
, K (bexp_tr' \<^syntax_const>\
_Cond\
)), (\<^const_syntax>\
While\
