theory Indukcija_III_cas_intro
imports Main

begin

(* Numerical examples that use the type of natural numbers, nat.
   This is a recursive datatype generated by the constructors zero
   and successor, so it works well with inductive proofs and primitive recursive
   function definitions. *)

value "(1 + 2::nat)"
value "1 + (2::int)"
value "1 - (2::nat)"
value "1 - (2::int)"

term Suc

primrec duplo :: "nat \<Rightarrow> nat" where
"duplo 0 = 0" |
"duplo (Suc n) = Suc (Suc (duplo n))"

thm duplo.simps

(* Zadatak sa proslog casa *)
lemma dupliranje: "duplo m = m + m"
proof (induction m)
case 0
  show ?case 
    by (simp only: duplo.simps(1))
next
case (Suc m)
  show ?case
  proof - 
    have "duplo (Suc m) = Suc(Suc(duplo m))" 
      by (simp only: duplo.simps(2))
    also have "... = Suc(Suc(m + m))" 
      using Suc by simp 
    finally show ?thesis by simp
  qed 
qed

(* Zadatak 1 - Matematicka indukcija *)

primrec zbir_do :: "nat \<Rightarrow> nat" where               
  "zbir_do 0 = 0"
| "zbir_do (Suc n) = Suc n + (zbir_do n)"

find_theorems name: "Suc_eq"

thm Suc_eq_plus1 (* Suc n = n+1 *)

find_theorems "_ * (_ + _) = _ * _ + _ * _"

(* teoreme vezane za sabiranje, oduzimanje i mnozenje *)
thm algebra_simps

(* dodatno za deljenje *)
thm field_simps

(* The modifiers for method "auto" are "simp add" and "simp del", 
   instead of just "add" and "del" *)
lemma suma_do_n_automatski: "zbir_do n = n * (n+1) div 2"
by (induction n, auto simp add: algebra_simps)

lemma suma_do_n: "zbir_do n = n * (n+1) div 2"
sorry

(* DOMACI --- Zadatak 2 - Matematicka indukcija*)

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

lemma neparni: "zbir_neparnih n = n*n"
(* by (induction n, auto simp add: algebra_simps) *)
sorry

(* Zadatak 8 - Matematicka indukcija *)

primrec zbir_kvadrata :: "nat \<Rightarrow> nat" where               
  "zbir_kvadrata 0 = 0"
| "zbir_kvadrata (Suc n) = (Suc n)*(Suc n) + (zbir_kvadrata n)"

value "zbir_kvadrata 3"

lemma kvadrati_do_n_automatski: "zbir_kvadrata n = n * (n+1) * (2*n + 1) div 6"
by (induction n, auto simp add: algebra_simps)

lemma kvadrati_do_n: "zbir_kvadrata n = n * (n+1) * (2*n + 1) div 6"
sorry

(* Zadatak 3 - Matematicka indukcija *)

(* Type synonyms are abbreviations for existing types.
   Type synonyms are expanded after parsing and are not present in internal
   representation and output. They are mere conveniences for the reader. *)
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) *)
sorry 

(* Zadatak 11 - Matematicka indukcija *)
   
(* Structured Lemma Statements: fixes, assumes, shows:
  The optional "fixes" part allows you to state the types of variables up front
  rather than by decorating one of their occurrences in the formula with a type
  constraint. 
  The key advantage of the structured format is the "assumes" part that
  allows you to name each assumption; multiple assumptions can be separated
  by "and". 
  The "shows" part gives the goal.*)

thm power2_eq_square

(* Pomocno tvrdjenje *)

lemma n2_2np1:
  fixes n::nat
  assumes "n > 2"
  shows "n^2 > 2*n + 1"
  using assms
proof (induction n)
  case 0
  thus ?case
    by simp
next
  case (Suc n)
  thm Suc
  show ?case
  proof (cases "n = 2")
    case True
    thus ?thesis
      by simp
  next
    case False
    (*from this and Suc
    have "n > 2" 
    by simp*)
    hence "n > 2"  
      using Suc(2)
      by simp

    have "2 * (Suc n) + 1 < 2 * (Suc n) + 2 * n"
      using `n > 2`
      by simp
    also have "... = 2 * n + 1 + 2 * n + 1"
      by simp
    also have "... < n^2 + 2 * n + 1"
      using Suc(1) `n > 2`
      by simp
    also have "... = (Suc n)^2"
      by (simp add: power2_eq_square)
    finally
    show ?thesis
      .
  qed
qed

(* Zadatak 11 *)

lemma 
  assumes "n \<ge> 5"
  shows "2^n > n^2"
  using assms
  sorry

end