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