Theory Rect_Intersect

(*
  File: Rect_Intersect.thy
  Author: Bohua Zhan
*)

section ‹Rectangle intersection›

theory Rect_Intersect
  imports Interval_Tree
begin

text ‹
  Functional version of algorithm for detecting rectangle intersection.
  See \<^cite>‹‹Exercise 14.3-7› in "cormen2009introduction"› for a reference.
›

subsection ‹Definition of rectangles›

datatype 'a rectangle = Rectangle (xint: "'a interval") (yint: "'a interval")
setup ‹add_simple_datatype "rectangle"›

definition is_rect :: "('a::linorder) rectangle ⇒ bool" where [rewrite]:
  "is_rect rect ⟷ is_interval (xint rect) ∧ is_interval (yint rect)"

definition is_rect_list :: "('a::linorder) rectangle list ⇒ bool" where [rewrite]:
  "is_rect_list rects ⟷ (∀i<length rects. is_rect (rects ! i))"

lemma is_rect_listD: "is_rect_list rects ⟹ i < length rects ⟹ is_rect (rects ! i)" by auto2
setup ‹add_forward_prfstep_cond @{thm is_rect_listD} [with_term "?rects ! ?i"]›

setup ‹del_prfstep_thm_eqforward @{thm is_rect_list_def}›

definition is_rect_overlap :: "('a::linorder) rectangle ⇒ ('a::linorder) rectangle ⇒ bool" where [rewrite]:
  "is_rect_overlap A B ⟷ (is_overlap (xint A) (xint B) ∧ is_overlap (yint A) (yint B))"

definition has_rect_overlap :: "('a::linorder) rectangle list ⇒ bool" where [rewrite]:
  "has_rect_overlap As ⟷ (∃i<length As. ∃j<length As. i ≠ j ∧ is_rect_overlap (As ! i) (As ! j))"

subsection ‹INS / DEL operations›

datatype 'a operation =
  INS (pos: 'a) (op_idx: nat) (op_int: "'a interval")
| DEL (pos: 'a) (op_idx: nat) (op_int: "'a interval")
setup ‹fold add_rewrite_rule_back @{thms operation.collapse}›
setup ‹fold add_rewrite_rule @{thms operation.sel}›
setup ‹fold add_rewrite_rule @{thms operation.case}›
setup ‹add_resolve_prfstep @{thm operation.distinct(1)}›
setup ‹add_forward_prfstep_cond @{thm operation.disc(1)} [with_term "INS ?x11.0 ?x12.0 ?x13.0"]›
setup ‹add_forward_prfstep_cond @{thm operation.disc(2)} [with_term "DEL ?x21.0 ?x22.0 ?x23.0"]›

instantiation operation :: (linorder) linorder begin

definition less: "(a < b) = (if pos a ≠ pos b then pos a < pos b else
                             if is_INS a ≠ is_INS b then is_INS a ∧ ¬is_INS b
                             else if op_idx a ≠ op_idx b then op_idx a < op_idx b else op_int a < op_int b)"
definition less_eq: "(a ≤ b) = (if pos a ≠ pos b then pos a < pos b else
                              if is_INS a ≠ is_INS b then is_INS a ∧ ¬is_INS b
                              else if op_idx a ≠ op_idx b then op_idx a < op_idx b else op_int a ≤ op_int b)"

instance proof
  fix x y z :: "'a operation"
  show a: "(x < y) = (x ≤ y ∧ ¬ y ≤ x)"
    by (smt Rect_Intersect.less Rect_Intersect.less_eq leD le_cases3 not_less_iff_gr_or_eq)
  show b: "x ≤ x"
    by (simp add: local.less_eq)
  show c: "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
    by (smt Rect_Intersect.less Rect_Intersect.less_eq a dual_order.trans less_trans)
  show d: "x ≤ y ⟹ y ≤ x ⟹ x = y"
    by (metis Rect_Intersect.less Rect_Intersect.less_eq a le_imp_less_or_eq operation.expand)
  show e: "x ≤ y ∨ y ≤ x"
    using local.less_eq by fastforce
qed end

setup ‹fold add_rewrite_rule [@{thm less_eq}, @{thm less}]›

lemma operation_leD [forward]:
  "(a::('a::linorder operation)) ≤ b ⟹ pos a ≤ pos b" by auto2

lemma operation_lessI [backward]:
  "p1 ≤ p2 ⟹ INS p1 n1 i1 < DEL p2 n2 i2"
@proof
  @have "is_INS (INS p1 n1 i1) = True"
  @have "is_INS (DEL p2 n2 i2) = False"
@qed

setup ‹fold del_prfstep_thm [@{thm less_eq}, @{thm less}]›

subsection ‹Set of operations corresponding to a list of rectangles›

fun ins_op :: "'a rectangle list ⇒ nat ⇒ ('a::linorder) operation" where
  "ins_op rects i = INS (low (yint (rects ! i))) i (xint (rects ! i))"
setup ‹add_rewrite_rule @{thm ins_op.simps}›

fun del_op :: "'a rectangle list ⇒ nat ⇒ ('a::linorder) operation" where
  "del_op rects i = DEL (high (yint (rects ! i))) i (xint (rects ! i))"
setup ‹add_rewrite_rule @{thm del_op.simps}›

definition ins_ops :: "'a rectangle list ⇒ ('a::linorder) operation list" where [rewrite]:
  "ins_ops rects = list (λi. ins_op rects i) (length rects)"

definition del_ops :: "'a rectangle list ⇒ ('a::linorder) operation list" where [rewrite]:
  "del_ops rects = list (λi. del_op rects i) (length rects)"

lemma ins_ops_distinct [forward]: "distinct (ins_ops rects)"
@proof
  @let "xs = ins_ops rects"
  @have "∀i<length xs. ∀j<length xs. i ≠ j ⟶ xs ! i ≠ xs ! j"
@qed

lemma del_ops_distinct [forward]: "distinct (del_ops rects)"
@proof
  @let "xs = del_ops rects"
  @have "∀i<length xs. ∀j<length xs. i ≠ j ⟶ xs ! i ≠ xs ! j"
@qed

lemma set_ins_ops [rewrite]:
  "oper ∈ set (ins_ops rects) ⟷ op_idx oper < length rects ∧ oper = ins_op rects (op_idx oper)"
@proof
  @case "oper ∈ set (ins_ops rects)" @with
    @obtain i where "i < length rects" "ins_ops rects ! i = oper" @end
  @case "op_idx oper < length rects ∧ oper = ins_op rects (op_idx oper)" @with
    @have "oper = (ins_ops rects) ! (op_idx oper)" @end
@qed

lemma set_del_ops [rewrite]:
  "oper ∈ set (del_ops rects) ⟷ op_idx oper < length rects ∧ oper = del_op rects (op_idx oper)"
@proof
  @case "oper ∈ set (del_ops rects)" @with
    @obtain i where "i < length rects" "del_ops rects ! i = oper" @end
  @case "op_idx oper < length rects ∧ oper = del_op rects (op_idx oper)" @with
    @have "oper = (del_ops rects) ! (op_idx oper)" @end
@qed

definition all_ops :: "'a rectangle list ⇒ ('a::linorder) operation list" where [rewrite]:
  "all_ops rects = sort (ins_ops rects @ del_ops rects)"

lemma all_ops_distinct [forward]: "distinct (all_ops rects)"
@proof @have "distinct (ins_ops rects @ del_ops rects)" @qed

lemma set_all_ops_idx [forward]:
  "oper ∈ set (all_ops rects) ⟹ op_idx oper < length rects" by auto2

lemma set_all_ops_ins [forward]:
  "INS p n i ∈ set (all_ops rects) ⟹ INS p n i = ins_op rects n" by auto2

lemma set_all_ops_del [forward]:
  "DEL p n i ∈ set (all_ops rects) ⟹ DEL p n i = del_op rects n" by auto2

lemma ins_in_set_all_ops:
  "i < length rects ⟹ ins_op rects i ∈ set (all_ops rects)" by auto2
setup ‹add_forward_prfstep_cond @{thm ins_in_set_all_ops} [with_term "ins_op ?rects ?i"]›

lemma del_in_set_all_ops:
  "i < length rects ⟹ del_op rects i ∈ set (all_ops rects)" by auto2
setup ‹add_forward_prfstep_cond @{thm del_in_set_all_ops} [with_term "del_op ?rects ?i"]›

lemma all_ops_sorted [forward]: "sorted (all_ops rects)" by auto2

lemma all_ops_nonempty [backward]: "rects ≠ [] ⟹ all_ops rects ≠ []"
@proof @have "length (all_ops rects) > 0" @qed

setup ‹del_prfstep_thm @{thm all_ops_def}›

subsection ‹Applying a set of operations›

definition apply_ops_k :: "('a::linorder) rectangle list ⇒ nat ⇒ nat set" where [rewrite]:
  "apply_ops_k rects k = (let ops = all_ops rects in
     {i. i < length rects ∧ (∃j<k. ins_op rects i = ops ! j) ∧ ¬(∃j<k. del_op rects i = ops ! j)})"
setup ‹register_wellform_data ("apply_ops_k rects k", ["k < length (all_ops rects)"])›

lemma apply_ops_set_mem [rewrite]:
  "ops = all_ops rects ⟹
   i ∈ apply_ops_k rects k ⟷ (i < length rects ∧ (∃j<k. ins_op rects i = ops ! j) ∧ ¬(∃j<k. del_op rects i = ops ! j))"
  by auto2
setup ‹del_prfstep_thm @{thm apply_ops_k_def}›

definition xints_of :: "'a rectangle list ⇒ nat set ⇒ (('a::linorder) idx_interval) set" where [rewrite]:
  "xints_of rect is = (λi. IdxInterval (xint (rect ! i)) i) ` is"

lemma xints_of_mem [rewrite]:
  "IdxInterval it i ∈ xints_of rect is ⟷ (i ∈ is ∧ xint (rect ! i) = it)" using xints_of_def by auto

lemma xints_diff [rewrite]:
  "xints_of rects (A - B) = xints_of rects A - xints_of rects B"
@proof @have "inj (λi. IdxInterval (xint (rects ! i)) i)" @qed

definition has_overlap_at_k :: "('a::linorder) rectangle list ⇒ nat ⇒ bool" where [rewrite]:
  "has_overlap_at_k rects k ⟷ (
    let S = apply_ops_k rects k; ops = all_ops rects in
      is_INS (ops ! k) ∧ has_overlap (xints_of rects S) (op_int (ops ! k)))"
setup ‹register_wellform_data ("has_overlap_at_k rects k", ["k < length (all_ops rects)"])›

lemma has_overlap_at_k_equiv [forward]:
  "is_rect_list rects ⟹ ops = all_ops rects ⟹ k < length ops ⟹
   has_overlap_at_k rects k ⟹ has_rect_overlap rects"
@proof
  @let "S = apply_ops_k rects k"
  @have "has_overlap (xints_of rects S) (op_int (ops ! k))"
  @obtain "xs' ∈ xints_of rects S" where "is_overlap (int xs') (op_int (ops ! k))"
  @let "xs = int xs'" "i = idx xs'"
  @let "j = op_idx (ops ! k)"
  @have "ops ! k = ins_op rects j"
  @have "i ≠ j" @with @contradiction
    @obtain k' where "k' < k" "ops ! k' = ins_op rects i"
    @have "ops ! k = ops ! k'"
  @end
  @have "low (yint (rects ! i)) ≤ pos (ops ! k)" @with
    @obtain k' where "k' < k" "ops ! k' = ins_op rects i"
    @have "ops ! k' ≤ ops ! k"
  @end
  @have "high (yint (rects ! i)) ≥ pos (ops ! k)" @with
    @obtain k' where "k' < length ops" "ops ! k' = del_op rects i"
    @have "ops ! k' ≥ ops ! k"
  @end
  @have "is_rect_overlap (rects ! i) (rects ! j)"
@qed

lemma has_overlap_at_k_equiv2 [resolve]:
  "is_rect_list rects ⟹ ops = all_ops rects ⟹ has_rect_overlap rects ⟹
   ∃k<length ops. has_overlap_at_k rects k"
@proof
  @obtain i j where "i < length rects" "j < length rects" "i ≠ j"
                    "is_rect_overlap (rects ! i) (rects ! j)"
  @have "is_rect_overlap (rects ! j) (rects ! i)"
  @obtain i1 where "i1 < length ops" "ops ! i1 = ins_op rects i"
  @obtain j1 where "j1 < length ops" "ops ! j1 = ins_op rects j"
  @obtain i2 where "i2 < length ops" "ops ! i2 = del_op rects i"
  @obtain j2 where "j2 < length ops" "ops ! j2 = del_op rects j"
  @case "ins_op rects i < ins_op rects j" @with
    @have "i1 < j1"
    @have "j1 < i2" @with @have "ops ! j1 < ops ! i2" @end
    @have "is_overlap (int (IdxInterval (xint (rects ! i)) i)) (xint (rects ! j))"
    @have "has_overlap_at_k rects j1"
  @end
  @case "ins_op rects j < ins_op rects i" @with
    @have "j1 < i1"
    @have "i1 < j2" @with @have "ops ! i1 < ops ! j2" @end
    @have "is_overlap (int (IdxInterval (xint (rects ! j)) j)) (xint (rects ! i))"
    @have "has_overlap_at_k rects i1"
  @end
@qed

definition has_overlap_lst :: "('a::linorder) rectangle list ⇒ bool" where [rewrite]:
  "has_overlap_lst rects = (let ops = all_ops rects in (∃k<length ops. has_overlap_at_k rects k))"

lemma has_overlap_equiv [rewrite]:
  "is_rect_list rects ⟹ has_overlap_lst rects ⟷ has_rect_overlap rects" by auto2

subsection ‹Implementation of apply\_ops\_k›

lemma apply_ops_k_next1 [rewrite]:
  "is_rect_list rects ⟹ ops = all_ops rects ⟹ n < length ops ⟹ is_INS (ops ! n) ⟹
   apply_ops_k rects (n + 1) = apply_ops_k rects n ∪ {op_idx (ops ! n)}"
@proof
  @have "∀i. i∈apply_ops_k rects (n + 1) ⟷ i∈apply_ops_k rects n ∪ {op_idx (ops ! n)}" @with
    @case "i ∈ apply_ops_k rects n ∪ {op_idx (ops ! n)}" @with
      @case "i = op_idx (ops ! n)" @with
        @have "ins_op rects i < del_op rects i"
      @end
    @end
  @end
@qed

lemma apply_ops_k_next2 [rewrite]:
  "is_rect_list rects ⟹ ops = all_ops rects ⟹ n < length ops ⟹ ¬is_INS (ops ! n) ⟹
   apply_ops_k rects (n + 1) = apply_ops_k rects n - {op_idx (ops ! n)}" by auto2

definition apply_ops_k_next :: "('a::linorder) rectangle list ⇒ 'a idx_interval set ⇒ nat ⇒ 'a idx_interval set" where
  "apply_ops_k_next rects S k = (let ops = all_ops rects in
   (case ops ! k of
      INS p n i ⇒ S ∪ {IdxInterval i n}
    | DEL p n i ⇒ S - {IdxInterval i n}))"
setup ‹add_rewrite_rule @{thm apply_ops_k_next_def}›

lemma apply_ops_k_next_is_correct [rewrite]:
  "is_rect_list rects ⟹ ops = all_ops rects ⟹ n < length ops ⟹
   S = xints_of rects (apply_ops_k rects n) ⟹
   xints_of rects (apply_ops_k rects (n + 1)) = apply_ops_k_next rects S n"
@proof @case "is_INS (ops ! n)" @qed

function rect_inter :: "nat rectangle list ⇒ nat idx_interval set ⇒ nat ⇒ bool" where
  "rect_inter rects S k = (let ops = all_ops rects in
    if k ≥ length ops then False
    else if is_INS (ops ! k) then
      if has_overlap S (op_int (ops ! k)) then True
      else if k = length ops - 1 then False
      else rect_inter rects (apply_ops_k_next rects S k) (k + 1)
    else if k = length ops - 1 then False
      else rect_inter rects (apply_ops_k_next rects S k) (k + 1))"
  by auto
  termination by (relation "measure (λ(rects,S,k). length (all_ops rects) - k)") auto

lemma rect_inter_correct_ind [rewrite]:
  "is_rect_list rects ⟹ ops = all_ops rects ⟹ n < length ops ⟹
   rect_inter rects (xints_of rects (apply_ops_k rects n)) n ⟷
   (∃k<length ops. k ≥ n ∧ has_overlap_at_k rects k)"
@proof
  @let "ints = xints_of rects (apply_ops_k rects n)"
  @fun_induct "rect_inter rects ints n"
  @unfold "rect_inter rects ints n"
  @case "n ≥ length ops"
  @case "is_INS (ops ! n) ∧ has_overlap ints (op_int (ops ! n))"
  @case "n = length ops - 1"
@qed

text ‹Correctness of functional algorithm.›
theorem rect_inter_correct [rewrite]:
  "is_rect_list rects ⟹ rect_inter rects {} 0 ⟷ has_rect_overlap rects"
@proof
  @have "{} = xints_of rects (apply_ops_k rects 0)"
  @have "rect_inter rects {} 0 = has_overlap_lst rects" @with
    @unfold "rect_inter rects {} 0"
  @end
@qed

end