tuning multisets
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Fri Oct 07 17:58:36 2016 +0200 (2016-10-07)
changeset 640769f089287687b
parent 64075 3d4c3eec5143
child 64077 6d770c2dc60d
tuning multisets
NEWS
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
     1.1 --- a/NEWS	Fri Oct 07 17:57:17 2016 +0200
     1.2 +++ b/NEWS	Fri Oct 07 17:58:36 2016 +0200
     1.3 @@ -592,6 +592,13 @@
     1.4      le_multiset_plus_plus_right_iff ~> add_less_cancel_left
     1.5      add_eq_self_empty_iff ~> add_cancel_left_right
     1.6      mset_subset_add_bothsides ~> subset_mset.add_less_cancel_right
     1.7 +    empty_inter ~> subset_mset.inf_bot_left
     1.8 +    inter_empty ~> subset_mset.inf_bot_right
     1.9 +    empty_sup ~> subset_mset.sup_bot_left
    1.10 +    sup_empty ~> subset_mset.sup_bot_right
    1.11 +    bdd_below_multiset ~> subset_mset.bdd_above_bot
    1.12 +    subset_eq_empty ~> subset_mset.le_zero_eq
    1.13 +    mset_subset_empty_nonempty ~> subset_mset.zero_less_iff_neq_zero
    1.14  
    1.15  * HOL-Library: some typeclass constraints about multisets have been
    1.16  reduced from ordered or linordered to preorder. Multisets have the
     2.1 --- a/src/HOL/Library/Multiset.thy	Fri Oct 07 17:57:17 2016 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Fri Oct 07 17:58:36 2016 +0200
     2.3 @@ -522,7 +522,6 @@
     2.4  
     2.5  interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
     2.6    by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
     2.7 -  \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
     2.8  
     2.9  interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<le>#" "op <#"
    2.10    by standard
    2.11 @@ -644,27 +643,21 @@
    2.12    "A - C \<subseteq># B \<longleftrightarrow> A \<subseteq># B + C"
    2.13    by (simp add: subseteq_mset_def le_diff_conv)
    2.14  
    2.15 -lemma subset_eq_empty[simp]: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
    2.16 -  by auto
    2.17 -
    2.18  lemma multi_psub_of_add_self [simp]: "A \<subset># add_mset x A"
    2.19    by (auto simp: subset_mset_def subseteq_mset_def)
    2.20  
    2.21 -lemma multi_psub_self[simp]: "(A::'a multiset) \<subset># A = False"
    2.22 +lemma multi_psub_self: "A \<subset># A = False"
    2.23    by simp
    2.24  
    2.25  lemma mset_subset_add_mset [simp]: "add_mset x N \<subset># add_mset x M \<longleftrightarrow> N \<subset># M"
    2.26    unfolding add_mset_add_single[of _ N] add_mset_add_single[of _ M]
    2.27    by (fact subset_mset.add_less_cancel_right)
    2.28  
    2.29 -lemma mset_subset_empty_nonempty: "{#} \<subset># S \<longleftrightarrow> S \<noteq> {#}"
    2.30 -  by (fact subset_mset.zero_less_iff_neq_zero)
    2.31 -
    2.32  lemma mset_subset_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
    2.33    by (auto simp: subset_mset_def elim: mset_add)
    2.34  
    2.35  
    2.36 -subsubsection \<open>Intersection\<close>
    2.37 +subsubsection \<open>Intersection and bounded union\<close>
    2.38  
    2.39  definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "\<inter>#" 70) where
    2.40    multiset_inter_def: "inf_subset_mset A B = A - (A - B)"
    2.41 @@ -678,6 +671,25 @@
    2.42  qed
    2.43    \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    2.44  
    2.45 +definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "\<union>#" 70)
    2.46 +  where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close>
    2.47 +
    2.48 +interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#"
    2.49 +proof -
    2.50 +  have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
    2.51 +    by arith
    2.52 +  show "class.semilattice_sup op \<union># op \<subseteq># op \<subset>#"
    2.53 +    by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
    2.54 +qed
    2.55 +  \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    2.56 +
    2.57 +interpretation subset_mset: bounded_lattice_bot "op \<inter>#" "op \<subseteq>#" "op \<subset>#"
    2.58 +  "op \<union>#" "{#}"
    2.59 +  by standard auto
    2.60 +
    2.61 +
    2.62 +subsubsection \<open>Additional intersection facts\<close>
    2.63 +
    2.64  lemma multiset_inter_count [simp]:
    2.65    fixes A B :: "'a multiset"
    2.66    shows "count (A \<inter># B) x = min (count A x) (count B x)"
    2.67 @@ -752,12 +764,6 @@
    2.68    "{#} = A \<inter># add_mset b B \<longleftrightarrow> b \<notin># A \<and> {#} = A \<inter># B"
    2.69    by (auto simp: disjunct_not_in)
    2.70  
    2.71 -lemma empty_inter[simp]: "{#} \<inter># M = {#}"
    2.72 -  by (simp add: multiset_eq_iff)
    2.73 -
    2.74 -lemma inter_empty[simp]: "M \<inter># {#} = {#}"
    2.75 -  by (simp add: multiset_eq_iff)
    2.76 -
    2.77  lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) \<inter># N = M \<inter># N"
    2.78    by (simp add: multiset_eq_iff not_in_iff)
    2.79  
    2.80 @@ -813,23 +819,7 @@
    2.81    by (auto simp add: subseteq_mset_def)
    2.82  
    2.83  
    2.84 -subsubsection \<open>Bounded union\<close>
    2.85 -
    2.86 -definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "\<union>#" 70)
    2.87 -  where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close>
    2.88 -
    2.89 -interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#"
    2.90 -proof -
    2.91 -  have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
    2.92 -    by arith
    2.93 -  show "class.semilattice_sup op \<union># op \<subseteq># op \<subset>#"
    2.94 -    by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
    2.95 -qed
    2.96 -  \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
    2.97 -
    2.98 -interpretation subset_mset: bounded_lattice_bot "op \<inter>#" "op \<subseteq>#" "op \<subset>#"
    2.99 -  "op \<union>#" "{#}"
   2.100 -  by standard auto
   2.101 +subsubsection \<open>Additional bounded union facts\<close>
   2.102  
   2.103  lemma sup_subset_mset_count [simp]: \<comment> \<open>FIXME irregular fact name\<close>
   2.104    "count (A \<union># B) x = max (count A x) (count B x)"
   2.105 @@ -840,12 +830,6 @@
   2.106    by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count)
   2.107      (auto simp add: not_in_iff elim: mset_add)
   2.108  
   2.109 -lemma empty_sup: "{#} \<union># M = M"
   2.110 -  by (fact subset_mset.sup_bot.left_neutral)
   2.111 -
   2.112 -lemma sup_empty: "M \<union># {#} = M"
   2.113 -  by (fact subset_mset.sup_bot.right_neutral)
   2.114 -
   2.115  lemma sup_union_left1 [simp]: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) \<union># N = add_mset x (M \<union># N)"
   2.116    by (simp add: multiset_eq_iff not_in_iff)
   2.117  
   2.118 @@ -881,7 +865,7 @@
   2.119  
   2.120  subsubsection \<open>Subset is an order\<close>
   2.121  
   2.122 -interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
   2.123 +interpretation subset_mset: order "op \<subseteq>#" "op \<subset>#" by unfold_locales
   2.124  
   2.125  
   2.126  subsection \<open>Replicate and repeat operations\<close>
   2.127 @@ -1051,8 +1035,6 @@
   2.128  
   2.129  end
   2.130  
   2.131 -lemma bdd_below_multiset [simp]: "subset_mset.bdd_below A"
   2.132 -  by (intro subset_mset.bdd_belowI[of _ "{#}"]) simp_all
   2.133  
   2.134  lemma bdd_above_multiset_imp_bdd_above_count:
   2.135    assumes "subset_mset.bdd_above (A :: 'a multiset set)"
   2.136 @@ -1465,7 +1447,7 @@
   2.137  lemma mset_subset_size: "(A::'a multiset) \<subset># B \<Longrightarrow> size A < size B"
   2.138  proof (induct A arbitrary: B)
   2.139    case (empty M)
   2.140 -  then have "M \<noteq> {#}" by (simp add: mset_subset_empty_nonempty)
   2.141 +  then have "M \<noteq> {#}" by (simp add: subset_mset.zero_less_iff_neq_zero)
   2.142    then obtain M' x where "M = add_mset x M'"
   2.143      by (blast dest: multi_nonempty_split)
   2.144    then show ?case by simp
   2.145 @@ -1750,8 +1732,8 @@
   2.146  lemma mset_zero_iff_right[simp]: "({#} = mset x) = (x = [])"
   2.147  by (induct x) auto
   2.148  
   2.149 -lemma set_mset_mset[simp]: "set_mset (mset x) = set x"
   2.150 -by (induct x) auto
   2.151 +lemma set_mset_mset[simp]: "set_mset (mset xs) = set xs"
   2.152 +  by (induct xs) auto
   2.153  
   2.154  lemma set_mset_comp_mset [simp]: "set_mset \<circ> mset = set"
   2.155    by (simp add: fun_eq_iff)
   2.156 @@ -2921,12 +2903,7 @@
   2.157  subsubsection \<open>Monotonicity of multiset union\<close>
   2.158  
   2.159  lemma mult1_union: "(B, D) \<in> mult1 r \<Longrightarrow> (C + B, C + D) \<in> mult1 r"
   2.160 -apply (unfold mult1_def)
   2.161 -apply auto
   2.162 -apply (rule_tac x = a in exI)
   2.163 -apply (rule_tac x = "C + M0" in exI)
   2.164 -apply (simp add: add.assoc)
   2.165 -done
   2.166 +  by (force simp: mult1_def)
   2.167  
   2.168  lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
   2.169  apply (unfold less_multiset_def mult_def)
   2.170 @@ -3266,7 +3243,7 @@
   2.171    (subset_eq_mset_impl xs ys = Some False \<longrightarrow> mset xs = mset ys)"
   2.172  proof (induct xs arbitrary: ys)
   2.173    case (Nil ys)
   2.174 -  show ?case by (auto simp: mset_subset_empty_nonempty)
   2.175 +  show ?case by (auto simp: subset_mset.zero_less_iff_neq_zero)
   2.176  next
   2.177    case (Cons x xs ys)
   2.178    show ?case
     3.1 --- a/src/HOL/Library/Multiset_Order.thy	Fri Oct 07 17:57:17 2016 +0200
     3.2 +++ b/src/HOL/Library/Multiset_Order.thy	Fri Oct 07 17:58:36 2016 +0200
     3.3 @@ -199,7 +199,7 @@
     3.4    by (simp add: less_multiset\<^sub>H\<^sub>O)
     3.5  
     3.6  lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
     3.7 -  using subset_eq_empty less_multiset\<^sub>D\<^sub>M by blast
     3.8 +  using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
     3.9  
    3.10  lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
    3.11    by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)