src/HOL/Isar_examples/Hoare.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 18241 afdba6b3e383
child 19122 e1b6a5071348
permissions -rw-r--r--
adaptions to codegen_package
     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:
   164   assumes body: "|- (P Int b) c P"
   165   shows "|- P (While b X c) (P Int -b)"
   166 proof
   167   fix s s' assume s: "s : P"
   168   assume "Sem (While b X c) s s'"
   169   then obtain n where "iter n b (Sem c) s s'" by auto
   170   from this and s show "s' : P Int -b"
   171   proof (induct n fixing: s)
   172     case (0 s)
   173     thus ?case by auto
   174   next
   175     case (Suc n s)
   176     then obtain s'' where b: "s : b" and sem: "Sem c s s''"
   177       and iter: "iter n b (Sem c) s'' s'"
   178       by auto
   179     from Suc and b have "s : P Int b" by simp
   180     with body sem have "s'' : P" ..
   181     with iter show ?case by (rule Suc)
   182   qed
   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 add: 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:
   428   "\<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
   429        (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)"
   430   apply(induct n)
   431    apply clarsimp
   432    apply (simp (no_asm_use))
   433    apply blast
   434   done
   435 
   436 lemma WhileRule:
   437     "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
   438   apply (clarsimp simp: Valid_def)
   439   apply (drule iter_aux)
   440     prefer 2
   441     apply assumption
   442    apply blast
   443   apply blast
   444   done
   445 
   446 ML {* val Valid_def = thm "Valid_def" *}
   447 use "~~/src/HOL/Hoare/hoare.ML"
   448 
   449 method_setup hoare = {*
   450   Method.no_args
   451     (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
   452   "verification condition generator for Hoare logic"
   453 
   454 end