theory Indukcija_IV_cas
(* imports Main *)
(* Real numbers are not included by Main.thy.
   Theory Complex_Main.thy imports Main.thy together with many more 
   theories containing, for example, all the basic properties of real 
   and complex numbers. *)
imports Complex_Main
(* imports HOL.Real -- Samo realne, bez kompleksnih *)

begin

(* Pravilo indukcije koje zadovoljava uslov n\<ge>m *)
thm nat_induct_at_least

(* Zahvaljujuci ovom pravilu mozemo zapisati dokaze sa proslog casa tako da vise 
   lice na dokaze u udzbeniku *)

(* Zadatak 11 - pomocno tvrdjenje *)

lemma n2_2np1_at_least:
  fixes n::nat
  assumes "n \<ge> 3"
  shows "n^2 > 2*n + 1"
  using assms
proof (induction n rule: nat_induct_at_least)
  (* bazni slucaj *)
  case base
  thus ?case
    by simp
next
  case (Suc n)
  have "2 * (Suc n) + 1 < 2 * (Suc n) + 2 * n"
    using `n \<ge> 3`
    by simp
  also have "... = 2 * n + 1 + 2 * n + 1"
    by simp
  also have "... < n^2 + 2 * n + 1"
    using Suc
    by simp
  also have "... = (Suc n)^2"
    by (simp add: power2_eq_square)
  finally
  show ?case
  .
  qed

(* Primeri sa realnim brojevima *)
  
(* 4. zadatak - Matematicka indukcija *)

lemma
  fixes x::real and n::nat
  assumes "x > -1"
  shows "(1 + x)^n \<ge> 1 + n * x"
  (* bez using assms da bi bili jednostavniji dokazi, pa cemo se pozivati na 
     pretpostavku samo na onom mestu u dokazu gde cemo je eksplicitno koristiti *)
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                                            

(* Zadatak 5 *)

primrec zbir_naizmenicno:: "nat \<Rightarrow> int" where
"zbir_naizmenicno 0 = 0" | 
"zbir_naizmenicno (Suc n) = zbir_naizmenicno (n) + (-1)^(Suc n) * (2 * (Suc n) - 1)"
(* eventualno int(Suc n) kada je potrebno eksplicitno prebaciti u int zbog oduzimanja *)

(* nakon raspisivanja dokaza na papiru, vidimo da su nam potrebne neke teoreme 
   odredjenog formata *)
find_theorems "_ ^ Suc _"
find_theorems " _ * ( _ + _ ) = _ * _ + _ * _ "
thm int_distrib

lemma zad5: "zbir_naizmenicno n = (-1)^n * n"
proof (induction n)
case 0
then show ?case by simp
next
case (Suc n)
show ?case 
proof - 
have "zbir_naizmenicno (Suc n) = zbir_naizmenicno (n) + (-1)^(Suc n) * (2 * (Suc n) - 1)"
by (simp only: zbir_naizmenicno.simps)
also have "... = (-1)^n * n + (-1)^(n+1)*(2*(n+1)-1)"
using Suc by simp
also have "... = (-1)^n *(-1)*(-1)*n + (-1)^(n+1)*(2*n+1)"
by simp
also have "... = (-1)^(n+1)*(-1)*n + (-1)^(n+1)*(2*n+1)" 
by simp
also have "... = (-1)^(n+1) * ((-1)*n + (2*n+1))"
(* Naredni korak se moze dokazati na nekoliko nacina:

(1) Eksplicitna naredba kojom kazemo Isabelle-u da unutar onoga sto dokazujemo
    (unutar cilja) pronadje unifikacijom levu stranu teoreme koju navodimo i
    zameni desnom stranom te teoreme. *)

(*
apply (subst int_distrib)
apply simp
*)

(*  Slicno bi pozvali i "apply (subst ime_teoreme[symmetric])" gde se izdaje naredba
    da se unutar cilja pronadje desna strana navedene teoreme i da se zameni levom. *)

(* (2) *)

(* by (subst int_distrib, simp)*)

(* (3) Koriscenje simp add ne ubacuje teoremu u pretpostavke, vec je da simplifikatoru
   kao rewrite pravilo, sto znaci da se ona ne simplifikuje pre primene. *)

(* by (simp add: int_distrib)*)

(* (4) Koriscenje using ubacuje teoremu u svoje pretpostavke i onda se simplifikator
       primenjuje i na nju *)
using int_distrib 
by simp
also have "... = (-1)^(n+1) * (n+1)" by simp
finally show ?thesis by simp
qed
qed

(* Neke teoreme vezane za deljivost *)
find_theorems "_ dvd _"
find_theorems "_ dvd _ * _"
find_theorems "_ dvd _ + _"
find_theorems "_ \<Longrightarrow>  _ dvd _ + _"

thm nat_induct
thm dvd_def
thm dvd_add

thm dvd_refl
find_theorems "_ ^ _"
thm power_0
thm power_one_right

(* Zadatak 9 *)

(* mora biti naglaseno da je n tipa nat. Mozemo to zapisati na dva nacina: 
lemma deljivost_sa_6 :
shows "6 dvd (n::nat)*(n+1)*(2*n+1)" 
*)
lemma deljivost_sa_6:
fixes n :: nat 
shows "6 dvd n*(n+1)*(2*n+1)" 
(* koriscenje naredne naredbe moze da otkrije potrebu za uvodjenjem tipova u teoremi 
 using [[show_types]]
 nakon utvrdjivanja tipova, naredba moze da se obrise. *)
proof (induction n)
case 0
then show ?case 
by simp (* apply simp --- ispisuje sta dobije, ovu naredbu mozete pozvati bilo gde*)
next
case (Suc n)
then show ?case 
  proof - 
  have "Suc n * (Suc n + 1) * (2 * Suc n + 1) = (n+1)*(n+2)*(2*n+3)" 
  by (simp add: algebra_simps)
  also have "... = n*(n+1)*(2*n+3) + 2*(n+1)*(2*n+3)" 
  by (simp add: algebra_simps)
  also have "... = n*(n+1)*(2*n+1) + 2*n*(n+1) + 2*(n+1)*(2*n+3)"
  by (simp add: algebra_simps)
  also have "... = n*(n+1)*(2*n+1) + 2*(n+1)*(3*n+3)"
  by (simp add: algebra_simps)
  also have "... = n*(n+1)*(2*n+1) + 6*(n+1)*(n+1)"
  by (simp add: algebra_simps) 
  (* sledgehammer --- mozete pokusati kada nemate ideju kako dalje dokazati *)
   
  finally show ?thesis
  using Suc
  thm One_nat_def
  (* using [[simp_trace]]
     by simp 
     --- mozete pokrenuti i ovako da bi se videlo sta je tacno primenjivano tokom 
         simplifikacije. Ako krene pogresnim putem onda se moze obrisati teorema 
         koja u stvari nije potrebna za ispravan dokaz.
  *)
  by (simp del: One_nat_def)   
  
  (* drugi nacin: imenujemo izvedenu jednakost da bi se dobio oblik primeren za 
     primenu dvd_add
  finally 
  have *: "Suc n * (Suc n + 1) * (2 * Suc n + 1) = n*(n+1)*(2*n+1) + 6*(n+1)*(n+1)"   
  .
   show ?thesis
    using Suc
    by (subst *, rule dvd_add, simp)
    
    --- ovde je prikazana kombinacija vise metoda koji se nalaze u zagradi iza by, 
        primenjuju se redom jedan po jedan. Metode mozete primeniti i pomocu apply 
        i tada se vidi sta se dobilo primenom metoda

    --- detaljnije:
        Cilj je oblika 6 dvd izraz1. Pre toga je dokazana jednakost 
        izraz1 = izraz2 + izraz3 i nazvali smo je *. 
        
        Kada se primeni metod subst * cilj postaje 6 dvd izraz1 + izraz2 
        (subst u cilju menja levu stranu date jednakosti desnom stranom). 
        
        Nakon toga primenjujemo metod rule dvd_add. 
        Metod rule cilj unifikuje sa desnom stranom date teoreme, unifikujuci 
        pri tom premise teoreme sa premisama u trenutnom cilju. 
        
        Sve premise koje nisu na taj nacin pronadjene postaju novi ciljevi 
        koje je potrebno dokazati. U nasem primeru dvd_add ima dve premise. 
        Jedna se uspesno unifikuje sa nasim Suc i ona je time automatski dokazana, 
        a druga postaje novi cilj koji treba dokazati. 
        Taj cilj je trivijalan i simp ga automatski dokazuje. 
  *)
  qed
  qed

(* Zadatak 10 *)  
lemma deljivost_sa_3:
fixes n :: nat 
shows "(3::nat) dvd 5^n + 2^(n+1)" 
(* using [[show_types]] *)
proof (induct n)
case 0
thus ?case
  (* sledgehammer daje slicno resenje *)
  (* Naredba apply simp sugerise da je potrebno koristiti pravilo narednog tipa *)
  (* apply simp 
  find_theorems "3 = _"
  thm numeral_3_eq_3 *)
  by (simp add: numeral_3_eq_3)
next
case (Suc n)
  (* Konvertovanje je neophodno kada iz konteksta nije moguce zakljuciti tip. 
     Operator ^ je polimorfan i primenjuje se na objekte razlicitih tipova.
     U situaciji kada ne prolazi dokaz koji deluje da bi trebalo da prodje automatski
     moguce je da tipovi nisu u redu i da se moraju precizirati. *)
     
  have "(5::nat) ^ Suc n + 2 ^ (Suc n + 1) = 5 * 5 ^ n + 2 * 2 ^ (n + 1)"
  using[[show_types]] (* pokrenite ovu naredbu bez ::nat u prethodnom redu *)
  by simp
  
  also have "... = 3 * 5 ^ n + 2 * (5 ^ n + 2 ^ (n + 1))"
    by simp
  finally 
  show ?case
(* ispis teorema koje se koriste 
  thm Suc
  thm dvd_triv_left
  thm dvd_mult
  thm dvd_add *)
    using dvd_add[OF dvd_triv_left[of "3::nat" "5^n"] dvd_mult[OF Suc, of 2]]
    by simp
    (*  dvd_triv_left[of...] sluzi da instanciramo promenljive
        
        dvd_mult[OF Suc, of 2] omogucava da istovremeno zadamo premisu i 
                               instanciramo jednu promenljivu.

        dvd_add[OF...] nam omogucava da zadamo premise teoreme dvd_add, 
                       to su dve cinjenice koje dobijamo uz pomoc teorema 
                       dvd_triv_left i dvd_mult.

    *)
qed

(* Funkcije za kastovanje izmedju razlicitih tipova se mogu naci narednim naredbama *)
find_consts "nat \<Rightarrow> int"
find_consts "nat \<Rightarrow> real"
find_consts "real \<Rightarrow> complex"                                 

(* Primer funkcije int. Tip i funkcija mogu imati isto ime. 
   Ovde int predstavlja funkciju koja slika nat u int *)
term "3::nat"
term "int (3::nat)"
term "int 3"

(* @{term t} prints a well-typed term t.
   @{value t} evaluates a term t and prints its result *)
value "int (3::nat)"
term "3::nat"
value "3::nat"

thm Re_complex_of_real
thm Im_complex_of_real
thm complex_of_real_def

(* 12 zadatak - Moavrova formula *)

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>))"
      thm cos_add
      thm sin_add
(*  
      apply (subst cos_add[of "n * \<phi>" \<phi>, symmetric])
      apply (subst sin_add[of "n * \<phi>" \<phi>, symmetric])      
      by simp
*)
    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

(* Princip jake indukcije 
   Prvi je opstiji (radi za bilo koji wellfounded order), 
   ali drugi je specificniji i zadovoljava nase potrebe *)
thm less_induct
thm nat_less_induct

(* (⋀x. (⋀y. y < x ⟹ ?P y) ⟹ ?P x) ⟹ ?P ?a *)

(* Zadatak 6 *)

definition gm where
 "gm = (1 + sqrt 5) / 2"

fun fib :: "nat \<Rightarrow> nat" where
  "fib 0 = 0"
| "fib (Suc 0) = 1"
| "fib (Suc (Suc n)) = fib (Suc n) + fib n"

lemma fibonaci:
shows "fib (n + 1) \<le> gm ^ n"
proof (induction n rule: nat_less_induct)
case (1 n)
thm 1
  show ?case
  proof (cases "n = 0")
    case True
    thus ?thesis
      by simp
  next
    case False
    show ?thesis
    proof (cases "n = 1")
      case True
      have "fib 2 = 1"
        (* by eval --- drugi nacin uz pomoc metoda koji izracunava tu rekurzivnu 
                       funkciju *)
        by (simp add: numeral_2_eq_2)
        thus ?thesis
        using `n = 1`
        by (simp add: gm_def)
    next
      case False
      show ?thesis
      proof-
        obtain m where "m = n - 2"
          by auto
          have "n > 1" using `n \<noteq> 0` `n \<noteq> 1`
          by simp
        have "fib (m + 3) = fib (m + 2) + fib (m + 1)"
          by (simp add: numeral_3_eq_3)             
        also have "... \<le> gm ^ (m + 1) + gm ^ m"
          (* modifikator [rule_format] od "\forall x. P x" pravi "P ?x" 
             na koji onda mozemo dalje da primenimo of da bi ubacili vrednost za x. 
             To se obicno koristi kada imamo premisu sa univerzalnim kvantifikatorom 
             koju hocemo da instanciramo. *)
          using 1[rule_format, of "m+1"] 1[rule_format, of m] `m = n - 2` `n > 1`
          by force
        also have "... = gm ^ m * (gm + 1)"       
          by (simp add: algebra_simps)
        also have "... = gm ^ m * (gm ^ 2)"
          (* drugi nacin:
             unfolding gm_def 
               by (simp add: power2_eq_square algebra_simps) 
             naredba unfolding prikazuje raspisanu definiciju
          *)
          by (simp add: power2_eq_square algebra_simps gm_def) 
        also have "... = gm ^ (m + 2)"
          by (simp add: power_add power2_eq_square)
        finally
        show ?thesis
          using `m = n - 2` `n > 1`
          by (simp add: numeral_2_eq_2 Suc_diff_Suc)
      qed
    qed
  qed
qed

end