author nipkow Wed May 22 08:46:39 2013 +0200 (2013-05-22 ago) changeset 52108 06db08182c4b parent 52107 0c21dffc177a child 52109 39ac12f31f5c child 52111 1fd184eaa310
simplified example and proof
```     1.1 --- a/src/HOL/IMP/Hoare_Examples.thy	Wed May 22 00:30:36 2013 +0200
1.2 +++ b/src/HOL/IMP/Hoare_Examples.thy	Wed May 22 08:46:39 2013 +0200
1.3 @@ -2,14 +2,11 @@
1.4
1.5  theory Hoare_Examples imports Hoare begin
1.6
1.7 -subsection{* Example: Sums *}
1.8 +text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
1.9
1.10 -text{* Summing up the first @{text n} natural numbers. The sum is accumulated
1.11 -in variable @{text x}, the loop counter is variable @{text y}. *}
1.12 -
1.13 -abbreviation "w n ==
1.14 -  WHILE Less (V ''y'') (N n)
1.15 -  DO ( ''y'' ::= Plus (V ''y'') (N 1);; ''x'' ::= Plus (V ''x'') (V ''y'') )"
1.16 +abbreviation "wsum ==
1.17 +  WHILE Less (N 0) (V ''x'')
1.18 +  DO (''y'' ::= Plus (V ''y'') (V ''x'');; ''x'' ::= Plus (V ''x'') (N -1))"
1.19
1.20  text{* For this example we make use of some predefined functions.  Function
1.21  @{const Setsum}, also written @{text"\<Sum>"}, sums up the elements of a set. The
1.22 @@ -19,14 +16,16 @@
1.23
1.24  text{* The behaviour of the loop is proved by induction: *}
1.25
1.27 -  "m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {m+1..n::int}"
1.28 -by (subst simp_from_to) simp
1.29 -
1.30 +lemma set_ivl_lemma:
1.31 +  "i \<le> j \<Longrightarrow> {i..j} = insert j {i..j - (1::int)}"
1.32 +apply(simp add:atLeastAtMost_def atLeast_def atMost_def del: simp_from_to)
1.33 +apply(fastforce)
1.34 +done
1.35 +
1.36  lemma while_sum:
1.37 -  "(w n, s) \<Rightarrow> t \<Longrightarrow> t ''x'' = s ''x'' + \<Sum> {s ''y'' + 1 .. n}"
1.38 -apply(induction "w n" s t rule: big_step_induct)
1.40 +  "(wsum, s) \<Rightarrow> t \<Longrightarrow> t ''y'' = s ''y'' + \<Sum> {1 .. s ''x''}"
1.41 +apply(induction wsum s t rule: big_step_induct)
1.43  done
1.44
1.45  text{* We were lucky that the proof was practically automatic, except for the
1.46 @@ -37,10 +36,10 @@
1.47  Now we prefix the loop with the necessary initialization: *}
1.48
1.49  lemma sum_via_bigstep:
1.50 -assumes "(''x'' ::= N 0;; ''y'' ::= N 0;; w n, s) \<Rightarrow> t"
1.51 -shows "t ''x'' = \<Sum> {1 .. n}"
1.52 +assumes "(''y'' ::= N 0;; wsum, s) \<Rightarrow> t"
1.53 +shows "t ''y'' = \<Sum> {1 .. s ''x''}"
1.54  proof -
1.55 -  from assms have "(w n,s(''x'':=0,''y'':=0)) \<Rightarrow> t" by auto
1.56 +  from assms have "(wsum,s(''y'':=0)) \<Rightarrow> t" by auto
1.57    from while_sum[OF this] show ?thesis by simp
1.58  qed
1.59
1.60 @@ -50,20 +49,18 @@
1.61  text{* Note that we deal with sequences of commands from right to left,
1.62  pulling back the postcondition towards the precondition. *}
1.63
1.64 -lemma "\<turnstile> {\<lambda>s. 0 <= n} ''x'' ::= N 0;; ''y'' ::= N 0;; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}"
1.65 +lemma "\<turnstile> {\<lambda>s. s ''x'' = n} ''y'' ::= N 0;; wsum {\<lambda>s. s ''y'' = \<Sum> {1 .. n}}"
1.66  apply(rule hoare.Seq)
1.67  prefer 2
1.68 -apply(rule While'
1.69 -  [where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n"])
1.70 +apply(rule While' [where P = "\<lambda>s. (s ''y'' = \<Sum> {1..n} - \<Sum> {1 .. s ''x''})"])
1.71  apply(rule Seq)
1.72  prefer 2
1.73  apply(rule Assign)
1.74  apply(rule Assign')
1.75 -apply(fastforce simp: atLeastAtMostPlus1_int_conv algebra_simps)
1.76 -apply(fastforce)
1.77 -apply(rule Seq)
1.78 -prefer 2
1.79 -apply(rule Assign)
1.80 +apply simp
1.81 +apply(simp add: algebra_simps set_ivl_lemma minus_numeral_simps(1)[symmetric]
1.82 +  del: minus_numeral_simps)
1.83 +apply(simp)
1.84  apply(rule Assign')
1.85  apply simp
1.86  done
```