# 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: "\ heap h; h \ Leaf \ \ 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 \ 'a" where -"Min_mset = Min o set_mset" - -(* FIXME intros needed? *) - -lemma Min_mset_contained[simp, intro]: "m\{#} \ Min_mset m \# m" -by (simp add: Min_mset_def) - -lemma Min_mset_min[simp, intro]: "x\# m \ Min_mset m \ x" -by (simp add: Min_mset_def) - -lemma Min_mset_alt: "m\{#} \ (x=Min_mset m) \ (x\#m \ (\y\#m. x\y))" -by (simp add: antisym) - -(* FIXME a bit special *) -lemma eq_min_msetI[intro?]: - "m\{#} \ (x\#m \ (\y\#m. x\y)) \ 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\{#} \ Min_mset (add_mset x m) = min x (Min_mset m)" -by (simp add: Min_mset_def) - text \Priority queue interface:\ 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 \ Max A" by simp qed +lemma eq_Min_iff: + "\ finite A; A \ {} \ \ m = Min A \ m \ A \ (\a \ A. m \ a)" +by (meson Min_in Min_le antisym) + +lemma Min_eq_iff: + "\ finite A; A \ {} \ \ Min A = m \ m \ A \ (\a \ A. m \ a)" +by (meson Min_in Min_le antisym) + +lemma eq_Max_iff: + "\ finite A; A \ {} \ \ m = Max A \ m \ A \ (\a \ A. a \ m)" +by (meson Max_in Max_ge antisym) + +lemma Max_eq_iff: + "\ finite A; A \ {} \ \ Max A = m \ m \ A \ (\a \ A. a \ m)" +by (meson Max_in Max_ge antisym) + context fixes A :: "'a set" assumes fin_nonempty: "finite A" "A \ {}" 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 \Min and Max\ + +abbreviation Min_mset :: "'a::linorder multiset \ 'a" where +"Min_mset m \ Min (set_mset m)" + +abbreviation Max_mset :: "'a::linorder multiset \ 'a" where +"Max_mset m \ Max (set_mset m)" + + subsubsection \Equality of multisets\ lemma single_eq_single [simp]: "{#a#} = {#b#} \ 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"