header {*

  Please send your solutions by email at noon 
  on 29th April at latest. 

*}

theory Hw03test
  imports Main
begin


section {* Task 1 (easy) *}

text {* 

  The term 

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

  stands for the sum of all i where i ranges 
  from i=0 to n. In other words

    0 + 1 + 2 + 3 + \<dots> + n

  Prove the lemma below! 

  Hint: The proof is by induction. Remember that 
  numbers often need to have 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"
sorry

section {* Task 2a (easy) *}

text {* 
  
  Define the function that calculates the following 
  sum

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

  Call this function sum_odds. Make sure sum_odds calculates 
  the 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 *)


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

  Hint 2: There is an oddity about natural 
  numbers, namely: 0 - 1 = 0.

*}

section {* Task 2b (easy) *}

text {* 
  
  Using the definition from 2a, prove the lemma below!

*}

lemma sum_odds:
  shows "sum_odds n = n * n"
sorry

section {* Task 3a (easy) *}

text {* 

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

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

  Hint 2: Define them completely independently.

*}

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 auxiliary lemmas about even and 
  addition might be needed (same for odd). 

*}

lemma even_lem:
  assumes a: "even n"
  shows "even (n*n)"
sorry

lemma odd_lem:
  assumes a: "odd n"
  shows "odd (n*n)"
sorry

section {* Task 3c (easy) *}

text {*
  
  Prove the two lemmas below!

  Hint: By induction on (even n) and , respectively,
  on (odd n).
*}

lemma odd_suc:
  assumes a: "even n"
  shows "odd (Suc n)"
sorry

lemma even_suc:
  assumes a: "odd n"
  shows "even (Suc n)"
sorry

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. A problem might arise 
  from the fact that 0 - 2 = 0 and 1 - 2 = 0.
  
  *}

lemma even_minus_two:
  assumes a: "even n"
  shows "even (n - 2)"
sorry

text {* 
  
  Think first how you can state this lemma for 
  odd so that it is provable.  
  
  lemma odd_minus_two: 
  ???
*}

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 attempt to 
  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
  again 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 {*
  
  The purpose of the previous two lemmas are to 
  prove the following lemma. 

  Can you find a proof on paper for it? Again please
  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