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

theory Exercise06
  imports 
    Complex_Main (* imports real numbers and exponentiation with real exponent: powr *)
begin

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

text \<open>The aim is to prove @{term "sqrt 2 \<notin> \<rat>"}.\<close>

text \<open>To this end, first develop a variant of the proof that was given in Demo06 in the lecture.
  Here, the difference is that we consider the real numbers and identify the rational numbers 
  as a specific set of real numbers: @{term \<rat>}.\<close>

lemma sqrt_2_irrational_main: "\<not> (\<exists> (q :: real) \<in> \<rat>. q^2 = 2)" sorry

text \<open>Afterwards show the desired lemma\<close>

lemma sqrt_2_irrational[intro]: "sqrt 2 \<notin> \<rat>" sorry


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

text \<open>Show that there exists two irrational numbers $x$ and $y$ such that $x^y$ is rational.
  To this end, there is a nice non-constructive proof:

  Choose $y = \sqrt{2}$, and 
  choose $x = \sqrt{2}$ or $\sqrt{2}^{\sqrt{2}}$, depending on whether the latter number is rational or not.
\<close>

lemma power_of_two_irrationals_is_rational: "\<exists> x y :: real. x \<notin> \<rat> \<and> y \<notin> \<rat> \<and> x powr y \<in> \<rat>" sorry

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

text \<open>Consider a variant of mergesort where the number of comparisons are counted.\<close>

text \<open>The aim is to prove that mergesort has a complexity of O(n log(n)). To this
  end, you will prove that on inputs of length $2^n$ there will be at most $2^n * n$ many
  comparisons.\<close>

fun split_list :: "'a list \<Rightarrow> 'a list \<times> 'a list" where
  "split_list (x # y # xs) = (case split_list xs of (one,two) \<Rightarrow> (x # one, y # two))" 
| "split_list xs = (xs,[])" 

fun merge :: "'a :: linorder list \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> nat" where
  "merge [] ys = (ys,0)" 
| "merge xs [] = (xs,0)" 
| "merge (x # xs) (y # ys) = (if x \<le> y then case merge xs (y # ys) of (zs,n) \<Rightarrow> (x # zs, Suc n)
    else case merge (x # xs) ys of (zs,n) \<Rightarrow> (y # zs, Suc n))" 

function (sequential) msort :: "'a :: linorder list \<Rightarrow> 'a list \<times> nat" where
  "msort [] = ([], 0)" 
| "msort [x] = ([x], 0)"
| "msort xs = (case split_list xs of (one,two) \<Rightarrow>
      case msort one of (ys1,c1) \<Rightarrow>
      case msort two of (ys2,c2) \<Rightarrow>
      case merge ys1 ys2 of (ys,c3) \<Rightarrow>
      (ys, c1 + c2 + c3))" 
  by pat_completeness auto

lemma split_len: "split_list xs = (one,two) \<Longrightarrow> length xs = length one + length two" 
  by (induction xs arbitrary: one two rule: split_list.induct) (auto split: prod.splits)

termination by (relation "measure length") (auto dest: split_len split: prod.splits)


text \<open>You will have to figure out useful properties of @{const split_list} and @{const merge} that help to prove
  the complexity of mergesort. Most of these are one-liners by using the right modifiers. 

  Hints: 
  - division on natural numbers is @{term "x div y"} and there also exists a predicate @{const even}.
  - besides @{thm list.splits}, @{thm nat.splits}, @{thm prod.splits}, etc., 
    there also is a split-rule for if-then-else: @{thm if_split}\<close>
  


text \<open>For proving the complexity of mergesort (in combination with the other required property,
  I would be surprised to see a one-line solution, so you have to perform several manual steps.\<close>

lemma msort: "msort xs = (ys, m) \<Longrightarrow> length xs = 2^n \<Longrightarrow> m \<le> n * 2^n \<and> length ys = length xs" 
proof (induction xs arbitrary: ys n m rule: msort.induct)
  case (3 x1 x2 xs ys n m)
  let ?xs = "x1 # x2 # xs" 
  obtain one two where xs: "split_list ?xs = (one, two)" by force (* force splits pairs for you *)
  obtain ys1 c1 where one: "msort one = (ys1, c1)" by force
  show ?case sorry
qed auto

end