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