# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1473083270 -7200
# Node ID 7f6128adfe677371f3f6c98098a5f8cbe6f01260
# Parent  bcec0534aeea61f54b95265758284ae96bdd3fdb
tuning multisets; more interpretations

diff -r bcec0534aeea -r 7f6128adfe67 NEWS
--- a/NEWS	Mon Sep 05 15:47:50 2016 +0200
+++ b/NEWS	Mon Sep 05 15:47:50 2016 +0200
@@ -493,8 +493,8 @@
 ordering, and the subset ordering on multisets.
 INCOMPATIBILITY.
 
-* The subset ordering on multisets has now the interpretation
-ordered_ab_semigroup_monoid_add_imp_le.
+* The subset ordering on multisets has now the interpretations
+ordered_ab_semigroup_monoid_add_imp_le and bounded_lattice_bot.
 INCOMPATIBILITY.
 
 * Multiset: single has been removed in favor of add_mset that roughly
@@ -577,6 +577,10 @@
   mset_subset_eq_mono_add_left_cancel [simp] ~> []
   fold_mset_single [simp] ~> []
   subset_eq_empty [simp] ~> []
+  empty_sup [simp] ~> []
+  sup_empty [simp] ~> []
+  inter_empty [simp] ~> []
+  empty_inter [simp] ~> []
 INCOMPATIBILITY.
 
 * The order of the variables in the second cases of multiset_induct,
@@ -587,6 +591,10 @@
 of the procedure on natural numbers.
 INCOMPATIBILITY.
 
+* The lemma one_step_implies_mult_aux on multisets has been removed, use
+one_step_implies_mult instead.
+INCOMPATIBILITY.
+
 * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
 INCOMPATIBILITY.
 
diff -r bcec0534aeea -r 7f6128adfe67 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 05 15:47:50 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 05 15:47:50 2016 +0200
@@ -557,7 +557,7 @@
   by (auto simp add: subseteq_mset_def Suc_le_eq)
 
 lemma mset_subset_eq_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B"
-  by (simp add: subseteq_mset_def Suc_le_eq)
+  by simp
 
 lemma mset_subset_eq_add_mset_cancel: \<open>add_mset a A \<subseteq># add_mset a B \<longleftrightarrow> A \<subseteq># B\<close>
   unfolding add_mset_add_single[of _ A] add_mset_add_single[of _ B]
@@ -609,11 +609,11 @@
   "add_mset x A \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
   by (rule mset_subset_eq_insertD) simp
 
-lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
-  by (auto simp add: subseteq_mset_def subset_mset_def multiset_eq_iff)
-
-lemma empty_le [simp]: "{#} \<subseteq># A"
-  unfolding mset_subset_eq_exists_conv by auto
+lemma mset_subset_of_empty: "A \<subset># {#} \<longleftrightarrow> False"
+  by (simp only: subset_mset.not_less_zero)
+
+lemma empty_le: "{#} \<subseteq># A"
+  by (fact subset_mset.zero_le)
 
 lemma insert_subset_eq_iff:
   "add_mset a A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
@@ -739,10 +739,10 @@
   "{#} = A #\<inter> add_mset b B \<longleftrightarrow> b \<notin># A \<and> {#} = A #\<inter> B"
   by (auto simp: disjunct_not_in)
 
-lemma empty_inter [simp]: "{#} #\<inter> M = {#}"
+lemma empty_inter: "{#} #\<inter> M = {#}"
   by (simp add: multiset_eq_iff)
 
-lemma inter_empty [simp]: "M #\<inter> {#} = {#}"
+lemma inter_empty: "M #\<inter> {#} = {#}"
   by (simp add: multiset_eq_iff)
 
 lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) #\<inter> N = M #\<inter> N"
@@ -814,6 +814,10 @@
 qed
   \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
 
+interpretation subset_mset: bounded_lattice_bot "op #\<inter>" "op \<subseteq>#" "op \<subset>#"
+  "op #\<union>" "{#}"
+  by standard auto
+
 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)
@@ -823,11 +827,11 @@
   by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count)
     (auto simp add: not_in_iff elim: mset_add)
 
-lemma empty_sup [simp]: "{#} #\<union> M = M"
-  by (simp add: multiset_eq_iff)
-
-lemma sup_empty [simp]: "M #\<union> {#} = M"
-  by (simp add: multiset_eq_iff)
+lemma empty_sup: "{#} #\<union> M = M"
+  by (fact subset_mset.sup_bot.left_neutral)
+
+lemma sup_empty: "M #\<union> {#} = M"
+  by (fact subset_mset.sup_bot.right_neutral)
 
 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)
@@ -1231,9 +1235,12 @@
 lemma filter_inter_mset [simp]: "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N"
   by (rule multiset_eqI) simp
 
+lemma filter_sup_mset[simp]: "filter_mset P (A #\<union> B) = filter_mset P A #\<union> filter_mset P B"
+  by (rule multiset_eqI) simp
+
 lemma filter_mset_add_mset [simp]:
    "filter_mset P (add_mset x A) =
-     (if P x then add_mset x (filter_mset P A) else (filter_mset P A))"
+     (if P x then add_mset x (filter_mset P A) else filter_mset P A)"
    by (auto simp: multiset_eq_iff)
 
 lemma multiset_filter_subset[simp]: "filter_mset f M \<subseteq># M"
@@ -1624,6 +1631,9 @@
     by (auto simp: setsum.distrib setsum.delta' intro!: setsum.mono_neutral_left)
 qed
 
+lemma image_mset_subseteq_mono: "A \<subseteq># B \<Longrightarrow> image_mset f A \<subseteq># image_mset f B"
+  by (metis image_mset_union subset_mset.le_iff_add)
+
 syntax (ASCII)
   "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ :# _#})")
 syntax
@@ -2097,6 +2107,9 @@
   shows "setsum f A = {#} \<longleftrightarrow> (\<forall>a\<in>A. f a = {#})"
   using assms by induct simp_all
 
+lemma Union_mset_empty_conv[simp]: "\<Union># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})"
+  by (induction M) auto
+
 context comm_monoid_mult
 begin
 
@@ -2529,76 +2542,73 @@
 
 text \<open>One direction.\<close>
 lemma mult_implies_one_step:
-  "trans r \<Longrightarrow> (M, N) \<in> mult r \<Longrightarrow>
-    \<exists>I J K. N = 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> r)"
-apply (unfold mult_def mult1_def)
-apply (erule converse_trancl_induct, clarify)
- apply (rule_tac x = M0 in exI, simp)
-apply clarify
-apply (case_tac "a \<in># K")
- apply (rule_tac x = I in exI)
- apply (simp (no_asm))
- apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
- apply (simp (no_asm_simp) add: add.assoc [symmetric])
- apply (drule union_single_eq_diff)
- apply (auto simp: subset_mset.add_diff_assoc dest: in_diffD)[]
- apply (meson transD)
-apply (subgoal_tac "a \<in># I")
- apply (rule_tac x = "I - {#a#}" in exI)
- apply (rule_tac x = "add_mset a J" in exI)
- apply (rule_tac x = "K + Ka" in exI)
- apply (rule conjI)
-  apply (simp add: multiset_eq_iff union_single_eq_diff split: nat_diff_split)
- apply (rule conjI)
- apply (drule union_single_eq_diff)
- apply (simp add: add.assoc subset_mset.add_diff_assoc2)
-  apply (simp)
-  apply (simp add: multiset_eq_iff split: nat_diff_split)
- apply (simp (no_asm_use) add: trans_def)
-apply (subgoal_tac "a \<in># add_mset a M0")
- apply (simp_all add: not_in_iff)
- apply blast
-by (metis (no_types, lifting) not_in_iff union_iff union_single_eq_member)
-
-lemma one_step_implies_mult_aux:
-  "\<forall>I J K. size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)
-    \<longrightarrow> (I + K, I + J) \<in> mult r"
-apply (induct n)
- apply auto
-apply (frule size_eq_Suc_imp_eq_union, clarify)
-apply (rename_tac "J'", simp)
-apply (case_tac "J' = {#}")
- apply (simp add: mult_def)
- apply (rule r_into_trancl)
- apply (simp add: mult1_def, blast)
-txt \<open>Now we know @{term "J' \<noteq> {#}"}.\<close>
-apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
-apply (erule_tac P = "\<forall>k \<in> set_mset K. P k" for P in rev_mp)
-apply (simp add: Ball_def, auto)
-apply (subgoal_tac
-  "((I + {# x \<in># K. (x, a) \<in> r #}) + {# x \<in># K. (x, a) \<notin> r #},
-    (I + {# x \<in># K. (x, a) \<in> r #}) + J') \<in> mult r")
-prefer 2
-  apply (drule_tac x = "I + {# x \<in># K. (x, a) \<in> r#}" in spec)
-  apply (drule_tac x = "J'" in spec)
-  apply (drule_tac x = "{# x \<in># K. (x, a) \<notin> r#}" in spec)
-  apply auto[]
-apply (simp (no_asm_use) add: add.assoc [symmetric] mult_def)
-apply (subst (asm)(1) add.assoc)
-apply (subst (asm)(2) multiset_partition[symmetric])
-apply (erule trancl_trans)
-apply (rule r_into_trancl)
-apply (simp add: mult1_def)
-apply (rule_tac x = a in exI)
-apply (rule_tac x = "I + J'" in exI)
-apply simp
-done
+  assumes
+    trans: "trans r" and
+    MN: "(M, N) \<in> mult r"
+  shows "\<exists>I J K. N = 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> r)"
+  using MN unfolding mult_def mult1_def
+proof (induction rule: converse_trancl_induct)
+  case (base y)
+  then show ?case by force
+next
+  case (step y z) note yz = this(1) and zN = this(2) and N_decomp = this(3)
+  obtain I J K where
+    N: "N = I + J" "z = I + K" "J \<noteq> {#}" "\<forall>k\<in>#K. \<exists>j\<in>#J. (k, j) \<in> r"
+    using N_decomp by blast
+  obtain a M0 K' where
+    z: "z = add_mset a M0" and y: "y = M0 + K'" and K: "\<forall>b. b \<in># K' \<longrightarrow> (b, a) \<in> r"
+    using yz by blast
+  show ?case
+  proof (cases "a \<in># K")
+    case True
+    moreover have "\<exists>j\<in>#J. (k, j) \<in> r" if "k \<in># K'" for k
+      using K N trans True by (meson that transE)
+    ultimately show ?thesis
+      by (rule_tac x = I in exI, rule_tac x = J in exI, rule_tac x = "(K - {#a#}) + K'" in exI)
+        (use z y N in \<open>auto simp: subset_mset.add_diff_assoc dest: in_diffD\<close>)
+  next
+    case False
+    then have "a \<in># I" by (metis N(2) union_iff union_single_eq_member z)
+    moreover have "M0 = I + K - {#a#}"
+      using N(2) z by force
+    ultimately show ?thesis
+      by (rule_tac x = "I - {#a#}" in exI, rule_tac x = "add_mset a J" in exI,
+          rule_tac x = "K + K'" in exI)
+        (use z y N False K in \<open>auto simp: subset_mset.diff_add_assoc2\<close>)
+  qed
+qed
 
 lemma one_step_implies_mult:
-  "J \<noteq> {#} \<Longrightarrow> \<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r
-    \<Longrightarrow> (I + K, I + J) \<in> mult r"
-using one_step_implies_mult_aux by blast
+  assumes
+    "J \<noteq> {#}" and
+    "\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r"
+  shows "(I + K, I + J) \<in> mult r"
+  using assms
+proof (induction "size J" arbitrary: I J K)
+  case 0
+  then show ?case by auto
+next
+  case (Suc n) note IH = this(1) and size_J = this(2)[THEN sym]
+  obtain J' a where J: "J = add_mset a J'"
+    using size_J by (blast dest: size_eq_Suc_imp_eq_union)
+  show ?case
+  proof (cases "J' = {#}")
+    case True
+    then show ?thesis
+      using J Suc by (fastforce simp add: mult_def mult1_def)
+  next
+    case [simp]: False
+    have K: "K = {#x \<in># K. (x, a) \<in> r#} + {#x \<in># K. (x, a) \<notin> r#}"
+      by (rule multiset_partition)
+    have "(I + K, (I + {# x \<in># K. (x, a) \<in> r #}) + J') \<in> mult r"
+      using IH[of J' "{# x \<in># K. (x, a) \<notin> r#}" "I + {# x \<in># K. (x, a) \<in> r#}"]
+        J Suc.prems K size_J by (auto simp: ac_simps)
+    moreover have "(I + {#x \<in># K. (x, a) \<in> r#} + J', I + J) \<in> mult r"
+      by (fastforce simp: J mult1_def mult_def)
+    ultimately show ?thesis
+      unfolding mult_def by simp
+  qed
+qed
 
 
 subsection \<open>The multiset extension is cancellative for multiset union\<close>