author  nipkow 
Sun, 26 May 2013 11:56:55 +0200  
changeset 52149  32b1dbda331c 
parent 52108  06db08182c4b 
child 52529  48b52b039150 
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 

52149  7 
fun sum :: "int \<Rightarrow> int" where 
8 
"sum i = (if i <= 0 then 0 else sum (i  1) + i)" 

9 

10 
lemma [simp]: "0 < i \<Longrightarrow> sum i = sum (i  1) + i" "i <= 0 \<Longrightarrow> sum i = 0" 

11 
by(simp_all) 

12 

13 
declare sum.simps[simp del] 

14 

52108  15 
abbreviation "wsum == 
16 
WHILE Less (N 0) (V ''x'') 

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

43158  18 

19 

20 
subsubsection{* Proof by Operational Semantics *} 

21 

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

23 

52149  24 
lemma while_sum: 
25 
"(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')" 

26 
apply(induction wsum s t rule: big_step_induct) 

27 
apply(auto) 

52108  28 
done 
29 

52149  30 
text{* We were lucky that the proof was automatic, except for the 
43158  31 
induction. In general, such proofs will not be so easy. The automation is 
32 
partly due to the right inversion rules that we set up as automatic 

33 
elimination rules that decompose bigstep premises. 

34 

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

36 

37 
lemma sum_via_bigstep: 

52149  38 
assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t" 
39 
shows "t ''y'' = sum (s ''x'')" 

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

44 

45 

46 
subsubsection{* Proof by Hoare Logic *} 

47 

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

49 
pulling back the postcondition towards the precondition. *} 

50 

52149  51 
lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}" 
47818  52 
apply(rule Seq) 
52149  53 
prefer 2 
54 
apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n  sum(s ''x''))"]) 

55 
apply(rule Seq) 

56 
prefer 2 

57 
apply(rule Assign) 

58 
apply(rule Assign') 

59 
apply simp 

60 
apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps) 

61 
apply(simp) 

43158  62 
apply(rule Assign') 
63 
apply simp 

64 
done 

65 

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

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

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

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

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

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

72 

73 
end 