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