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