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