Theory PST_General

section ‹General Priority Search Trees›

theory PST_General
imports 
  "HOL-Data_Structures.Tree2"
  Prio_Map_Specs
begin

text ‹\noindent
  We show how to implement priority maps
  by augmented binary search trees. That is, the basic data structure is some 
  arbitrary binary search tree, e.g.\ a red-black tree, implementing the map 
  from @{typ 'a} to @{typ 'b} by storing pairs ‹(k,p)› in each node. At this
  point we need to assume that the keys are also linearly ordered. To 
  implement ‹getmin› efficiently we annotate/augment each node with another pair
  ‹(k',p')›, the intended result of ‹getmin› when applied to that subtree. The 
  specification of ‹getmin› tells us that ‹(k',p')› must be in that subtree and
  that ‹p'› is the minimal priority in that subtree. Thus the annotation can be 
  computed by passing the ‹(k',p')› with the minimal ‹p'› up the tree. We will 
  now make this more precise for balanced binary trees in general.
  
  We assume that our trees are either leaves of the form @{term Leaf} or nodes 
  of the form @{term "Node l (kp, b) r"} where ‹l› and ‹r› are subtrees, ‹kp› is 
  the contents of the node (a key-priority pair) and ‹b› is some additional 
  balance information (e.g.\ colour, height, size, \dots). Augmented nodes are 
  of the form \<^term>‹Node l (kp, (b,kp')) r›.
›

type_synonym ('k,'p,'c) pstree = "(('k×'p) × ('c × ('k × 'p))) tree"
 
text ‹ 
  The following invariant states that a node annotation is actually a minimal 
  key-priority pair for the node's subtree.
›

fun invpst :: "('k,'p::linorder,'c) pstree ⇒ bool" where
  "invpst Leaf = True"
| "invpst (Node l (x, _,mkp) r) ⟷ invpst l ∧ invpst r
    ∧ is_min2 mkp (set (inorder l @ x # inorder r))"

text ‹The implementation of ‹getmin› is trivial:›

fun pst_getmin where
"pst_getmin (Node _ (_, _,a) _) = a"

lemma pst_getmin_ismin: 
  "invpst t ⟹ t≠Leaf ⟹ is_min2 (pst_getmin t) (set_tree t)"
by (cases t rule: pst_getmin.cases) auto

  
text ‹  
  It remains to upgrade the existing map operations to work with augmented nodes.
  Therefore we now show how to transform any function definition on un-augmented 
  trees into one on trees augmented with ‹(k',p')› pairs. A defining equation
  ‹f pats = e› for the original type of nodes is transformed into an equation
  ‹f pats' = e'› on the augmented type of nodes as follows:
  ▪ Every pattern @{term "Node l (kp, b) r"} in ‹pats› and ‹e› is replaced by
    @{term "Node l (kp, (b,DUMMY)) r"} to obtain ‹pats'› and ‹e⇩2›.
  ▪ To obtain ‹e'›, every expression @{term "Node l (kp, b) r"} in ‹e⇩2› is 
    replaced by ‹mkNode l kp b r› where:
›
  
definition "min2 ≡ λ(k,p) (k',p'). if p≤p' then (k,p) else (k',p')"

definition "min_kp a l r ≡ case (l,r) of
  (Leaf,Leaf) ⇒ a
| (Leaf,Node _ (_, (_,kpr)) _) ⇒ min2 a kpr
| (Node _ (_, (_,kpl)) _,Leaf) ⇒ min2 a kpl
| (Node _ (_, (_,kpl)) _,Node _ (_, (_,kpr)) _) ⇒ min2 a (min2 kpl kpr)"

definition "mkNode c l a r ≡ Node l (a, (c,min_kp a l r)) r"

text ‹  
  Note that this transformation does not affect the asymptotic complexity 
  of ‹f›. Therefore the priority search tree operations have the same complexity 
  as the underlying search tree operations, i.e.\ typically logarithmic 
  (‹update›, ‹delete›, ‹lookup›) and constant time (‹empty›, ‹is_empty›).
›

text ‹It is straightforward to show that @{const mkNode} preserves the invariant:› 
  
lemma is_min2_Empty[simp]: "¬is_min2 x {}"
by (auto simp: is_min2_def)

lemma is_min2_singleton[simp]: "is_min2 a {b} ⟷ b=a"
by (auto simp: is_min2_def)

lemma is_min2_insert:
  "is_min2 x (insert y ys) 
  ⟷ (y=x ∧ (∀z∈ys. snd x ≤ snd z)) ∨ (snd x ≤ snd y ∧ is_min2 x ys)"
by (auto simp: is_min2_def)

lemma is_min2_union:
  "is_min2 x (ys ∪ zs) 
  ⟷ (is_min2 x ys ∧ (∀z∈zs. snd x ≤ snd z)) 
    ∨ ((∀y∈ys. snd x ≤ snd y) ∧ is_min2 x zs)"
by (auto simp: is_min2_def)

lemma is_min2_min2_insI: "is_min2 y ys ⟹ is_min2 (min2 x y) (insert x ys)"
by (auto simp: is_min2_def min2_def split: prod.split)

lemma is_min2_mergeI: 
  "is_min2 x xs ⟹ is_min2 y ys ⟹ is_min2 (min2 x y) (xs ∪ ys)"
by (auto simp: is_min2_def min2_def split: prod.split)

theorem invpst_mkNode[simp]: "invpst (mkNode c l a r) ⟷ invpst l ∧ invpst r"
apply (cases l rule: invpst.cases; 
       cases r rule: invpst.cases; 
       simp add: mkNode_def min_kp_def)
  subgoal using is_min2_min2_insI by blast
 subgoal by (auto intro!: is_min2_min2_insI simp: insert_commute)
subgoal by (smt Un_insert_left Un_insert_right is_min2_mergeI is_min2_min2_insI 
                sup_assoc)
done

end