# Theory Hoare_Examples

Up to index of Isabelle/HOL/HOL-IMP

theory Hoare_Examples
imports Hoare
`(* Author: Tobias Nipkow *)theory Hoare_Examples imports Hoare beginsubsection{* Example: Sums *}text{* Summing up the first @{text n} natural numbers. The sum is accumulatedin variable @{text x}, the loop counter is variable @{text y}. *}abbreviation "w n ==  WHILE Less (V ''y'') (N n)  DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"text{* For this example we make use of some predefined functions.  Function@{const Setsum}, also written @{text"∑"}, sums up the elements of a set. Theset of numbers from @{text m} to @{text n} is written @{term "{m .. n}"}. *}subsubsection{* Proof by Operational Semantics *}text{* The behaviour of the loop is proved by induction: *}lemma setsum_head_plus_1:  "m ≤ n ==> setsum f {m..n} = f m + setsum f {m+1..n::int}"by (subst simp_from_to) simp  lemma while_sum:  "(w n, s) => t ==> t ''x'' = s ''x'' + ∑ {s ''y'' + 1 .. n}"apply(induction "w n" s t rule: big_step_induct)apply(auto simp add: setsum_head_plus_1)donetext{* We were lucky that the proof was practically automatic, except for theinduction. In general, such proofs will not be so easy. The automation ispartly due to the right inversion rules that we set up as automaticelimination rules that decompose big-step premises.Now we prefix the loop with the necessary initialization: *}lemma sum_via_bigstep:assumes "(''x'' ::= N 0; ''y'' ::= N 0; w n, s) => t"shows "t ''x'' = ∑ {1 .. n}"proof -  from assms have "(w n,s(''x'':=0,''y'':=0)) => t" by auto  from while_sum[OF this] show ?thesis by simpqedsubsubsection{* Proof by Hoare Logic *}text{* Note that we deal with sequences of commands from right to left,pulling back the postcondition towards the precondition. *}lemma "\<turnstile> {λs. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {λs. s ''x'' = ∑ {1 .. n}}"apply(rule hoare.Seq)prefer 2apply(rule While'  [where P = "λs. s ''x'' = ∑ {1..s ''y''} ∧ 0 ≤ s ''y'' ∧ s ''y'' ≤ n"])apply(rule Seq)prefer 2apply(rule Assign)apply(rule Assign')apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps)apply(fastforce)apply(rule Seq)prefer 2apply(rule Assign)apply(rule Assign')apply simpdonetext{* The proof is intentionally an apply skript because it merely composesthe rules of Hoare logic. Of course, in a few places side conditions have tobe proved. But since those proofs are 1-liners, a structured proof isoverkill. In fact, we shall learn later that the application of the Hoarerules can be automated completely and all that is left for the user is toprovide the loop invariants and prove the side-conditions. *}end`