author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45015  fdac1e9880eb 
child 47818  151d137f1095 
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 

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}" 

45015  28 
apply(induction "w n" s t rule: big_step_induct) 
43158  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') 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44177
diff
changeset

62 
apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps) 
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44177
diff
changeset

63 
apply(fastforce) 
43158  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 