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