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