1.1 --- a/src/HOL/ex/Execute_Choice.thy	Wed Feb 17 11:01:01 2010 +0100
     1.2 +++ b/src/HOL/ex/Execute_Choice.thy	Wed Feb 17 11:21:59 2010 +0100
     1.3 @@ -6,9 +6,18 @@
     1.4  imports Main AssocList
     1.5  begin
     1.6  
     1.7 -definition valuesum :: "('a, 'b :: comm_monoid_add) mapping \<Rightarrow> 'b" where
     1.8 +text {*
     1.9 +  A trivial example:
    1.10 +*}
    1.11 +
    1.12 +definition valuesum :: "('a, 'b :: ab_group_add) mapping \<Rightarrow> 'b" where
    1.13    "valuesum m = (\<Sum>k \<in> Mapping.keys m. the (Mapping.lookup m k))"
    1.14  
    1.15 +text {*
    1.16 +  Not that instead of defining @{term valuesum} with choice, we define it
    1.17 +  directly and derive a description involving choice afterwards:
    1.18 +*}
    1.19 +
    1.20  lemma valuesum_rec:
    1.21    assumes fin: "finite (dom (Mapping.lookup m))"
    1.22    shows "valuesum m = (if Mapping.is_empty m then 0 else
    1.23 @@ -35,30 +44,59 @@
    1.24    then show ?thesis by (simp add: keys_def valuesum_def is_empty_def)
    1.25  qed
    1.26  
    1.27 +text {*
    1.28 +  In the context of the else-branch we can show that the exact choice is
    1.29 +  irrelvant; in practice, finding this point where choice becomes irrelevant is the
    1.30 +  most difficult thing!
    1.31 +*}
    1.32 +
    1.33 +lemma valuesum_choice:
    1.34 +  "finite (Mapping.keys M) \<Longrightarrow> x \<in> Mapping.keys M \<Longrightarrow> y \<in> Mapping.keys M \<Longrightarrow>
    1.35 +    the (Mapping.lookup M x) + valuesum (Mapping.delete x M) =
    1.36 +    the (Mapping.lookup M y) + valuesum (Mapping.delete y M)"
    1.37 +  by (simp add: valuesum_def keys_def setsum_diff)
    1.38 +
    1.39 +text {*
    1.40 +  Given @{text valuesum_rec} as initial description, we stepwise refine it to something executable;
    1.41 +  first, we formally insert the constructor @{term AList} and split the one equation into two,
    1.42 +  where the second one provides the necessary context:
    1.43 +*}
    1.44 +
    1.45  lemma valuesum_rec_AList:
    1.46 -  "valuesum (AList []) = 0"
    1.47 -  "valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in
    1.48 +  shows [code]: "valuesum (AList []) = 0"
    1.49 +  and "valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in
    1.50      the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
    1.51    by (simp_all add: valuesum_rec finite_dom_map_of is_empty_AList)
    1.52  
    1.53 -axioms
    1.54 -  FIXME: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> C x = C y"
    1.55 +text {*
    1.56 +  As a side effect the precondition disappears (but note this has nothing to do with choice!).
    1.57 +  The first equation deals with the uncritical empty case and can already be used for code generation.
    1.58  
    1.59 -lemma aux: "(SOME l. l \<in> Mapping.keys (AList (x # xs))) = fst (hd (x # xs))"
    1.60 -proof (rule FIXME)
    1.61 -  show "fst (hd (x # xs)) \<in> Mapping.keys (AList (x # xs))"
    1.62 -    by (simp add: keys_AList)
    1.63 -  show "(SOME l. l \<in> Mapping.keys (AList (x # xs))) \<in> Mapping.keys (AList (x # xs))"
    1.64 -    apply (rule someI) apply (simp add: keys_AList) apply auto
    1.65 -    done
    1.66 -qed
    1.67 +  Using @{text valuesum_choice}, we are able to prove an executable version of @{term valuesum}:
    1.68 +*}
    1.69  
    1.70  lemma valuesum_rec_exec [code]:
    1.71 -  "valuesum (AList []) = 0"
    1.72    "valuesum (AList (x # xs)) = (let l = fst (hd (x # xs)) in
    1.73      the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
    1.74 -  by (simp_all add: valuesum_rec_AList aux)
    1.75 +proof -
    1.76 +  let ?M = "AList (x # xs)"
    1.77 +  let ?l1 = "(SOME l. l \<in> Mapping.keys ?M)"
    1.78 +  let ?l2 = "fst (hd (x # xs))"
    1.79 +  have "finite (Mapping.keys ?M)" by (simp add: keys_AList)
    1.80 +  moreover have "?l1 \<in> Mapping.keys ?M"
    1.81 +    by (rule someI) (auto simp add: keys_AList)
    1.82 +  moreover have "?l2 \<in> Mapping.keys ?M"
    1.83 +    by (simp add: keys_AList)
    1.84 +  ultimately have "the (Mapping.lookup ?M ?l1) + valuesum (Mapping.delete ?l1 ?M) =
    1.85 +    the (Mapping.lookup ?M ?l2) + valuesum (Mapping.delete ?l2 ?M)"
    1.86 +    by (rule valuesum_choice)
    1.87 +  then show ?thesis by (simp add: valuesum_rec_AList)
    1.88 +qed
    1.89 +  
    1.90 +text {*
    1.91 +  See how it works:
    1.92 +*}
    1.93  
    1.94 -value "valuesum (AList [(''abc'', (42::nat)), (''def'', 1705)])"
    1.95 +value "valuesum (AList [(''abc'', (42::int)), (''def'', 1705)])"
    1.96  
    1.97  end

     2.1 --- a/src/HOL/ex/ROOT.ML	Wed Feb 17 11:01:01 2010 +0100
     2.2 +++ b/src/HOL/ex/ROOT.ML	Wed Feb 17 11:21:59 2010 +0100
     2.3 @@ -66,7 +66,8 @@
     2.4    "Refute_Examples",
     2.5    "Quickcheck_Examples",
     2.6    "Landau",
     2.7 -  "Execute_Choice"
     2.8 +  "Execute_Choice",
     2.9 +  "Summation"
    2.10  ];
    2.11  
    2.12  HTML.with_charset "utf-8" (no_document use_thys)

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Summation.thy	Wed Feb 17 11:21:59 2010 +0100
     3.3 @@ -0,0 +1,107 @@
     3.4 +(* Author: Florian Haftmann, TU Muenchen *)
     3.5 +
     3.6 +header {* Some basic facts about discrete summation *}
     3.7 +
     3.8 +theory Summation
     3.9 +imports Main
    3.10 +begin
    3.11 +
    3.12 +text {* Auxiliary. *}
    3.13 +
    3.14 +lemma add_setsum_orient:
    3.15 +  "setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
    3.16 +  by (fact plus.commute)
    3.17 +
    3.18 +lemma add_setsum_int:
    3.19 +  fixes j k l :: int
    3.20 +  shows "j < k \<Longrightarrow> k < l \<Longrightarrow> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}"
    3.21 +  by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un)
    3.22 +
    3.23 +text {* The shift operator. *}
    3.24 +
    3.25 +definition \<Delta> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> 'a" where
    3.26 +  "\<Delta> f k = f (k + 1) - f k"
    3.27 +
    3.28 +lemma \<Delta>_shift:
    3.29 +  "\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
    3.30 +  by (simp add: \<Delta>_def expand_fun_eq)
    3.31 +
    3.32 +lemma \<Delta>_same_shift:
    3.33 +  assumes "\<Delta> f = \<Delta> g"
    3.34 +  shows "\<exists>l. (op +) l \<circ> f = g"
    3.35 +proof -
    3.36 +  fix k
    3.37 +  from assms have "\<And>k. \<Delta> f k = \<Delta> g k" by simp
    3.38 +  then have k_incr: "\<And>k. f (k + 1) - g (k + 1) = f k - g k"
    3.39 +    by (simp add: \<Delta>_def algebra_simps)
    3.40 +  then have "\<And>k. f ((k - 1) + 1) - g ((k - 1) + 1) = f (k - 1) - g (k - 1)"
    3.41 +    by blast
    3.42 +  then have k_decr: "\<And>k. f (k - 1) - g (k - 1) = f k - g k"
    3.43 +    by simp
    3.44 +  have "\<And>k. f k - g k = f 0 - g 0"
    3.45 +  proof -
    3.46 +    fix k
    3.47 +    show "f k - g k = f 0 - g 0"
    3.48 +      by (induct k rule: int_induct) (simp_all add: k_incr k_decr)
    3.49 +  qed
    3.50 +  then have "\<And>k. ((op +) (g 0 - f 0) \<circ> f) k = g k"
    3.51 +    by (simp add: algebra_simps)
    3.52 +  then have "(op +) (g 0 - f 0) \<circ> f = g" ..
    3.53 +  then show ?thesis ..
    3.54 +qed
    3.55 +
    3.56 +text {* The formal sum operator. *}
    3.57 +
    3.58 +definition \<Sigma> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a" where
    3.59 +  "\<Sigma> f j l = (if j < l then setsum f {j..<l}
    3.60 +    else if j > l then - setsum f {l..<j}
    3.61 +    else 0)"
    3.62 +
    3.63 +lemma \<Sigma>_same [simp]:
    3.64 +  "\<Sigma> f j j = 0"
    3.65 +  by (simp add: \<Sigma>_def)
    3.66 +
    3.67 +lemma \<Sigma>_positive:
    3.68 +  "j < l \<Longrightarrow> \<Sigma> f j l = setsum f {j..<l}"
    3.69 +  by (simp add: \<Sigma>_def)
    3.70 +
    3.71 +lemma \<Sigma>_negative:
    3.72 +  "j > l \<Longrightarrow> \<Sigma> f j l = - \<Sigma> f l j"
    3.73 +  by (simp add: \<Sigma>_def)
    3.74 +
    3.75 +lemma add_\<Sigma>:
    3.76 +  "\<Sigma> f j k + \<Sigma> f k l = \<Sigma> f j l"
    3.77 +  by (simp add: \<Sigma>_def algebra_simps add_setsum_int)
    3.78 +   (simp_all add: add_setsum_orient [of f k j l]
    3.79 +      add_setsum_orient [of f j l k]
    3.80 +      add_setsum_orient [of f j k l] add_setsum_int)
    3.81 +
    3.82 +lemma \<Sigma>_incr_upper:
    3.83 +  "\<Sigma> f j (l + 1) = \<Sigma> f j l + f l"
    3.84 +proof -
    3.85 +  have "{l..<l+1} = {l}" by auto
    3.86 +  then have "\<Sigma> f l (l + 1) = f l" by (simp add: \<Sigma>_def)
    3.87 +  moreover have "\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)" by (simp add: add_\<Sigma>)
    3.88 +  ultimately show ?thesis by simp
    3.89 +qed
    3.90 +
    3.91 +text {* Fundamental lemmas: The relation between @{term \<Delta>} and @{term \<Sigma>}. *}
    3.92 +
    3.93 +lemma \<Delta>_\<Sigma>:
    3.94 +  "\<Delta> (\<Sigma> f j) = f"
    3.95 +proof
    3.96 +  fix k
    3.97 +  show "\<Delta> (\<Sigma> f j) k = f k"
    3.98 +    by (simp add: \<Delta>_def \<Sigma>_incr_upper)
    3.99 +qed
   3.100 +
   3.101 +lemma \<Sigma>_\<Delta>:
   3.102 +  "\<Sigma> (\<Delta> f) j l = f l - f j"
   3.103 +proof -
   3.104 +  from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
   3.105 +  then obtain k where "(op +) k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
   3.106 +  then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: expand_fun_eq)
   3.107 +  then show ?thesis by simp
   3.108 +qed
   3.109 +
   3.110 +end