summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/IMP/Hoare_Examples.thy

author | paulson <lp15@cam.ac.uk> |

Mon May 23 15:33:24 2016 +0100 (2016-05-23) | |

changeset 63114 | 27afe7af7379 |

parent 61028 | 99d58362eeeb |

child 64851 | 33aab75ff423 |

permissions | -rw-r--r-- |

Lots of new material for multivariate analysis

1 (* Author: Tobias Nipkow *)

3 theory Hoare_Examples imports Hoare begin

5 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}

7 fun sum :: "int \<Rightarrow> int" where

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

10 lemma sum_simps[simp]:

11 "0 < i \<Longrightarrow> sum i = sum (i - 1) + i"

12 "i \<le> 0 \<Longrightarrow> sum i = 0"

13 by(simp_all)

15 declare sum.simps[simp del]

17 abbreviation "wsum ==

18 WHILE Less (N 0) (V ''x'')

19 DO (''y'' ::= Plus (V ''y'') (V ''x'');;

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

23 subsubsection{* Proof by Operational Semantics *}

25 text{* The behaviour of the loop is proved by induction: *}

27 lemma while_sum:

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

29 apply(induction wsum s t rule: big_step_induct)

30 apply(auto)

31 done

33 text{* We were lucky that the proof was automatic, except for the

34 induction. In general, such proofs will not be so easy. The automation is

35 partly due to the right inversion rules that we set up as automatic

36 elimination rules that decompose big-step premises.

38 Now we prefix the loop with the necessary initialization: *}

40 lemma sum_via_bigstep:

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

42 shows "t ''y'' = sum (s ''x'')"

43 proof -

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

45 from while_sum[OF this] show ?thesis by simp

46 qed

49 subsubsection{* Proof by Hoare Logic *}

51 text{* Note that we deal with sequences of commands from right to left,

52 pulling back the postcondition towards the precondition. *}

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

55 apply(rule Seq)

56 prefer 2

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

58 apply(rule Seq)

59 prefer 2

60 apply(rule Assign)

61 apply(rule Assign')

62 apply simp

63 apply simp

64 apply(rule Assign')

65 apply simp

66 done

68 text{* The proof is intentionally an apply script because it merely composes

69 the rules of Hoare logic. Of course, in a few places side conditions have to

70 be proved. But since those proofs are 1-liners, a structured proof is

71 overkill. In fact, we shall learn later that the application of the Hoare

72 rules can be automated completely and all that is left for the user is to

73 provide the loop invariants and prove the side-conditions. *}

75 end