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