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