author  nipkow 
Wed, 22 May 2013 08:46:39 +0200  
changeset 52108  06db08182c4b 
parent 52046  bc01725d7918 
child 52149  32b1dbda331c 
permissions  rwrr 
43158  1 
(* Author: Tobias Nipkow *) 
2 

44177
b4b5cbca2519
IMP/Util distinguishes between sets and functions again; imported only where used.
kleing
parents:
43158
diff
changeset

3 
theory Hoare_Examples imports Hoare begin 
43158  4 

52108  5 
text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} 
43158  6 

52108  7 
abbreviation "wsum == 
8 
WHILE Less (N 0) (V ''x'') 

9 
DO (''y'' ::= Plus (V ''y'') (V ''x'');; ''x'' ::= Plus (V ''x'') (N 1))" 

43158  10 

11 
text{* For this example we make use of some predefined functions. Function 

12 
@{const Setsum}, also written @{text"\<Sum>"}, sums up the elements of a set. The 

13 
set of numbers from @{text m} to @{text n} is written @{term "{m .. n}"}. *} 

14 

15 
subsubsection{* Proof by Operational Semantics *} 

16 

17 
text{* The behaviour of the loop is proved by induction: *} 

18 

52108  19 
lemma set_ivl_lemma: 
20 
"i \<le> j \<Longrightarrow> {i..j} = insert j {i..j  (1::int)}" 

21 
apply(simp add:atLeastAtMost_def atLeast_def atMost_def del: simp_from_to) 

22 
apply(fastforce) 

23 
done 

24 

43158  25 
lemma while_sum: 
52108  26 
"(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + \<Sum> {1 .. s ''x''}" 
27 
apply(induction wsum s t rule: big_step_induct) 

28 
apply(auto simp add: set_ivl_lemma) 

43158  29 
done 
30 

31 
text{* We were lucky that the proof was practically automatic, except for the 

32 
induction. In general, such proofs will not be so easy. The automation is 

33 
partly due to the right inversion rules that we set up as automatic 

34 
elimination rules that decompose bigstep premises. 

35 

36 
Now we prefix the loop with the necessary initialization: *} 

37 

38 
lemma sum_via_bigstep: 

52108  39 
assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t" 
40 
shows "t ''y'' = \<Sum> {1 .. s ''x''}" 

43158  41 
proof  
52108  42 
from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto 
43158  43 
from while_sum[OF this] show ?thesis by simp 
44 
qed 

45 

46 

47 
subsubsection{* Proof by Hoare Logic *} 

48 

49 
text{* Note that we deal with sequences of commands from right to left, 

50 
pulling back the postcondition towards the precondition. *} 

51 

52108  52 
lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = \<Sum> {1 .. n}}" 
47818  53 
apply(rule hoare.Seq) 
43158  54 
prefer 2 
52108  55 
apply(rule While' [where P = "\<lambda>s. (s ''y'' = \<Sum> {1..n}  \<Sum> {1 .. s ''x''})"]) 
47818  56 
apply(rule Seq) 
43158  57 
prefer 2 
58 
apply(rule Assign) 

59 
apply(rule Assign') 

52108  60 
apply simp 
61 
apply(simp add: algebra_simps set_ivl_lemma minus_numeral_simps(1)[symmetric] 

62 
del: minus_numeral_simps) 

63 
apply(simp) 

43158  64 
apply(rule Assign') 
65 
apply simp 

66 
done 

67 

68 
text{* The proof is intentionally an apply skript because it merely composes 

69 
the rules of Hoare logic. Of course, in a few places side conditions have to 

70 
be proved. But since those proofs are 1liners, a structured proof is 

71 
overkill. In fact, we shall learn later that the application of the Hoare 

72 
rules can be automated completely and all that is left for the user is to 

73 
provide the loop invariants and prove the sideconditions. *} 

74 

75 
end 