# HG changeset patch
# User haftmann
# Date 1613980188 0
# Node ID e2d03448d5b5ab07d4fe162b5f0c4d73c8dd03e6
# Parent  f5a77ee9106cd14a0c5992aa10bf7ab50c16cbbf
get rid of traditional predicate

diff -r f5a77ee9106c -r e2d03448d5b5 NEWS
--- a/NEWS	Sun Feb 21 13:33:05 2021 +0100
+++ b/NEWS	Mon Feb 22 07:49:48 2021 +0000
@@ -3,6 +3,10 @@
 
 (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.)
 
+*** HOL ***
+
+* Theory Multiset: dedicated predicate "multiset" is gone, use
+explict expression instead.  Minor INCOMPATIBILITY.
 
 New in this Isabelle version
 ----------------------------
diff -r f5a77ee9106c -r e2d03448d5b5 src/HOL/Algebra/Polynomial_Divisibility.thy
--- a/src/HOL/Algebra/Polynomial_Divisibility.thy	Sun Feb 21 13:33:05 2021 +0100
+++ b/src/HOL/Algebra/Polynomial_Divisibility.thy	Mon Feb 22 07:49:48 2021 +0000
@@ -1507,7 +1507,7 @@
   assumes "p \<in> carrier (poly_ring R)" shows "alg_mult p = count (roots p)"
   using finite_number_of_roots[OF assms]
   unfolding sym[OF alg_mult_gt_zero_iff_is_root[OF assms]]
-  by (simp add: multiset_def roots_def) 
+  by (simp add: roots_def) 
 
 lemma (in domain) roots_mem_iff_is_root:
   assumes "p \<in> carrier (poly_ring R)" shows "x \<in># roots p \<longleftrightarrow> is_root p x"
diff -r f5a77ee9106c -r e2d03448d5b5 src/HOL/Computational_Algebra/Factorial_Ring.thy
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sun Feb 21 13:33:05 2021 +0100
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Mon Feb 22 07:49:48 2021 +0000
@@ -1208,8 +1208,7 @@
 
 lift_definition prime_factorization :: "'a \<Rightarrow> 'a multiset" is
   "\<lambda>x p. if prime p then multiplicity p x else 0"
-  unfolding multiset_def
-proof clarify
+proof -
   fix x :: 'a
   show "finite {p. 0 < (if prime p then multiplicity p x else 0)}" (is "finite ?A")
   proof (cases "x = 0")
@@ -2097,7 +2096,7 @@
   from \<open>finite S\<close> S(1) have "(\<Prod>p\<in>S. p ^ f p) \<noteq> 0" by auto
   with S(2) have nz: "n \<noteq> 0" by auto
   from S_eq \<open>finite S\<close> have count_A: "count A = f"
-    unfolding A_def by (subst multiset.Abs_multiset_inverse) (simp_all add: multiset_def)
+    unfolding A_def by (subst multiset.Abs_multiset_inverse) simp_all
   from S_eq count_A have set_mset_A: "set_mset A = S"
     by (simp only: set_mset_def)
   from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
diff -r f5a77ee9106c -r e2d03448d5b5 src/HOL/Computational_Algebra/Primes.thy
--- a/src/HOL/Computational_Algebra/Primes.thy	Sun Feb 21 13:33:05 2021 +0100
+++ b/src/HOL/Computational_Algebra/Primes.thy	Mon Feb 22 07:49:48 2021 +0000
@@ -728,8 +728,8 @@
   define g where "g = (\<lambda>x. if x \<in> S then f x else 0)"
   define A where "A = Abs_multiset g"
   have "{x. g x > 0} \<subseteq> S" by (auto simp: g_def)
-  from finite_subset[OF this assms(1)] have [simp]: "g \<in> multiset"
-    by (simp add: multiset_def)
+  from finite_subset[OF this assms(1)] have [simp]: "finite {x. 0 < g x}"
+    by simp
   from assms have count_A: "count A x = g x" for x unfolding A_def
     by simp
   have set_mset_A: "set_mset A = {x\<in>S. f x > 0}"
diff -r f5a77ee9106c -r e2d03448d5b5 src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Sun Feb 21 13:33:05 2021 +0100
+++ b/src/HOL/Library/DAList_Multiset.thy	Mon Feb 22 07:49:48 2021 +0000
@@ -100,7 +100,7 @@
 definition count_of :: "('a \<times> nat) list \<Rightarrow> 'a \<Rightarrow> nat"
   where "count_of xs x = (case map_of xs x of None \<Rightarrow> 0 | Some n \<Rightarrow> n)"
 
-lemma count_of_multiset: "count_of xs \<in> multiset"
+lemma count_of_multiset: "finite {x. 0 < count_of xs x}"
 proof -
   let ?A = "{x::'a. 0 < (case map_of xs x of None \<Rightarrow> 0::nat | Some n \<Rightarrow> n)}"
   have "?A \<subseteq> dom (map_of xs)"
@@ -117,7 +117,7 @@
   with finite_dom_map_of [of xs] have "finite ?A"
     by (auto intro: finite_subset)
   then show ?thesis
-    by (simp add: count_of_def fun_eq_iff multiset_def)
+    by (simp add: count_of_def fun_eq_iff)
 qed
 
 lemma count_simps [simp]:
@@ -291,7 +291,7 @@
   let ?inv = "{xs :: ('a \<times> nat) list. (distinct \<circ> map fst) xs}"
   note cs[simp del] = count_simps
   have count[simp]: "\<And>x. count (Abs_multiset (count_of x)) = count_of x"
-    by (rule Abs_multiset_inverse[OF count_of_multiset])
+    by (rule Abs_multiset_inverse) (simp add: count_of_multiset)
   assume ys: "ys \<in> ?inv"
   then show "fold_mset f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))"
     unfolding Bag_def unfolding Alist_inverse[OF ys]
diff -r f5a77ee9106c -r e2d03448d5b5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Feb 21 13:33:05 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Feb 22 07:49:48 2021 +0000
@@ -14,17 +14,19 @@
 
 subsection \<open>The type of multisets\<close>
 
-definition "multiset = {f :: 'a \<Rightarrow> nat. finite {x. f x > 0}}"
-
-typedef 'a multiset = "multiset :: ('a \<Rightarrow> nat) set"
+typedef 'a multiset = \<open>{f :: 'a \<Rightarrow> nat. finite {x. f x > 0}}\<close>
   morphisms count Abs_multiset
-  unfolding multiset_def
 proof
-  show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
+  show \<open>(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}\<close>
+    by simp
 qed
 
 setup_lifting type_definition_multiset
 
+lemma count_Abs_multiset:
+  \<open>count (Abs_multiset f) = f\<close> if \<open>finite {x. f x > 0}\<close>
+  by (rule Abs_multiset_inverse) (simp add: that)
+
 lemma multiset_eq_iff: "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
   by (simp only: count_inject [symmetric] fun_eq_iff)
 
@@ -33,37 +35,15 @@
 
 text \<open>Preservation of the representing set \<^term>\<open>multiset\<close>.\<close>
 
-lemma const0_in_multiset: "(\<lambda>a. 0) \<in> multiset"
-  by (simp add: multiset_def)
-
-lemma only1_in_multiset: "(\<lambda>b. if b = a then n else 0) \<in> multiset"
-  by (simp add: multiset_def)
-
-lemma union_preserves_multiset: "M \<in> multiset \<Longrightarrow> N \<in> multiset \<Longrightarrow> (\<lambda>a. M a + N a) \<in> multiset"
-  by (simp add: multiset_def)
-
 lemma diff_preserves_multiset:
-  assumes "M \<in> multiset"
-  shows "(\<lambda>a. M a - N a) \<in> multiset"
-proof -
-  have "{x. N x < M x} \<subseteq> {x. 0 < M x}"
-    by auto
-  with assms show ?thesis
-    by (auto simp add: multiset_def intro: finite_subset)
-qed
+  \<open>finite {x. 0 < M x - N x}\<close> if \<open>finite {x. 0 < M x}\<close> for M N :: \<open>'a \<Rightarrow> nat\<close>
+  using that by (rule rev_finite_subset) auto
 
 lemma filter_preserves_multiset:
-  assumes "M \<in> multiset"
-  shows "(\<lambda>x. if P x then M x else 0) \<in> multiset"
-proof -
-  have "{x. (P x \<longrightarrow> 0 < M x) \<and> P x} \<subseteq> {x. 0 < M x}"
-    by auto
-  with assms show ?thesis
-    by (auto simp add: multiset_def intro: finite_subset)
-qed
-
-lemmas in_multiset = const0_in_multiset only1_in_multiset
-  union_preserves_multiset diff_preserves_multiset filter_preserves_multiset
+  \<open>finite {x. 0 < (if P x then M x else 0)}\<close> if \<open>finite {x. 0 < M x}\<close> for M N :: \<open>'a \<Rightarrow> nat\<close>
+  using that by (rule rev_finite_subset) auto
+
+lemmas in_multiset = diff_preserves_multiset filter_preserves_multiset
 
 
 subsection \<open>Representing multisets\<close>
@@ -74,19 +54,19 @@
 begin
 
 lift_definition zero_multiset :: "'a multiset" is "\<lambda>a. 0"
-by (rule const0_in_multiset)
+  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)"
-by (rule union_preserves_multiset)
+  by simp
 
 lift_definition minus_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is "\<lambda> M N. \<lambda>a. M a - N a"
-by (rule diff_preserves_multiset)
+  by (rule diff_preserves_multiset)
 
 instance
-  by (standard; transfer; simp add: fun_eq_iff)
+  by (standard; transfer) (simp_all add: fun_eq_iff)
 
 end
 
@@ -99,9 +79,9 @@
 end
 
 lemma add_mset_in_multiset:
-  assumes M: \<open>M \<in> multiset\<close>
-  shows \<open>(\<lambda>b. if b = a then Suc (M b) else M b) \<in> multiset\<close>
-  using assms by (simp add: multiset_def flip: insert_Collect)
+  \<open>finite {x. 0 < (if x = a then Suc (M x) else M x)}\<close>
+  if \<open>finite {x. 0 < M x}\<close>
+  using that by (simp add: flip: insert_Collect)
 
 lift_definition add_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is
   "\<lambda>a M b. if b = a then Suc (M b) else M b"
@@ -246,7 +226,7 @@
 
 lemma finite_set_mset [iff]:
   "finite (set_mset M)"
-  using count [of M] by (simp add: multiset_def)
+  using count [of M] by simp
 
 lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close>
   by (auto simp flip: count_greater_eq_Suc_zero_iff split: if_splits)
@@ -1029,18 +1009,18 @@
 lift_definition Inf_multiset :: "'a multiset set \<Rightarrow> 'a multiset" is
   "\<lambda>A i. if A = {} then 0 else Inf ((\<lambda>f. f i) ` A)"
 proof -
-  fix A :: "('a \<Rightarrow> nat) set" assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<in> multiset"
-  have "finite {i. (if A = {} then 0 else Inf ((\<lambda>f. f i) ` A)) > 0}" unfolding multiset_def
+  fix A :: "('a \<Rightarrow> nat) set"
+  assume *: "\<And>f. f \<in> A \<Longrightarrow> finite {x. 0 < f x}"
+  show \<open>finite {i. 0 < (if A = {} then 0 else INF f\<in>A. f i)}\<close>
   proof (cases "A = {}")
     case False
     then obtain f where "f \<in> A" by blast
     hence "{i. Inf ((\<lambda>f. f i) ` A) > 0} \<subseteq> {i. f i > 0}"
       by (auto intro: less_le_trans[OF _ cInf_lower])
-    moreover from \<open>f \<in> A\<close> * have "finite \<dots>" by (simp add: multiset_def)
+    moreover from \<open>f \<in> A\<close> * have "finite \<dots>" by simp
     ultimately have "finite {i. Inf ((\<lambda>f. f i) ` A) > 0}" by (rule finite_subset)
     with False show ?thesis by simp
   qed simp_all
-  thus "(\<lambda>i. if A = {} then 0 else INF f\<in>A. f i) \<in> multiset" by (simp add: multiset_def)
 qed
 
 instance ..
@@ -1098,10 +1078,9 @@
 qed
 
 lemma Sup_multiset_in_multiset:
-  assumes "A \<noteq> {}" "subset_mset.bdd_above A"
-  shows   "(\<lambda>i. SUP X\<in>A. count X i) \<in> multiset"
-  unfolding multiset_def
-proof
+  \<open>finite {i. 0 < (SUP M\<in>A. count M i)}\<close>
+  if \<open>A \<noteq> {}\<close> \<open>subset_mset.bdd_above A\<close>
+proof -
   have "{i. Sup ((\<lambda>X. count X i) ` A) > 0} \<subseteq> (\<Union>X\<in>A. {i. 0 < count X i})"
   proof safe
     fix i assume pos: "(SUP X\<in>A. count X i) > 0"
@@ -1109,20 +1088,21 @@
     proof (rule ccontr)
       assume "i \<notin> (\<Union>X\<in>A. {i. 0 < count X i})"
       hence "\<forall>X\<in>A. count X i \<le> 0" by (auto simp: count_eq_zero_iff)
-      with assms have "(SUP X\<in>A. count X i) \<le> 0"
+      with that have "(SUP X\<in>A. count X i) \<le> 0"
         by (intro cSup_least bdd_above_multiset_imp_bdd_above_count) auto
       with pos show False by simp
     qed
   qed
-  moreover from assms have "finite \<dots>" by (rule bdd_above_multiset_imp_finite_support)
-  ultimately show "finite {i. Sup ((\<lambda>X. count X i) ` A) > 0}" by (rule finite_subset)
+  moreover from that have "finite \<dots>"
+    by (rule bdd_above_multiset_imp_finite_support)
+  ultimately show "finite {i. Sup ((\<lambda>X. count X i) ` A) > 0}"
+    by (rule finite_subset)
 qed
 
 lemma count_Sup_multiset_nonempty:
-  assumes "A \<noteq> {}" "subset_mset.bdd_above A"
-  shows   "count (Sup A) x = (SUP X\<in>A. count X x)"
-  using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset)
-
+  \<open>count (Sup A) x = (SUP X\<in>A. count X x)\<close>
+  if \<open>A \<noteq> {}\<close> \<open>subset_mset.bdd_above A\<close>
+  using that by (simp add: Sup_multiset_def Sup_multiset_in_multiset count_Abs_multiset)
 
 interpretation subset_mset: conditionally_complete_lattice Inf Sup "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)"
 proof
@@ -3700,7 +3680,7 @@
     by (rule natLeq_cinfinite)
   show "ordLeq3 (card_of (set_mset X)) natLeq" for X
     by transfer
-      (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
+      (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric])
   show "rel_mset R OO rel_mset S \<le> rel_mset (R OO S)" for R S
     unfolding rel_mset_def[abs_def] OO_def
     apply clarify
@@ -3749,9 +3729,8 @@
 unfolding rel_mset_def Grp_def by auto
 
 declare multiset.count[simp]
-declare Abs_multiset_inverse[simp]
+declare count_Abs_multiset[simp]
 declare multiset.count_inverse[simp]
-declare union_preserves_multiset[simp]
 
 lemma rel_mset_Plus:
   assumes ab: "R a b"