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