src/HOL/Isar_examples/HoareEx.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21226 a607ae87ee81
child 25706 45d090186bbe
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
wenzelm@10148
     1
wenzelm@10148
     2
header {* Using Hoare Logic *}
wenzelm@10148
     3
haftmann@16417
     4
theory HoareEx imports Hoare begin
wenzelm@10148
     5
wenzelm@10148
     6
subsection {* State spaces *}
wenzelm@10148
     7
wenzelm@10148
     8
text {*
wenzelm@10148
     9
 First of all we provide a store of program variables that
wenzelm@10148
    10
 occur in any of the programs considered later.  Slightly unexpected
wenzelm@10148
    11
 things may happen when attempting to work with undeclared variables.
wenzelm@10148
    12
*}
wenzelm@10148
    13
wenzelm@10148
    14
record vars =
wenzelm@10148
    15
  I :: nat
wenzelm@10148
    16
  M :: nat
wenzelm@10148
    17
  N :: nat
wenzelm@10148
    18
  S :: nat
wenzelm@10148
    19
wenzelm@10148
    20
text {*
wenzelm@10148
    21
 While all of our variables happen to have the same type, nothing
wenzelm@10148
    22
 would prevent us from working with many-sorted programs as well, or
wenzelm@10148
    23
 even polymorphic ones.  Also note that Isabelle/HOL's extensible
wenzelm@10148
    24
 record types even provides simple means to extend the state space
wenzelm@10148
    25
 later.
wenzelm@10148
    26
*}
wenzelm@10148
    27
wenzelm@10148
    28
wenzelm@10148
    29
subsection {* Basic examples *}
wenzelm@10148
    30
wenzelm@10148
    31
text {*
wenzelm@10148
    32
 We look at few trivialities involving assignment and sequential
wenzelm@10148
    33
 composition, in order to get an idea of how to work with our
wenzelm@10148
    34
 formulation of Hoare Logic.
wenzelm@10148
    35
*}
wenzelm@10148
    36
wenzelm@10148
    37
text {*
wenzelm@10148
    38
 Using the basic \name{assign} rule directly is a bit cumbersome.
wenzelm@10148
    39
*}
wenzelm@10148
    40
wenzelm@10148
    41
lemma
schirmer@21226
    42
  "|- .{\<acute>(N_update (K_record (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
wenzelm@10148
    43
  by (rule assign)
wenzelm@10148
    44
wenzelm@10148
    45
text {*
wenzelm@10148
    46
 Certainly we want the state modification already done, e.g.\ by
wenzelm@10148
    47
 simplification.  The \name{hoare} method performs the basic state
wenzelm@10148
    48
 update for us; we may apply the Simplifier afterwards to achieve
wenzelm@10148
    49
 ``obvious'' consequences as well.
wenzelm@10148
    50
*}
wenzelm@10148
    51
wenzelm@11704
    52
lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."
wenzelm@10148
    53
  by hoare
wenzelm@10148
    54
wenzelm@11704
    55
lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
wenzelm@10148
    56
  by hoare
wenzelm@10148
    57
wenzelm@11704
    58
lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."
wenzelm@10148
    59
  by hoare simp
wenzelm@10148
    60
wenzelm@10838
    61
lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
wenzelm@10148
    62
  by hoare
wenzelm@10148
    63
wenzelm@10838
    64
lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
wenzelm@10148
    65
  by hoare simp
wenzelm@10148
    66
wenzelm@10838
    67
lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
wenzelm@10148
    68
  by hoare
wenzelm@10148
    69
wenzelm@10838
    70
lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."
wenzelm@10148
    71
  by hoare simp
wenzelm@10148
    72
wenzelm@10148
    73
lemma
wenzelm@10838
    74
"|- .{\<acute>M = a & \<acute>N = b}.
wenzelm@10838
    75
    \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I
wenzelm@10838
    76
    .{\<acute>M = b & \<acute>N = a}."
wenzelm@10148
    77
  by hoare simp
wenzelm@10148
    78
wenzelm@10148
    79
text {*
wenzelm@10148
    80
 It is important to note that statements like the following one can
wenzelm@10148
    81
 only be proven for each individual program variable.  Due to the
wenzelm@10148
    82
 extra-logical nature of record fields, we cannot formulate a theorem
wenzelm@10148
    83
 relating record selectors and updates schematically.
wenzelm@10148
    84
*}
wenzelm@10148
    85
wenzelm@10838
    86
lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."
wenzelm@10148
    87
  by hoare
wenzelm@10148
    88
wenzelm@10838
    89
lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}."
wenzelm@10148
    90
  oops
wenzelm@10148
    91
wenzelm@10148
    92
lemma
wenzelm@10148
    93
  "Valid {s. x s = a} (Basic (\<lambda>s. x_update (x s) s)) {s. x s = n}"
wenzelm@10148
    94
  -- {* same statement without concrete syntax *}
wenzelm@10148
    95
  oops
wenzelm@10148
    96
wenzelm@10148
    97
wenzelm@10148
    98
text {*
wenzelm@10148
    99
 In the following assignments we make use of the consequence rule in
wenzelm@10148
   100
 order to achieve the intended precondition.  Certainly, the
wenzelm@10148
   101
 \name{hoare} method is able to handle this case, too.
wenzelm@10148
   102
*}
wenzelm@10148
   103
wenzelm@10838
   104
lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
wenzelm@10148
   105
proof -
wenzelm@10838
   106
  have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}."
wenzelm@10148
   107
    by auto
wenzelm@10838
   108
  also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
wenzelm@10148
   109
    by hoare
wenzelm@10148
   110
  finally show ?thesis .
wenzelm@10148
   111
qed
wenzelm@10148
   112
wenzelm@10838
   113
lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
wenzelm@10148
   114
proof -
wenzelm@11701
   115
  have "!!m n::nat. m = n --> m + 1 ~= n"
wenzelm@10148
   116
      -- {* inclusion of assertions expressed in ``pure'' logic, *}
wenzelm@10148
   117
      -- {* without mentioning the state space *}
wenzelm@10148
   118
    by simp
wenzelm@10838
   119
  also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
wenzelm@10148
   120
    by hoare
wenzelm@10148
   121
  finally show ?thesis .
wenzelm@10148
   122
qed
wenzelm@10148
   123
wenzelm@10838
   124
lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
wenzelm@10148
   125
  by hoare simp
wenzelm@10148
   126
wenzelm@10148
   127
wenzelm@10148
   128
subsection {* Multiplication by addition *}
wenzelm@10148
   129
wenzelm@10148
   130
text {*
wenzelm@10148
   131
 We now do some basic examples of actual \texttt{WHILE} programs.
wenzelm@10148
   132
 This one is a loop for calculating the product of two natural
wenzelm@10148
   133
 numbers, by iterated addition.  We first give detailed structured
wenzelm@10148
   134
 proof based on single-step Hoare rules.
wenzelm@10148
   135
*}
wenzelm@10148
   136
wenzelm@10148
   137
lemma
wenzelm@10838
   138
  "|- .{\<acute>M = 0 & \<acute>S = 0}.
wenzelm@10838
   139
      WHILE \<acute>M ~= a
wenzelm@10838
   140
      DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
wenzelm@10838
   141
      .{\<acute>S = a * b}."
wenzelm@10148
   142
proof -
wenzelm@10148
   143
  let "|- _ ?while _" = ?thesis
wenzelm@10838
   144
  let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}."
wenzelm@10148
   145
wenzelm@10838
   146
  have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto
wenzelm@10838
   147
  also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}."
wenzelm@10148
   148
  proof
wenzelm@10838
   149
    let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1"
wenzelm@10838
   150
    have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}."
wenzelm@10148
   151
      by auto
wenzelm@10838
   152
    also have "|- ... ?c .{\<acute>?inv}." by hoare
wenzelm@10838
   153
    finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." .
wenzelm@10148
   154
  qed
wenzelm@10838
   155
  also have "... <= .{\<acute>S = a * b}." by auto
wenzelm@10148
   156
  finally show ?thesis .
wenzelm@10148
   157
qed
wenzelm@10148
   158
wenzelm@10148
   159
text {*
wenzelm@10148
   160
 The subsequent version of the proof applies the \name{hoare} method
wenzelm@10148
   161
 to reduce the Hoare statement to a purely logical problem that can be
wenzelm@10148
   162
 solved fully automatically.  Note that we have to specify the
wenzelm@10148
   163
 \texttt{WHILE} loop invariant in the original statement.
wenzelm@10148
   164
*}
wenzelm@10148
   165
wenzelm@10148
   166
lemma
wenzelm@10838
   167
  "|- .{\<acute>M = 0 & \<acute>S = 0}.
wenzelm@10838
   168
      WHILE \<acute>M ~= a
wenzelm@10838
   169
      INV .{\<acute>S = \<acute>M * b}.
wenzelm@10838
   170
      DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD
wenzelm@10838
   171
      .{\<acute>S = a * b}."
wenzelm@10148
   172
  by hoare auto
wenzelm@10148
   173
wenzelm@10148
   174
wenzelm@10148
   175
subsection {* Summing natural numbers *}
wenzelm@10148
   176
wenzelm@10148
   177
text {*
wenzelm@10148
   178
 We verify an imperative program to sum natural numbers up to a given
wenzelm@10148
   179
 limit.  First some functional definition for proper specification of
wenzelm@10148
   180
 the problem.
wenzelm@10148
   181
*}
wenzelm@10148
   182
wenzelm@10148
   183
text {*
wenzelm@10148
   184
 The following proof is quite explicit in the individual steps taken,
wenzelm@10148
   185
 with the \name{hoare} method only applied locally to take care of
wenzelm@10148
   186
 assignment and sequential composition.  Note that we express
wenzelm@10148
   187
 intermediate proof obligation in pure logic, without referring to the
wenzelm@10148
   188
 state space.
wenzelm@10148
   189
*}
wenzelm@10148
   190
nipkow@15912
   191
declare atLeast0LessThan[symmetric,simp]
nipkow@15569
   192
wenzelm@10148
   193
theorem
wenzelm@10148
   194
  "|- .{True}.
wenzelm@10838
   195
      \<acute>S := 0; \<acute>I := 1;
wenzelm@10838
   196
      WHILE \<acute>I ~= n
wenzelm@10148
   197
      DO
wenzelm@10838
   198
        \<acute>S := \<acute>S + \<acute>I;
wenzelm@10838
   199
        \<acute>I := \<acute>I + 1
wenzelm@10148
   200
      OD
wenzelm@10838
   201
      .{\<acute>S = (SUM j<n. j)}."
wenzelm@10148
   202
  (is "|- _ (_; ?while) _")
wenzelm@10148
   203
proof -
nipkow@15049
   204
  let ?sum = "\<lambda>k::nat. SUM j<k. j"
nipkow@15049
   205
  let ?inv = "\<lambda>s i::nat. s = ?sum i"
wenzelm@10148
   206
wenzelm@10838
   207
  have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
wenzelm@10148
   208
  proof -
wenzelm@10148
   209
    have "True --> 0 = ?sum 1"
wenzelm@10148
   210
      by simp
wenzelm@10838
   211
    also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."
wenzelm@10148
   212
      by hoare
wenzelm@10148
   213
    finally show ?thesis .
wenzelm@10148
   214
  qed
wenzelm@10838
   215
  also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}."
wenzelm@10148
   216
  proof
wenzelm@10838
   217
    let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
wenzelm@10148
   218
    have "!!s i. ?inv s i & i ~= n -->  ?inv (s + i) (i + 1)"
wenzelm@10148
   219
      by simp
wenzelm@10838
   220
    also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}."
wenzelm@10148
   221
      by hoare
wenzelm@10838
   222
    finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." .
wenzelm@10148
   223
  qed
wenzelm@10148
   224
  also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n"
wenzelm@10148
   225
    by simp
wenzelm@10148
   226
  finally show ?thesis .
wenzelm@10148
   227
qed
wenzelm@10148
   228
wenzelm@10148
   229
text {*
wenzelm@10148
   230
 The next version uses the \name{hoare} method, while still explaining
wenzelm@10148
   231
 the resulting proof obligations in an abstract, structured manner.
wenzelm@10148
   232
*}
wenzelm@10148
   233
wenzelm@10148
   234
theorem
wenzelm@10148
   235
  "|- .{True}.
wenzelm@10838
   236
      \<acute>S := 0; \<acute>I := 1;
wenzelm@10838
   237
      WHILE \<acute>I ~= n
wenzelm@10838
   238
      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
wenzelm@10148
   239
      DO
wenzelm@10838
   240
        \<acute>S := \<acute>S + \<acute>I;
wenzelm@10838
   241
        \<acute>I := \<acute>I + 1
wenzelm@10148
   242
      OD
wenzelm@10838
   243
      .{\<acute>S = (SUM j<n. j)}."
wenzelm@10148
   244
proof -
nipkow@15049
   245
  let ?sum = "\<lambda>k::nat. SUM j<k. j"
nipkow@15049
   246
  let ?inv = "\<lambda>s i::nat. s = ?sum i"
wenzelm@10148
   247
wenzelm@10148
   248
  show ?thesis
wenzelm@10148
   249
  proof hoare
wenzelm@10148
   250
    show "?inv 0 1" by simp
wenzelm@10148
   251
  next
wenzelm@10148
   252
    fix s i assume "?inv s i & i ~= n"
wenzelm@10148
   253
    thus "?inv (s + i) (i + 1)" by simp
wenzelm@10148
   254
  next
wenzelm@10148
   255
    fix s i assume "?inv s i & ~ i ~= n"
wenzelm@10148
   256
    thus "s = ?sum n" by simp
wenzelm@10148
   257
  qed
wenzelm@10148
   258
qed
wenzelm@10148
   259
wenzelm@10148
   260
text {*
wenzelm@10148
   261
 Certainly, this proof may be done fully automatic as well, provided
wenzelm@10148
   262
 that the invariant is given beforehand.
wenzelm@10148
   263
*}
wenzelm@10148
   264
wenzelm@10148
   265
theorem
wenzelm@10148
   266
  "|- .{True}.
wenzelm@10838
   267
      \<acute>S := 0; \<acute>I := 1;
wenzelm@10838
   268
      WHILE \<acute>I ~= n
wenzelm@10838
   269
      INV .{\<acute>S = (SUM j<\<acute>I. j)}.
wenzelm@10148
   270
      DO
wenzelm@10838
   271
        \<acute>S := \<acute>S + \<acute>I;
wenzelm@10838
   272
        \<acute>I := \<acute>I + 1
wenzelm@10148
   273
      OD
wenzelm@10838
   274
      .{\<acute>S = (SUM j<n. j)}."
wenzelm@10148
   275
  by hoare auto
wenzelm@10148
   276
wenzelm@18193
   277
wenzelm@18193
   278
subsection{* Time *}
nipkow@13473
   279
nipkow@13473
   280
text{*
wenzelm@18193
   281
  A simple embedding of time in Hoare logic: function @{text timeit}
wenzelm@18193
   282
  inserts an extra variable to keep track of the elapsed time.
nipkow@13473
   283
*}
nipkow@13473
   284
nipkow@13473
   285
record tstate = time :: nat
nipkow@13473
   286
wenzelm@18193
   287
types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
nipkow@13473
   288
nipkow@13473
   289
consts timeit :: "'a time com \<Rightarrow> 'a time com"
nipkow@13473
   290
primrec
wenzelm@18193
   291
  "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
wenzelm@18193
   292
  "timeit (c1; c2) = (timeit c1; timeit c2)"
wenzelm@18193
   293
  "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
wenzelm@18193
   294
  "timeit (While b iv c) = While b iv (timeit c)"
nipkow@13473
   295
nipkow@13473
   296
record tvars = tstate +
nipkow@13473
   297
  I :: nat
nipkow@13473
   298
  J :: nat
nipkow@13473
   299
wenzelm@18193
   300
lemma lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)"
wenzelm@18193
   301
  by (induct n) simp_all
nipkow@13473
   302
nipkow@13473
   303
lemma "|- .{i = \<acute>I & \<acute>time = 0}.
nipkow@13473
   304
 timeit(
nipkow@13473
   305
 WHILE \<acute>I \<noteq> 0
nipkow@13473
   306
 INV .{2*\<acute>time + \<acute>I*\<acute>I + 5*\<acute>I = i*i + 5*i}.
nipkow@13473
   307
 DO
nipkow@13473
   308
   \<acute>J := \<acute>I;
nipkow@13473
   309
   WHILE \<acute>J \<noteq> 0
nipkow@13473
   310
   INV .{0 < \<acute>I & 2*\<acute>time + \<acute>I*\<acute>I + 3*\<acute>I + 2*\<acute>J - 2 = i*i + 5*i}.
nipkow@13473
   311
   DO \<acute>J := \<acute>J - 1 OD;
nipkow@13473
   312
   \<acute>I := \<acute>I - 1
nipkow@13473
   313
 OD
nipkow@13473
   314
 ) .{2*\<acute>time = i*i + 5*i}."
wenzelm@18193
   315
  apply simp
wenzelm@18193
   316
  apply hoare
wenzelm@18193
   317
      apply simp
wenzelm@18193
   318
     apply clarsimp
wenzelm@18193
   319
    apply clarsimp
webertj@20432
   320
   apply arith
wenzelm@18193
   321
   prefer 2
nipkow@13473
   322
   apply clarsimp
wenzelm@18193
   323
  apply (clarsimp simp: nat_distrib)
wenzelm@18193
   324
  apply (frule lem)
nipkow@13473
   325
  apply arith
wenzelm@18193
   326
  done
nipkow@13473
   327
nipkow@13473
   328
end