src/HOL/IMP/Hoare_Examples.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45015 fdac1e9880eb
child 47818 151d137f1095
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
kleing@43158
     1
(* Author: Tobias Nipkow *)
kleing@43158
     2
kleing@44177
     3
theory Hoare_Examples imports Hoare begin
kleing@43158
     4
kleing@43158
     5
subsection{* Example: Sums *}
kleing@43158
     6
kleing@43158
     7
text{* Summing up the first @{text n} natural numbers. The sum is accumulated
kleing@43158
     8
in variable @{text 0}, the loop counter is variable @{text 1}. *}
kleing@43158
     9
kleing@43158
    10
abbreviation "w n ==
kleing@43158
    11
  WHILE Less (V ''y'') (N n)
kleing@43158
    12
  DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )"
kleing@43158
    13
kleing@43158
    14
text{* For this example we make use of some predefined functions.  Function
kleing@43158
    15
@{const Setsum}, also written @{text"\<Sum>"}, sums up the elements of a set. The
kleing@43158
    16
set of numbers from @{text m} to @{text n} is written @{term "{m .. n}"}. *}
kleing@43158
    17
kleing@43158
    18
subsubsection{* Proof by Operational Semantics *}
kleing@43158
    19
kleing@43158
    20
text{* The behaviour of the loop is proved by induction: *}
kleing@43158
    21
kleing@43158
    22
lemma setsum_head_plus_1:
kleing@43158
    23
  "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {m+1..n::int}"
kleing@43158
    24
by (subst simp_from_to) simp
kleing@43158
    25
  
kleing@43158
    26
lemma while_sum:
kleing@43158
    27
  "(w n, s) \<Rightarrow> t \<Longrightarrow> t ''x'' = s ''x'' + \<Sum> {s ''y'' + 1 .. n}"
nipkow@45015
    28
apply(induction "w n" s t rule: big_step_induct)
kleing@43158
    29
apply(auto simp add: setsum_head_plus_1)
kleing@43158
    30
done
kleing@43158
    31
kleing@43158
    32
text{* We were lucky that the proof was practically automatic, except for the
kleing@43158
    33
induction. In general, such proofs will not be so easy. The automation is
kleing@43158
    34
partly due to the right inversion rules that we set up as automatic
kleing@43158
    35
elimination rules that decompose big-step premises.
kleing@43158
    36
kleing@43158
    37
Now we prefix the loop with the necessary initialization: *}
kleing@43158
    38
kleing@43158
    39
lemma sum_via_bigstep:
kleing@43158
    40
assumes "(''x'' ::= N 0; ''y'' ::= N 0; w n, s) \<Rightarrow> t"
kleing@43158
    41
shows "t ''x'' = \<Sum> {1 .. n}"
kleing@43158
    42
proof -
kleing@43158
    43
  from assms have "(w n,s(''x'':=0,''y'':=0)) \<Rightarrow> t" by auto
kleing@43158
    44
  from while_sum[OF this] show ?thesis by simp
kleing@43158
    45
qed
kleing@43158
    46
kleing@43158
    47
kleing@43158
    48
subsubsection{* Proof by Hoare Logic *}
kleing@43158
    49
kleing@43158
    50
text{* Note that we deal with sequences of commands from right to left,
kleing@43158
    51
pulling back the postcondition towards the precondition. *}
kleing@43158
    52
kleing@43158
    53
lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
kleing@43158
    54
apply(rule hoare.Semi)
kleing@43158
    55
prefer 2
kleing@43158
    56
apply(rule While'
kleing@43158
    57
  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"])
kleing@43158
    58
apply(rule Semi)
kleing@43158
    59
prefer 2
kleing@43158
    60
apply(rule Assign)
kleing@43158
    61
apply(rule Assign')
nipkow@44890
    62
apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps)
nipkow@44890
    63
apply(fastforce)
kleing@43158
    64
apply(rule Semi)
kleing@43158
    65
prefer 2
kleing@43158
    66
apply(rule Assign)
kleing@43158
    67
apply(rule Assign')
kleing@43158
    68
apply simp
kleing@43158
    69
done
kleing@43158
    70
kleing@43158
    71
text{* The proof is intentionally an apply skript because it merely composes
kleing@43158
    72
the rules of Hoare logic. Of course, in a few places side conditions have to
kleing@43158
    73
be proved. But since those proofs are 1-liners, a structured proof is
kleing@43158
    74
overkill. In fact, we shall learn later that the application of the Hoare
kleing@43158
    75
rules can be automated completely and all that is left for the user is to
kleing@43158
    76
provide the loop invariants and prove the side-conditions. *}
kleing@43158
    77
kleing@43158
    78
end