--- a/src/HOL/Data_Structures/Leftist_Heap.thy Tue Aug 15 11:41:58 2017 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy Tue Aug 15 11:52:17 2017 +0200
@@ -98,7 +98,7 @@
by (auto simp add: insert_def mset_merge)
lemma get_min: "\<lbrakk> heap h; h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)"
-by (induction h) (auto simp add:Min_mset_alt)
+by (induction h) (auto simp add: eq_Min_iff)
lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
by (cases h) (auto simp: mset_merge)
--- a/src/HOL/Data_Structures/Priority_Queue.thy Tue Aug 15 11:41:58 2017 +0200
+++ b/src/HOL/Data_Structures/Priority_Queue.thy Tue Aug 15 11:52:17 2017 +0200
@@ -6,33 +6,6 @@
imports "~~/src/HOL/Library/Multiset"
begin
-(* FIXME abbreviation? mv *)
-definition Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
-"Min_mset = Min o set_mset"
-
-(* FIXME intros needed? *)
-
-lemma Min_mset_contained[simp, intro]: "m\<noteq>{#} \<Longrightarrow> Min_mset m \<in># m"
-by (simp add: Min_mset_def)
-
-lemma Min_mset_min[simp, intro]: "x\<in># m \<Longrightarrow> Min_mset m \<le> x"
-by (simp add: Min_mset_def)
-
-lemma Min_mset_alt: "m\<noteq>{#} \<Longrightarrow> (x=Min_mset m) \<longleftrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y))"
-by (simp add: antisym)
-
-(* FIXME a bit special *)
-lemma eq_min_msetI[intro?]:
- "m\<noteq>{#} \<Longrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y)) \<Longrightarrow> x=Min_mset m"
-using Min_mset_alt by blast
-
-lemma Min_mset_singleton[simp]: "Min_mset {#x#} = x"
-by (simp add: Min_mset_def)
-
-lemma Min_mset_insert[simp]:
- "m\<noteq>{#} \<Longrightarrow> Min_mset (add_mset x m) = min x (Min_mset m)"
-by (simp add: Min_mset_def)
-
text \<open>Priority queue interface:\<close>
locale Priority_Queue =
--- a/src/HOL/Lattices_Big.thy Tue Aug 15 11:41:58 2017 +0200
+++ b/src/HOL/Lattices_Big.thy Tue Aug 15 11:52:17 2017 +0200
@@ -580,6 +580,22 @@
from assms show "x \<le> Max A" by simp
qed
+lemma eq_Min_iff:
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Min A \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
+by (meson Min_in Min_le antisym)
+
+lemma Min_eq_iff:
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A = m \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
+by (meson Min_in Min_le antisym)
+
+lemma eq_Max_iff:
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Max A \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
+by (meson Max_in Max_ge antisym)
+
+lemma Max_eq_iff:
+ "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A = m \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
+by (meson Max_in Max_ge antisym)
+
context
fixes A :: "'a set"
assumes fin_nonempty: "finite A" "A \<noteq> {}"
--- a/src/HOL/Library/Multiset.thy Tue Aug 15 11:41:58 2017 +0200
+++ b/src/HOL/Library/Multiset.thy Tue Aug 15 11:52:17 2017 +0200
@@ -388,6 +388,15 @@
by auto
+subsubsection \<open>Min and Max\<close>
+
+abbreviation Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
+"Min_mset m \<equiv> Min (set_mset m)"
+
+abbreviation Max_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
+"Max_mset m \<equiv> Max (set_mset m)"
+
+
subsubsection \<open>Equality of multisets\<close>
lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
@@ -1469,7 +1478,7 @@
case (Suc k)
note ih = this(1) and Sk_eq_sz_M = this(2)
- let ?y = "Min (set_mset M)"
+ let ?y = "Min_mset M"
let ?N = "M - {#?y#}"
have M: "M = add_mset ?y ?N"
@@ -1490,7 +1499,7 @@
case (Suc k)
note ih = this(1) and Sk_eq_sz_M = this(2)
- let ?y = "Max (set_mset M)"
+ let ?y = "Max_mset M"
let ?N = "M - {#?y#}"
have M: "M = add_mset ?y ?N"