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