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)"       ("(.'(_').)"  1000)

   221   "_antiquote"   :: "('a => 'b) => 'b"       ("\<acute>_"  1000)

   222   "_Subst"       :: "'a bexp \<Rightarrow> 'b \<Rightarrow> idt \<Rightarrow> 'a bexp"

   223         ("_[_'/\<acute>_]"  999)

   224   "_Assert"      :: "'a => 'a set"           ("(.{_}.)"  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>)"  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