Theory Rect_Intersect_Impl

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

section ‹Implementation of rectangle intersection›

theory Rect_Intersect_Impl
  imports "../Functional/Rect_Intersect" IntervalTree_Impl Quicksort_Impl
begin

text ‹Imperative version of rectangle-intersection algorithm.›

subsection ‹Operations›

fun operation_encode :: "('a::heap) operation ⇒ nat" where
  "operation_encode oper =
   (case oper of INS p i n ⇒ to_nat (is_INS oper, p, i, n)
               | DEL p i n ⇒ to_nat (is_INS oper, p, i, n))"

instance operation :: (heap) heap
  apply (rule heap_class.intro)
  apply (rule countable_classI [of "operation_encode"])
  apply (case_tac x, simp_all, case_tac y, simp_all)
  apply (simp add: operation.case_eq_if)
  ..

subsection ‹Initial state›

definition rect_inter_init :: "nat rectangle list ⇒ nat operation array Heap" where
  "rect_inter_init rects = do {
     p ← Array.of_list (ins_ops rects @ del_ops rects);
     quicksort_all p;
     return p }"

setup ‹add_rewrite_rule @{thm all_ops_def}›
lemma rect_inter_init_rule [hoare_triple]:
  "<emp> rect_inter_init rects <λp. p ↦⇩a all_ops rects>" by auto2
setup ‹del_prfstep_thm @{thm all_ops_def}›

definition rect_inter_next :: "nat operation array ⇒ int_tree ⇒ nat ⇒ int_tree Heap" where
  "rect_inter_next a b k = do {
    oper ← Array.nth a k;
    if is_INS oper then
      IntervalTree_Impl.insert_impl (IdxInterval (op_int oper) (op_idx oper)) b
    else
      IntervalTree_Impl.delete_impl (IdxInterval (op_int oper) (op_idx oper)) b }"

lemma op_int_is_interval:
  "is_rect_list rects ⟹ ops = all_ops rects ⟹ k < length ops ⟹
   is_interval (op_int (ops ! k))"
@proof @have "ops ! k ∈ set ops" @case "is_INS (ops ! k)" @qed
setup ‹add_forward_prfstep_cond @{thm op_int_is_interval} [with_term "op_int (?ops ! ?k)"]›

lemma rect_inter_next_rule [hoare_triple]:
  "is_rect_list rects ⟹ k < length (all_ops rects) ⟹
   <a ↦⇩a all_ops rects * int_tree_set S b>
   rect_inter_next a b k
   <λr. a ↦⇩a all_ops rects * int_tree_set (apply_ops_k_next rects S k) r>⇩t" by auto2

partial_function (heap) rect_inter_impl ::
  "nat operation array ⇒ int_tree ⇒ nat ⇒ bool Heap" where
  "rect_inter_impl a b k = do {
    n ← Array.len a;
    (if k ≥ n then return False
     else do {
       oper ← Array.nth a k;
       (if is_INS oper then do {
          overlap ← IntervalTree_Impl.search_impl (op_int oper) b;
          if overlap then return True
          else if k = n - 1 then return False
          else do {
            b' ← rect_inter_next a b k;
            rect_inter_impl a b' (k + 1)}}
        else
          if k = n - 1 then return False
          else do {
            b' ← rect_inter_next a b k;
            rect_inter_impl a b' (k + 1)})})}"

lemma rect_inter_to_fun_ind [hoare_triple]:
  "is_rect_list rects ⟹ k < length (all_ops rects) ⟹
   <a ↦⇩a all_ops rects * int_tree_set S b>
   rect_inter_impl a b k
   <λr. a ↦⇩a all_ops rects * ↑(r ⟷ rect_inter rects S k)>⇩t"
@proof
  @let "d = length (all_ops rects) - k"
  @strong_induct d arbitrary k S b
  @case "k ≥ length (all_ops rects)"
  @unfold "rect_inter rects S k"
  @case "is_INS (all_ops rects ! k)" @with
    @case "has_overlap S (op_int (all_ops rects ! k))"
    @case "k = length (all_ops rects) - 1"
    @apply_induct_hyp "length (all_ops rects) - (k + 1)" "k + 1"
    @have "length (all_ops rects) - (k + 1) < d"
  @end
  @case "k = length (all_ops rects) - 1"
  @apply_induct_hyp "length (all_ops rects) - (k + 1)" "k + 1"
  @have "length (all_ops rects) - (k + 1) < d"
@qed

definition rect_inter_all :: "nat rectangle list ⇒ bool Heap" where
  "rect_inter_all rects =
    (if rects = [] then return False
     else do {
       a ← rect_inter_init rects;
       b ← int_tree_empty;
       rect_inter_impl a b 0 })"

text ‹Correctness of rectangle intersection algorithm.›
theorem rect_inter_all_correct:
  "is_rect_list rects ⟹
   <emp>
   rect_inter_all rects
   <λr. ↑(r = has_rect_overlap rects)>⇩t" by auto2

end