# HG changeset patch
# User nipkow
# Date 1369562215 -7200
# Node ID 32b1dbda331c2a286b0c91838e81e6150ff4faab
# Parent  893b15200ec1ee0e167186c90ed82a873c5485bd
simpler proof through custom summation function

diff -r 893b15200ec1 -r 32b1dbda331c src/HOL/IMP/Hoare_Examples.thy
--- a/src/HOL/IMP/Hoare_Examples.thy	Sat May 25 18:30:38 2013 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy	Sun May 26 11:56:55 2013 +0200
@@ -4,31 +4,30 @@
 
 text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
 
+fun sum :: "int \<Rightarrow> int" where
+"sum i = (if i <= 0 then 0 else sum (i - 1) + i)"
+
+lemma [simp]: "0 < i \<Longrightarrow> sum i = sum (i - 1) + i" "i <= 0 \<Longrightarrow> sum i = 0"
+by(simp_all)
+
+declare sum.simps[simp del]
+
 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
-set of numbers from @{text m} to @{text n} is written @{term "{m .. n}"}. *}
 
 subsubsection{* Proof by Operational Semantics *}
 
 text{* The behaviour of the loop is proved by induction: *}
 
-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)
+lemma while_sum:
+  "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + sum(s ''x'')"
+apply(induction wsum s t rule: big_step_induct)
+apply(auto)
 done
 
-lemma while_sum:
-  "(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
+text{* We were lucky that the proof was automatic, except for the
 induction. In general, such proofs will not be so easy. The automation is
 partly due to the right inversion rules that we set up as automatic
 elimination rules that decompose big-step premises.
@@ -36,8 +35,8 @@
 Now we prefix the loop with the necessary initialization: *}
 
 lemma sum_via_bigstep:
-assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t"
-shows "t ''y'' = \<Sum> {1 .. s ''x''}"
+  assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t"
+  shows "t ''y'' = sum (s ''x'')"
 proof -
   from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto
   from while_sum[OF this] show ?thesis by simp
@@ -49,18 +48,17 @@
 text{* Note that we deal with sequences of commands from right to left,
 pulling back the postcondition towards the precondition. *}
 
-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 ''y'' = \<Sum> {1..n} - \<Sum> {1 .. s ''x''})"])
+lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = sum n}"
 apply(rule Seq)
-prefer 2
-apply(rule Assign)
-apply(rule Assign')
-apply simp
-apply(simp add: algebra_simps set_ivl_lemma minus_numeral_simps(1)[symmetric]
-  del: minus_numeral_simps)
-apply(simp)
+ prefer 2
+ apply(rule While' [where P = "\<lambda>s. (s ''y'' = sum n - sum(s ''x''))"])
+  apply(rule Seq)
+   prefer 2
+   apply(rule Assign)
+  apply(rule Assign')
+  apply simp
+  apply(simp add: minus_numeral_simps(1)[symmetric] del: minus_numeral_simps)
+ apply(simp)
 apply(rule Assign')
 apply simp
 done