src/HOL/Isar_examples/HoareEx.thy
author wenzelm
Tue, 03 Oct 2000 22:39:49 +0200
changeset 10148 739327964a5c
child 10838 9423817dee84
permissions -rw-r--r--
Hoare logic in Isar;
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    42
  "|- .{`(N_update (2 * `N)) : .{`N = #10}.}. `N := 2 * `N .{`N = #10}."
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    52
lemma "|- .{True}. `N := #10 .{`N = #10}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    53
  by hoare
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    54
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    55
lemma "|- .{2 * `N = #10}. `N := 2 * `N .{`N = #10}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    56
  by hoare
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    57
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    58
lemma "|- .{`N = #5}. `N := 2 * `N .{`N = #10}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    59
  by hoare simp
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    60
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    61
lemma "|- .{`N + 1 = a + 1}. `N := `N + 1 .{`N = a + 1}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    62
  by hoare
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    63
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    64
lemma "|- .{`N = a}. `N := `N + 1 .{`N = a + 1}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    65
  by hoare simp
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    66
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    67
lemma "|- .{a = a & b = b}. `M := a; `N := b .{`M = a & `N = b}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    68
  by hoare
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    69
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    70
lemma "|- .{True}. `M := a; `N := b .{`M = a & `N = b}."
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    74
"|- .{`M = a & `N = b}.
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    75
    `I := `M; `M := `N; `N := `I
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    76
    .{`M = b & `N = a}."
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    86
lemma "|- .{`N = a}. `N := `N .{`N = a}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    87
  by hoare
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    88
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
    89
lemma "|- .{`x = a}. `x := `x .{`x = a}."
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   104
lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   105
proof -
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   106
  have ".{`M = `N}. <= .{`M + 1 ~= `N}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   107
    by auto
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   108
  also have "|- ... `M := `M + 1 .{`M ~= `N}."
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   113
lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   119
  also have "|- .{`M + 1 ~= `N}. `M := `M + 1 .{`M ~= `N}."
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   124
lemma "|- .{`M = `N}. `M := `M + 1 .{`M ~= `N}."
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   138
  "|- .{`M = 0 & `S = 0}.
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   139
      WHILE `M ~= a
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   140
      DO `S := `S + b; `M := `M + 1 OD
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   141
      .{`S = a * b}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   142
proof -
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   143
  let "|- _ ?while _" = ?thesis
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   144
  let ".{`?inv}." = ".{`S = `M * b}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   145
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   146
  have ".{`M = 0 & `S = 0}. <= .{`?inv}." by auto
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   147
  also have "|- ... ?while .{`?inv & ~ (`M ~= a)}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   148
  proof
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   149
    let ?c = "`S := `S + b; `M := `M + 1"
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   150
    have ".{`?inv & `M ~= a}. <= .{`S + b = (`M + 1) * b}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   151
      by auto
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   152
    also have "|- ... ?c .{`?inv}." by hoare
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   153
    finally show "|- .{`?inv & `M ~= a}. ?c .{`?inv}." .
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   154
  qed
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   155
  also have "... <= .{`S = a * b}." by auto
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   167
  "|- .{`M = 0 & `S = 0}.
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   168
      WHILE `M ~= a
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   169
      INV .{`S = `M * b}.
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   170
      DO `S := `S + b; `M := `M + 1 OD
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   171
      .{`S = a * b}."
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}.
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   205
      `S := 0; `I := 1;
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   206
      WHILE `I ~= n
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   207
      DO
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   208
        `S := `S + `I;
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   209
        `I := `I + 1
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   210
      OD
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   211
      .{`S = (SUM j<n. j)}."
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   217
  have "|- .{True}. `S := 0; `I := 1 .{?inv `S `I}."
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   221
    also have "|- .{...}. `S := 0; `I := 1 .{?inv `S `I}."
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   225
  also have "|- ... ?while .{?inv `S `I & ~ `I ~= n}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   226
  proof
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   227
    let ?body = "`S := `S + `I; `I := `I + 1"
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
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   230
    also have "|- .{`S + `I = ?sum (`I + 1)}. ?body .{?inv `S `I}."
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   231
      by hoare
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   232
    finally show "|- .{?inv `S `I & `I ~= n}. ?body .{?inv `S `I}." .
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}.
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   246
      `S := 0; `I := 1;
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   247
      WHILE `I ~= n
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   248
      INV .{`S = (SUM j<`I. j)}.
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   249
      DO
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   250
        `S := `S + `I;
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   251
        `I := `I + 1
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   252
      OD
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   253
      .{`S = (SUM j<n. j)}."
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}.
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   277
      `S := 0; `I := 1;
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   278
      WHILE `I ~= n
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   279
      INV .{`S = (SUM j<`I. j)}.
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   280
      DO
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   281
        `S := `S + `I;
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   282
        `I := `I + 1
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   283
      OD
739327964a5c Hoare logic in Isar;
wenzelm
parents:
diff changeset
   284
      .{`S = (SUM j<n. j)}."
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