Theory Prio_Map_Specs

section ‹Priority Map Specifications›

theory Prio_Map_Specs
imports "HOL-Data_Structures.Map_Specs"
begin

(*<*)
(** TODO/FIXME:
  Duplicated from List_Ins_Del.
  We cannot import this theory, as it has name clashed with AList_Upd_Del!
*)
lemma sorted_Cons_iff:
  "sorted(x # xs) = ((∀y ∈ set xs. x < y) ∧ sorted xs)"
by(simp add: sorted_wrt_Cons)

(** TODO: Belongs into AList_Upd_Del *)
lemma sorted_map_of_Some_eq: 
  "sorted1 xs ⟹ map_of xs k = Some v ⟷ (k,v)∈set xs"
by (induction xs arbitrary: k v) (auto split: if_splits simp: sorted_Cons_iff)

(*>*)
  
subsection ‹Abstract Data Type›
  
locale PrioMap = Map where lookup = lookup 
  for lookup :: "'m ⇒ 'a ⇒ 'b::linorder option" +
  fixes is_empty :: "'m ⇒ bool"
  fixes getmin :: "'m ⇒ 'a × 'b"
  assumes map_is_empty: "invar m ⟹ is_empty m ⟷ lookup m = Map.empty"
  and map_getmin: "getmin m = (k,p) ⟹ invar m ⟹ lookup m ≠ Map.empty 
  ⟹ lookup m k = Some p ∧ (∀p'∈ran (lookup m). p≤p')"
begin

lemmas prio_map_specs = map_specs map_is_empty 

lemma map_getminE:
  assumes "getmin m = (k,p)" "invar m" "lookup m ≠ Map.empty" 
  obtains "lookup m k = Some p" "∀k' p'. lookup m k' = Some p' ⟶ p≤p'"  
using map_getmin[OF assms] by (auto simp: ran_def)

end

definition is_min2 :: "(_×'a::linorder) ⇒ (_×'a) set ⇒ bool" where
"is_min2 x xs ≡ x∈xs ∧ (∀y∈xs. snd x ≤ snd y)"


subsection ‹Inorder-Based Specification›  
  
locale PrioMap_by_Ordered = Map_by_Ordered 
  where lookup=lookup for lookup :: "'t ⇒ 'a::linorder ⇒ 'b::linorder option" +
  fixes is_empty :: "'t ⇒ bool"
  fixes getmin :: "'t ⇒ 'a×'b"
  assumes inorder_isempty': "⟦inv t; sorted1 (inorder t)⟧ 
      ⟹ is_empty t ⟷ inorder t = []"
  and inorder_getmin': 
      "⟦inv t; sorted1 (inorder t); inorder t ≠ []; getmin t = (a,b)⟧ 
        ⟹ is_min2 (a,b) (set (inorder t))"
begin

lemma 
  inorder_isempty: "invar t ⟹ is_empty t ⟷ inorder t = []"
  and inorder_getmin: "⟦invar t; inorder t ≠ []; getmin t = (a,b)⟧ 
        ⟹ is_min2 (a,b) (set (inorder t))"
unfolding invar_def by (auto simp: inorder_isempty' inorder_getmin') 

lemma inorder_lookup_empty_iff: 
  "invar m ⟹ lookup m = Map.empty ⟷ inorder m = []"
using inorder_lookup[of m]
apply (auto split: if_splits simp: invar_def)
by (metis map_of.elims option.discI)

lemma inorder_lookup_ran_eq: 
  "⟦inv m; sorted1 (inorder m)⟧ ⟹ ran (lookup m) = snd ` set (inorder m)"
using inorder_lookup[of m] unfolding ran_def
by (force simp: sorted_map_of_Some_eq)

sublocale PrioMap empty update delete invar lookup is_empty getmin
apply unfold_locales
 apply (auto simp: inorder_isempty inorder_lookup_empty_iff)
 apply (frule (2) inorder_getmin)
 apply (auto simp: is_min2_def sorted_map_of_Some_eq invar_def inorder_lookup) []
apply (frule (2) inorder_getmin)
apply (force simp: is_min2_def sorted_map_of_Some_eq inorder_lookup_ran_eq 
                   eq_Min_iff invar_def inorder_lookup) []
done

end

end