# HG changeset patch
# User haftmann
# Date 1615056130 0
# Node ID 716d256259d5c99ee73f0ac570bafc0be559cbf5
# Parent  24f0df084aad5fd6e07c16a1ca28a007f658f5c6
consolidated names

diff -r 24f0df084aad -r 716d256259d5 NEWS
--- a/NEWS	Sat Mar 06 18:42:10 2021 +0000
+++ b/NEWS	Sat Mar 06 18:42:10 2021 +0000
@@ -22,6 +22,18 @@
 * Theory Multiset: dedicated predicate "multiset" is gone, use
 explict expression instead.  Minor INCOMPATIBILITY.
 
+* Theory Multiset: consolidated abbreviations Mempty, Melem, not_Melem
+to empty_mset, member_mset, not_member_mset respectively.  Minor
+INCOMPATIBILITY.
+
+* Theory Multiset: consolidated operation and fact names:
+    inf_subset_mset ~> inter_mset
+    sup_subset_mset ~> union_mset
+    multiset_inter_def ~> inter_mset_def
+    sup_subset_mset_def ~> union_mset_def
+    multiset_inter_count ~> count_inter_mset
+    sup_subset_mset_count ~> count_union_mset
+
 * HOL-Analysis/HOL-Probability: indexed products of discrete
 distributions, negative binomial distribution, Hoeffding's inequality,
 Chernoff bounds, Cauchy–Schwarz inequality for nn_integral, and some
diff -r 24f0df084aad -r 716d256259d5 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sat Mar 06 18:42:10 2021 +0000
+++ b/src/HOL/Algebra/Divisibility.thy	Sat Mar 06 18:42:10 2021 +0000
@@ -2128,11 +2128,11 @@
   proof (simp add: isgcd_def, safe)
     from csmset
     have "fmset G cs \<subseteq># fmset G as"
-      by (simp add: multiset_inter_def subset_mset_def)
+      by simp
     then show "c divides a" by (rule fmsubset_divides) fact+
   next
     from csmset have "fmset G cs \<subseteq># fmset G bs"
-      by (simp add: multiset_inter_def subseteq_mset_def, force)
+      by simp
     then show "c divides b"
       by (rule fmsubset_divides) fact+
   next
diff -r 24f0df084aad -r 716d256259d5 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Sat Mar 06 18:42:10 2021 +0000
+++ b/src/HOL/Library/DAList_Multiset.thy	Sat Mar 06 18:42:10 2021 +0000
@@ -12,7 +12,7 @@
 
 declare [[code drop: "{#}" Multiset.is_empty add_mset
   "plus :: 'a multiset \<Rightarrow> _" "minus :: 'a multiset \<Rightarrow> _"
-  inf_subset_mset sup_subset_mset image_mset filter_mset count
+  inter_mset union_mset image_mset filter_mset count
   "size :: _ multiset \<Rightarrow> nat" sum_mset prod_mset
   set_mset sorted_list_of_multiset subset_mset subseteq_mset
   equal_multiset_inst.equal_multiset]]
@@ -261,8 +261,8 @@
     unfolding mset_less_eq_Bag0 by auto
 qed
 
-declare multiset_inter_def [code]
-declare sup_subset_mset_def [code]
+declare inter_mset_def [code]
+declare union_mset_def [code]
 declare mset.simps [code]
 
 
diff -r 24f0df084aad -r 716d256259d5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Mar 06 18:42:10 2021 +0000
+++ b/src/HOL/Library/Multiset.thy	Sat Mar 06 18:42:10 2021 +0000
@@ -53,16 +53,19 @@
 instantiation multiset :: (type) cancel_comm_monoid_add
 begin
 
-lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0"
+lift_definition zero_multiset :: \<open>'a multiset\<close>
+  is \<open>\<lambda>a. 0\<close>
   by simp
 
-abbreviation Mempty :: "'a multiset" ("{#}") where
-  "Mempty \<equiv> 0"
-
-lift_definition plus_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda>M N. (\<lambda>a. M a + N a)"
+abbreviation empty_mset :: \<open>'a multiset\<close> (\<open>{#}\<close>)
+  where \<open>empty_mset \<equiv> 0\<close>
+
+lift_definition plus_multiset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>
+  is \<open>\<lambda>M N a. M a + N a\<close>
   by simp
 
-lift_definition minus_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
+lift_definition minus_multiset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>
+  is \<open>\<lambda>M N a. M a - N a\<close>
   by (rule diff_preserves_multiset)
 
 instance
@@ -121,30 +124,30 @@
 
 subsubsection \<open>Conversion to set and membership\<close>
 
-definition set_mset :: "'a multiset \<Rightarrow> 'a set"
-  where "set_mset M = {x. count M x > 0}"
-
-abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
-  where "Melem a M \<equiv> a \<in> set_mset M"
+definition set_mset :: \<open>'a multiset \<Rightarrow> 'a set\<close>
+  where \<open>set_mset M = {x. count M x > 0}\<close>
+
+abbreviation member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close>
+  where \<open>member_mset a M \<equiv> a \<in> set_mset M\<close>
 
 notation
-  Melem  ("'(\<in>#')") and
-  Melem  ("(_/ \<in># _)" [51, 51] 50)
+  member_mset  (\<open>'(\<in>#')\<close>) and
+  member_mset  (\<open>(_/ \<in># _)\<close> [51, 51] 50)
 
 notation  (ASCII)
-  Melem  ("'(:#')") and
-  Melem  ("(_/ :# _)" [51, 51] 50)
-
-abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
-  where "not_Melem a M \<equiv> a \<notin> set_mset M"
+  member_mset  (\<open>'(:#')\<close>) and
+  member_mset  (\<open>(_/ :# _)\<close> [51, 51] 50)
+
+abbreviation not_member_mset :: \<open>'a \<Rightarrow> 'a multiset \<Rightarrow> bool\<close>
+  where \<open>not_member_mset a M \<equiv> a \<notin> set_mset M\<close>
 
 notation
-  not_Melem  ("'(\<notin>#')") and
-  not_Melem  ("(_/ \<notin># _)" [51, 51] 50)
+  not_member_mset  (\<open>'(\<notin>#')\<close>) and
+  not_member_mset  (\<open>(_/ \<notin># _)\<close> [51, 51] 50)
 
 notation  (ASCII)
-  not_Melem  ("'(~:#')") and
-  not_Melem  ("(_/ ~:# _)" [51, 51] 50)
+  not_member_mset  (\<open>'(~:#')\<close>) and
+  not_member_mset  (\<open>(_/ ~:# _)\<close> [51, 51] 50)
 
 context
 begin
@@ -671,26 +674,26 @@
 
 subsubsection \<open>Intersection and bounded union\<close>
 
-definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "\<inter>#" 70) where
-  multiset_inter_def: "inf_subset_mset A B = A - (A - B)"
-
-interpretation subset_mset: semilattice_inf inf_subset_mset "(\<subseteq>#)" "(\<subset>#)"
+definition inter_mset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>  (infixl \<open>\<inter>#\<close> 70)
+  where \<open>A \<inter># B = A - (A - B)\<close>
+
+interpretation subset_mset: semilattice_inf \<open>(\<inter>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
 proof -
   have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat
     by arith
   show "class.semilattice_inf (\<inter>#) (\<subseteq>#) (\<subset>#)"
-    by standard (auto simp add: multiset_inter_def subseteq_mset_def)
+    by standard (auto simp add: inter_mset_def subseteq_mset_def)
 qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
 
-definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "\<union>#" 70)
-  where "sup_subset_mset A B = A + (B - A)" \<comment> \<open>FIXME irregular fact name\<close>
-
-interpretation subset_mset: semilattice_sup sup_subset_mset "(\<subseteq>#)" "(\<subset>#)"
+definition union_mset :: \<open>'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>  (infixl \<open>\<union>#\<close> 70)
+  where \<open>A \<union># B = A + (B - A)\<close>
+
+interpretation subset_mset: semilattice_sup \<open>(\<union>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
 proof -
   have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
     by arith
   show "class.semilattice_sup (\<union>#) (\<subseteq>#) (\<subset>#)"
-    by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
+    by standard (auto simp add: union_mset_def subseteq_mset_def)
 qed \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
 
 interpretation subset_mset: bounded_lattice_bot "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)"
@@ -701,14 +704,13 @@
 
 subsubsection \<open>Additional intersection facts\<close>
 
-lemma multiset_inter_count [simp]:
-  fixes A B :: "'a multiset"
-  shows "count (A \<inter># B) x = min (count A x) (count B x)"
-  by (simp add: multiset_inter_def)
+lemma count_inter_mset [simp]:
+  \<open>count (A \<inter># B) x = min (count A x) (count B x)\<close>
+  by (simp add: inter_mset_def)
 
 lemma set_mset_inter [simp]:
   "set_mset (A \<inter># B) = set_mset A \<inter> set_mset B"
-  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] multiset_inter_count) simp
+  by (simp only: set_mset_def) auto
 
 lemma diff_intersect_left_idem [simp]:
   "M - M \<inter># N = M - N"
@@ -766,10 +768,9 @@
 lemma inter_mset_empty_distrib_left: "(A + B) \<inter># C = {#} \<longleftrightarrow> A \<inter># C = {#} \<and> B \<inter># C = {#}"
   by (meson disjunct_not_in union_iff)
 
-lemma add_mset_inter_add_mset[simp]:
+lemma add_mset_inter_add_mset [simp]:
   "add_mset a A \<inter># add_mset a B = add_mset a (A \<inter># B)"
-  by (metis add_mset_add_single add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def
-      subset_mset.diff_add_assoc2)
+  by (rule multiset_eqI) simp
 
 lemma add_mset_disjoint [simp]:
   "add_mset a A \<inter># B = {#} \<longleftrightarrow> a \<notin># B \<and> A \<inter># B = {#}"
@@ -838,14 +839,13 @@
 
 subsubsection \<open>Additional bounded union facts\<close>
 
-lemma sup_subset_mset_count [simp]: \<comment> \<open>FIXME irregular fact name\<close>
-  "count (A \<union># B) x = max (count A x) (count B x)"
-  by (simp add: sup_subset_mset_def)
+lemma count_union_mset [simp]:
+  \<open>count (A \<union># B) x = max (count A x) (count B x)\<close>
+  by (simp add: union_mset_def)
 
 lemma set_mset_sup [simp]:
-  "set_mset (A \<union># B) = set_mset A \<union> set_mset B"
-  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count)
-    (auto simp add: not_in_iff elim: mset_add)
+  \<open>set_mset (A \<union># B) = set_mset A \<union> set_mset B\<close>
+  by (simp only: set_mset_def) (auto simp add: less_max_iff_disj)
 
 lemma sup_union_left1 [simp]: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) \<union># N = add_mset x (M \<union># N)"
   by (simp add: multiset_eq_iff not_in_iff)
@@ -894,12 +894,19 @@
 lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
   unfolding replicate_mset_def by (induct n) auto
 
-fun repeat_mset :: "nat \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
-  "repeat_mset 0 _ = {#}" |
-  "repeat_mset (Suc n) A = A + repeat_mset n A"
+lift_definition repeat_mset :: \<open>nat \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset\<close>
+  is \<open>\<lambda>n M a. n * M a\<close> by simp
 
 lemma count_repeat_mset [simp]: "count (repeat_mset i A) a = i * count A a"
-  by (induction i) auto
+  by transfer rule
+
+lemma repeat_mset_0 [simp]:
+  \<open>repeat_mset 0 M = {#}\<close>
+  by transfer simp
+
+lemma repeat_mset_Suc [simp]:
+  \<open>repeat_mset (Suc n) M = M + repeat_mset n M\<close>
+  by transfer simp
 
 lemma repeat_mset_right [simp]: "repeat_mset a (repeat_mset b A) = repeat_mset (a * b) A"
   by (auto simp: multiset_eq_iff left_diff_distrib')
@@ -928,7 +935,7 @@
   by (auto simp: multiset_eq_iff)
 
 lemma repeat_mset_empty[simp]: "repeat_mset n {#} = {#}"
-  by (induction n) simp_all
+  by transfer simp
 
 
 subsubsection \<open>Simprocs\<close>
@@ -3254,10 +3261,10 @@
   let
     fun msetT T = Type (\<^type_name>\<open>multiset\<close>, [T]);
 
-    fun mk_mset T [] = Const (\<^const_abbrev>\<open>Mempty\<close>, msetT T)
+    fun mk_mset T [] = Const (\<^const_abbrev>\<open>empty_mset\<close>, msetT T)
       | mk_mset T [x] =
         Const (\<^const_name>\<open>add_mset\<close>, T --> msetT T --> msetT T) $ x $
-          Const (\<^const_abbrev>\<open>Mempty\<close>, msetT T)
+          Const (\<^const_abbrev>\<open>empty_mset\<close>, msetT T)
       | mk_mset T (x :: xs) =
         Const (\<^const_name>\<open>plus\<close>, msetT T --> msetT T --> msetT T) $
           mk_mset T [x] $ mk_mset T xs
@@ -3274,7 +3281,7 @@
       resolve_tac ctxt @{thms nonempty_single}
 
     fun regroup_munion_conv ctxt =
-      Function_Lib.regroup_conv ctxt \<^const_abbrev>\<open>Mempty\<close> \<^const_name>\<open>plus\<close>
+      Function_Lib.regroup_conv ctxt \<^const_abbrev>\<open>empty_mset\<close> \<^const_name>\<open>plus\<close>
         (map (fn t => t RS eq_reflection) (@{thms ac_simps} @ @{thms empty_neutral}))
 
     fun unfold_pwleq_tac ctxt i =