author nipkow Wed, 22 May 2013 08:46:39 +0200 changeset 52108 06db08182c4b parent 52107 0c21dffc177a child 52109 39ac12f31f5c child 52111 1fd184eaa310
simplified example and proof
```--- a/src/HOL/IMP/Hoare_Examples.thy	Wed May 22 00:30:36 2013 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy	Wed May 22 08:46:39 2013 +0200
@@ -2,14 +2,11 @@

theory Hoare_Examples imports Hoare begin

-subsection{* Example: Sums *}
+text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}

-text{* Summing up the first @{text n} natural numbers. The sum is accumulated
-in variable @{text x}, the loop counter is variable @{text y}. *}
-
-abbreviation "w n ==
-  WHILE Less (V ''y'') (N n)
-  DO ( ''y'' ::= Plus (V ''y'') (N 1);; ''x'' ::= Plus (V ''x'') (V ''y'') )"
+abbreviation "wsum ==
+  WHILE Less (N 0) (V ''x'')
+  DO (''y'' ::= Plus (V ''y'') (V ''x'');; ''x'' ::= Plus (V ''x'') (N -1))"

text{* For this example we make use of some predefined functions.  Function
@{const Setsum}, also written @{text"\<Sum>"}, sums up the elements of a set. The
@@ -19,14 +16,16 @@

text{* The behaviour of the loop is proved by induction: *}

-  "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {m+1..n::int}"
-by (subst simp_from_to) simp
-
+lemma set_ivl_lemma:
+  "i \<le> j \<Longrightarrow> {i..j} = insert j {i..j - (1::int)}"
+apply(simp add:atLeastAtMost_def atLeast_def atMost_def del: simp_from_to)
+apply(fastforce)
+done
+
lemma while_sum:
-  "(w n, s) \<Rightarrow> t \<Longrightarrow> t ''x'' = s ''x'' + \<Sum> {s ''y'' + 1 .. n}"
-apply(induction "w n" s t rule: big_step_induct)
+  "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + \<Sum> {1 .. s ''x''}"
+apply(induction wsum s t rule: big_step_induct)
done

text{* We were lucky that the proof was practically automatic, except for the
@@ -37,10 +36,10 @@
Now we prefix the loop with the necessary initialization: *}

lemma sum_via_bigstep:
-assumes "(''x'' ::= N 0;; ''y'' ::= N 0;; w n, s) \<Rightarrow> t"
-shows "t ''x'' = \<Sum> {1 .. n}"
+assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t"
+shows "t ''y'' = \<Sum> {1 .. s ''x''}"
proof -
-  from assms have "(w n,s(''x'':=0,''y'':=0)) \<Rightarrow> t" by auto
+  from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto
from while_sum[OF this] show ?thesis by simp
qed

@@ -50,20 +49,18 @@
text{* Note that we deal with sequences of commands from right to left,
pulling back the postcondition towards the precondition. *}

-lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0;; ''y'' ::= N 0;; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
+lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = \<Sum> {1 .. n}}"
apply(rule hoare.Seq)
prefer 2
-apply(rule While'
-  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"])
+apply(rule While' [where P = "\<lambda>s. (s ''y'' = \<Sum> {1..n} - \<Sum> {1 .. s ''x''})"])
apply(rule Seq)
prefer 2
apply(rule Assign)
apply(rule Assign')
-apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps)
-apply(fastforce)
-apply(rule Seq)
-prefer 2
-apply(rule Assign)
+apply simp