# HG changeset patch # User haftmann # Date 1410469952 -7200 # Node ID 351810c45a4821a069f59100b04a3dad424bbbf4 # Parent 9228350683d05499af0243ea25249f84bf5fc3b6 abstract product over monoid for lists diff -r 9228350683d0 -r 351810c45a48 src/HOL/Groups_List.thy --- 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 \ 'a" where - "listsum xs = foldr plus xs 0" - -subsubsection {* List summation: @{const listsum} and @{text"\"}*} +no_notation times (infixl "*" 70) +no_notation Groups.one ("1") + +locale monoid_list = monoid +begin + +definition F :: "'a list \ '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 \ 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 \ '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 "\ = fold plus (x # xs) 0" by simp - also have "\ = foldr plus (rev xs @ [x]) 0" by (simp add: foldr_conv_fold) - also have "\ = listsum (rev xs @ [x])" by (simp add: listsum_def) - also have "\ = 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)" "\x\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 "\ = 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 \ set xs \ 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.. 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 diff -r 9228350683d0 -r 351810c45a48 src/HOL/ex/Transfer_Int_Nat.thy --- 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