src/HOL/Data_Structures/Priority_Queue.thy
changeset 66425 8756322dc5de
parent 66419 8194ed7cf2cb
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Data_Structures/Priority_Queue.thy	Mon Aug 14 21:42:55 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/Priority_Queue.thy	Tue Aug 15 09:29:35 2017 +0200
     1.3 @@ -6,33 +6,6 @@
     1.4  imports "~~/src/HOL/Library/Multiset"
     1.5  begin
     1.6  
     1.7 -(* FIXME abbreviation? mv *)
     1.8 -definition Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
     1.9 -"Min_mset = Min o set_mset"
    1.10 -
    1.11 -(* FIXME intros needed? *)
    1.12 -
    1.13 -lemma Min_mset_contained[simp, intro]: "m\<noteq>{#} \<Longrightarrow> Min_mset m \<in># m"    
    1.14 -by (simp add: Min_mset_def)
    1.15 -
    1.16 -lemma Min_mset_min[simp, intro]: "x\<in># m \<Longrightarrow> Min_mset m \<le> x"
    1.17 -by (simp add: Min_mset_def)
    1.18 -    
    1.19 -lemma Min_mset_alt: "m\<noteq>{#} \<Longrightarrow> (x=Min_mset m) \<longleftrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y))"
    1.20 -by (simp add: antisym)    
    1.21 -
    1.22 -(* FIXME a bit special *)
    1.23 -lemma eq_min_msetI[intro?]: 
    1.24 -  "m\<noteq>{#} \<Longrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y)) \<Longrightarrow> x=Min_mset m"    
    1.25 -using Min_mset_alt by blast
    1.26 -    
    1.27 -lemma Min_mset_singleton[simp]: "Min_mset {#x#} = x"
    1.28 -by (simp add: Min_mset_def)
    1.29 -    
    1.30 -lemma Min_mset_insert[simp]: 
    1.31 -  "m\<noteq>{#} \<Longrightarrow> Min_mset (add_mset x m) = min x (Min_mset m)"
    1.32 -by (simp add: Min_mset_def)
    1.33 -
    1.34  text \<open>Priority queue interface:\<close>
    1.35      
    1.36  locale Priority_Queue =