# HG changeset patch
# User desharna
# Date 1638006417 -3600
# Node ID c256bba593f3beef6cfca564d9a26714bd526bb1
# Parent  691131ce4641a268ee32178ab5111735042292c4
redefined less_multiset to be based on multp

diff -r 691131ce4641 -r c256bba593f3 NEWS
--- a/NEWS	Sat Nov 27 10:28:48 2021 +0100
+++ b/NEWS	Sat Nov 27 10:46:57 2021 +0100
@@ -26,6 +26,7 @@
   - Added predicate multp equivalent to set mult. Reuse name previously
     used for what is now called multp_code. Minor INCOMPATIBILITY.
   - Lifted multiple lemmas from mult to multp.
+  - Redefined less_multiset to be based on multp. INCOMPATIBILITY.
 
 
 New in Isabelle2021-1 (December 2021)
diff -r 691131ce4641 -r c256bba593f3 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Nov 27 10:28:48 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Nov 27 10:46:57 2021 +0100
@@ -3100,6 +3100,63 @@
     folded multp_def transp_trans irreflp_irrefl_eq, simplified]
 
 
+subsubsection \<open>Partial-order properties\<close>
+
+lemma mult1_lessE:
+  assumes "(N, M) \<in> mult1 {(a, b). r a b}" and "asymp r"
+  obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
+    "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
+proof -
+  from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
+    *: "b \<in># K \<Longrightarrow> r b a" for b by (blast elim: mult1E)
+  moreover from * [of a] have "a \<notin># K"
+    using \<open>asymp r\<close> by (meson asymp.cases)
+  ultimately show thesis by (auto intro: that)
+qed
+
+instantiation multiset :: (preorder) order begin
+
+definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+  where "M < N \<longleftrightarrow> multp (<) M N"
+
+definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
+  where "less_eq_multiset M N \<longleftrightarrow> M < N \<or> M = N"
+
+instance
+proof -
+  have irrefl: "\<not> M < M" for M :: "'a multiset"
+  proof
+    assume "M < M"
+    then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def multp_def)
+    have "trans {(x'::'a, x). x' < x}"
+      by (metis (mono_tags, lifting) case_prodD case_prodI less_trans mem_Collect_eq transI)
+    moreover note MM
+    ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
+      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
+      by (rule mult_implies_one_step)
+    then obtain I J K where "M = I + J" and "M = I + K"
+      and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
+    then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
+    have "finite (set_mset K)" by simp
+    moreover note **
+    ultimately have "set_mset K = {}"
+      by (induct rule: finite_induct) (auto intro: order_less_trans)
+    with * show False by simp
+  qed
+  have trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < N" for K M N :: "'a multiset"
+    unfolding less_multiset_def multp_def mult_def by (blast intro: trancl_trans)
+  show "OFCLASS('a multiset, order_class)"
+    by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
+qed
+
+end
+
+lemma mset_le_irrefl [elim!]:
+  fixes M :: "'a::preorder multiset"
+  shows "M < M \<Longrightarrow> R"
+  by simp
+
+
 subsection \<open>Quasi-executable version of the multiset extension\<close>
 
 text \<open>
@@ -3165,71 +3222,13 @@
   by blast
 
 
-subsubsection \<open>Partial-order properties\<close>
-
-lemma mult1_lessE:
-  assumes "(N, M) \<in> mult1 {(a, b). r a b}" and "asymp r"
-  obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
-    "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
-proof -
-  from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
-    *: "b \<in># K \<Longrightarrow> r b a" for b by (blast elim: mult1E)
-  moreover from * [of a] have "a \<notin># K"
-    using \<open>asymp r\<close> by (meson asymp.cases)
-  ultimately show thesis by (auto intro: that)
-qed
-
-instantiation multiset :: (preorder) order
-begin
-
-definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
-  where "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"
-  where "less_eq_multiset M' M \<longleftrightarrow> M' < M \<or> M' = M"
-
-instance
-proof -
-  have irrefl: "\<not> M < M" for M :: "'a multiset"
-  proof
-    assume "M < M"
-    then have MM: "(M, M) \<in> mult {(x, y). x < y}" by (simp add: less_multiset_def)
-    have "trans {(x'::'a, x). x' < x}"
-      by (metis (mono_tags, lifting) case_prodD case_prodI less_trans mem_Collect_eq transI)
-    moreover note MM
-    ultimately have "\<exists>I J K. M = I + J \<and> M = I + K
-      \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})"
-      by (rule mult_implies_one_step)
-    then obtain I J K where "M = I + J" and "M = I + K"
-      and "J \<noteq> {#}" and "(\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset J. (k, j) \<in> {(x, y). x < y})" by blast
-    then have *: "K \<noteq> {#}" and **: "\<forall>k\<in>set_mset K. \<exists>j\<in>set_mset K. k < j" by auto
-    have "finite (set_mset K)" by simp
-    moreover note **
-    ultimately have "set_mset K = {}"
-      by (induct rule: finite_induct) (auto intro: order_less_trans)
-    with * show False by simp
-  qed
-  have trans: "K < M \<Longrightarrow> M < N \<Longrightarrow> K < N" for K M N :: "'a multiset"
-    unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
-  show "OFCLASS('a multiset, order_class)"
-    by standard (auto simp add: less_eq_multiset_def irrefl dest: trans)
-qed
-
-end
-
-lemma mset_le_irrefl [elim!]:
-  fixes M :: "'a::preorder multiset"
-  shows "M < M \<Longrightarrow> R"
-  by simp
-
-
 subsubsection \<open>Monotonicity of multiset union\<close>
 
 lemma mult1_union: "(B, D) \<in> mult1 r \<Longrightarrow> (C + B, C + D) \<in> mult1 r"
   by (force simp: mult1_def)
 
 lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
-apply (unfold less_multiset_def mult_def)
+apply (unfold less_multiset_def multp_def mult_def)
 apply (erule trancl_induct)
  apply (blast intro: mult1_union)
 apply (blast intro: mult1_union trancl_trans)
diff -r 691131ce4641 -r c256bba593f3 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Sat Nov 27 10:28:48 2021 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Sat Nov 27 10:46:57 2021 +0100
@@ -167,26 +167,26 @@
 end
 
 lemma less_multiset_less_multiset\<^sub>H\<^sub>O: "M < N \<longleftrightarrow> less_multiset\<^sub>H\<^sub>O M N"
-  unfolding less_multiset_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
+  unfolding less_multiset_def multp_def mult\<^sub>H\<^sub>O less_multiset\<^sub>H\<^sub>O_def ..
 
 lemmas less_multiset\<^sub>D\<^sub>M = mult\<^sub>D\<^sub>M[folded less_multiset_def]
 lemmas less_multiset\<^sub>H\<^sub>O = mult\<^sub>H\<^sub>O[folded less_multiset_def]
 
 lemma subset_eq_imp_le_multiset:
   shows "M \<subseteq># N \<Longrightarrow> M \<le> N"
-  unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O
+  unfolding less_eq_multiset_def less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O
   by (simp add: less_le_not_le subseteq_mset_def)
 
 (* FIXME: "le" should be "less" in this and other names *)
 lemma le_multiset_right_total: "M < add_mset x M"
-  unfolding less_eq_multiset_def less_multiset\<^sub>H\<^sub>O by simp
+  unfolding less_eq_multiset_def less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O by simp
 
 lemma less_eq_multiset_empty_left[simp]:
   shows "{#} \<le> M"
   by (simp add: subset_eq_imp_le_multiset)
 
 lemma ex_gt_imp_less_multiset: "(\<exists>y. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
-  unfolding less_multiset\<^sub>H\<^sub>O
+  unfolding less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O
   by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
 
 lemma less_eq_multiset_empty_right[simp]: "M \<noteq> {#} \<Longrightarrow> \<not> M \<le> {#}"
@@ -194,11 +194,11 @@
 
 (* FIXME: "le" should be "less" in this and other names *)
 lemma le_multiset_empty_left[simp]: "M \<noteq> {#} \<Longrightarrow> {#} < M"
-  by (simp add: less_multiset\<^sub>H\<^sub>O)
+  by (simp add: less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O)
 
 (* FIXME: "le" should be "less" in this and other names *)
 lemma le_multiset_empty_right[simp]: "\<not> M < {#}"
-  using subset_mset.le_zero_eq less_multiset\<^sub>D\<^sub>M by blast
+  using subset_mset.le_zero_eq less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M by blast
 
 (* FIXME: "le" should be "less" in this and other names *)
 lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
@@ -209,7 +209,7 @@
 
 lemma less_eq_multiset\<^sub>H\<^sub>O:
   "M \<le> N \<longleftrightarrow> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
-  by (auto simp: less_eq_multiset_def less_multiset\<^sub>H\<^sub>O)
+  by (auto simp: less_eq_multiset_def less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O)
 
 instance by standard (auto simp: less_eq_multiset\<^sub>H\<^sub>O)
 
@@ -247,7 +247,7 @@
   obtain Y X where
     y_nemp: "Y \<noteq> {#}" and y_sub_N: "Y \<subseteq># N" and M_eq: "M = N - Y + X" and
     ex_y: "\<forall>x. x \<in># X \<longrightarrow> (\<exists>y. y \<in># Y \<and> x < y)"
-    using less[unfolded less_multiset\<^sub>D\<^sub>M] by blast
+    using less[unfolded less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M] by blast
 
   have x_sub_M: "X \<subseteq># M"
     using M_eq by simp
@@ -256,7 +256,7 @@
   let ?fX = "image_mset f X"
 
   show ?thesis
-    unfolding less_multiset\<^sub>D\<^sub>M
+    unfolding less_multiset_def multp_def less_multiset\<^sub>D\<^sub>M
   proof (intro exI conjI)
     show "image_mset f M = image_mset f N - ?fY + ?fX"
       using M_eq[THEN arg_cong, of "image_mset f"] y_sub_N
@@ -360,11 +360,11 @@
 
 lemma ex_gt_count_imp_le_multiset:
   "(\<forall>y :: 'a :: order. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M < N"
-  unfolding less_multiset\<^sub>H\<^sub>O
+  unfolding less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O
   by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)
 
 lemma mset_lt_single_iff[iff]: "{#x#} < {#y#} \<longleftrightarrow> x < y"
-  unfolding less_multiset\<^sub>H\<^sub>O by simp
+  unfolding less_multiset_def multp_def less_multiset\<^sub>H\<^sub>O by simp
 
 lemma mset_le_single_iff[iff]: "{#x#} \<le> {#y#} \<longleftrightarrow> x \<le> y" for x y :: "'a::order"
   unfolding less_eq_multiset\<^sub>H\<^sub>O by force
@@ -381,9 +381,9 @@
 begin
 
 lemma wf_less_multiset: "wf {(M :: 'a multiset, N). M < N}"
-  unfolding less_multiset_def by (auto intro: wf_mult wf)
+  unfolding less_multiset_def multp_def by (auto intro: wf_mult wf)
 
-instance by standard (metis less_multiset_def wf wf_def wf_mult)
+instance by standard (metis less_multiset_def multp_def wf wf_def wf_mult)
 
 end