2 |
2 |
3 theory Hoare_Examples imports Hoare begin |
3 theory Hoare_Examples imports Hoare begin |
4 |
4 |
5 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} |
5 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} |
6 |
6 |
|
7 fun sum :: "int \<Rightarrow> int" where |
|
8 "sum i = (if i <= 0 then 0 else sum (i - 1) + i)" |
|
9 |
|
10 lemma [simp]: "0 < i \<Longrightarrow> sum i = sum (i - 1) + i" "i <= 0 \<Longrightarrow> sum i = 0" |
|
11 by(simp_all) |
|
12 |
|
13 declare sum.simps[simp del] |
|
14 |
7 abbreviation "wsum == |
15 abbreviation "wsum == |
8 WHILE Less (N 0) (V ''x'') |
16 WHILE Less (N 0) (V ''x'') |
9 DO (''y'' ::= Plus (V ''y'') (V ''x'');; ''x'' ::= Plus (V ''x'') (N -1))" |
17 DO (''y'' ::= Plus (V ''y'') (V ''x'');; ''x'' ::= Plus (V ''x'') (N -1))" |
10 |
18 |
11 text{* For this example we make use of some predefined functions. Function |
|
12 @{const Setsum}, also written @{text"\<Sum>"}, sums up the elements of a set. The |
|
13 set of numbers from @{text m} to @{text n} is written @{term "{m .. n}"}. *} |
|
14 |
19 |
15 subsubsection{* Proof by Operational Semantics *} |
20 subsubsection{* Proof by Operational Semantics *} |
16 |
21 |
17 text{* The behaviour of the loop is proved by induction: *} |
22 text{* The behaviour of the loop is proved by induction: *} |
18 |
23 |
19 lemma set_ivl_lemma: |
24 lemma while_sum: |
20 "i \<le> j \<Longrightarrow> {i..j} = insert j {i..j - (1::int)}" |
25 "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')" |
21 apply(simp add:atLeastAtMost_def atLeast_def atMost_def del: simp_from_to) |
26 apply(induction wsum s t rule: big_step_induct) |
22 apply(fastforce) |
27 apply(auto) |
23 done |
28 done |
24 |
29 |
25 lemma while_sum: |
30 text{* We were lucky that the proof was automatic, except for the |
26 "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + \<Sum> {1 .. s ''x''}" |
|
27 apply(induction wsum s t rule: big_step_induct) |
|
28 apply(auto simp add: set_ivl_lemma) |
|
29 done |
|
30 |
|
31 text{* We were lucky that the proof was practically automatic, except for the |
|
32 induction. In general, such proofs will not be so easy. The automation is |
31 induction. In general, such proofs will not be so easy. The automation is |
33 partly due to the right inversion rules that we set up as automatic |
32 partly due to the right inversion rules that we set up as automatic |
34 elimination rules that decompose big-step premises. |
33 elimination rules that decompose big-step premises. |
35 |
34 |
36 Now we prefix the loop with the necessary initialization: *} |
35 Now we prefix the loop with the necessary initialization: *} |
37 |
36 |
38 lemma sum_via_bigstep: |
37 lemma sum_via_bigstep: |
39 assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t" |
38 assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t" |
40 shows "t ''y'' = \<Sum> {1 .. s ''x''}" |
39 shows "t ''y'' = sum (s ''x'')" |
41 proof - |
40 proof - |
42 from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto |
41 from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto |
43 from while_sum[OF this] show ?thesis by simp |
42 from while_sum[OF this] show ?thesis by simp |
44 qed |
43 qed |
45 |
44 |
47 subsubsection{* Proof by Hoare Logic *} |
46 subsubsection{* Proof by Hoare Logic *} |
48 |
47 |
49 text{* Note that we deal with sequences of commands from right to left, |
48 text{* Note that we deal with sequences of commands from right to left, |
50 pulling back the postcondition towards the precondition. *} |
49 pulling back the postcondition towards the precondition. *} |
51 |
50 |
52 lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = \<Sum> {1 .. n}}" |
51 lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}" |
53 apply(rule hoare.Seq) |
|
54 prefer 2 |
|
55 apply(rule While' [where P = "\<lambda>s. (s ''y'' = \<Sum> {1..n} - \<Sum> {1 .. s ''x''})"]) |
|
56 apply(rule Seq) |
52 apply(rule Seq) |
57 prefer 2 |
53 prefer 2 |
58 apply(rule Assign) |
54 apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n - sum(s ''x''))"]) |
59 apply(rule Assign') |
55 apply(rule Seq) |
60 apply simp |
56 prefer 2 |
61 apply(simp add: algebra_simps set_ivl_lemma minus_numeral_simps(1)[symmetric] |
57 apply(rule Assign) |
62 del: minus_numeral_simps) |
58 apply(rule Assign') |
63 apply(simp) |
59 apply simp |
|
60 apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps) |
|
61 apply(simp) |
64 apply(rule Assign') |
62 apply(rule Assign') |
65 apply simp |
63 apply simp |
66 done |
64 done |
67 |
65 |
68 text{* The proof is intentionally an apply skript because it merely composes |
66 text{* The proof is intentionally an apply skript because it merely composes |