simplified example and proof
authornipkow
Wed May 22 08:46:39 2013 +0200 (2013-05-22 ago)
changeset 5210806db08182c4b
parent 52107 0c21dffc177a
child 52109 39ac12f31f5c
child 52111 1fd184eaa310
simplified example and proof
src/HOL/IMP/Hoare_Examples.thy
     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.26 -lemma setsum_head_plus_1:
    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.39 -apply(auto simp add: setsum_head_plus_1)
    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.42 +apply(auto simp add: set_ivl_lemma)
    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