author  nipkow 
Mon, 09 Jan 2017 19:32:40 +0100  
changeset 64851  33aab75ff423 
parent 61028  99d58362eeeb 
child 67406  23307fd33906 
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 

64851  5 
hide_const (open) sum 
6 

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

52149  9 
fun sum :: "int \<Rightarrow> int" where 
52554  10 
"sum i = (if i \<le> 0 then 0 else sum (i  1) + i)" 
52149  11 

52554  12 
lemma sum_simps[simp]: 
13 
"0 < i \<Longrightarrow> sum i = sum (i  1) + i" 

14 
"i \<le> 0 \<Longrightarrow> sum i = 0" 

52149  15 
by(simp_all) 
16 

17 
declare sum.simps[simp del] 

18 

52108  19 
abbreviation "wsum == 
20 
WHILE Less (N 0) (V ''x'') 

52554  21 
DO (''y'' ::= Plus (V ''y'') (V ''x'');; 
58410
6d46ad54a2ab
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents:
54489
diff
changeset

22 
''x'' ::= Plus (V ''x'') (N ( 1)))" 
43158  23 

24 

25 
subsubsection{* Proof by Operational Semantics *} 

26 

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

28 

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

31 
apply(induction wsum s t rule: big_step_induct) 

32 
apply(auto) 

52108  33 
done 
34 

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

38 
elimination rules that decompose bigstep premises. 

39 

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

41 

42 
lemma sum_via_bigstep: 

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

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

49 

50 

51 
subsubsection{* Proof by Hoare Logic *} 

52 

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

54 
pulling back the postcondition towards the precondition. *} 

55 

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

60 
apply(rule Seq) 

61 
prefer 2 

62 
apply(rule Assign) 

63 
apply(rule Assign') 

64 
apply simp 

61028  65 
apply simp 
43158  66 
apply(rule Assign') 
67 
apply simp 

68 
done 

69 

61028  70 
text{* The proof is intentionally an apply script because it merely composes 
43158  71 
the rules of Hoare logic. Of course, in a few places side conditions have to 
72 
be proved. But since those proofs are 1liners, a structured proof is 

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

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

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

76 

77 
end 