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