src/HOL/Data_Structures/Priority_Queue.thy
changeset 66419 8194ed7cf2cb
child 66425 8756322dc5de
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/Priority_Queue.thy	Mon Aug 14 22:06:26 2017 +0200
     1.3 @@ -0,0 +1,68 @@
     1.4 +(* Author: Tobias Nipkow, Peter Lammich *)
     1.5 +
     1.6 +section \<open>Priority Queue Interface\<close>
     1.7 +
     1.8 +theory Priority_Queue
     1.9 +imports "~~/src/HOL/Library/Multiset"
    1.10 +begin
    1.11 +
    1.12 +(* FIXME abbreviation? mv *)
    1.13 +definition Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
    1.14 +"Min_mset = Min o set_mset"
    1.15 +
    1.16 +(* FIXME intros needed? *)
    1.17 +
    1.18 +lemma Min_mset_contained[simp, intro]: "m\<noteq>{#} \<Longrightarrow> Min_mset m \<in># m"    
    1.19 +by (simp add: Min_mset_def)
    1.20 +
    1.21 +lemma Min_mset_min[simp, intro]: "x\<in># m \<Longrightarrow> Min_mset m \<le> x"
    1.22 +by (simp add: Min_mset_def)
    1.23 +    
    1.24 +lemma Min_mset_alt: "m\<noteq>{#} \<Longrightarrow> (x=Min_mset m) \<longleftrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y))"
    1.25 +by (simp add: antisym)    
    1.26 +
    1.27 +(* FIXME a bit special *)
    1.28 +lemma eq_min_msetI[intro?]: 
    1.29 +  "m\<noteq>{#} \<Longrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y)) \<Longrightarrow> x=Min_mset m"    
    1.30 +using Min_mset_alt by blast
    1.31 +    
    1.32 +lemma Min_mset_singleton[simp]: "Min_mset {#x#} = x"
    1.33 +by (simp add: Min_mset_def)
    1.34 +    
    1.35 +lemma Min_mset_insert[simp]: 
    1.36 +  "m\<noteq>{#} \<Longrightarrow> Min_mset (add_mset x m) = min x (Min_mset m)"
    1.37 +by (simp add: Min_mset_def)
    1.38 +
    1.39 +text \<open>Priority queue interface:\<close>
    1.40 +    
    1.41 +locale Priority_Queue =
    1.42 +fixes empty :: "'q"
    1.43 +and is_empty :: "'q \<Rightarrow> bool"
    1.44 +and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
    1.45 +and get_min :: "'q \<Rightarrow> 'a"
    1.46 +and del_min :: "'q \<Rightarrow> 'q"
    1.47 +and invar :: "'q \<Rightarrow> bool"
    1.48 +and mset :: "'q \<Rightarrow> 'a multiset"
    1.49 +assumes mset_empty: "mset empty = {#}"
    1.50 +and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
    1.51 +and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
    1.52 +and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    1.53 +    mset (del_min q) = mset q - {# get_min q #}"
    1.54 +and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
    1.55 +and invar_empty: "invar empty"
    1.56 +and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
    1.57 +and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
    1.58 +begin
    1.59 +
    1.60 +(* FIXME why? *)
    1.61 +
    1.62 +lemma get_min_alt: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    1.63 +  get_min q \<in># mset q \<and> (\<forall>x\<in>#mset q. get_min q \<le> x)"
    1.64 +  by (simp add: mset_get_min)
    1.65 +  
    1.66 +lemmas invar_simps[simp] = invar_empty invar_insert invar_del_min
    1.67 +lemmas mset_simps[simp] = mset_empty is_empty mset_insert mset_del_min mset_get_min
    1.68 +
    1.69 +end
    1.70 +
    1.71 +end