# HG changeset patch
# User desharna
# Date 1637836418 -3600
# Node ID 825cd198d85cb8c7cb990b293fad48cb459aec7e
# Parent  b61bd2c12de33999811106ae82bbc042e71b4bd6
renamed Multiset.multp and Multiset.multeqp

diff -r b61bd2c12de3 -r 825cd198d85c NEWS
--- a/NEWS	Wed Nov 17 16:13:00 2021 +0100
+++ b/NEWS	Thu Nov 25 11:33:38 2021 +0100
@@ -7,6 +7,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** HOL ***
+
+* Theory "HOL-Library.Multiset": consolidated operation and fact namesd
+    multp ~> multp_code
+    multeqp ~> multeqp_code
+  Minor INCOMPATIBILITY.
 
 
 New in Isabelle2021-1 (December 2021)
diff -r b61bd2c12de3 -r 825cd198d85c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Nov 17 16:13:00 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Thu Nov 25 11:33:38 2021 +0100
@@ -4,6 +4,7 @@
     Author:     Jasmin Blanchette, Inria, LORIA, MPII
     Author:     Dmitriy Traytel, TU Muenchen
     Author:     Mathias Fleury, MPII
+    Author:     Martin Desharnais, MPI-INF Saarbruecken
 *)
 
 section \<open>(Finite) Multisets\<close>
@@ -3063,22 +3064,22 @@
   Predicate variants of \<open>mult\<close> and the reflexive closure of \<open>mult\<close>, which are
   executable whenever the given predicate \<open>P\<close> is. Together with the standard
   code equations for \<open>(\<inter>#\<close>) and \<open>(-\<close>) this should yield quadratic
-  (with respect to calls to \<open>P\<close>) implementations of \<open>multp\<close> and \<open>multeqp\<close>.
+  (with respect to calls to \<open>P\<close>) implementations of \<open>multp_code\<close> and \<open>multeqp_code\<close>.
 \<close>
 
-definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
-  "multp P N M =
+definition multp_code :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  "multp_code P N M =
     (let Z = M \<inter># N; X = M - Z in
     X \<noteq> {#} \<and> (let Y = N - Z in (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x)))"
 
-definition multeqp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
-  "multeqp P N M =
+definition multeqp_code :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  "multeqp_code P N M =
     (let Z = M \<inter># N; X = M - Z; Y = N - Z in
     (\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. P y x))"
 
-lemma multp_iff:
+lemma multp_code_iff:
   assumes "irrefl R" and "trans R" and [simp]: "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
-  shows "multp P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
+  shows "multp_code P N M \<longleftrightarrow> (N, M) \<in> mult R" (is "?L \<longleftrightarrow> ?R")
 proof -
   have *: "M \<inter># N + (N - M \<inter># N) = N" "M \<inter># N + (M - M \<inter># N) = M"
     "(M - M \<inter># N) \<inter># (N - M \<inter># N) = {#}" by (auto simp flip: count_inject)
@@ -3086,29 +3087,29 @@
   proof
     assume ?L thus ?R
       using one_step_implies_mult[of "M - M \<inter># N" "N - M \<inter># N" R "M \<inter># N"] *
-      by (auto simp: multp_def Let_def)
+      by (auto simp: multp_code_def Let_def)
   next
     { fix I J K :: "'a multiset" assume "(I + J) \<inter># (I + K) = {#}"
       then have "I = {#}" by (metis inter_union_distrib_right union_eq_empty)
     } note [dest!] = this
     assume ?R thus ?L
       using mult_implies_one_step[OF assms(2), of "N - M \<inter># N" "M - M \<inter># N"]
-        mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_def)
+        mult_cancel_max[OF assms(2,1), of "N" "M"] * by (auto simp: multp_code_def)
   qed
 qed
 
-lemma multeqp_iff:
+lemma multeqp_code_iff:
   assumes "irrefl R" and "trans R" and "\<And>x y. P x y \<longleftrightarrow> (x, y) \<in> R"
-  shows "multeqp P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
+  shows "multeqp_code P N M \<longleftrightarrow> (N, M) \<in> (mult R)\<^sup>="
 proof -
   { assume "N \<noteq> M" "M - M \<inter># N = {#}"
     then obtain y where "count N y \<noteq> count M y" by (auto simp flip: count_inject)
     then have "\<exists>y. count M y < count N y" using \<open>M - M \<inter># N = {#}\<close>
       by (auto simp flip: count_inject dest!: le_neq_implies_less fun_cong[of _ _ y])
   }
-  then have "multeqp P N M \<longleftrightarrow> multp P N M \<or> N = M"
-    by (auto simp: multeqp_def multp_def Let_def in_diff_count)
-  thus ?thesis using multp_iff[OF assms] by simp
+  then have "multeqp_code P N M \<longleftrightarrow> multp_code P N M \<or> N = M"
+    by (auto simp: multeqp_code_def multp_code_def Let_def in_diff_count)
+  thus ?thesis using multp_code_iff[OF assms] by simp
 qed