Theory Range_Search

(*
  File:     Range_Search.thy
  Author:   Martin Rau, TU München
*)

section ‹Range Searching›

theory Range_Search
imports
  KD_Tree
begin

text‹
  Given two ‹k›-dimensional points ‹p0› and ‹p1› which bound the search space, the search should
  return only the points which satisfy the following criteria:

  For every point p in the resulting set: \newline
  \hspace{1cm}  For every axis @{term "k"}: \newline
  \hspace{2cm}    @{term "p0$k ≤ p$k ∧ p$k ≤ p1$k"} \newline

  For a ‹2›-d tree a query corresponds to selecting all the points in the rectangle that
  has ‹p0› and ‹p1› as its defining edges.
›

subsection ‹Rectangle Definition›

lemma cbox_point_def:
  fixes p0 :: "('k::finite) point"
  shows "cbox p0 p1 = { p. ∀k. p0$k ≤ p$k ∧ p$k ≤ p1$k }"
proof -
  have "cbox p0 p1 = { p. ∀k. p0 ∙ axis k 1 ≤ p ∙ axis k 1 ∧ p ∙ axis k 1 ≤ p1 ∙ axis k 1 }"
    unfolding cbox_def using axis_inverse by auto
  also have "... = { p. ∀k. p0$k ∙ 1 ≤ p$k ∙ 1 ∧ p$k ∙ 1 ≤ p1$k ∙ 1 }"
    using inner_axis[of _ _ 1]
    by (metis (mono_tags, opaque_lifting))
  also have "... = { p. ∀k. p0$k ≤ p$k ∧ p$k ≤ p1$k }"
    by simp
  finally show ?thesis .
qed


subsection ‹Search Function›

fun search :: "('k::finite) point ⇒ 'k point ⇒ 'k kdt ⇒ 'k point set" where
  "search p0 p1 (Leaf p) = (if p ∈ cbox p0 p1 then { p } else {})"
| "search p0 p1 (Node k v l r) = (
    if v < p0$k then
      search p0 p1 r
    else if p1$k < v then
      search p0 p1 l
    else
      search p0 p1 l ∪ search p0 p1 r
  )"


subsection ‹Auxiliary Lemmas›

lemma l_empty:
  assumes "invar (Node k v l r)" "v < p0$k"
  shows "set_kdt l ∩ cbox p0 p1 = {}"
proof -
  have "∀p ∈ set_kdt l. p$k < p0$k"
    using assms by auto
  hence "∀p ∈ set_kdt l. p ∉ cbox p0 p1"
    using cbox_point_def leD by blast
  thus ?thesis by blast
qed

lemma r_empty:
  assumes "invar (Node k v l r)" "p1$k < v"
  shows "set_kdt r ∩ cbox p0 p1 = {}"
proof -
  have "∀p ∈ set_kdt r. p1$k < p$k"
    using assms by auto
  hence "∀p ∈ set_kdt r. p ∉ cbox p0 p1"
    using cbox_point_def leD by blast
  thus ?thesis by blast
qed


subsection ‹Main Theorem›

theorem search_cbox:
  assumes "invar kdt"
  shows "search p0 p1 kdt = set_kdt kdt ∩ cbox p0 p1"
  using assms l_empty r_empty by (induction kdt) (auto, blast+)

end