Quelle  Range_Search.thy

(*
  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 ‹p₀› and ‹p₁› 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 "p₀$k ≤ p$k ∧ p$k ≤ p₁$k"} \newline

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

subsection ‹Rectangle Definition›

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


subsection ‹Search Function›

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


subsection ‹Auxiliary Lemmas›

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

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


subsection ‹Main Theorem›

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

end