43158

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 bigstep 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 1liners, 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 sideconditions. *}


77 


78 
end
