src/HOL/IMP/Hoare_Examples.thy
 author paulson 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 *)
```
```     2
```
```     3 theory Hoare_Examples imports Hoare begin
```
```     4
```
```     5 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
```
```     6
```
```     7 fun sum :: "int \<Rightarrow> int" where
```
```     8 "sum i = (if i \<le> 0 then 0 else sum (i - 1) + i)"
```
```     9
```
```    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)
```
```    14
```
```    15 declare sum.simps[simp del]
```
```    16
```
```    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)))"
```
```    21
```
```    22
```
```    23 subsubsection{* Proof by Operational Semantics *}
```
```    24
```
```    25 text{* The behaviour of the loop is proved by induction: *}
```
```    26
```
```    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
```
```    32
```
```    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.
```
```    37
```
```    38 Now we prefix the loop with the necessary initialization: *}
```
```    39
```
```    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
```
```    47
```
```    48
```
```    49 subsubsection{* Proof by Hoare Logic *}
```
```    50
```
```    51 text{* Note that we deal with sequences of commands from right to left,
```
```    52 pulling back the postcondition towards the precondition. *}
```
```    53
```
```    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
```
```    67
```
```    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. *}
```
```    74
```
```    75 end
```