author | haftmann |
Sun, 21 Sep 2014 16:56:11 +0200 | |
changeset 58410 | 6d46ad54a2ab |
parent 54489 | 03ff4d1e6784 |
child 61028 | 99d58362eeeb |
permissions | -rw-r--r-- |
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 |
52554 | 8 |
"sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)" |
52149 | 9 |
|
52554 | 10 |
lemma sum_simps[simp]: |
11 |
"0 < i \<Longrightarrow> sum i = sum (i - 1) + i" |
|
12 |
"i \<le> 0 \<Longrightarrow> sum i = 0" |
|
52149 | 13 |
by(simp_all) |
14 |
||
15 |
declare sum.simps[simp del] |
|
16 |
||
52108 | 17 |
abbreviation "wsum == |
18 |
WHILE Less (N 0) (V ''x'') |
|
52554 | 19 |
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
|
20 |
''x'' ::= Plus (V ''x'') (N (- 1)))" |
43158 | 21 |
|
22 |
||
23 |
subsubsection{* Proof by Operational Semantics *} |
|
24 |
||
25 |
text{* The behaviour of the loop is proved by induction: *} |
|
26 |
||
52149 | 27 |
lemma while_sum: |
28 |
"(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')" |
|
29 |
apply(induction wsum s t rule: big_step_induct) |
|
30 |
apply(auto) |
|
52108 | 31 |
done |
32 |
||
52149 | 33 |
text{* We were lucky that the proof was automatic, except for the |
43158 | 34 |
induction. In general, such proofs will not be so easy. The automation is |
35 |
partly due to the right inversion rules that we set up as automatic |
|
36 |
elimination rules that decompose big-step premises. |
|
37 |
||
38 |
Now we prefix the loop with the necessary initialization: *} |
|
39 |
||
40 |
lemma sum_via_bigstep: |
|
52149 | 41 |
assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t" |
42 |
shows "t ''y'' = sum (s ''x'')" |
|
43158 | 43 |
proof - |
52108 | 44 |
from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto |
43158 | 45 |
from while_sum[OF this] show ?thesis by simp |
46 |
qed |
|
47 |
||
48 |
||
49 |
subsubsection{* Proof by Hoare Logic *} |
|
50 |
||
51 |
text{* Note that we deal with sequences of commands from right to left, |
|
52 |
pulling back the postcondition towards the precondition. *} |
|
53 |
||
52149 | 54 |
lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}" |
47818 | 55 |
apply(rule Seq) |
52149 | 56 |
prefer 2 |
57 |
apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n - sum(s ''x''))"]) |
|
58 |
apply(rule Seq) |
|
59 |
prefer 2 |
|
60 |
apply(rule Assign) |
|
61 |
apply(rule Assign') |
|
62 |
apply simp |
|
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 1-liners, 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 side-conditions. *} |
|
74 |
||
75 |
end |