# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1467353993 -7200
# Node ID a500677d4cecb29aa92263795dd9bcdfc718d452
# Parent  bf2cf06537411435fc18e7c0fdb7d363b8fab2c8
Conditionally complete lattice of multisets

diff -r bf2cf0653741 -r a500677d4cec src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Jun 26 01:03:03 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Jul 01 08:19:53 2016 +0200
@@ -779,6 +779,228 @@
 
 interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
 
+subsubsection \<open>Conditionally complete lattice\<close>
+
+instantiation multiset :: (type) Inf
+begin
+
+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
+  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)
+    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:A. f i) \<in> multiset" by (simp add: multiset_def)
+qed
+
+instance ..
+
+end
+
+lemma Inf_multiset_empty: "Inf {} = {#}"
+  by transfer simp_all
+
+lemma count_Inf_multiset_nonempty: "A \<noteq> {} \<Longrightarrow> count (Inf A) x = Inf ((\<lambda>X. count X x) ` A)"
+  by transfer simp_all
+
+
+instantiation multiset :: (type) Sup
+begin
+
+lift_definition Sup_multiset :: "'a multiset set \<Rightarrow> 'a multiset" is
+  "\<lambda>A i. if A \<noteq> {} \<and> (\<forall>i. bdd_above ((\<lambda>f. f i) ` A)) \<and> finite (\<Union>f\<in>A. {i. f i > 0}) then
+           Sup ((\<lambda>f. f i) ` A) else 0"
+proof -
+  fix A :: "('a \<Rightarrow> nat) set" assume *: "\<And>x. x \<in> A \<Longrightarrow> x \<in> multiset"
+  show "(\<lambda>i. if A \<noteq> {} \<and> (\<forall>i. bdd_above ((\<lambda>f. f i) ` A)) \<and> finite (\<Union>f\<in>A. {i. 0 < f i})
+               then SUP f:A. f i else 0) \<in> multiset"
+  proof (cases "A \<noteq> {} \<and> (\<forall>i. bdd_above ((\<lambda>f. f i) ` A)) \<and> finite (\<Union>f\<in>A. {i. 0 < f i})")
+    case True
+    have "{i. Sup ((\<lambda>f. f i) ` A) > 0} \<subseteq> (\<Union>f\<in>A. {i. 0 < f i})"
+    proof safe
+      fix i assume pos: "(SUP f:A. f i) > 0"
+      show "i \<in> (\<Union>f\<in>A. {i. 0 < f i})"
+      proof (rule ccontr)
+        assume "i \<notin> (\<Union>f\<in>A. {i. 0 < f i})"
+        hence "\<forall>f\<in>A. f i \<le> 0" by auto
+        with True have "(SUP f:A. f i) \<le> 0"
+          by (intro cSup_least) auto
+        with pos show False by simp
+      qed
+    qed
+    moreover from True have "finite \<dots>" by blast
+    ultimately have "finite {i. Sup ((\<lambda>f. f i) ` A) > 0}" by (rule finite_subset)
+    with True show ?thesis by (simp add: multiset_def)
+  qed (simp_all add: multiset_def)
+qed
+
+instance ..
+
+end
+
+lemma Sup_multiset_empty: "Sup {} = {#}"
+  by transfer simp_all
+
+lemma bdd_below_multiset [simp]: "subset_mset.bdd_below A"
+  by (intro subset_mset.bdd_belowI[of _ "{#}"]) simp_all
+
+lemma bdd_above_multiset_imp_bdd_above_count:
+  assumes "subset_mset.bdd_above (A :: 'a multiset set)"
+  shows   "bdd_above ((\<lambda>X. count X x) ` A)"
+proof -
+  from assms obtain Y where Y: "\<forall>X\<in>A. X \<subseteq># Y"
+    by (auto simp: subset_mset.bdd_above_def)
+  hence "count X x \<le> count Y x" if "X \<in> A" for X
+    using that by (auto intro: mset_subset_eq_count)
+  thus ?thesis by (intro bdd_aboveI[of _ "count Y x"]) auto
+qed
+
+lemma bdd_above_multiset_imp_finite_support:
+  assumes "A \<noteq> {}" "subset_mset.bdd_above (A :: 'a multiset set)"
+  shows   "finite (\<Union>X\<in>A. {x. count X x > 0})"
+proof -
+  from assms obtain Y where Y: "\<forall>X\<in>A. X \<subseteq># Y"
+    by (auto simp: subset_mset.bdd_above_def)
+  hence "count X x \<le> count Y x" if "X \<in> A" for X x
+    using that by (auto intro: mset_subset_eq_count)
+  hence "(\<Union>X\<in>A. {x. count X x > 0}) \<subseteq> {x. count Y x > 0}"
+    by safe (erule less_le_trans)
+  moreover have "finite \<dots>" by simp
+  ultimately show ?thesis 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:A. count X x)"
+proof -
+  from bdd_above_multiset_imp_bdd_above_count[OF assms(2)]
+    have "\<forall>x. bdd_above ((\<lambda>X. count X x) ` A)" ..
+  moreover from bdd_above_multiset_imp_finite_support[OF assms]
+    have "finite (\<Union>X\<in>A. {x. count X x > 0})" .
+  ultimately show ?thesis using assms(1) by transfer simp
+qed
+
+
+interpretation subset_mset: conditionally_complete_lattice Inf Sup "op #\<inter>" "op \<subseteq>#" "op \<subset>#" "op #\<union>"
+proof
+  fix X :: "'a multiset" and A
+  assume "X \<in> A"
+  show "Inf A \<subseteq># X"
+  proof (rule mset_subset_eqI)
+    fix x
+    from \<open>X \<in> A\<close> have "A \<noteq> {}" by auto
+    hence "count (Inf A) x = (INF X:A. count X x)"
+      by (simp add: count_Inf_multiset_nonempty)
+    also from \<open>X \<in> A\<close> have "\<dots> \<le> count X x"
+      by (intro cInf_lower) simp_all
+    finally show "count (Inf A) x \<le> count X x" .
+  qed
+next
+  fix X :: "'a multiset" and A
+  assume nonempty: "A \<noteq> {}" and le: "\<And>Y. Y \<in> A \<Longrightarrow> X \<subseteq># Y"
+  show "X \<subseteq># Inf A"
+  proof (rule mset_subset_eqI)
+    fix x
+    from nonempty have "count X x \<le> (INF X:A. count X x)"
+      by (intro cInf_greatest) (auto intro: mset_subset_eq_count le)
+    also from nonempty have "\<dots> = count (Inf A) x" by (simp add: count_Inf_multiset_nonempty)
+    finally show "count X x \<le> count (Inf A) x" .
+  qed
+next
+  fix X :: "'a multiset" and A
+  assume X: "X \<in> A" and bdd: "subset_mset.bdd_above A"
+  show "X \<subseteq># Sup A"
+  proof (rule mset_subset_eqI)
+    fix x
+    from X have "A \<noteq> {}" by auto
+    have "count X x \<le> (SUP X:A. count X x)"
+      by (intro cSUP_upper X bdd_above_multiset_imp_bdd_above_count bdd)
+    also from count_Sup_multiset_nonempty[OF \<open>A \<noteq> {}\<close> bdd]
+      have "(SUP X:A. count X x) = count (Sup A) x" by simp
+    finally show "count X x \<le> count (Sup A) x" .
+  qed
+next
+  fix X :: "'a multiset" and A
+  assume nonempty: "A \<noteq> {}" and ge: "\<And>Y. Y \<in> A \<Longrightarrow> Y \<subseteq># X"
+  from ge have bdd: "subset_mset.bdd_above A" by (rule subset_mset.bdd_aboveI[of _ X])
+  show "Sup A \<subseteq># X"
+  proof (rule mset_subset_eqI)
+    fix x
+    from count_Sup_multiset_nonempty[OF \<open>A \<noteq> {}\<close> bdd]
+      have "count (Sup A) x = (SUP X:A. count X x)" .
+    also from nonempty have "\<dots> \<le> count X x"
+      by (intro cSup_least) (auto intro: mset_subset_eq_count ge)
+    finally show "count (Sup A) x \<le> count X x" .
+  qed
+qed
+
+lemma set_mset_Inf:
+  assumes "A \<noteq> {}"
+  shows   "set_mset (Inf A) = (\<Inter>X\<in>A. set_mset X)"
+proof safe
+  fix x X assume "x \<in># Inf A" "X \<in> A"
+  hence nonempty: "A \<noteq> {}" by (auto simp: Inf_multiset_empty)
+  from \<open>x \<in># Inf A\<close> have "{#x#} \<subseteq># Inf A" by auto
+  also from \<open>X \<in> A\<close> have "\<dots> \<subseteq># X" by (rule subset_mset.cInf_lower) simp_all
+  finally show "x \<in># X" by simp
+next
+  fix x assume x: "x \<in> (\<Inter>X\<in>A. set_mset X)"
+  hence "{#x#} \<subseteq># X" if "X \<in> A" for X using that by auto
+  from assms and this have "{#x#} \<subseteq># Inf A" by (rule subset_mset.cInf_greatest)
+  thus "x \<in># Inf A" by simp
+qed
+
+lemma in_Inf_multiset_iff:
+  assumes "A \<noteq> {}"
+  shows   "x \<in># Inf A \<longleftrightarrow> (\<forall>X\<in>A. x \<in># X)"
+proof -
+  from assms have "set_mset (Inf A) = (\<Inter>X\<in>A. set_mset X)" by (rule set_mset_Inf)
+  also have "x \<in> \<dots> \<longleftrightarrow> (\<forall>X\<in>A. x \<in># X)" by simp
+  finally show ?thesis .
+qed
+
+lemma set_mset_Sup:
+  assumes "subset_mset.bdd_above A"
+  shows   "set_mset (Sup A) = (\<Union>X\<in>A. set_mset X)"
+proof safe
+  fix x assume "x \<in># Sup A"
+  hence nonempty: "A \<noteq> {}" by (auto simp: Sup_multiset_empty)
+  show "x \<in> (\<Union>X\<in>A. set_mset X)"
+  proof (rule ccontr)
+    assume x: "x \<notin> (\<Union>X\<in>A. set_mset X)"
+    have "count X x \<le> count (Sup A) x" if "X \<in> A" for X x
+      using that by (intro mset_subset_eq_count subset_mset.cSup_upper assms)
+    with x have "X \<subseteq># Sup A - {#x#}" if "X \<in> A" for X
+      using that by (auto simp: subseteq_mset_def algebra_simps not_in_iff)
+    hence "Sup A \<subseteq># Sup A - {#x#}" by (intro subset_mset.cSup_least nonempty)
+    with \<open>x \<in># Sup A\<close> show False
+      by (auto simp: subseteq_mset_def count_greater_zero_iff [symmetric]
+               simp del: count_greater_zero_iff dest!: spec[of _ x])
+  qed
+next
+  fix x X assume "x \<in> set_mset X" "X \<in> A"
+  hence "{#x#} \<subseteq># X" by auto
+  also have "X \<subseteq># Sup A" by (intro subset_mset.cSup_upper \<open>X \<in> A\<close> assms)
+  finally show "x \<in> set_mset (Sup A)" by simp
+qed
+
+lemma in_Sup_multiset_iff:
+  assumes "subset_mset.bdd_above A"
+  shows   "x \<in># Sup A \<longleftrightarrow> (\<exists>X\<in>A. x \<in># X)"
+proof -
+  from assms have "set_mset (Sup A) = (\<Union>X\<in>A. set_mset X)" by (rule set_mset_Sup)
+  also have "x \<in> \<dots> \<longleftrightarrow> (\<exists>X\<in>A. x \<in># X)" by simp
+  finally show ?thesis .
+qed
+
 
 subsubsection \<open>Filter (with comprehension syntax)\<close>