added Min_mset and Max_mset
authornipkow
Tue Aug 15 09:29:35 2017 +0200 (22 months ago)
changeset 664258756322dc5de
parent 66423 df186e69b651
child 66426 a5dd01b68218
added Min_mset and Max_mset
src/HOL/Data_Structures/Leftist_Heap.thy
src/HOL/Data_Structures/Priority_Queue.thy
src/HOL/Lattices_Big.thy
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Data_Structures/Leftist_Heap.thy	Mon Aug 14 21:42:55 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Tue Aug 15 09:29:35 2017 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4  by (auto simp add: insert_def mset_merge)
     1.5  
     1.6  lemma get_min: "\<lbrakk> heap h;  h \<noteq> Leaf \<rbrakk> \<Longrightarrow> get_min h = Min_mset (mset_tree h)"
     1.7 -by (induction h) (auto simp add:Min_mset_alt)
     1.8 +by (induction h) (auto simp add: eq_Min_iff)
     1.9  
    1.10  lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}"
    1.11  by (cases h) (auto simp: mset_merge)
     2.1 --- a/src/HOL/Data_Structures/Priority_Queue.thy	Mon Aug 14 21:42:55 2017 +0100
     2.2 +++ b/src/HOL/Data_Structures/Priority_Queue.thy	Tue Aug 15 09:29:35 2017 +0200
     2.3 @@ -6,33 +6,6 @@
     2.4  imports "~~/src/HOL/Library/Multiset"
     2.5  begin
     2.6  
     2.7 -(* FIXME abbreviation? mv *)
     2.8 -definition Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
     2.9 -"Min_mset = Min o set_mset"
    2.10 -
    2.11 -(* FIXME intros needed? *)
    2.12 -
    2.13 -lemma Min_mset_contained[simp, intro]: "m\<noteq>{#} \<Longrightarrow> Min_mset m \<in># m"    
    2.14 -by (simp add: Min_mset_def)
    2.15 -
    2.16 -lemma Min_mset_min[simp, intro]: "x\<in># m \<Longrightarrow> Min_mset m \<le> x"
    2.17 -by (simp add: Min_mset_def)
    2.18 -    
    2.19 -lemma Min_mset_alt: "m\<noteq>{#} \<Longrightarrow> (x=Min_mset m) \<longleftrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y))"
    2.20 -by (simp add: antisym)    
    2.21 -
    2.22 -(* FIXME a bit special *)
    2.23 -lemma eq_min_msetI[intro?]: 
    2.24 -  "m\<noteq>{#} \<Longrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y)) \<Longrightarrow> x=Min_mset m"    
    2.25 -using Min_mset_alt by blast
    2.26 -    
    2.27 -lemma Min_mset_singleton[simp]: "Min_mset {#x#} = x"
    2.28 -by (simp add: Min_mset_def)
    2.29 -    
    2.30 -lemma Min_mset_insert[simp]: 
    2.31 -  "m\<noteq>{#} \<Longrightarrow> Min_mset (add_mset x m) = min x (Min_mset m)"
    2.32 -by (simp add: Min_mset_def)
    2.33 -
    2.34  text \<open>Priority queue interface:\<close>
    2.35      
    2.36  locale Priority_Queue =
     3.1 --- a/src/HOL/Lattices_Big.thy	Mon Aug 14 21:42:55 2017 +0100
     3.2 +++ b/src/HOL/Lattices_Big.thy	Tue Aug 15 09:29:35 2017 +0200
     3.3 @@ -580,6 +580,22 @@
     3.4    from assms show "x \<le> Max A" by simp
     3.5  qed
     3.6  
     3.7 +lemma eq_Min_iff:
     3.8 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Min A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
     3.9 +by (meson Min_in Min_le antisym)
    3.10 +
    3.11 +lemma Min_eq_iff:
    3.12 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
    3.13 +by (meson Min_in Min_le antisym)
    3.14 +
    3.15 +lemma eq_Max_iff:
    3.16 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Max A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
    3.17 +by (meson Max_in Max_ge antisym)
    3.18 +
    3.19 +lemma Max_eq_iff:
    3.20 +  "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
    3.21 +by (meson Max_in Max_ge antisym)
    3.22 +
    3.23  context
    3.24    fixes A :: "'a set"
    3.25    assumes fin_nonempty: "finite A" "A \<noteq> {}"
     4.1 --- a/src/HOL/Library/Multiset.thy	Mon Aug 14 21:42:55 2017 +0100
     4.2 +++ b/src/HOL/Library/Multiset.thy	Tue Aug 15 09:29:35 2017 +0200
     4.3 @@ -388,6 +388,15 @@
     4.4    by auto
     4.5  
     4.6  
     4.7 +subsubsection \<open>Min and Max\<close>
     4.8 +
     4.9 +abbreviation Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
    4.10 +"Min_mset m \<equiv> Min (set_mset m)"
    4.11 +
    4.12 +abbreviation Max_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
    4.13 +"Max_mset m \<equiv> Max (set_mset m)"
    4.14 +
    4.15 +
    4.16  subsubsection \<open>Equality of multisets\<close>
    4.17  
    4.18  lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
    4.19 @@ -1469,7 +1478,7 @@
    4.20    case (Suc k)
    4.21    note ih = this(1) and Sk_eq_sz_M = this(2)
    4.22  
    4.23 -  let ?y = "Min (set_mset M)"
    4.24 +  let ?y = "Min_mset M"
    4.25    let ?N = "M - {#?y#}"
    4.26  
    4.27    have M: "M = add_mset ?y ?N"
    4.28 @@ -1490,7 +1499,7 @@
    4.29    case (Suc k)
    4.30    note ih = this(1) and Sk_eq_sz_M = this(2)
    4.31  
    4.32 -  let ?y = "Max (set_mset M)"
    4.33 +  let ?y = "Max_mset M"
    4.34    let ?N = "M - {#?y#}"
    4.35  
    4.36    have M: "M = add_mset ?y ?N"