14 |
14 |
15 text \<open> |
15 text \<open> |
16 The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\<open>WHILE\<close> |
16 The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\<open>WHILE\<close> |
17 programs closely follows the existing tradition in Isabelle/HOL of |
17 programs closely follows the existing tradition in Isabelle/HOL of |
18 formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See also |
18 formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See also |
19 @{dir "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}. |
19 \<^dir>\<open>~~/src/HOL/Hoare\<close> and @{cite "Nipkow:1998:Winskel"}. |
20 \<close> |
20 \<close> |
21 |
21 |
22 type_synonym 'a bexp = "'a set" |
22 type_synonym 'a bexp = "'a set" |
23 type_synonym 'a assn = "'a set" |
23 type_synonym 'a assn = "'a set" |
24 |
24 |
356 |
356 |
357 subsection \<open>Verification conditions \label{sec:hoare-vcg}\<close> |
357 subsection \<open>Verification conditions \label{sec:hoare-vcg}\<close> |
358 |
358 |
359 text \<open> |
359 text \<open> |
360 We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic definition |
360 We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic definition |
361 for the Hoare Verification Condition Generator (see @{dir |
361 for the Hoare Verification Condition Generator (see \<^dir>\<open>~~/src/HOL/Hoare\<close>). |
362 "~~/src/HOL/Hoare/"}). As far as we are concerned here, the result is a |
362 As far as we are concerned here, the result is a proof method \<open>hoare\<close>, which |
363 proof method \<open>hoare\<close>, which may be applied to a Hoare Logic assertion to |
363 may be applied to a Hoare Logic assertion to extract purely logical |
364 extract purely logical verification conditions. It is important to note that |
364 verification conditions. It is important to note that the method requires |
365 the method requires \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with invariants |
365 \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with invariants beforehand. |
366 beforehand. Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are handled --- the |
366 Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are handled --- the underlying |
367 underlying tactic fails ungracefully if supplied with meta-variables or |
367 tactic fails ungracefully if supplied with meta-variables or parameters, for |
368 parameters, for example. |
368 example. |
369 \<close> |
369 \<close> |
370 |
370 |
371 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q" |
371 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q" |
372 by (auto simp add: Valid_def) |
372 by (auto simp add: Valid_def) |
373 |
373 |