# HG changeset patch
# User nipkow
# Date 1369205199 -7200
# Node ID 06db08182c4bb59bc6203924529c938a033a313e
# Parent  0c21dffc177ab9704f21c22cf833fb28a54ebf52
simplified example and proof

diff -r 0c21dffc177a -r 06db08182c4b src/HOL/IMP/Hoare_Examples.thy
--- 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: *}
 
-lemma setsum_head_plus_1:
-  "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)
-apply(auto simp add: setsum_head_plus_1)
+  "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + \<Sum> {1 .. s ''x''}"
+apply(induction wsum s t rule: big_step_induct)
+apply(auto simp add: set_ivl_lemma)
 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
+apply(simp add: algebra_simps set_ivl_lemma minus_numeral_simps(1)[symmetric]
+  del: minus_numeral_simps)
+apply(simp)
 apply(rule Assign')
 apply simp
 done