# HG changeset patch # User blanchet # Date 1410513426 -7200 # Node ID 29b8688c5f76154667a8ea0183355c472d9421f6 # Parent f13f6e27d68e3c0707107c4694ef181ed4120b1d# Parent 44692d31a3994b9781019d15f9de04d132e988b3 merge diff -r f13f6e27d68e -r 29b8688c5f76 NEWS --- a/NEWS Fri Sep 12 11:16:47 2014 +0200 +++ b/NEWS Fri Sep 12 11:17:06 2014 +0200 @@ -23,6 +23,11 @@ *** HOL *** +* Bootstrap of listsum as special case of abstract product over lists. +Fact rename: + listsum_def ~> listsum.eq_foldr +INCOMPATIBILITY. + * Command and antiquotation "value" provide different evaluation slots (again), where the previous strategy (nbe after ML) serves as default. Minor INCOMPATIBILITY. diff -r f13f6e27d68e -r 29b8688c5f76 src/HOL/Groups_List.thy --- a/src/HOL/Groups_List.thy Fri Sep 12 11:16:47 2014 +0200 +++ b/src/HOL/Groups_List.thy Fri Sep 12 11:17:06 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 f13f6e27d68e -r 29b8688c5f76 src/HOL/ex/Transfer_Int_Nat.thy --- a/src/HOL/ex/Transfer_Int_Nat.thy Fri Sep 12 11:16:47 2014 +0200 +++ b/src/HOL/ex/Transfer_Int_Nat.thy Fri Sep 12 11:17:06 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 diff -r f13f6e27d68e -r 29b8688c5f76 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Fri Sep 12 11:16:47 2014 +0200 +++ b/src/Pure/Isar/class_declaration.ML Fri Sep 12 11:17:06 2014 +0200 @@ -146,14 +146,14 @@ let val param_Ts = (fold o fold_aterms) (fn Free (v, T) => if is_param v then fold_atyps (insert (op =)) T else I | _ => I) ts []; - val param_Ts_subst = map_filter (try dest_TVar) param_Ts; - val param_T = if null param_Ts_subst then NONE + val param_namesT = map_filter (try (fst o dest_TVar)) param_Ts; + val param_T = if null param_namesT then NONE else SOME (case get_first (try dest_TFree) param_Ts of SOME v_sort => TFree v_sort | - NONE => TVar ((fst o hd) param_Ts_subst, fold (inter_sort o snd) param_Ts_subst [])); + NONE => TVar (hd param_namesT, proto_base_sort)); in case param_T of NONE => ts | - SOME T => map (subst_TVars (map (rpair T o fst) param_Ts_subst)) ts + SOME T => map (subst_TVars (map (rpair T) param_namesT)) ts end; (* preprocessing elements, retrieving base sort from type-checked elements *)