more lemmas
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Fri Oct 07 17:57:17 2016 +0200 (2016-10-07)
changeset 640753d4c3eec5143
parent 64074 7dccbbd8d71d
child 64076 9f089287687b
more lemmas
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Oct 07 10:45:21 2016 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Oct 07 17:57:17 2016 +0200
     1.3 @@ -2061,6 +2061,15 @@
     1.4  locale comm_monoid_mset = comm_monoid
     1.5  begin
     1.6  
     1.7 +interpretation comp_fun_commute f
     1.8 +  by standard (simp add: fun_eq_iff left_commute)
     1.9 +
    1.10 +interpretation comp?: comp_fun_commute "f \<circ> g"
    1.11 +  by (fact comp_comp_fun_commute)
    1.12 +
    1.13 +context
    1.14 +begin
    1.15 +
    1.16  definition F :: "'a multiset \<Rightarrow> 'a"
    1.17    where eq_fold: "F M = fold_mset f \<^bold>1 M"
    1.18  
    1.19 @@ -2085,6 +2094,43 @@
    1.20  lemma add_mset [simp]: "F (add_mset x N) = x \<^bold>* F N"
    1.21    unfolding add_mset_add_single[of x N] union by (simp add: ac_simps)
    1.22  
    1.23 +lemma insert [simp]:
    1.24 +  shows "F (image_mset g (add_mset x A)) = g x \<^bold>* F (image_mset g A)"
    1.25 +  by (simp add: eq_fold)
    1.26 +
    1.27 +lemma remove:
    1.28 +  assumes "x \<in># A"
    1.29 +  shows "F A = x \<^bold>* F (A - {#x#})"
    1.30 +  using multi_member_split[OF assms] by auto
    1.31 +
    1.32 +lemma neutral:
    1.33 +  "\<forall>x\<in>#A. x = \<^bold>1 \<Longrightarrow> F A = \<^bold>1"
    1.34 +  by (induct A) simp_all
    1.35 +
    1.36 +lemma neutral_const [simp]:
    1.37 +  "F (image_mset (\<lambda>_. \<^bold>1) A) = \<^bold>1"
    1.38 +  by (simp add: neutral)
    1.39 +
    1.40 +private lemma F_image_mset_product:
    1.41 +  "F {#g x j \<^bold>* F {#g i j. i \<in># A#}. j \<in># B#} =
    1.42 +    F (image_mset (g x) B) \<^bold>* F {#F {#g i j. i \<in># A#}. j \<in># B#}"
    1.43 +  by (induction B) (simp_all add: left_commute semigroup.assoc semigroup_axioms)
    1.44 +
    1.45 +lemma commute:
    1.46 +  "F (image_mset (\<lambda>i. F (image_mset (g i) B)) A) =
    1.47 +    F (image_mset (\<lambda>j. F (image_mset (\<lambda>i. g i j) A)) B)"
    1.48 +  apply (induction A, simp)
    1.49 +  apply (induction B, auto simp add: F_image_mset_product ac_simps)
    1.50 +  done
    1.51 +
    1.52 +lemma distrib: "F (image_mset (\<lambda>x. g x \<^bold>* h x) A) = F (image_mset g A) \<^bold>* F (image_mset h A)"
    1.53 +  by (induction A) (auto simp: ac_simps)
    1.54 +
    1.55 +lemma union_disjoint:
    1.56 +  "A \<inter># B = {#} \<Longrightarrow> F (image_mset g (A \<union># B)) = F (image_mset g A) \<^bold>* F (image_mset g B)"
    1.57 +  by (induction A) (auto simp: ac_simps)
    1.58 +
    1.59 +end
    1.60  end
    1.61  
    1.62  lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute (op + :: 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
    1.63 @@ -2156,6 +2202,26 @@
    1.64    shows "c * (\<Sum>x \<in># M. f x) = (\<Sum>x \<in># M. c * f(x))"
    1.65  by (induction M) (simp_all add: distrib_left)
    1.66  
    1.67 +lemma sum_mset_distrib_right:
    1.68 +  fixes f :: "'a \<Rightarrow> 'b::semiring_0"
    1.69 +  shows "(\<Sum>b \<in># B. f b) * a = (\<Sum>b \<in># B. f b * a)"
    1.70 +  by (induction B) (auto simp: distrib_right)
    1.71 +
    1.72 +lemma sum_mset_constant [simp]:
    1.73 +  fixes y :: "'b::semiring_1"
    1.74 +  shows \<open>(\<Sum>x\<in>#A. y) = of_nat (size A) * y\<close>
    1.75 +  by (induction A) (auto simp: algebra_simps)
    1.76 +
    1.77 +lemma (in ordered_comm_monoid_add) sum_mset_mono:
    1.78 +  assumes "\<And>i. i \<in># K \<Longrightarrow> f i \<le> g i"
    1.79 +  shows "sum_mset (image_mset f K) \<le> sum_mset (image_mset g K)"
    1.80 +  using assms by (induction K) (simp_all add: local.add_mono)
    1.81 +
    1.82 +lemma sum_mset_product:
    1.83 +  fixes f :: "'a::{comm_monoid_add,times} \<Rightarrow> 'b::semiring_0"
    1.84 +  shows "(\<Sum>i \<in># A. f i) * (\<Sum>i \<in># B. g i) = (\<Sum>i\<in>#A. \<Sum>j\<in>#B. f i * g j)"
    1.85 +  by (subst sum_mset.commute) (simp add: sum_mset_distrib_left sum_mset_distrib_right)
    1.86 +
    1.87  abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
    1.88    where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
    1.89      could likewise refer to \<open>\<Squnion>#\<close>\<close>