theory Cas8
  imports Complex_Main 
begin

section \<open>Zbir kvadrata\<close>

(* Definišemo funkciju koja izračunava zbir kvadrata brojeva od 1 do n *)
primrec zbir_kvadrata :: "nat \<Rightarrow> nat" where               
  "zbir_kvadrata 0 = 0"
| "zbir_kvadrata (Suc n) = zbir_kvadrata n + (Suc n)*(Suc n)"

value "zbir_kvadrata 4"

(* Zbir kvadrata smo mogli izraziti i bibliotečkim funkcijama za rad sa listama *) 
value "sum_list (map (\<lambda> x. x ^ 2) [0..<5])"
value "\<Sum> x \<leftarrow> [0..<5]. x ^ 2"

lemma "zbir_kvadrata n = (\<Sum> x \<leftarrow> [0..<n+1]. x ^ 2)"
  by (induction n, simp, simp add: power2_eq_square)

lemma kvadrati_do_n:
  "(\<Sum> x \<leftarrow> [0..<n+1]. x ^ 2) = n * (n+1) * (2*n + 1) div 6"
proof (induction n)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  have "(\<Sum> x \<leftarrow> [0..<Suc n+1]. x ^ 2) = (\<Sum> x \<leftarrow> [0..<n+1]. x ^ 2) + (Suc n) ^ 2"
    by simp
  also have "... = n * (n + 1) * (2 * n + 1) div 6 + (n + 1) * (n + 1)"
    using Suc
    by (simp add: power2_eq_square)
  also have "... = (n * (n + 1) * (2 * n + 1) + 6 * (n + 1) * (n + 1)) div 6"
    by (simp add: algebra_simps)
  also have "... = ((n + 1) * (n + 2) * (2 * (n + 1) + 1)) div 6"
    by (simp add: algebra_simps)
  finally
  show ?case
    by simp
qed

section \<open>Mnozenje matrica\<close>

type_synonym mat2 = "nat \<times> nat \<times> nat \<times> nat"

(* Mnozenje matrica dimenzije 2x2 *)
fun mat_mul :: "mat2 \<Rightarrow> mat2 \<Rightarrow> mat2" where
  "mat_mul (a1, b1, c1, d1) (a2, b2, c2, d2) = (a1*a2 + b1*c2, a1*b2 + b1*d2, c1*a2 + d1*c2, c1*b2 + d1*d2)"

(* Jedinicna matrica *)
definition eye :: mat2 where
  "eye = (1, 0, 0, 1)"

(* Stepenovanje *)
primrec mat_pow :: "mat2 \<Rightarrow> nat \<Rightarrow> mat2" where
  "mat_pow A 0 = eye"
| "mat_pow A (Suc n) = mat_mul A (mat_pow A n)"

lemma "mat_pow (1, 1, 0, 1) n = (1, n, 0, 1)"
(*  by (induction n, auto simp add: eye_def) *)
proof (induct n)
  case 0
  show ?case
    by (simp add: eye_def)
next
  case (Suc n)
  show ?case
  proof-
    have "mat_pow (1, 1, 0, 1) (Suc n) = mat_mul (1, 1, 0, 1) (mat_pow (1, 1, 0, 1) n)"
      by simp
    also have "... = mat_mul (1, 1, 0, 1) (1, n, 0, 1)"
      using Suc
      by simp
    finally show ?thesis
      by simp
  qed
qed 

section \<open>Odnos eksponencijalne i kvadratne funkcije\<close>

lemma twonplus1_lt_twopown:
  assumes "n > 2"
  shows "2 * n + 1 < 2 ^ n"
  using assms
proof (induction n)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  show ?case
  proof (cases "n = 2")
    case True
    then show ?thesis
      by simp
  next
    case False
    hence *: "2 * n + 1 < 2 ^ n" "n > 2"
      using Suc
      by auto
    have "2 * Suc n + 1 < 2 * (Suc n) + 2 * n"
      using `n > 2`
      by simp
    also have "... = 2 * (2 * n + 1)"
      by simp
    also have "... < 2 * 2 ^ n"
      using *
      by simp
    finally show ?thesis
      by simp
  qed
qed

lemma 
  assumes "n \<ge> 5"
  shows "2^n > n^2"
  using assms
proof (induction n)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  show ?case
  proof (cases "n = 4")
    case True
    then show ?thesis
      by simp
  next
    case False   
    hence *: "n ^ 2 < 2 ^ n" "n \<ge> 5"
      using Suc
      by auto
    have "(Suc n) ^ 2 = n ^ 2 + 2 * n + 1"
      by (simp add: power2_eq_square)
    also have "... < 2 ^ n + 2 ^ n"
      using * twonplus1_lt_twopown[of n]
      by simp
    also have "... = 2 * 2 ^ n"
      by simp
    also have "... = 2 ^ (Suc n)"
      by simp
    finally show ?thesis
      .
  qed
qed

section \<open>Deljivost sa 3\<close>

lemma deljivost_sa_3:
fixes n :: nat 
shows "(3::nat) dvd 5^n + 2^(n+1)" 
proof (induct n)
  case 0
  thus ?case
    by (simp add: numeral_Bit1)
next
  case (Suc n)
  have "(5::nat) ^ Suc n + 2 ^ (Suc n + 1) = 5 * 5 ^ n + 2 * 2 ^ (n + 1)"
    by simp
  also have "... = 3 * 5 ^ n + 2 * (5 ^ n + 2 ^ (n + 1))"
    by simp
  finally 
  show ?case
    using dvd_add[OF dvd_triv_left[of "3::nat" "5^n"] dvd_mult[OF Suc, of 2]]
    by simp
qed

section \<open>Bernulijeva nejednakost\<close>

lemma
  fixes x::real and n::nat
  assumes "x > -1"
  shows "(1 + x)^n \<ge> 1 + n * x"
proof (induction n)
  case 0
  show ?case
    by simp
next
  case (Suc n)
  show ?case
  proof-
    have "1 + (n + 1) * x \<le> 1 + (n + 1) * x + n * x^2"
      by simp
    also have "... = (1 + x) * (1 + n * x)"
      by (simp add: algebra_simps power2_eq_square)
    also have "... \<le> (1 + x) * (1 + x) ^ n"
      using Suc `x > -1` (* ovde se pozivamo na pretpostavku *)
      by simp
    also have "... = (1 + x) ^ (Suc n)"
      by simp
    finally
    show ?thesis
      by simp
  qed
qed

section \<open>Moavrova formula\<close>

lemma
  fixes r \<phi> :: real and n :: nat
  shows "(r * (cos \<phi> + \<i> * sin \<phi>)) ^ n = r ^ n * (cos (n * \<phi>) + \<i> * sin(n * \<phi>))"
proof (induction n)
  case 0
  show ?case
    by simp
next
  case (Suc n)
  show ?case
  proof-
    have "(r * (cos \<phi> + \<i> * sin \<phi>)) ^ Suc n = 
          (r * (cos \<phi> + \<i> * sin \<phi>)) ^ n * r * (cos \<phi> + \<i> * sin \<phi>)"
      by simp                                                            
    also have "... = r^n * (cos (n * \<phi>) + \<i> * sin (n * \<phi>)) * r * (cos \<phi> + \<i> * sin \<phi>)"
      using Suc
      by simp
    also have "... = r^(Suc n) * ((cos (n * \<phi>) * cos \<phi> - sin (n * \<phi>) * sin \<phi>) + \<i> * (sin(n * \<phi>) * cos \<phi> + cos (n * \<phi>) * sin \<phi>))"
      by (simp add: algebra_simps)
    also have "... = r^(Suc n) * (cos (n * \<phi> + \<phi>) + \<i> * sin (n * \<phi> + \<phi>))"
      using cos_add[of "n * \<phi>" \<phi>, symmetric] sin_add[of "n * \<phi>" \<phi>, symmetric]
      by simp
    finally
    show ?thesis
      by (simp add: algebra_simps)
  qed
qed

end