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

theory Exercise08
  imports 
    Main
begin

section \<open>Exercise 1 -- 6 points\<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)" 

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: all of the proofs are one-liners\<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, 4 points\<close>

text \<open>Complete the following formalization that has been developed in the lecture.
  Adjust proofs and specifications as required.\<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 x Leaf = Leaf" 
| "delete x (Node l y r) = (if x < y then Node (delete x l) y r
      else if x > y then Node l y (delete x r)
      else if l = Leaf then r else case delete_right l of (l',z) \<Rightarrow> Node l' z r)" 

lemma delete_right: assumes "ordered t" "t \<noteq> Leaf" "delete_right t = (t',x)" 
  shows "set_t t' = set_t t - {x} \<and> ordered t' \<and> Ball (set_t t') (\<lambda> x. Ball f (A x))" 
  oops


lemma delete: assumes "ordered t"
  shows "ordered (delete y t) \<and> set_t (delete y t) = set_t t - {y}"  
  using assms 
proof (induction)
  case (oNode l r x)
  consider (L) "y < x" | (R) "y > x" | (Le) "x = y" "l = Leaf" | (DR) "x = y" "l \<noteq> Leaf" 
    by fastforce
  then show ?case 
  proof cases
    case L
    then show ?thesis using oNode.IH(1) oNode.hyps 
      by (auto intro!: ordered.intros) 
  next
    case R
    then show ?thesis using oNode.IH(2) oNode.hyps by (auto intro!: ordered.intros)
  next
    case Le
    then show ?thesis using oNode.hyps by (auto intro!: ordered.intros)
  next
    case DR
    obtain l' z where dr: "delete_right l = (l',z)" by force
    from dr DR show ?thesis apply simp sorry
  qed
qed (auto intro: ordered.intros)




section \<open>Exercise 2 - 4 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 -- 2 points: 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