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