author | haftmann |
Fri, 01 Nov 2013 18:51:14 +0100 | |
changeset 54230 | b1d955791529 |
parent 52554 | 19764bef2730 |
child 54489 | 03ff4d1e6784 |
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 |
|
52554 | 5 |
text{* Improves proof automation for negative numerals: *} |
52529 | 6 |
|
7 |
lemma add_neg1R[simp]: |
|
52554 | 8 |
"x + -1 = x - (1 :: int)" |
9 |
by arith |
|
52529 | 10 |
|
52554 | 11 |
lemma add_neg_numeralR[simp]: |
52529 | 12 |
"x + neg_numeral n = (x::'a::neg_numeral) - numeral(n)" |
13 |
by (simp only: diff_minus_eq_add[symmetric] minus_neg_numeral) |
|
14 |
||
15 |
||
52108 | 16 |
text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} |
43158 | 17 |
|
52149 | 18 |
fun sum :: "int \<Rightarrow> int" where |
52554 | 19 |
"sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)" |
52149 | 20 |
|
52554 | 21 |
lemma sum_simps[simp]: |
22 |
"0 < i \<Longrightarrow> sum i = sum (i - 1) + i" |
|
23 |
"i \<le> 0 \<Longrightarrow> sum i = 0" |
|
52149 | 24 |
by(simp_all) |
25 |
||
26 |
declare sum.simps[simp del] |
|
27 |
||
52108 | 28 |
abbreviation "wsum == |
29 |
WHILE Less (N 0) (V ''x'') |
|
52554 | 30 |
DO (''y'' ::= Plus (V ''y'') (V ''x'');; |
31 |
''x'' ::= Plus (V ''x'') (N -1))" |
|
43158 | 32 |
|
33 |
||
34 |
subsubsection{* Proof by Operational Semantics *} |
|
35 |
||
36 |
text{* The behaviour of the loop is proved by induction: *} |
|
37 |
||
52149 | 38 |
lemma while_sum: |
39 |
"(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')" |
|
40 |
apply(induction wsum s t rule: big_step_induct) |
|
41 |
apply(auto) |
|
52108 | 42 |
done |
43 |
||
52149 | 44 |
text{* We were lucky that the proof was automatic, except for the |
43158 | 45 |
induction. In general, such proofs will not be so easy. The automation is |
46 |
partly due to the right inversion rules that we set up as automatic |
|
47 |
elimination rules that decompose big-step premises. |
|
48 |
||
49 |
Now we prefix the loop with the necessary initialization: *} |
|
50 |
||
51 |
lemma sum_via_bigstep: |
|
52149 | 52 |
assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t" |
53 |
shows "t ''y'' = sum (s ''x'')" |
|
43158 | 54 |
proof - |
52108 | 55 |
from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto |
43158 | 56 |
from while_sum[OF this] show ?thesis by simp |
57 |
qed |
|
58 |
||
59 |
||
60 |
subsubsection{* Proof by Hoare Logic *} |
|
61 |
||
62 |
text{* Note that we deal with sequences of commands from right to left, |
|
63 |
pulling back the postcondition towards the precondition. *} |
|
64 |
||
52149 | 65 |
lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}" |
47818 | 66 |
apply(rule Seq) |
52149 | 67 |
prefer 2 |
68 |
apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n - sum(s ''x''))"]) |
|
69 |
apply(rule Seq) |
|
70 |
prefer 2 |
|
71 |
apply(rule Assign) |
|
72 |
apply(rule Assign') |
|
73 |
apply simp |
|
74 |
apply(simp) |
|
43158 | 75 |
apply(rule Assign') |
76 |
apply simp |
|
77 |
done |
|
78 |
||
79 |
text{* The proof is intentionally an apply skript because it merely composes |
|
80 |
the rules of Hoare logic. Of course, in a few places side conditions have to |
|
81 |
be proved. But since those proofs are 1-liners, a structured proof is |
|
82 |
overkill. In fact, we shall learn later that the application of the Hoare |
|
83 |
rules can be automated completely and all that is left for the user is to |
|
84 |
provide the loop invariants and prove the side-conditions. *} |
|
85 |
||
86 |
end |