src/HOL/IMP/Hoare_Examples.thy
 author huffman Thu Aug 11 09:11:15 2011 -0700 (2011-08-11) changeset 44165 d26a45f3c835 parent 43158 686fa0a0696e child 44177 b4b5cbca2519 permissions -rw-r--r--
remove lemma stupid_ext
```     1 (* Author: Tobias Nipkow *)
```
```     2
```
```     3 theory Hoare_Examples imports Hoare Util begin
```
```     4
```
```     5 subsection{* Example: Sums *}
```
```     6
```
```     7 text{* Summing up the first @{text n} natural numbers. The sum is accumulated
```
```     8 in variable @{text 0}, the loop counter is variable @{text 1}. *}
```
```     9
```
```    10 abbreviation "w n ==
```
```    11   WHILE Less (V ''y'') (N n)
```
```    12   DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
```
```    13
```
```    14 text{* For this example we make use of some predefined functions.  Function
```
```    15 @{const Setsum}, also written @{text"\<Sum>"}, sums up the elements of a set. The
```
```    16 set of numbers from @{text m} to @{text n} is written @{term "{m .. n}"}. *}
```
```    17
```
```    18 subsubsection{* Proof by Operational Semantics *}
```
```    19
```
```    20 text{* The behaviour of the loop is proved by induction: *}
```
```    21
```
```    22 lemma setsum_head_plus_1:
```
```    23   "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {m+1..n::int}"
```
```    24 by (subst simp_from_to) simp
```
```    25
```
```    26 lemma while_sum:
```
```    27   "(w n, s) \<Rightarrow> t \<Longrightarrow> t ''x'' = s ''x'' + \<Sum> {s ''y'' + 1 .. n}"
```
```    28 apply(induct "w n" s t rule: big_step_induct)
```
```    29 apply(auto simp add: setsum_head_plus_1)
```
```    30 done
```
```    31
```
```    32 text{* We were lucky that the proof was practically automatic, except for the
```
```    33 induction. In general, such proofs will not be so easy. The automation is
```
```    34 partly due to the right inversion rules that we set up as automatic
```
```    35 elimination rules that decompose big-step premises.
```
```    36
```
```    37 Now we prefix the loop with the necessary initialization: *}
```
```    38
```
```    39 lemma sum_via_bigstep:
```
```    40 assumes "(''x'' ::= N 0; ''y'' ::= N 0; w n, s) \<Rightarrow> t"
```
```    41 shows "t ''x'' = \<Sum> {1 .. n}"
```
```    42 proof -
```
```    43   from assms have "(w n,s(''x'':=0,''y'':=0)) \<Rightarrow> t" by auto
```
```    44   from while_sum[OF this] show ?thesis by simp
```
```    45 qed
```
```    46
```
```    47
```
```    48 subsubsection{* Proof by Hoare Logic *}
```
```    49
```
```    50 text{* Note that we deal with sequences of commands from right to left,
```
```    51 pulling back the postcondition towards the precondition. *}
```
```    52
```
```    53 lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
```
```    54 apply(rule hoare.Semi)
```
```    55 prefer 2
```
```    56 apply(rule While'
```
```    57   [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"])
```
```    58 apply(rule Semi)
```
```    59 prefer 2
```
```    60 apply(rule Assign)
```
```    61 apply(rule Assign')
```
```    62 apply(fastsimp simp: atLeastAtMostPlus1_int_conv algebra_simps)
```
```    63 apply(fastsimp)
```
```    64 apply(rule Semi)
```
```    65 prefer 2
```
```    66 apply(rule Assign)
```
```    67 apply(rule Assign')
```
```    68 apply simp
```
```    69 done
```
```    70
```
```    71 text{* The proof is intentionally an apply skript because it merely composes
```
```    72 the rules of Hoare logic. Of course, in a few places side conditions have to
```
```    73 be proved. But since those proofs are 1-liners, a structured proof is
```
```    74 overkill. In fact, we shall learn later that the application of the Hoare
```
```    75 rules can be automated completely and all that is left for the user is to
```
```    76 provide the loop invariants and prove the side-conditions. *}
```
```    77
```
```    78 end
```