Theory Challenge2B

section ‹Challenge 2.B›
theory Challenge2B
  imports Challenge2A
begin

text ‹We did not get very far on this part of the competition. Only Task 2 was finished.›

subsection ‹Basic Definitions›

datatype tree = Leaf | Node int (lc: tree) (rc: tree)

text ‹Analogous to @{term left_spec} from 2.A.›
definition
  "right_spec xs j =
  (if (∃i>j. xs ! i < xs ! j) then Some (LEAST i. i > j ∧ xs ! i < xs ! j) else None)"

context
  fixes xs :: "int list"
  assumes "distinct xs"
begin

subsection ‹Specification of the Parent›
definition
  "parent i = (
    case (left_spec xs i, right_spec xs i) of
      (None, None) ⇒ None
    | (Some x, None) ⇒ Some x
    | (None, Some y) ⇒ Some y
    | (Some x, Some y) ⇒ Some (max x y)
  )"

subsection ‹The Heap Property (Task 2)›

lemma parent_heap:
  assumes "parent j = Some p"
  shows "xs ! j > xs ! p"
proof -
  note [simp del] = left_spec_None_iff swap_adhoc
  show ?thesis
  proof (cases "(∃i<j. xs ! i < xs ! j)")
    case True
    then have *: "xs ! the (left_spec xs j) < xs ! j" "left_spec xs j ≠ None"
      unfolding left_spec_def by auto (metis (no_types, lifting) GreatestI_nat True less_le)
    show ?thesis
    proof (cases "(∃i>j. xs ! i < xs ! j)")
      case True
      then have "xs ! the (right_spec xs j) < xs ! j" "right_spec xs j ≠ None"
        unfolding right_spec_def by auto (metis (no_types, lifting) LeastI)
      then show ?thesis
        using * assms unfolding parent_def by auto
    next
      case False
      then have "right_spec xs j = None"
        unfolding right_spec_def by auto
      then show ?thesis
        using * assms unfolding parent_def by auto
    qed
  next
    case False
    then have [simp]: "left_spec xs j = None"
      unfolding left_spec_def by auto
    show ?thesis
    proof (cases "(∃i>j. xs ! i < xs ! j)")
      case True
      then have "xs ! the (right_spec xs j) < xs ! j" "right_spec xs j ≠ None"
        unfolding right_spec_def by auto (metis (no_types, lifting) LeastI)
      then show ?thesis
        using assms unfolding parent_def by auto
    next
      case False
      then have "right_spec xs j = None"
        unfolding right_spec_def by auto
      then show ?thesis
        using assms unfolding parent_def by auto
    qed
  qed
qed

end

end