theory Hw03_sol
  imports Main
begin


section {* Task 1 (easy) *}

text {* 

  The term 

   (\<Sum> i=0..n. i)

  stands for the sum of i where i ranges 
  from i=0 to n.

  Prove the following lemma! 

  Hint: The proof is by induction. Remember that 
  numbers often need an explicit type annotation 
  (for example 1::nat).

*}

lemma sum_n:
  fixes n::"nat"
  shows "(\<Sum> i=0..n. i) = n * (n + 1) div 2"
proof(induct n)
  case 0
  show "(\<Sum> i=0..0. i) = 0 * (0 + 1) div (2::nat)" by simp
next
  case (Suc n)
  have ih: "(\<Sum>i=0..n. i) = n * (n + 1) div (2::nat)" by fact
  show "(\<Sum>i=0..(Suc n). i) = (Suc n) * ((Suc n) + 1) div (2::nat)" 
    using ih by simp
qed

section {* Task 2a (easy) *}

text {* 
  
  Define the function that calculates the sum

  1 + 3 + \<dots> + (2n - 1)

  Call this function sum_odds.

  Hint: You have to give an equation for 0
  and (Suc n).

  Make sure your function calculates teh correct
  result by testing: 

  normal_form "sum_odds 0"   (* = 0 *)
  normal_form "sum_odds 1"   (* = Suc 0 *)
  normal_form "sum_odds 2"   (* = Suc (Suc (Suc (Suc 0))) *)
  normal_form "sum_odds 3"   (* should be 9 *)

*}

fun
  sum_odds :: "nat \<Rightarrow> nat"
where
  "sum_odds 0 = 0"
| "sum_odds (Suc n) = (2*(Suc n) - 1) + sum_odds n"

normal_form "sum_odds 0"
normal_form "sum_odds 1"
normal_form "sum_odds 2"
normal_form "sum_odds 3"

section {* Task 2b (easy) *}

text {* 
  
  Prove the lemma

*}

lemma sum_odds:
  shows "sum_odds n = n * n"
by (induct n) (simp_all)

lemma sum_odds_longer:
  shows "sum_odds n = n * n"
proof (induct n)
  case 0
  show "sum_odds 0 = 0 * 0" by simp
next
  case (Suc n)
  have ih: "sum_odds n = n * n" by fact
  show "sum_odds (Suc n) = Suc n * Suc n" using ih by simp
qed


section {* Task 3a (easy) *}

text {* 

  Define inductively the predicates for a number
  being even and a number being odd. 

  Hint 1: Both predicates have type "nat \<Rightarrow> bool". 

  Hint 2: Define them separately.

*}

inductive
  even :: "nat \<Rightarrow> bool"
where
  e0: "even 0"
| eN: "even n \<Longrightarrow> even (Suc (Suc n))"

inductive
  odd :: "nat \<Rightarrow> bool"
where
  "odd (Suc 0)"
| "odd n \<Longrightarrow> odd (Suc (Suc n))"

section {* Task 3b (hard) *}

text {*
  
  Prove that assuming even n holds, then also 
  even (n*n) holds. Prove the same for odd.
  
  Hint 1: Prove these statements by induction over
  the predicates even n and odd n, respectively.
  
  Hint 2: Two lemmas about even and addition might 
  be helpful (same for odd). *}

lemma even_plus:
  shows "even (n+n)"
by (induct n) (auto intro: even.intros)

lemma even_plus_ext:
  assumes a: "even m" 
  shows "even (n+(n+m))"
using a
by (induct) (auto intro: even.intros even_plus)

lemma even_lem:
  assumes a: "even n"
  shows "even (n*n)"
using a
by (induct) (auto intro: even.intros even_plus_ext)

lemma odd_plus:
  shows "odd (Suc (n+n))"
by (induct n) (auto intro: odd.intros)

lemma odd_plus_ext:
  assumes a: "odd m" 
  shows "odd (n+(n+m))"
using a
by (induct) (auto intro: odd.intros odd_plus)

lemma odd_lem:
  assumes a: "odd n"
  shows "odd (n*n)"
using a
by (induct) (auto intro: odd.intros odd_plus_ext)

section {* Task 3c (easy) *}

text {*
  
  Prove the two lemmas below!

  *}

lemma odd_suc:
  assumes a: "even n"
  shows "odd (Suc n)"
using a
by (induct) (auto intro: odd.intros)

lemma even_suc:
  assumes a: "odd n"
  shows "even (Suc n)"
using a
by (induct) (auto intro: even.intros)

section {* Task 3d (hard) *}

text {*
  
  Prove that assuming even n holds, then  
  even (n - 2) holds. Prove the same for odd.
  
  Hint 1: Be careful about how you state the
  lemma in the odd case. The problem arises 
  from the fact that 0 - 2 = 0 and 1 - 2 = 0.
  
  *}

lemma even_minus_two:
  assumes a: "even n"
  shows "even (n - 2)"
using a
by (induct n) (auto intro: even.intros)

lemma odd_minus_two:
  assumes a: "odd n" "n > 1"
  shows "odd (n - 2)"
using a
by (induct n) (auto intro: odd.intros)

text {*

  Warning! The remaining tasks only make sense
  if you had the right definitions for even and
  odd. If they do not make sense to you, then
  check with me via email (though I am not able
  to answer this weekend).

  email: urbanc@in.tum.de

*}

section {* Task 4a (interesting) *}

text {*
  
  Have a look at the next proof and reconstruct
  a proof on paper. Make all steps explicit.
  
  *}

lemma odd_or_even:
  shows "even n \<or> odd n"
proof (induct n)
  case 0
  have aux: "even 0" by (auto intro: even.intros)
  show "even 0 \<or> odd 0" using aux by simp
next
  case (Suc n)
  have ih: "even n \<or> odd n" by fact
  moreover
  { assume a1: "even n"
    have a2: "odd (Suc n)" using a1 by (simp add: odd_suc)
    have "even (Suc n) \<or> odd (Suc n)" using a2 by simp
  } 
  moreover
  { assume b1: "odd n"
    have b2: "even (Suc n)" using b1 by (simp add: even_suc)
    have "even (Suc n) \<or> odd (Suc n)" using b2 by simp
  }
  ultimately show "even (Suc n) \<or> odd (Suc n)" by blast
qed
  
section {* Task 4b (interesting) *}

text {*
  
  Have a look at the next proof and reconstruct
  a proof on paper. Make all steps explicit.
  
  *}

lemma odd_and_even:
  assumes a: "even n \<and> odd n"
  shows "False"
using a
proof (induct n)
  case 0
  have "even 0 \<and> odd 0" by fact
  then have "odd 0" by simp
  then show "False" by (cases rule: odd.cases) (auto)
next
  case (Suc n)
  have ih: "even n \<and> odd n \<Longrightarrow> False" by fact
  have as: "even (Suc n) \<and> odd (Suc n)" by fact
  from as have "odd (Suc n)" by simp
  then have "even (Suc (Suc n))" by (simp add: even_suc)
  then have "even ((Suc (Suc n)) - 2)" by (simp only: even_minus_two)
  then have A: "even n" by simp
  from as have "even (Suc n)" by simp
  then have "odd (Suc (Suc n))" by (simp add: odd_suc)
  moreover have "(Suc (Suc n)) > 1" by simp
  ultimately have "odd ((Suc (Suc n)) - 2)" by (simp only: odd_minus_two)
  then have B: "odd n" by simp
  show "False" using ih A B by simp
qed

section {* Task 5 (?) *}

text {*
  
  Can you find a proof on paper for the
  next lemma. Again make reasonable effort
  to show all details. 
  
  *}

lemma odd_even:
  shows "(even n \<and> \<not>odd n) \<or> (\<not>even n \<and> odd n)"
by (metis odd_and_even odd_or_even)

end