src/HOL/Isar_Examples/Hoare.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 58249 180f1b3508ed
child 58310 91ea607a34d8
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     1 (*  Title:      HOL/Isar_Examples/Hoare.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 
     4 A formulation of Hoare logic suitable for Isar.
     5 *)
     6 
     7 header {* Hoare Logic *}
     8 
     9 theory Hoare
    10 imports Main
    11 begin
    12 
    13 subsection {* Abstract syntax and semantics *}
    14 
    15 text {* The following abstract syntax and semantics of Hoare Logic
    16   over \texttt{WHILE} programs closely follows the existing tradition
    17   in Isabelle/HOL of formalizing the presentation given in
    18   \cite[\S6]{Winskel:1993}.  See also @{file "~~/src/HOL/Hoare"} and
    19   \cite{Nipkow:1998:Winskel}. *}
    20 
    21 type_synonym 'a bexp = "'a set"
    22 type_synonym 'a assn = "'a set"
    23 
    24 datatype_new 'a com =
    25     Basic "'a \<Rightarrow> 'a"
    26   | Seq "'a com" "'a com"    ("(_;/ _)" [60, 61] 60)
    27   | Cond "'a bexp" "'a com" "'a com"
    28   | While "'a bexp" "'a assn" "'a com"
    29 
    30 abbreviation Skip  ("SKIP")
    31   where "SKIP \<equiv> Basic id"
    32 
    33 type_synonym 'a sem = "'a \<Rightarrow> 'a \<Rightarrow> bool"
    34 
    35 primrec iter :: "nat \<Rightarrow> 'a bexp \<Rightarrow> 'a sem \<Rightarrow> 'a sem"
    36 where
    37   "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
    38 | "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
    39 
    40 primrec Sem :: "'a com \<Rightarrow> 'a sem"
    41 where
    42   "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
    43 | "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
    44 | "Sem (Cond b c1 c2) s s' \<longleftrightarrow>
    45     (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
    46 | "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
    47 
    48 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
    49     ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
    50   where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
    51 
    52 lemma ValidI [intro?]:
    53     "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
    54   by (simp add: Valid_def)
    55 
    56 lemma ValidD [dest?]:
    57     "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
    58   by (simp add: Valid_def)
    59 
    60 
    61 subsection {* Primitive Hoare rules *}
    62 
    63 text {* From the semantics defined above, we derive the standard set
    64   of primitive Hoare rules; e.g.\ see \cite[\S6]{Winskel:1993}.
    65   Usually, variant forms of these rules are applied in actual proof,
    66   see also \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}.
    67 
    68   \medskip The \name{basic} rule represents any kind of atomic access
    69   to the state space.  This subsumes the common rules of \name{skip}
    70   and \name{assign}, as formulated in \S\ref{sec:hoare-isar}. *}
    71 
    72 theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P"
    73 proof
    74   fix s s'
    75   assume s: "s \<in> {s. f s \<in> P}"
    76   assume "Sem (Basic f) s s'"
    77   then have "s' = f s" by simp
    78   with s show "s' \<in> P" by simp
    79 qed
    80 
    81 text {*
    82  The rules for sequential commands and semantic consequences are
    83  established in a straight forward manner as follows.
    84 *}
    85 
    86 theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R"
    87 proof
    88   assume cmd1: "\<turnstile> P c1 Q" and cmd2: "\<turnstile> Q c2 R"
    89   fix s s'
    90   assume s: "s \<in> P"
    91   assume "Sem (c1; c2) s s'"
    92   then obtain s'' where sem1: "Sem c1 s s''" and sem2: "Sem c2 s'' s'"
    93     by auto
    94   from cmd1 sem1 s have "s'' \<in> Q" ..
    95   with cmd2 sem2 show "s' \<in> R" ..
    96 qed
    97 
    98 theorem conseq: "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P' c Q'"
    99 proof
   100   assume P'P: "P' \<subseteq> P" and QQ': "Q \<subseteq> Q'"
   101   assume cmd: "\<turnstile> P c Q"
   102   fix s s' :: 'a
   103   assume sem: "Sem c s s'"
   104   assume "s : P'" with P'P have "s \<in> P" ..
   105   with cmd sem have "s' \<in> Q" ..
   106   with QQ' show "s' \<in> Q'" ..
   107 qed
   108 
   109 text {* The rule for conditional commands is directly reflected by the
   110   corresponding semantics; in the proof we just have to look closely
   111   which cases apply. *}
   112 
   113 theorem cond:
   114   assumes case_b: "\<turnstile> (P \<inter> b) c1 Q"
   115     and case_nb: "\<turnstile> (P \<inter> -b) c2 Q"
   116   shows "\<turnstile> P (Cond b c1 c2) Q"
   117 proof
   118   fix s s'
   119   assume s: "s \<in> P"
   120   assume sem: "Sem (Cond b c1 c2) s s'"
   121   show "s' \<in> Q"
   122   proof cases
   123     assume b: "s \<in> b"
   124     from case_b show ?thesis
   125     proof
   126       from sem b show "Sem c1 s s'" by simp
   127       from s b show "s \<in> P \<inter> b" by simp
   128     qed
   129   next
   130     assume nb: "s \<notin> b"
   131     from case_nb show ?thesis
   132     proof
   133       from sem nb show "Sem c2 s s'" by simp
   134       from s nb show "s : P \<inter> -b" by simp
   135     qed
   136   qed
   137 qed
   138 
   139 text {* The @{text while} rule is slightly less trivial --- it is the
   140   only one based on recursion, which is expressed in the semantics by
   141   a Kleene-style least fixed-point construction.  The auxiliary
   142   statement below, which is by induction on the number of iterations
   143   is the main point to be proven; the rest is by routine application
   144   of the semantics of \texttt{WHILE}. *}
   145 
   146 theorem while:
   147   assumes body: "\<turnstile> (P \<inter> b) c P"
   148   shows "\<turnstile> P (While b X c) (P \<inter> -b)"
   149 proof
   150   fix s s' assume s: "s \<in> P"
   151   assume "Sem (While b X c) s s'"
   152   then obtain n where "iter n b (Sem c) s s'" by auto
   153   from this and s show "s' \<in> P \<inter> -b"
   154   proof (induct n arbitrary: s)
   155     case 0
   156     then show ?case by auto
   157   next
   158     case (Suc n)
   159     then obtain s'' where b: "s \<in> b" and sem: "Sem c s s''"
   160       and iter: "iter n b (Sem c) s'' s'" by auto
   161     from Suc and b have "s \<in> P \<inter> b" by simp
   162     with body sem have "s'' \<in> P" ..
   163     with iter show ?case by (rule Suc)
   164   qed
   165 qed
   166 
   167 
   168 subsection {* Concrete syntax for assertions *}
   169 
   170 text {* We now introduce concrete syntax for describing commands (with
   171   embedded expressions) and assertions. The basic technique is that of
   172   semantic ``quote-antiquote''.  A \emph{quotation} is a syntactic
   173   entity delimited by an implicit abstraction, say over the state
   174   space.  An \emph{antiquotation} is a marked expression within a
   175   quotation that refers the implicit argument; a typical antiquotation
   176   would select (or even update) components from the state.
   177 
   178   We will see some examples later in the concrete rules and
   179   applications. *}
   180 
   181 text {* The following specification of syntax and translations is for
   182   Isabelle experts only; feel free to ignore it.
   183 
   184   While the first part is still a somewhat intelligible specification
   185   of the concrete syntactic representation of our Hoare language, the
   186   actual ``ML drivers'' is quite involved.  Just note that the we
   187   re-use the basic quote/antiquote translations as already defined in
   188   Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and
   189   @{ML Syntax_Trans.quote_tr'},). *}
   190 
   191 syntax
   192   "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"
   193   "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"  ("\<acute>_" [1000] 1000)
   194   "_Subst" :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"  ("_[_'/\<acute>_]" [1000] 999)
   195   "_Assert" :: "'a \<Rightarrow> 'a set"  ("(\<lbrace>_\<rbrace>)" [0] 1000)
   196   "_Assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'a com"  ("(\<acute>_ :=/ _)" [70, 65] 61)
   197   "_Cond" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com \<Rightarrow> 'a com"
   198     ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
   199   "_While_inv" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"
   200     ("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)
   201   "_While" :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)
   202 
   203 translations
   204   "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect (_quote b)"
   205   "B [a/\<acute>x]" \<rightharpoonup> "\<lbrace>\<acute>(_update_name x (\<lambda>_. a)) \<in> B\<rbrace>"
   206   "\<acute>x := a" \<rightharpoonup> "CONST Basic (_quote (\<acute>(_update_name x (\<lambda>_. a))))"
   207   "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "CONST Cond \<lbrace>b\<rbrace> c1 c2"
   208   "WHILE b INV i DO c OD" \<rightharpoonup> "CONST While \<lbrace>b\<rbrace> i c"
   209   "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
   210 
   211 parse_translation {*
   212   let
   213     fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
   214       | quote_tr ts = raise TERM ("quote_tr", ts);
   215   in [(@{syntax_const "_quote"}, K quote_tr)] end
   216 *}
   217 
   218 text {* As usual in Isabelle syntax translations, the part for
   219   printing is more complicated --- we cannot express parts as macro
   220   rules as above.  Don't look here, unless you have to do similar
   221   things for yourself. *}
   222 
   223 print_translation {*
   224   let
   225     fun quote_tr' f (t :: ts) =
   226           Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
   227       | quote_tr' _ _ = raise Match;
   228 
   229     val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
   230 
   231     fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) =
   232           quote_tr' (Syntax.const name) (t :: ts)
   233       | bexp_tr' _ _ = raise Match;
   234 
   235     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
   236           quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
   237             (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
   238       | assign_tr' _ = raise Match;
   239   in
   240    [(@{const_syntax Collect}, K assert_tr'),
   241     (@{const_syntax Basic}, K assign_tr'),
   242     (@{const_syntax Cond}, K (bexp_tr' @{syntax_const "_Cond"})),
   243     (@{const_syntax While}, K (bexp_tr' @{syntax_const "_While_inv"}))]
   244   end
   245 *}
   246 
   247 
   248 subsection {* Rules for single-step proof \label{sec:hoare-isar} *}
   249 
   250 text {* We are now ready to introduce a set of Hoare rules to be used
   251   in single-step structured proofs in Isabelle/Isar.  We refer to the
   252   concrete syntax introduce above.
   253 
   254   \medskip Assertions of Hoare Logic may be manipulated in
   255   calculational proofs, with the inclusion expressed in terms of sets
   256   or predicates.  Reversed order is supported as well. *}
   257 
   258 lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q"
   259   by (unfold Valid_def) blast
   260 lemma [trans] : "P' \<subseteq> P \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P' c Q"
   261   by (unfold Valid_def) blast
   262 
   263 lemma [trans]: "Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q \<Longrightarrow> \<turnstile> P c Q'"
   264   by (unfold Valid_def) blast
   265 lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> Q \<subseteq> Q' \<Longrightarrow> \<turnstile> P c Q'"
   266   by (unfold Valid_def) blast
   267 
   268 lemma [trans]:
   269     "\<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> (\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
   270   by (simp add: Valid_def)
   271 lemma [trans]:
   272     "(\<And>s. P' s \<longrightarrow> P s) \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> c Q \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P'\<rbrace> c Q"
   273   by (simp add: Valid_def)
   274 
   275 lemma [trans]:
   276     "\<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> (\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
   277   by (simp add: Valid_def)
   278 lemma [trans]:
   279     "(\<And>s. Q s \<longrightarrow> Q' s) \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q\<rbrace> \<Longrightarrow> \<turnstile> P c \<lbrace>\<acute>Q'\<rbrace>"
   280   by (simp add: Valid_def)
   281 
   282 
   283 text {* Identity and basic assignments.\footnote{The $\idt{hoare}$
   284   method introduced in \S\ref{sec:hoare-vcg} is able to provide proper
   285   instances for any number of basic assignments, without producing
   286   additional verification conditions.} *}
   287 
   288 lemma skip [intro?]: "\<turnstile> P SKIP P"
   289 proof -
   290   have "\<turnstile> {s. id s \<in> P} SKIP P" by (rule basic)
   291   then show ?thesis by simp
   292 qed
   293 
   294 lemma assign: "\<turnstile> P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
   295   by (rule basic)
   296 
   297 text {* Note that above formulation of assignment corresponds to our
   298   preferred way to model state spaces, using (extensible) record types
   299   in HOL \cite{Naraschewski-Wenzel:1998:HOOL}.  For any record field
   300   $x$, Isabelle/HOL provides a functions $x$ (selector) and
   301   $\idt{x{\dsh}update}$ (update).  Above, there is only a place-holder
   302   appearing for the latter kind of function: due to concrete syntax
   303   \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that
   304   due to the external nature of HOL record fields, we could not even
   305   state a general theorem relating selector and update functions (if
   306   this were required here); this would only work for any particular
   307   instance of record fields introduced so far.} *}
   308 
   309 text {* Sequential composition --- normalizing with associativity
   310   achieves proper of chunks of code verified separately. *}
   311 
   312 lemmas [trans, intro?] = seq
   313 
   314 lemma seq_assoc [simp]: "\<turnstile> P c1;(c2;c3) Q \<longleftrightarrow> \<turnstile> P (c1;c2);c3 Q"
   315   by (auto simp add: Valid_def)
   316 
   317 text {* Conditional statements. *}
   318 
   319 lemmas [trans, intro?] = cond
   320 
   321 lemma [trans, intro?]:
   322   "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c1 Q
   323       \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace> c2 Q
   324       \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> IF \<acute>b THEN c1 ELSE c2 FI Q"
   325     by (rule cond) (simp_all add: Valid_def)
   326 
   327 text {* While statements --- with optional invariant. *}
   328 
   329 lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b P c) (P \<inter> -b)"
   330   by (rule while)
   331 
   332 lemma [intro?]: "\<turnstile> (P \<inter> b) c P \<Longrightarrow> \<turnstile> P (While b undefined c) (P \<inter> -b)"
   333   by (rule while)
   334 
   335 
   336 lemma [intro?]:
   337   "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
   338     \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b INV \<lbrace>\<acute>P\<rbrace> DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
   339   by (simp add: while Collect_conj_eq Collect_neg_eq)
   340 
   341 lemma [intro?]:
   342   "\<turnstile> \<lbrace>\<acute>P \<and> \<acute>b\<rbrace> c \<lbrace>\<acute>P\<rbrace>
   343     \<Longrightarrow> \<turnstile> \<lbrace>\<acute>P\<rbrace> WHILE \<acute>b DO c OD \<lbrace>\<acute>P \<and> \<not> \<acute>b\<rbrace>"
   344   by (simp add: while Collect_conj_eq Collect_neg_eq)
   345 
   346 
   347 subsection {* Verification conditions \label{sec:hoare-vcg} *}
   348 
   349 text {* We now load the \emph{original} ML file for proof scripts and
   350   tactic definition for the Hoare Verification Condition Generator
   351   (see @{file "~~/src/HOL/Hoare/"}).  As far as we
   352   are concerned here, the result is a proof method \name{hoare}, which
   353   may be applied to a Hoare Logic assertion to extract purely logical
   354   verification conditions.  It is important to note that the method
   355   requires \texttt{WHILE} loops to be fully annotated with invariants
   356   beforehand.  Furthermore, only \emph{concrete} pieces of code are
   357   handled --- the underlying tactic fails ungracefully if supplied
   358   with meta-variables or parameters, for example. *}
   359 
   360 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
   361   by (auto simp add: Valid_def)
   362 
   363 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
   364   by (auto simp: Valid_def)
   365 
   366 lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
   367   by (auto simp: Valid_def)
   368 
   369 lemma CondRule:
   370   "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
   371     \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
   372   by (auto simp: Valid_def)
   373 
   374 lemma iter_aux:
   375   "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
   376        (\<And>s s'. s \<in> I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> I \<and> s' \<notin> b)"
   377   by (induct n) auto
   378 
   379 lemma WhileRule:
   380     "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
   381   apply (clarsimp simp: Valid_def)
   382   apply (drule iter_aux)
   383     prefer 2
   384     apply assumption
   385    apply blast
   386   apply blast
   387   done
   388 
   389 lemma Compl_Collect: "- Collect b = {x. \<not> b x}"
   390   by blast
   391 
   392 lemmas AbortRule = SkipRule  -- "dummy version"
   393 
   394 ML_file "~~/src/HOL/Hoare/hoare_tac.ML"
   395 
   396 method_setup hoare = {*
   397   Scan.succeed (fn ctxt =>
   398     (SIMPLE_METHOD'
   399        (Hoare.hoare_tac ctxt
   400         (simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm "Record.K_record_comp"}] ))))) *}
   401   "verification condition generator for Hoare logic"
   402 
   403 end