src/HOL/IMP/Hoare_Examples.thy
author nipkow
Sun, 26 May 2013 11:56:55 +0200
changeset 52149 32b1dbda331c
parent 52108 06db08182c4b
child 52529 48b52b039150
permissions -rw-r--r--
simpler proof through custom summation function
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
52108
06db08182c4b simplified example and proof
nipkow
parents: 52046
diff changeset
     5
text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
52149
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
     7
fun sum :: "int \<Rightarrow> int" where
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
     8
"sum i = (if i <= 0 then 0 else sum (i - 1) + i)"
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
     9
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    10
lemma [simp]: "0 < i \<Longrightarrow> sum i = sum (i - 1) + i" "i <= 0 \<Longrightarrow> sum i = 0"
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    11
by(simp_all)
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    12
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    13
declare sum.simps[simp del]
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    14
52108
06db08182c4b simplified example and proof
nipkow
parents: 52046
diff changeset
    15
abbreviation "wsum ==
06db08182c4b simplified example and proof
nipkow
parents: 52046
diff changeset
    16
  WHILE Less (N 0) (V ''x'')
06db08182c4b simplified example and proof
nipkow
parents: 52046
diff changeset
    17
  DO (''y'' ::= Plus (V ''y'') (V ''x'');; ''x'' ::= Plus (V ''x'') (N -1))"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    18
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    20
subsubsection{* Proof by Operational Semantics *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    21
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
text{* The behaviour of the loop is proved by induction: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    23
52149
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    24
lemma while_sum:
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    25
  "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')"
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    26
apply(induction wsum s t rule: big_step_induct)
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    27
apply(auto)
52108
06db08182c4b simplified example and proof
nipkow
parents: 52046
diff changeset
    28
done
06db08182c4b simplified example and proof
nipkow
parents: 52046
diff changeset
    29
52149
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    30
text{* We were lucky that the proof was automatic, except for the
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    31
induction. In general, such proofs will not be so easy. The automation is
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
partly due to the right inversion rules that we set up as automatic
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    33
elimination rules that decompose big-step premises.
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    34
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    35
Now we prefix the loop with the necessary initialization: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    37
lemma sum_via_bigstep:
52149
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    38
  assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t"
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    39
  shows "t ''y'' = sum (s ''x'')"
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
proof -
52108
06db08182c4b simplified example and proof
nipkow
parents: 52046
diff changeset
    41
  from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    42
  from while_sum[OF this] show ?thesis by simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    43
qed
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    44
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    45
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    46
subsubsection{* Proof by Hoare Logic *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    47
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    48
text{* Note that we deal with sequences of commands from right to left,
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    49
pulling back the postcondition towards the precondition. *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    50
52149
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    51
lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}"
47818
151d137f1095 renamed Semi to Seq
nipkow
parents: 45015
diff changeset
    52
apply(rule Seq)
52149
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    53
 prefer 2
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    54
 apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n - sum(s ''x''))"])
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    55
  apply(rule Seq)
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    56
   prefer 2
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    57
   apply(rule Assign)
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    58
  apply(rule Assign')
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    59
  apply simp
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    60
  apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps)
32b1dbda331c simpler proof through custom summation function
nipkow
parents: 52108
diff changeset
    61
 apply(simp)
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    62
apply(rule Assign')
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    63
apply simp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    64
done
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    65
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    66
text{* The proof is intentionally an apply skript because it merely composes
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    67
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
    68
be proved. But since those proofs are 1-liners, a structured proof is
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    69
overkill. In fact, we shall learn later that the application of the Hoare
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    70
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
    71
provide the loop invariants and prove the side-conditions. *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    72
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    73
end