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