# HG changeset patch
# User nipkow
# Date 1502782175 -7200
# Node ID 8756322dc5de7bef68298b38b774482f80201b83
# Parent  df186e69b651fd267edd86840ecb25e88e2e13cb
added Min_mset and Max_mset

diff -r df186e69b651 -r 8756322dc5de src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Mon Aug 14 21:42:55 2017 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Tue Aug 15 09:29:35 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)
diff -r df186e69b651 -r 8756322dc5de src/HOL/Data_Structures/Priority_Queue.thy
--- a/src/HOL/Data_Structures/Priority_Queue.thy	Mon Aug 14 21:42:55 2017 +0100
+++ b/src/HOL/Data_Structures/Priority_Queue.thy	Tue Aug 15 09:29:35 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 =
diff -r df186e69b651 -r 8756322dc5de src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Mon Aug 14 21:42:55 2017 +0100
+++ b/src/HOL/Lattices_Big.thy	Tue Aug 15 09:29:35 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> {}"
diff -r df186e69b651 -r 8756322dc5de src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Aug 14 21:42:55 2017 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Aug 15 09:29:35 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"