--- a/src/HOL/Groups_List.thy Thu Sep 11 18:33:56 2014 +0200
+++ b/src/HOL/Groups_List.thy Thu Sep 11 23:12:32 2014 +0200
@@ -1,43 +1,108 @@
(* Author: Tobias Nipkow, TU Muenchen *)
-header {* Summation over lists *}
+header {* Sum over lists *}
theory Groups_List
imports List
begin
-definition (in monoid_add) listsum :: "'a list \<Rightarrow> 'a" where
- "listsum xs = foldr plus xs 0"
-
-subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
+no_notation times (infixl "*" 70)
+no_notation Groups.one ("1")
+
+locale monoid_list = monoid
+begin
+
+definition F :: "'a list \<Rightarrow> 'a"
+where
+ eq_foldr [code]: "F xs = foldr f xs 1"
+
+lemma Nil [simp]:
+ "F [] = 1"
+ by (simp add: eq_foldr)
+
+lemma Cons [simp]:
+ "F (x # xs) = x * F xs"
+ by (simp add: eq_foldr)
+
+lemma append [simp]:
+ "F (xs @ ys) = F xs * F ys"
+ by (induct xs) (simp_all add: assoc)
+
+end
-lemma (in monoid_add) listsum_simps [simp]:
- "listsum [] = 0"
- "listsum (x # xs) = x + listsum xs"
- by (simp_all add: listsum_def)
+locale comm_monoid_list = comm_monoid + monoid_list
+begin
+
+lemma rev [simp]:
+ "F (rev xs) = F xs"
+ by (simp add: eq_foldr foldr_fold fold_rev fun_eq_iff assoc left_commute)
+
+end
+
+locale comm_monoid_list_set = list: comm_monoid_list + set: comm_monoid_set
+begin
-lemma (in monoid_add) listsum_append [simp]:
- "listsum (xs @ ys) = listsum xs + listsum ys"
- by (induct xs) (simp_all add: add.assoc)
+lemma distinct_set_conv_list:
+ "distinct xs \<Longrightarrow> set.F g (set xs) = list.F (map g xs)"
+ by (induct xs) simp_all
-lemma (in comm_monoid_add) listsum_rev [simp]:
- "listsum (rev xs) = listsum xs"
- by (simp add: listsum_def foldr_fold fold_rev fun_eq_iff add_ac)
+lemma set_conv_list [code]:
+ "set.F g (set xs) = list.F (map g (remdups xs))"
+ by (simp add: distinct_set_conv_list [symmetric])
+
+end
+
+notation times (infixl "*" 70)
+notation Groups.one ("1")
+
+
+subsection {* List summation *}
+
+context monoid_add
+begin
+
+definition listsum :: "'a list \<Rightarrow> 'a"
+where
+ "listsum = monoid_list.F plus 0"
-lemma (in monoid_add) fold_plus_listsum_rev:
- "fold plus xs = plus (listsum (rev xs))"
-proof
- fix x
- have "fold plus xs x = fold plus xs (x + 0)" by simp
- also have "\<dots> = fold plus (x # xs) 0" by simp
- also have "\<dots> = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_conv_fold)
- also have "\<dots> = listsum (rev xs @ [x])" by (simp add: listsum_def)
- also have "\<dots> = listsum (rev xs) + listsum [x]" by simp
- finally show "fold plus xs x = listsum (rev xs) + x" by simp
+sublocale listsum!: monoid_list plus 0
+where
+ "monoid_list.F plus 0 = listsum"
+proof -
+ show "monoid_list plus 0" ..
+ then interpret listsum!: monoid_list plus 0 .
+ from listsum_def show "monoid_list.F plus 0 = listsum" by rule
+qed
+
+end
+
+context comm_monoid_add
+begin
+
+sublocale listsum!: comm_monoid_list plus 0
+where
+ "monoid_list.F plus 0 = listsum"
+proof -
+ show "comm_monoid_list plus 0" ..
+ then interpret listsum!: comm_monoid_list plus 0 .
+ from listsum_def show "monoid_list.F plus 0 = listsum" by rule
qed
-text{* Some syntactic sugar for summing a function over a list: *}
+sublocale setsum!: comm_monoid_list_set plus 0
+where
+ "monoid_list.F plus 0 = listsum"
+ and "comm_monoid_set.F plus 0 = setsum"
+proof -
+ show "comm_monoid_list_set plus 0" ..
+ then interpret setsum!: comm_monoid_list_set plus 0 .
+ from listsum_def show "monoid_list.F plus 0 = listsum" by rule
+ from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
+qed
+
+end
+
+text {* Some syntactic sugar for summing a function over a list: *}
syntax
"_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
@@ -50,6 +115,23 @@
"SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
"\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
+text {* TODO duplicates *}
+lemmas listsum_simps = listsum.Nil listsum.Cons
+lemmas listsum_append = listsum.append
+lemmas listsum_rev = listsum.rev
+
+lemma (in monoid_add) fold_plus_listsum_rev:
+ "fold plus xs = plus (listsum (rev xs))"
+proof
+ fix x
+ have "fold plus xs x = listsum (rev xs @ [x])"
+ by (simp add: foldr_conv_fold listsum.eq_foldr)
+ also have "\<dots> = listsum (rev xs) + x"
+ by simp
+ finally show "fold plus xs x = listsum (rev xs) + x"
+ .
+qed
+
lemma (in comm_monoid_add) listsum_map_remove1:
"x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
by (induct xs) (auto simp add: ac_simps)
@@ -183,6 +265,8 @@
subsection {* Tools setup *}
+lemmas setsum_code = setsum.set_conv_list
+
lemma setsum_set_upto_conv_listsum_int [code_unfold]:
"setsum f (set [i..j::int]) = listsum (map f [i..j])"
by (simp add: interv_listsum_conv_setsum_set_int)
@@ -191,10 +275,6 @@
"setsum f (set [m..<n]) = listsum (map f [m..<n])"
by (simp add: interv_listsum_conv_setsum_set_nat)
-lemma setsum_code [code]:
- "setsum f (set xs) = listsum (map f (remdups xs))"
- by (simp add: listsum_distinct_conv_setsum_set)
-
context
begin
@@ -204,9 +284,9 @@
assumes [transfer_rule]: "A 0 0"
assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
shows "(list_all2 A ===> A) listsum listsum"
- unfolding listsum_def[abs_def]
+ unfolding listsum.eq_foldr [abs_def]
by transfer_prover
end
-end
\ No newline at end of file
+end
--- a/src/HOL/ex/Transfer_Int_Nat.thy Thu Sep 11 18:33:56 2014 +0200
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Thu Sep 11 23:12:32 2014 +0200
@@ -118,7 +118,7 @@
method to help generate transfer rules. *}
lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum"
- unfolding listsum_def [abs_def] by transfer_prover
+ by transfer_prover
end