chapter \<open>Exercise Sheet -- Week 8\<close>

theory Exercise08
  imports 
    Main
begin

section \<open>Exercise 1\<close>

text \<open>Reconsider the binary search tree from the lecture\<close>

datatype 'a tree = Leaf | Node "'a tree" 'a "'a tree" 

fun set_t :: "'a tree \<Rightarrow> 'a set" where
  "set_t Leaf = {}" 
| "set_t (Node l x r) = set_t l \<union> {x} \<union> set_t r" 

inductive ordered :: "'a :: linorder tree \<Rightarrow> bool" where
  oLeaf: "ordered Leaf" 
| oNode: "ordered l \<Longrightarrow> ordered r 
  \<Longrightarrow> Ball (set_t l) (\<lambda> y. y < x)
  \<Longrightarrow> Ball (set_t r) (\<lambda> y. y > x)
  \<Longrightarrow> ordered (Node l x r)" 

fun member:: "'a :: linorder \<Rightarrow> 'a tree \<Rightarrow> bool" where
  "member x Leaf = False" 
| "member y (Node l x r) = (if x = y then True else if y < x then member y l else member y r)" 

lemma member_correct: "ordered t \<Longrightarrow> member x t = (x \<in> set_t t)" 
  by (induction rule: ordered.induct, auto)

fun insert_t :: "'a :: linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
  "insert_t y Leaf = Node Leaf y Leaf" 
| "insert_t y (Node l x r) = (if x = y then Node l x r else
      if y < x then Node (insert_t y l) x r else Node l x (insert_t y r))" 

lemma set_insert_t[simp]: "set_t (insert_t x t) = insert x (set_t t)" 
  by (induct x t rule: insert_t.induct, auto)

lemma insert_t: assumes "ordered t" 
  shows "ordered (insert_t y t)" 
  using assms
  by (induction rule: ordered.induct, auto intro!: ordered.intros)

text \<open>Task 1 -- Flatten, 2 points\<close>

text \<open>Define a function to flatten a tree into a list and prove some properties on this conversion.

  Hint: each property can be proven within a single line by parametrizing automatic methods
        appropriately.\<close>

fun flatten :: "'a tree \<Rightarrow> 'a list" where
  "flatten t = undefined" 

lemma flatten_set: "set (flatten t) = set_t t"  
  oops

lemma flatten_distinct: "ordered t \<Longrightarrow> distinct (flatten t)" 
  oops

lemma flatten_sorted: "ordered t \<Longrightarrow> sorted (flatten t)" 
  oops

text \<open>Task 2 -- Delete, 5 points\<close>

text \<open>Complete the following formalization that has been developed in the lecture.
  Specify properties for \<open>delete_right\<close>, prove these, and use them
  to complete the missing case in the proof for \<open>delete\<close>.\<close>

fun delete_right :: "'a :: linorder tree \<Rightarrow> 'a tree \<times> 'a" where
  "delete_right (Node l x Leaf) = (l, x)"  
| "delete_right (Node l x r) = (case delete_right r of 
      (r', y) \<Rightarrow> (Node l x r', y))" 

fun delete :: "'a :: linorder \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
  "delete y Leaf = Leaf"
| "delete y (Node l x r) = (if y < x then Node (delete y l) x r
      else if y > x then Node l x (delete y r)
      else if l = Leaf then r
      else case delete_right l of (l', z) \<Rightarrow> Node l' z r)" 
  


lemma delete: "ordered t \<Longrightarrow> ordered (delete y t) 
  \<and> set_t (delete y t) = set_t t - {y}" 
proof (induction rule: ordered.induct)
  case oLeaf
  then show ?case by (auto intro: ordered.intros)
next
  case (oNode l r x)
  consider (left) "y < x" | (right) "y > x" | (eqSimple) "y = x" "l = Leaf" 
         | (eqComplex) "y = x" "l \<noteq> Leaf" 
    by (cases "y < x"; cases "y = x"; cases "y > x"; auto)
  thus ?case
  proof cases
    case left
    then show ?thesis using oNode by (auto intro: ordered.oNode)
  next
    case right
    hence res: "delete y (Node l x r) = Node l x (delete y r)" by auto
    from oNode 
    have IH: "ordered (delete y r)" "set_t (delete y r) = set_t r - {y}" by auto
    have set: "set_t (Node l x (delete y r)) = set_t (Node l x r) - {y}" 
      using IH right oNode by auto
    show ?thesis unfolding res set
      by (intro conjI refl ordered.oNode, insert IH right oNode, auto)
  next
    case eqSimple
    then show ?thesis using oNode by (auto intro: ordered.oNode)
  next
    case eqComplex
    then show ?thesis sorry
  qed
qed




section \<open>Exercise 2 - 3 points\<close>

text \<open>Prove the summation formula of Gauss without induction, i.e., just be manipulating
  sets. Follow the draft.\<close>

lemma Gauss: "2 * sum (\<lambda> i. i) {..< (n :: nat)} = (n - 1) * n"
proof -
  have "2 * sum (\<lambda> i. i) {..< n} = sum (\<lambda> i. i) {..< n} + sum (\<lambda> i. i) {..< n}" by simp
  (* now  Gauss' trick is applied to let one of the sums count downwards *)
  also have "\<dots> = sum (\<lambda> i. i) {..< n} + sum (\<lambda> i. n - 1 - i) {..< n}" 
    apply (rule arg_cong[of _ _ "\<lambda> s. _ + s"])
    apply (rule sum.reindex_cong)
  proof -

    text \<open>Task 1 -- 1 point: Choose undefined appropriately and remove the first two sorries\<close>

    show "inj_on undefined {..<n}" sorry 
    {
      fix x
      assume "x \<in> {..<n}" 
      thus "undefined x = n - 1 - x" sorry 
    }

    text \<open>Task 2 -- 1 point: remove the next sorry.
      
      Hint: one of the subset-directions is trivial; 
          do the other direction slowly and perhaps @{thm image_eqI} is useful.\<close>

    show "{..<n} = undefined ` {..<n}" sorry 
  qed

  text \<open>Task 3 -- 1 point: remove the remaining two sorries where you
    should use @{command find_theorems}, but not @{command sledgehammer} or @{command try}.\<close>

  also have "\<dots> = sum (\<lambda> i. i + (n - 1 - i)) {..< n}" sorry 
  also have "\<dots> = sum (\<lambda> i. n - 1) {..< n}" sorry
  also have "\<dots> = (n - 1) * n" by simp
  finally show ?thesis .
qed

end