src/HOL/Isar_examples/Hoare.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 16417 9bc16273c2d4
child 18193 54419506df9e
permissions -rw-r--r--
Constant "If" is now local
     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 imports Main
    11 uses ("~~/src/HOL/Hoare/hoare.ML") begin
    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 (xsymbols)
    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   have "!!s. iter n b (Sem c) s s' ==> s : P ==> s' : P Int -b"
   170   proof (induct n)
   171     case (0 s)
   172     thus ?case by auto
   173   next
   174     case (Suc n s)
   175     then obtain s'' where b: "s : b" and sem: "Sem c s s''"
   176       and iter: "iter n b (Sem c) s'' s'"
   177       by auto
   178     from Suc and b have "s : P Int b" by simp
   179     with body sem have "s'' : P" ..
   180     with iter show ?case by (rule Suc)
   181   qed
   182   from this iter s show "s' : P Int -b" .
   183 qed
   184 
   185 
   186 subsection {* Concrete syntax for assertions *}
   187 
   188 text {*
   189  We now introduce concrete syntax for describing commands (with
   190  embedded expressions) and assertions. The basic technique is that of
   191  semantic ``quote-antiquote''.  A \emph{quotation} is a syntactic
   192  entity delimited by an implicit abstraction, say over the state
   193  space.  An \emph{antiquotation} is a marked expression within a
   194  quotation that refers the implicit argument; a typical antiquotation
   195  would select (or even update) components from the state.
   196 
   197  We will see some examples later in the concrete rules and
   198  applications.
   199 *}
   200 
   201 text {*
   202  The following specification of syntax and translations is for
   203  Isabelle experts only; feel free to ignore it.
   204 
   205  While the first part is still a somewhat intelligible specification
   206  of the concrete syntactic representation of our Hoare language, the
   207  actual ``ML drivers'' is quite involved.  Just note that the we
   208  re-use the basic quote/antiquote translations as already defined in
   209  Isabelle/Pure (see \verb,Syntax.quote_tr, and
   210  \verb,Syntax.quote_tr',).
   211 *}
   212 
   213 syntax
   214   "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)" [0] 1000)
   215   "_antiquote"   :: "('a => 'b) => 'b"       ("\<acute>_" [1000] 1000)
   216   "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"
   217         ("_[_'/\<acute>_]" [1000] 999)
   218   "_Assert"      :: "'a => 'a set"           ("(.{_}.)" [0] 1000)
   219   "_Assign"      :: "idt => 'b => 'a com"    ("(\<acute>_ :=/ _)" [70, 65] 61)
   220   "_Cond"        :: "'a bexp => 'a com => 'a com => 'a com"
   221         ("(0IF _/ THEN _/ ELSE _/ FI)" [0, 0, 0] 61)
   222   "_While_inv"   :: "'a bexp => 'a assn => 'a com => 'a com"
   223         ("(0WHILE _/ INV _ //DO _ /OD)"  [0, 0, 0] 61)
   224   "_While"       :: "'a bexp => 'a com => 'a com"
   225         ("(0WHILE _ //DO _ /OD)"  [0, 0] 61)
   226 
   227 syntax (xsymbols)
   228   "_Assert"      :: "'a => 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
   229 
   230 translations
   231   ".{b}."                   => "Collect .(b)."
   232   "B [a/\<acute>x]"                => ".{\<acute>(_update_name x a) \<in> B}."
   233   "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x a))."
   234   "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
   235   "WHILE b INV i DO c OD"   => "While .{b}. i c"
   236   "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"
   237 
   238 parse_translation {*
   239   let
   240     fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
   241       | quote_tr ts = raise TERM ("quote_tr", ts);
   242   in [("_quote", quote_tr)] end
   243 *}
   244 
   245 text {*
   246  As usual in Isabelle syntax translations, the part for printing is
   247  more complicated --- we cannot express parts as macro rules as above.
   248  Don't look here, unless you have to do similar things for yourself.
   249 *}
   250 
   251 print_translation {*
   252   let
   253     fun quote_tr' f (t :: ts) =
   254           Term.list_comb (f $ Syntax.quote_tr' "_antiquote" t, ts)
   255       | quote_tr' _ _ = raise Match;
   256 
   257     val assert_tr' = quote_tr' (Syntax.const "_Assert");
   258 
   259     fun bexp_tr' name ((Const ("Collect", _) $ t) :: ts) =
   260           quote_tr' (Syntax.const name) (t :: ts)
   261       | bexp_tr' _ _ = raise Match;
   262 
   263     fun upd_tr' (x_upd, T) =
   264       (case try (unsuffix RecordPackage.updateN) x_upd of
   265         SOME x => (x, if T = dummyT then T else Term.domain_type T)
   266       | NONE => raise Match);
   267 
   268     fun update_name_tr' (Free x) = Free (upd_tr' x)
   269       | update_name_tr' ((c as Const ("_free", _)) $ Free x) =
   270           c $ Free (upd_tr' x)
   271       | update_name_tr' (Const x) = Const (upd_tr' x)
   272       | update_name_tr' _ = raise Match;
   273 
   274     fun assign_tr' (Abs (x, _, f $ t $ Bound 0) :: ts) =
   275           quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
   276             (Abs (x, dummyT, t) :: ts)
   277       | assign_tr' _ = raise Match;
   278   in
   279     [("Collect", assert_tr'), ("Basic", assign_tr'),
   280       ("Cond", bexp_tr' "_Cond"), ("While", bexp_tr' "_While_inv")]
   281   end
   282 *}
   283 
   284 
   285 subsection {* Rules for single-step proof \label{sec:hoare-isar} *}
   286 
   287 text {*
   288  We are now ready to introduce a set of Hoare rules to be used in
   289  single-step structured proofs in Isabelle/Isar.  We refer to the
   290  concrete syntax introduce above.
   291 
   292  \medskip Assertions of Hoare Logic may be manipulated in
   293  calculational proofs, with the inclusion expressed in terms of sets
   294  or predicates.  Reversed order is supported as well.
   295 *}
   296 
   297 lemma [trans]: "|- P c Q ==> P' <= P ==> |- P' c Q"
   298   by (unfold Valid_def) blast
   299 lemma [trans] : "P' <= P ==> |- P c Q ==> |- P' c Q"
   300   by (unfold Valid_def) blast
   301 
   302 lemma [trans]: "Q <= Q' ==> |- P c Q ==> |- P c Q'"
   303   by (unfold Valid_def) blast
   304 lemma [trans]: "|- P c Q ==> Q <= Q' ==> |- P c Q'"
   305   by (unfold Valid_def) blast
   306 
   307 lemma [trans]:
   308     "|- .{\<acute>P}. c Q ==> (!!s. P' s --> P s) ==> |- .{\<acute>P'}. c Q"
   309   by (simp add: Valid_def)
   310 lemma [trans]:
   311     "(!!s. P' s --> P s) ==> |- .{\<acute>P}. c Q ==> |- .{\<acute>P'}. c Q"
   312   by (simp add: Valid_def)
   313 
   314 lemma [trans]:
   315     "|- P c .{\<acute>Q}. ==> (!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q'}."
   316   by (simp add: Valid_def)
   317 lemma [trans]:
   318     "(!!s. Q s --> Q' s) ==> |- P c .{\<acute>Q}. ==> |- P c .{\<acute>Q'}."
   319   by (simp add: Valid_def)
   320 
   321 
   322 text {*
   323  Identity and basic assignments.\footnote{The $\idt{hoare}$ method
   324  introduced in \S\ref{sec:hoare-vcg} is able to provide proper
   325  instances for any number of basic assignments, without producing
   326  additional verification conditions.}
   327 *}
   328 
   329 lemma skip [intro?]: "|- P SKIP P"
   330 proof -
   331   have "|- {s. id s : P} SKIP P" by (rule basic)
   332   thus ?thesis by simp
   333 qed
   334 
   335 lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"
   336   by (rule basic)
   337 
   338 text {*
   339  Note that above formulation of assignment corresponds to our
   340  preferred way to model state spaces, using (extensible) record types
   341  in HOL \cite{Naraschewski-Wenzel:1998:HOOL}.  For any record field
   342  $x$, Isabelle/HOL provides a functions $x$ (selector) and
   343  $\idt{x{\dsh}update}$ (update).  Above, there is only a place-holder
   344  appearing for the latter kind of function: due to concrete syntax
   345  \isa{\'x := \'a} also contains \isa{x\_update}.\footnote{Note that due
   346  to the external nature of HOL record fields, we could not even state
   347  a general theorem relating selector and update functions (if this
   348  were required here); this would only work for any particular instance
   349  of record fields introduced so far.}
   350 *}
   351 
   352 text {*
   353  Sequential composition --- normalizing with associativity achieves
   354  proper of chunks of code verified separately.
   355 *}
   356 
   357 lemmas [trans, intro?] = seq
   358 
   359 lemma seq_assoc [simp]: "( |- P c1;(c2;c3) Q) = ( |- P (c1;c2);c3 Q)"
   360   by (auto simp add: Valid_def)
   361 
   362 text {*
   363  Conditional statements.
   364 *}
   365 
   366 lemmas [trans, intro?] = cond
   367 
   368 lemma [trans, intro?]:
   369   "|- .{\<acute>P & \<acute>b}. c1 Q
   370       ==> |- .{\<acute>P & ~ \<acute>b}. c2 Q
   371       ==> |- .{\<acute>P}. IF \<acute>b THEN c1 ELSE c2 FI Q"
   372     by (rule cond) (simp_all add: Valid_def)
   373 
   374 text {*
   375  While statements --- with optional invariant.
   376 *}
   377 
   378 lemma [intro?]:
   379     "|- (P Int b) c P ==> |- P (While b P c) (P Int -b)"
   380   by (rule while)
   381 
   382 lemma [intro?]:
   383     "|- (P Int b) c P ==> |- P (While b arbitrary c) (P Int -b)"
   384   by (rule while)
   385 
   386 
   387 lemma [intro?]:
   388   "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
   389     ==> |- .{\<acute>P}. WHILE \<acute>b INV .{\<acute>P}. DO c OD .{\<acute>P & ~ \<acute>b}."
   390   by (simp add: while Collect_conj_eq Collect_neg_eq)
   391 
   392 lemma [intro?]:
   393   "|- .{\<acute>P & \<acute>b}. c .{\<acute>P}.
   394     ==> |- .{\<acute>P}. WHILE \<acute>b DO c OD .{\<acute>P & ~ \<acute>b}."
   395   by (simp add: while Collect_conj_eq Collect_neg_eq)
   396 
   397 
   398 subsection {* Verification conditions \label{sec:hoare-vcg} *}
   399 
   400 text {*
   401  We now load the \emph{original} ML file for proof scripts and tactic
   402  definition for the Hoare Verification Condition Generator (see
   403  \url{http://isabelle.in.tum.de/library/Hoare/}).  As far as we are
   404  concerned here, the result is a proof method \name{hoare}, which may
   405  be applied to a Hoare Logic assertion to extract purely logical
   406  verification conditions.  It is important to note that the method
   407  requires \texttt{WHILE} loops to be fully annotated with invariants
   408  beforehand.  Furthermore, only \emph{concrete} pieces of code are
   409  handled --- the underlying tactic fails ungracefully if supplied with
   410  meta-variables or parameters, for example.
   411 *}
   412 
   413 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
   414 by (auto simp:Valid_def)
   415 
   416 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
   417 by (auto simp:Valid_def)
   418 
   419 lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
   420 by (auto simp:Valid_def)
   421 
   422 lemma CondRule:
   423  "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
   424   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
   425 by (auto simp:Valid_def)
   426 
   427 lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
   428        (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)";
   429 apply(induct n)
   430  apply clarsimp
   431 apply(simp (no_asm_use))
   432 apply blast
   433 done
   434 
   435 lemma WhileRule:
   436  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
   437 apply (clarsimp simp:Valid_def)
   438 apply(drule iter_aux)
   439   prefer 2 apply assumption
   440  apply blast
   441 apply blast
   442 done
   443 
   444 
   445 ML {* val Valid_def = thm "Valid_def" *}
   446 use "~~/src/HOL/Hoare/hoare.ML"
   447 
   448 method_setup hoare = {*
   449   Method.no_args
   450     (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
   451   "verification condition generator for Hoare logic"
   452 
   453 end