author | wenzelm |
Tue, 23 May 2017 10:59:01 +0200 | |
changeset 65908 | aefdb9e664c9 |
parent 64851 | 33aab75ff423 |
child 67406 | 23307fd33906 |
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 |
|
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 big-step 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 1-liners, 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 side-conditions. *} |
|
76 |
||
77 |
end |