src/HOL/Data_Structures/Priority_Queue.thy
author nipkow
Mon Aug 14 22:06:26 2017 +0200 (23 months ago)
changeset 66419 8194ed7cf2cb
child 66425 8756322dc5de
permissions -rw-r--r--
separate file for priority queue interface; extended Leftist_Heap.
     1 (* Author: Tobias Nipkow, Peter Lammich *)
     2 
     3 section \<open>Priority Queue Interface\<close>
     4 
     5 theory Priority_Queue
     6 imports "~~/src/HOL/Library/Multiset"
     7 begin
     8 
     9 (* FIXME abbreviation? mv *)
    10 definition Min_mset :: "'a::linorder multiset \<Rightarrow> 'a" where
    11 "Min_mset = Min o set_mset"
    12 
    13 (* FIXME intros needed? *)
    14 
    15 lemma Min_mset_contained[simp, intro]: "m\<noteq>{#} \<Longrightarrow> Min_mset m \<in># m"    
    16 by (simp add: Min_mset_def)
    17 
    18 lemma Min_mset_min[simp, intro]: "x\<in># m \<Longrightarrow> Min_mset m \<le> x"
    19 by (simp add: Min_mset_def)
    20     
    21 lemma Min_mset_alt: "m\<noteq>{#} \<Longrightarrow> (x=Min_mset m) \<longleftrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y))"
    22 by (simp add: antisym)    
    23 
    24 (* FIXME a bit special *)
    25 lemma eq_min_msetI[intro?]: 
    26   "m\<noteq>{#} \<Longrightarrow> (x\<in>#m \<and> (\<forall>y\<in>#m. x\<le>y)) \<Longrightarrow> x=Min_mset m"    
    27 using Min_mset_alt by blast
    28     
    29 lemma Min_mset_singleton[simp]: "Min_mset {#x#} = x"
    30 by (simp add: Min_mset_def)
    31     
    32 lemma Min_mset_insert[simp]: 
    33   "m\<noteq>{#} \<Longrightarrow> Min_mset (add_mset x m) = min x (Min_mset m)"
    34 by (simp add: Min_mset_def)
    35 
    36 text \<open>Priority queue interface:\<close>
    37     
    38 locale Priority_Queue =
    39 fixes empty :: "'q"
    40 and is_empty :: "'q \<Rightarrow> bool"
    41 and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
    42 and get_min :: "'q \<Rightarrow> 'a"
    43 and del_min :: "'q \<Rightarrow> 'q"
    44 and invar :: "'q \<Rightarrow> bool"
    45 and mset :: "'q \<Rightarrow> 'a multiset"
    46 assumes mset_empty: "mset empty = {#}"
    47 and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
    48 and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
    49 and mset_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    50     mset (del_min q) = mset q - {# get_min q #}"
    51 and mset_get_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> get_min q = Min_mset (mset q)"
    52 and invar_empty: "invar empty"
    53 and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
    54 and invar_del_min: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> invar (del_min q)"
    55 begin
    56 
    57 (* FIXME why? *)
    58 
    59 lemma get_min_alt: "invar q \<Longrightarrow> mset q \<noteq> {#} \<Longrightarrow> 
    60   get_min q \<in># mset q \<and> (\<forall>x\<in>#mset q. get_min q \<le> x)"
    61   by (simp add: mset_get_min)
    62   
    63 lemmas invar_simps[simp] = invar_empty invar_insert invar_del_min
    64 lemmas mset_simps[simp] = mset_empty is_empty mset_insert mset_del_min mset_get_min
    65 
    66 end
    67 
    68 end