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