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

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

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

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

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