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 *)
     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