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