summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/IMP/Hoare_Examples.thy

changeset 67406 | 23307fd33906 |

parent 64851 | 33aab75ff423 |

child 68776 | 403dd13cf6e9 |

equal
deleted
inserted
replaced

67405:e9ab4ad7bd15 | 67406:23307fd33906 |
---|---|

2 |
2 |

3 theory Hoare_Examples imports Hoare begin |
3 theory Hoare_Examples imports Hoare begin |

4 |
4 |

5 hide_const (open) sum |
5 hide_const (open) sum |

6 |
6 |

7 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} |
7 text\<open>Summing up the first @{text x} natural numbers in variable @{text y}.\<close> |

8 |
8 |

9 fun sum :: "int \<Rightarrow> int" where |
9 fun sum :: "int \<Rightarrow> int" where |

10 "sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)" |
10 "sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)" |

11 |
11 |

12 lemma sum_simps[simp]: |
12 lemma sum_simps[simp]: |

20 WHILE Less (N 0) (V ''x'') |
20 WHILE Less (N 0) (V ''x'') |

21 DO (''y'' ::= Plus (V ''y'') (V ''x'');; |
21 DO (''y'' ::= Plus (V ''y'') (V ''x'');; |

22 ''x'' ::= Plus (V ''x'') (N (- 1)))" |
22 ''x'' ::= Plus (V ''x'') (N (- 1)))" |

23 |
23 |

24 |
24 |

25 subsubsection{* Proof by Operational Semantics *} |
25 subsubsection\<open>Proof by Operational Semantics\<close> |

26 |
26 |

27 text{* The behaviour of the loop is proved by induction: *} |
27 text\<open>The behaviour of the loop is proved by induction:\<close> |

28 |
28 |

29 lemma while_sum: |
29 lemma while_sum: |

30 "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')" |
30 "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')" |

31 apply(induction wsum s t rule: big_step_induct) |
31 apply(induction wsum s t rule: big_step_induct) |

32 apply(auto) |
32 apply(auto) |

33 done |
33 done |

34 |
34 |

35 text{* We were lucky that the proof was automatic, except for the |
35 text\<open>We were lucky that the proof was automatic, except for the |

36 induction. In general, such proofs will not be so easy. The automation is |
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 |
37 partly due to the right inversion rules that we set up as automatic |

38 elimination rules that decompose big-step premises. |
38 elimination rules that decompose big-step premises. |

39 |
39 |

40 Now we prefix the loop with the necessary initialization: *} |
40 Now we prefix the loop with the necessary initialization:\<close> |

41 |
41 |

42 lemma sum_via_bigstep: |
42 lemma sum_via_bigstep: |

43 assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t" |
43 assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t" |

44 shows "t ''y'' = sum (s ''x'')" |
44 shows "t ''y'' = sum (s ''x'')" |

45 proof - |
45 proof - |

46 from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto |
46 from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto |

47 from while_sum[OF this] show ?thesis by simp |
47 from while_sum[OF this] show ?thesis by simp |

48 qed |
48 qed |

49 |
49 |

50 |
50 |

51 subsubsection{* Proof by Hoare Logic *} |
51 subsubsection\<open>Proof by Hoare Logic\<close> |

52 |
52 |

53 text{* Note that we deal with sequences of commands from right to left, |
53 text\<open>Note that we deal with sequences of commands from right to left, |

54 pulling back the postcondition towards the precondition. *} |
54 pulling back the postcondition towards the precondition.\<close> |

55 |
55 |

56 lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}" |
56 lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}" |

57 apply(rule Seq) |
57 apply(rule Seq) |

58 prefer 2 |
58 prefer 2 |

59 apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n - sum(s ''x''))"]) |
59 apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n - sum(s ''x''))"]) |

65 apply simp |
65 apply simp |

66 apply(rule Assign') |
66 apply(rule Assign') |

67 apply simp |
67 apply simp |

68 done |
68 done |

69 |
69 |

70 text{* The proof is intentionally an apply script because it merely composes |
70 text\<open>The proof is intentionally an apply script because it merely composes |

71 the rules of Hoare logic. Of course, in a few places side conditions have to |
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 |
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 |
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 |
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. *} |
75 provide the loop invariants and prove the side-conditions.\<close> |

76 |
76 |

77 end |
77 end |