--- a/src/HOL/ex/Execute_Choice.thy Wed Feb 17 11:01:01 2010 +0100
+++ b/src/HOL/ex/Execute_Choice.thy Wed Feb 17 11:21:59 2010 +0100
@@ -6,9 +6,18 @@
imports Main AssocList
begin
-definition valuesum :: "('a, 'b :: comm_monoid_add) mapping \<Rightarrow> 'b" where
+text {*
+ A trivial example:
+*}
+
+definition valuesum :: "('a, 'b :: ab_group_add) mapping \<Rightarrow> 'b" where
"valuesum m = (\<Sum>k \<in> Mapping.keys m. the (Mapping.lookup m k))"
+text {*
+ Not that instead of defining @{term valuesum} with choice, we define it
+ directly and derive a description involving choice afterwards:
+*}
+
lemma valuesum_rec:
assumes fin: "finite (dom (Mapping.lookup m))"
shows "valuesum m = (if Mapping.is_empty m then 0 else
@@ -35,30 +44,59 @@
then show ?thesis by (simp add: keys_def valuesum_def is_empty_def)
qed
+text {*
+ In the context of the else-branch we can show that the exact choice is
+ irrelvant; in practice, finding this point where choice becomes irrelevant is the
+ most difficult thing!
+*}
+
+lemma valuesum_choice:
+ "finite (Mapping.keys M) \<Longrightarrow> x \<in> Mapping.keys M \<Longrightarrow> y \<in> Mapping.keys M \<Longrightarrow>
+ the (Mapping.lookup M x) + valuesum (Mapping.delete x M) =
+ the (Mapping.lookup M y) + valuesum (Mapping.delete y M)"
+ by (simp add: valuesum_def keys_def setsum_diff)
+
+text {*
+ Given @{text valuesum_rec} as initial description, we stepwise refine it to something executable;
+ first, we formally insert the constructor @{term AList} and split the one equation into two,
+ where the second one provides the necessary context:
+*}
+
lemma valuesum_rec_AList:
- "valuesum (AList []) = 0"
- "valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in
+ shows [code]: "valuesum (AList []) = 0"
+ and "valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in
the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
by (simp_all add: valuesum_rec finite_dom_map_of is_empty_AList)
-axioms
- FIXME: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> C x = C y"
+text {*
+ As a side effect the precondition disappears (but note this has nothing to do with choice!).
+ The first equation deals with the uncritical empty case and can already be used for code generation.
-lemma aux: "(SOME l. l \<in> Mapping.keys (AList (x # xs))) = fst (hd (x # xs))"
-proof (rule FIXME)
- show "fst (hd (x # xs)) \<in> Mapping.keys (AList (x # xs))"
- by (simp add: keys_AList)
- show "(SOME l. l \<in> Mapping.keys (AList (x # xs))) \<in> Mapping.keys (AList (x # xs))"
- apply (rule someI) apply (simp add: keys_AList) apply auto
- done
-qed
+ Using @{text valuesum_choice}, we are able to prove an executable version of @{term valuesum}:
+*}
lemma valuesum_rec_exec [code]:
- "valuesum (AList []) = 0"
"valuesum (AList (x # xs)) = (let l = fst (hd (x # xs)) in
the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
- by (simp_all add: valuesum_rec_AList aux)
+proof -
+ let ?M = "AList (x # xs)"
+ let ?l1 = "(SOME l. l \<in> Mapping.keys ?M)"
+ let ?l2 = "fst (hd (x # xs))"
+ have "finite (Mapping.keys ?M)" by (simp add: keys_AList)
+ moreover have "?l1 \<in> Mapping.keys ?M"
+ by (rule someI) (auto simp add: keys_AList)
+ moreover have "?l2 \<in> Mapping.keys ?M"
+ by (simp add: keys_AList)
+ ultimately have "the (Mapping.lookup ?M ?l1) + valuesum (Mapping.delete ?l1 ?M) =
+ the (Mapping.lookup ?M ?l2) + valuesum (Mapping.delete ?l2 ?M)"
+ by (rule valuesum_choice)
+ then show ?thesis by (simp add: valuesum_rec_AList)
+qed
+
+text {*
+ See how it works:
+*}
-value "valuesum (AList [(''abc'', (42::nat)), (''def'', 1705)])"
+value "valuesum (AList [(''abc'', (42::int)), (''def'', 1705)])"
end
--- a/src/HOL/ex/ROOT.ML Wed Feb 17 11:01:01 2010 +0100
+++ b/src/HOL/ex/ROOT.ML Wed Feb 17 11:21:59 2010 +0100
@@ -66,7 +66,8 @@
"Refute_Examples",
"Quickcheck_Examples",
"Landau",
- "Execute_Choice"
+ "Execute_Choice",
+ "Summation"
];
HTML.with_charset "utf-8" (no_document use_thys)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Summation.thy Wed Feb 17 11:21:59 2010 +0100
@@ -0,0 +1,107 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Some basic facts about discrete summation *}
+
+theory Summation
+imports Main
+begin
+
+text {* Auxiliary. *}
+
+lemma add_setsum_orient:
+ "setsum f {k..<j} + setsum f {l..<k} = setsum f {l..<k} + setsum f {k..<j}"
+ by (fact plus.commute)
+
+lemma add_setsum_int:
+ fixes j k l :: int
+ shows "j < k \<Longrightarrow> k < l \<Longrightarrow> setsum f {j..<k} + setsum f {k..<l} = setsum f {j..<l}"
+ by (simp_all add: setsum_Un_Int [symmetric] ivl_disj_un)
+
+text {* The shift operator. *}
+
+definition \<Delta> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> 'a" where
+ "\<Delta> f k = f (k + 1) - f k"
+
+lemma \<Delta>_shift:
+ "\<Delta> (\<lambda>k. l + f k) = \<Delta> f"
+ by (simp add: \<Delta>_def expand_fun_eq)
+
+lemma \<Delta>_same_shift:
+ assumes "\<Delta> f = \<Delta> g"
+ shows "\<exists>l. (op +) l \<circ> f = g"
+proof -
+ fix k
+ from assms have "\<And>k. \<Delta> f k = \<Delta> g k" by simp
+ then have k_incr: "\<And>k. f (k + 1) - g (k + 1) = f k - g k"
+ by (simp add: \<Delta>_def algebra_simps)
+ then have "\<And>k. f ((k - 1) + 1) - g ((k - 1) + 1) = f (k - 1) - g (k - 1)"
+ by blast
+ then have k_decr: "\<And>k. f (k - 1) - g (k - 1) = f k - g k"
+ by simp
+ have "\<And>k. f k - g k = f 0 - g 0"
+ proof -
+ fix k
+ show "f k - g k = f 0 - g 0"
+ by (induct k rule: int_induct) (simp_all add: k_incr k_decr)
+ qed
+ then have "\<And>k. ((op +) (g 0 - f 0) \<circ> f) k = g k"
+ by (simp add: algebra_simps)
+ then have "(op +) (g 0 - f 0) \<circ> f = g" ..
+ then show ?thesis ..
+qed
+
+text {* The formal sum operator. *}
+
+definition \<Sigma> :: "(int \<Rightarrow> 'a\<Colon>ab_group_add) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a" where
+ "\<Sigma> f j l = (if j < l then setsum f {j..<l}
+ else if j > l then - setsum f {l..<j}
+ else 0)"
+
+lemma \<Sigma>_same [simp]:
+ "\<Sigma> f j j = 0"
+ by (simp add: \<Sigma>_def)
+
+lemma \<Sigma>_positive:
+ "j < l \<Longrightarrow> \<Sigma> f j l = setsum f {j..<l}"
+ by (simp add: \<Sigma>_def)
+
+lemma \<Sigma>_negative:
+ "j > l \<Longrightarrow> \<Sigma> f j l = - \<Sigma> f l j"
+ by (simp add: \<Sigma>_def)
+
+lemma add_\<Sigma>:
+ "\<Sigma> f j k + \<Sigma> f k l = \<Sigma> f j l"
+ by (simp add: \<Sigma>_def algebra_simps add_setsum_int)
+ (simp_all add: add_setsum_orient [of f k j l]
+ add_setsum_orient [of f j l k]
+ add_setsum_orient [of f j k l] add_setsum_int)
+
+lemma \<Sigma>_incr_upper:
+ "\<Sigma> f j (l + 1) = \<Sigma> f j l + f l"
+proof -
+ have "{l..<l+1} = {l}" by auto
+ then have "\<Sigma> f l (l + 1) = f l" by (simp add: \<Sigma>_def)
+ moreover have "\<Sigma> f j (l + 1) = \<Sigma> f j l + \<Sigma> f l (l + 1)" by (simp add: add_\<Sigma>)
+ ultimately show ?thesis by simp
+qed
+
+text {* Fundamental lemmas: The relation between @{term \<Delta>} and @{term \<Sigma>}. *}
+
+lemma \<Delta>_\<Sigma>:
+ "\<Delta> (\<Sigma> f j) = f"
+proof
+ fix k
+ show "\<Delta> (\<Sigma> f j) k = f k"
+ by (simp add: \<Delta>_def \<Sigma>_incr_upper)
+qed
+
+lemma \<Sigma>_\<Delta>:
+ "\<Sigma> (\<Delta> f) j l = f l - f j"
+proof -
+ from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
+ then obtain k where "(op +) k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
+ then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: expand_fun_eq)
+ then show ?thesis by simp
+qed
+
+end