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