Theory KD_Region_Tree2

section ‹K-dimensional Region Trees - Version 2›

(*
This version does not move quadrants by +2^n but by 2*.
Is internally consistent but not the image one expects.
Advantages: no need for 2^n, very concise, eg "even" test instead of ≥ 2^n.
Maybe reverse bits to get the desired image?
*)

theory KD_Region_Tree2
imports
  "HOL-Library.NList"
  "HOL-Library.Tree" (* only for ‹height› *)
begin                                         

(* TODO: In Isabelle after 2023 - remove *)
lemma nlists_Suc: "nlists (Suc n) A = (⋃a∈A. (#) a ` nlists n A)"
  by(auto simp: set_eq_iff image_iff in_nlists_Suc_iff)

lemma in_nlists_UNIV: "xs ∈ nlists k UNIV ⟷ length xs = k"
unfolding nlists_def by(auto)

datatype 'a kdt = Box 'a | Split "'a kdt" "'a kdt"

(* For quickcheck: *)
datatype_compat kdt

type_synonym kdtb = "bool kdt"

text ‹A ‹kdt› is most easily explained by showing how quad trees are represented:
‹Q t0 t1 t2 t3› becomes @{term "Split (Split t0' t1') (Split t2' t3')"}
where ‹ti'› is the representation of ‹ti›; ‹L a› becomes @{term "Box a"}.
In general, each level of an abstract ‹k› dimensional tree subdivides space into ‹2^k›
subregions. This subdivision is represented by a ‹kdt› of depth at most ‹k›.
Further subdivisions of the subregions are seamlessly represented as the subtrees
at depth ‹k›. @{term "Box a"} represents a subregion entirely filled with ‹a›'s.
In contrast to quad trees, cubes can also occur half way down the subdivision.
For example, ‹Q (L a) (L a) (L b) (L c)› becomes @{term "Split (Box a) (Split (Box b) (Box c))"}.
›

instantiation kdt :: (type)height
begin

fun height_kdt :: "'a kdt ⇒ nat" where
"height (Box _) = 0" |
"height (Split l r) = max (height l) (height r) + 1"

instance ..

end

lemma height_0_iff: "height t = 0 ⟷ (∃x. t = Box x)"
by(cases t)auto

definition bits :: "nat ⇒ bool list set" where
"bits n ≡ nlists n UNIV"

(* for quickcheck *)
lemma bits_Suc[code]:
  "bits (Suc n) = (let B = bits n in (#) True ` B ∪ (#) False ` B)"
by(simp_all add: bits_def nlists_Suc UN_bool_eq Let_def)


subsection ‹Subtree›

fun subtree :: "'a kdt ⇒ bool list ⇒ 'a kdt" where
"subtree t [] = t" |
"subtree (Box x) _ = Box x" |
"subtree (Split l r) (b#bs) = subtree (if b then r else l) bs"

lemma subtree_Box[simp]: "subtree (Box x) bs = Box x"
by(cases bs)auto

lemma height_subtree: "height (subtree t bs) ≤ height t - length bs"
by(induction t bs rule: subtree.induct) auto

lemma height_subtree2: "⟦ height t ≤ k * (Suc n); length bs = k⟧ ⟹ height (subtree t bs) ≤ k * n"
using height_subtree[of t bs] by auto

lemma subtree_Split_Box: "length bs ≠ 0 ⟹ subtree (Split (Box b) (Box b)) bs = Box b"
by(auto simp: neq_Nil_conv)

(* Surprisingly, points_SplitC is not needed:
lemma points_Split_Box: "Suc 0 ≤ k*n ⟹ points k n (Split (Box b) (Box b)) = points k n (Box b)"
proof(induction n)
  case (Suc n)
  from ‹Suc 0 ≤ k*Suc n› have "k > 0" using neq0_conv by fastforce
  with Suc show ?case by(simp add: subtree_Split_Box nlists2_simp)
qed simp

lemma points_SplitC: "height (Split l r) ≤ k*n ⟹ points k n (SplitC l r) = points k n (Split l r)"
by(induction l r rule: SplitC.induct)
  (simp_all add: points_Split_Box)
*)

subsection ‹Shifting a coordinate by a boolean vector›

text ‹The ?›

definition mv :: "bool list ⇒ nat list ⇒ nat list" where
"mv = map2 (λb x. 2*x + (if b then 0 else 1))"

lemma map_zip1: "⟦ length xs = length ys; ∀p ∈ set(zip xs ys). f p = fst p ⟧ ⟹ map f (zip xs ys) = xs"
by (metis (no_types, lifting) map_eq_conv map_fst_zip)

lemma map_mv1: "⟦ length ps = length bs ⟧ ⟹ map even (mv bs ps) = bs"
by(auto simp: mv_def intro!: map_zip1 split: if_splits)

lemma map_zip2: "⟦ length xs = length ys; ∀p ∈ set(zip xs ys). f p = snd p ⟧ ⟹ map f (zip xs ys) = ys"
by (metis (no_types, lifting) map_eq_conv map_snd_zip)

lemma map_mv2: "⟦ length ps = length bs ⟧ ⟹ map (λx. x div 2) (mv bs ps) = ps"
by(auto simp: mv_def intro!: map_zip2)

lemma mv_map_map: "mv (map even ps) (map (λx. x div 2) ps) = ps"
unfolding nlists_def mv_def
by(auto simp add: map_eq_conv[where xs=ps and g=id,simplified] map2_map_map)

lemma mv_in_nlists:
  "⟦ p ∈ nlists k {0..<2 ^ n}; bs ∈ bits k ⟧ ⟹ mv bs p ∈ nlists k {0..<2 * 2 ^ n}"
unfolding mv_def nlists_def bits_def
by (fastforce dest: set_zip_rightD)


lemma in_nlists2D: "xs ∈ nlists k {0..<2 * 2 ^ n} ⟹ ∃bs∈ bits k. xs ∈ mv bs ` nlists k {0..<2 ^ n}"
unfolding nlists_def bits_def
apply(rule bexI[where x = "map even xs"])
 apply(auto simp: image_def)[1]
apply(rule exI[where x = "map (λi. i div 2) xs"])
apply(auto simp add: mv_map_map)
done

lemma nlists2_simp: "nlists k {0..<2 * 2 ^ n} = (⋃bs∈ bits k. mv bs ` nlists k {0..<2 ^ n})"
by (auto simp: mv_in_nlists in_nlists2D)


subsection ‹Points in a tree›

fun cube :: "nat ⇒ nat ⇒ nat list set" where
"cube k n = nlists k {0..<2^n}"

fun points :: "nat ⇒ nat ⇒ kdtb ⇒ nat list set" where
"points k n (Box b) = (if b then cube k n else {})" |
"points k (Suc n) t = (⋃bs ∈ bits k. mv bs ` points k n (subtree t bs))"

lemma points_Suc: "points k (Suc n) t = (⋃bs ∈ bits k. mv bs ` points k n (subtree t bs))"
by(cases t) (simp_all add: nlists2_simp)

lemma points_subset: "height t ≤ k*n ⟹ points k n t ⊆ nlists k {0..<2^n}"
proof(induction k n t rule: points.induct)
  case (2 k n l r)
  have "⋀bs. bs ∈ bits k ⟹ height (subtree (Split l r) bs) ≤ k*n"
    unfolding bits_def using "2.prems" height_subtree2 in_nlists_UNIV by blast
  with "2.IH" show ?case
    by(auto intro: mv_in_nlists dest: subsetD)
qed auto


subsection ‹Compression›

text ‹Compressing Split:›

fun SplitC :: "'a kdt ⇒ 'a kdt ⇒ 'a kdt" where
"SplitC (Box b1) (Box b2) = (if b1=b2 then Box b1 else Split (Box b1) (Box b2))" |
"SplitC t1 t2 = Split t1 t2"

fun compressed :: "'a kdt ⇒ bool" where
"compressed (Box _) = True" |
"compressed (Split l r) = (compressed l ∧ compressed r ∧ ¬(∃b. l = Box b ∧ r = Box b))"

lemma compressedI: "⟦ compressed t1; compressed t2 ⟧ ⟹ compressed (SplitC t1 t2)"
by(induction t1 t2 rule: SplitC.induct) auto

lemma subtree_SplitC:
  "1 ≤ length bs ⟹ subtree (SplitC l r) bs = subtree (Split l r) bs"
by(induction l r rule: SplitC.induct)
  (simp_all add: subtree_Split_Box Suc_le_eq)


subsection ‹Union›

fun union :: "kdtb ⇒ kdtb ⇒ kdtb" where
  "union (Box b) t = (if b then Box True else t)" |
  "union t (Box b) = (if b then Box True else t)" |
  "union (Split l1 r1) (Split l2 r2) = SplitC (union l1 l2) (union r1 r2)"

lemma union_Box2: "union t (Box b) = (if b then Box True else t)"
  by(cases t) auto

lemma in_mv_image: "⟦ ps ∈ nlists k {0..<2*2^n}; Ps ⊆ nlists k {0..<2^n}; bs ∈ bits k ⟧ ⟹
  ps ∈ mv bs ` Ps ⟷ map (λx. x div 2) ps ∈ Ps ∧ (bs = map even ps)"
  by (auto simp: map_mv1 map_mv2 mv_map_map bits_def intro!: image_eqI)

lemma subtree_union: "subtree (union t1 t2) bs = union (subtree t1 bs) (subtree t2 bs)"
proof(induction t1 t2 arbitrary: bs rule: union.induct)
  case 2 thus ?case by(auto simp: union_Box2)
next
  case 3 thus ?case by(cases bs) (auto simp: subtree_SplitC)
qed auto

lemma points_union:
  "⟦ max (height t1) (height t2) ≤ k*n ⟧ ⟹
  points k n (union t1 t2) = points k n t1 ∪ points k n t2"
proof(induction n arbitrary: t1 t2)
  case 0 thus ?case by(clarsimp simp add: height_0_iff)
next
  case (Suc n)
  have "height t1 ≤ k * Suc n" "height t2 ≤ k * Suc n"
    using Suc.prems by auto
  from height_subtree2[OF this(1)] height_subtree2[OF this(2)] show ?case
    by(auto simp: Suc.IH subtree_union points_Suc bits_def)
qed

lemma compressed_union: "compressed t1 ⟹ compressed t2 ⟹ compressed(union t1 t2)"
  by(induction t1 t2 rule: union.induct) (simp_all add: compressedI)

subsection ‹Extracting a point from a tree›

lemma size_subtree: "bs ≠ [] ⟹ (∀b. t ≠ Box b) ⟹ size (subtree t bs) < size t"
  by (induction t bs rule: subtree.induct) force+

text ‹For termination of ‹get›:›

corollary size_subtree_Split[termination_simp]:
  "bs ≠ [] ⟹ size (subtree (Split l r) bs) < Suc (size l + size r)"
  using size_subtree by fastforce

fun get :: "'a kdt ⇒ nat list ⇒ 'a"  where
  "get (Box b) _ = b" |
  "get t ps = (if ps=[] then undefined else get (subtree t (map even ps)) (map (λi. i div 2) ps))"

lemma points_get: "⟦ height t ≤ k*n; ps ∈ nlists k {0..<2^n} ⟧ ⟹
  get t ps = (ps ∈ points k n t)"
proof(induction n arbitrary: k t ps)
  case 0
  then show ?case by(clarsimp simp add: height_0_iff)
next
  case (Suc n)
  show ?case
  proof (cases t)
    case Box
    thus ?thesis using Suc.prems(2) by(simp)
  next
    case (Split l r)
    obtain k0 where "k = Suc k0" using Suc.prems(1) Split
      by(cases k) auto
    hence "ps ≠ []"
      using Suc.prems(2) by (auto simp: in_nlists_Suc_iff)
    then show ?thesis using Suc.prems Split Suc.IH[OF height_subtree2[OF Suc.prems(1)]] in_nlists2D
      by(simp add: height_subtree2 in_mv_image points_subset bits_def)
  qed
qed

end