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