1 theory Cas9_vezbe_resenja
   2 imports Complex_Main
   3 begin
   4 
   5 section ‹Prirodni brojevi i matematička indukcija›
   6 
   7 text‹Zadaci su preuzeti iz materijala profesora Ikodinovića: 
   8 @{url ‹http://www.matf.bg.ac.rs/p/files/43-matematicka_indukcija.pdf›}.›
   9 
  10 text‹
  11 U narednim primerima ćemo koristiti ugrađen tip prirodnih brojeva @{type nat}.
  12 Tip prirodnih brojeva je rekurzivno definisan tip sa konstruktorima nula i 
  13 sledbenik. Posebno se dobro slaže sa induktivnim dokazima i primitivno 
  14 rekurzivnim definicijama.
  15 
  16 Teorija prirodnih brojeva moze se naći na: 
  17 @{url ‹https://isabelle.in.tum.de/library/HOL/HOL/Nat.html›}
  18 
  19 Postoji jako puno teorema nad prirodnim brojevima koje možemo koristiti po 
  20 potrebi. Za pretraživanje skupa teorema možemo koristiti naredbu 
  21 \verb!find_theorems! koja nam nudi pretragu po imenu (uz ključnu reč \verb!name!, 
  22 ili pretragu po šablonu koji nam treba. Na primer, uz pomoć narednih
  23 dveju naredbi možemo pronaći teoreme @{text ‹Suc_eq_plus1:›} @{thm Suc_eq_plus1 
  24 [no_vars]} i @{text ‹add_mult_distrib2:›} @{thm add_mult_distrib2 [no_vars]}.›
  25 
  26 find_theorems name: "Suc_eq"
  27 thm Suc_eq_plus1 (* Suc n = n+1 *) ― ‹@{thm Suc_eq_plus1 [no_vars]}›
  28 
  29 find_theorems "_ * (_ + _) = _ * _ + _ * _" 
  30 thm add_mult_distrib2  ― ‹@{thm add_mult_distrib2 [no_vars]}›
  31 
  32 text‹U dokazima će nam često trebati teoreme vezane za sabiranje, oduzimanje i 
  33 množenje. Nekoliko najčešće korišćenih se nalaze u skupu teorema sa imenom 
  34 \verb!algebra_simps!. Teoreme vezane za deljenje se nalaze u posebnom skupu 
  35 teorema koji se zove \verb!field_simps! (ovaj skup je nadskup prethodnog skupa).›
  36 
  37 thm algebra_simps
  38 
  39 thm field_simps
  40 
  41 text‹Kada se neka od potrebnih lema, ili ceo skup lema, dodaje automatskim 
  42 alatima ključne reči koje se koriste za metod @{text ‹auto›} su 
  43 @{text ‹simp add›} i @{text ‹simp del›}.›
  44 
  45 text‹
  46 \begin{exmp}
  47 Dokazati da važi $1 + \ldots + n = n * (n+1) div 2$.
  48 \footnote{Zadatak 1 iz dodatnog materijala.}
  49 \end{exmp}
  50 
  51 Sada kada radimo sa prirodnim brojevima, možemo ponovo definisati neke od 
  52 funkcija koje smo videli na prošlom času:›
  53 
  54 primrec zbir_do :: "nat ⇒ nat" where               
  55 "zbir_do 0 = 0" |
  56 "zbir_do (Suc n) = Suc n + (zbir_do n)"
  57 
  58 text‹Sada uz pomoć automatskih alata, i skupa lema \verb!algebra_simps! možemo 
  59 dokazati narednu lemu. Primetite da smo na prošlom času koristili dodatnu 
  60 funkciju \verb!duplo!, zato što nismo definisali operaciju \verb!div! u 
  61 našem izvedenom skupu prirodnih brojeva. Sada kada radimo sa ugrađenim tipom 
  62 prirodnih brojeva, na raspolaganju imamo i operaciju \verb!div! pa lemu možemo 
  63 zapisati na sledeći način i dokazati je na sledeći način:›
  64 
  65 lemma suma_do_n_automatski: "zbir_do n = n * (n+1) div 2"
  66 by (induction n, auto simp add: algebra_simps)
  67 
  68 text‹Dokaz iste leme u Isar-u:›
  69 
  70 lemma suma_do_n_isar: "zbir_do n = n * (n+1) div 2"
  71 proof (induction n)
  72 case 0
  73   show ?case 
  74     by (simp only: zbir_do.simps(1))
  75 next
  76 case (Suc n)
  77 thm Suc
  78   show ?case 
  79   proof - 
  80     have "zbir_do (Suc n) = Suc n + zbir_do (n)" 
  81       by (simp only: zbir_do.simps(2))
  82     also have "... = Suc n + n * (n+1) div 2" 
  83     using Suc by simp
  84     also have "... = 2 * (Suc n) div 2 + (Suc n) * n div 2" 
  85     by simp
  86     also have "... = (Suc n) * (2 + n) div 2" 
  87     by simp
  88     finally show ?thesis by simp
  89   qed
  90 qed
  91 
  92 text‹
  93 \begin{exmp}
  94 Dokazati da važi $1 + 3 + 5 + \ldots + (2*n - 1) = n*n$.
  95 \footnote{Zadatak 2 iz dodatnog materijala.}
  96 \end{exmp}
  97 ›
  98 
  99 value "1 + 3 + 5 + 7 + 9::nat"
 100 value "5*5::nat"
 101 
 102 text‹U ovom zadatku prvo je potrebno definisati funkciju sa leve strane date 
 103 jednačine. U pitanju je zbir prvih $n$ neparnih brojeva, što možemo definisati 
 104 primitivnom rekurzijom na sledeći način:
 105 ›
 106 
 107 primrec zbir_neparnih :: "nat ⇒ nat" where               
 108 "zbir_neparnih 0 = 0" |
 109 "zbir_neparnih (Suc n) = 2*(Suc n) - 1 + (zbir_neparnih n)"
 110 
 111 text‹Sada možemo dokazati traženu lemu i automatski i raspisano u Isar-u.›
 112 
 113 lemma neparni_auto: "zbir_neparnih n = n*n"
 114 by (induction n, auto simp add: algebra_simps)
 115 
 116 lemma neparni_isar: "zbir_neparnih n = n*n"
 117 proof (induction n)
 118   case 0
 119   show ?case by (simp only: zbir_neparnih.simps(1))
 120 next
 121   case (Suc n)
 122   show ?case
 123   proof - 
 124     have "zbir_neparnih (Suc n) = 2*(Suc n) - 1 + zbir_neparnih n"
 125       by (simp only: zbir_neparnih.simps(2))
 126     also have "... = 2*(Suc n) - 1 + n*n" using Suc by simp
 127     also have "... = 2*n + 1 + n*n" by simp
 128     finally show ?thesis by simp
 129   qed
 130 qed
 131 
 132 text‹
 133 \begin{exmp}
 134 Dokazati da važi: $-1 + 3 - 5 + \ldots + (-1)^n * (2*n-1) = (-1)^n * n$.
 135 \footnote{Zadatak 5 iz dodatnog materijala.}
 136 \end{exmp}
 137 
 138 Prvi korak je definisanje funkcije koja opisuje izraz sa leve strane:
 139 ›
 140 
 141 primrec zbir_naizmenicno:: "nat ⇒ int" where
 142 "zbir_naizmenicno 0 = 0" | 
 143 "zbir_naizmenicno (Suc n) = zbir_naizmenicno n + (-1)^(Suc n) * (2 * (Suc n) - 1)"
 144 
 145 text‹Kada se radi sa celim brojevima, oduzimanje može u nekim situacijama 
 146 napraviti problem i biće potrebna konverzija u ceo broj, na primer: 
 147 @{text ‹int(Suc n)›}. 
 148 
 149 Nakon raspisivanja dokaza na papiru, vidimo da su nam potrebne neke teoreme 
 150 određenog formata. Pretragu po formatu smo već koristili: ›
 151 
 152 find_theorems "_ ^ Suc _"
 153 find_theorems " _ * ( _ + _ ) = _ * _ + _ * _ "
 154 thm int_distrib
 155 
 156 lemma zad5: "zbir_naizmenicno n = (-1)^n * n"
 157 proof (induction n)
 158   case 0
 159   then show ?case 
 160     by simp
 161 next
 162   case (Suc n)
 163   show ?case
 164   proof -
 165     have "zbir_naizmenicno (Suc n) = zbir_naizmenicno (n) + (-1)^(Suc n) * (2 * (Suc n) - 1)"
 166       by (simp only: zbir_naizmenicno.simps)
 167     also have "... = (-1)^n * n + (-1)^(n+1)*(2*(n+1)-1)"
 168       using Suc by simp
 169     also have "... = (-1)^n *(-1)*(-1)*n + (-1)^(n+1)*(2*n+1)"
 170       by simp
 171     also have "... = (-1)^(n+1)*(-1)*n + (-1)^(n+1)*(2*n+1)" 
 172       by simp
 173     also have "... = (-1)^(n+1) * ((-1)*n + (2*n+1))"
 174       by (simp add: int_distrib) ― ‹ili @{text ‹using int_distrib by simp›}›
 175     also have "... = (-1)^(n+1) * (n+1)" by simp
 176     finally show ?thesis by simp
 177   qed
 178 qed
 179 
 180 subsection‹Zbir kvadrata›
 181 
 182 text‹
 183 \begin{exmp}
 184 Dokazati da važi da je $1 + 2^2 + ... + n^2 = n * (n+1) * (2*n+1) div 6$.
 185 \footnote{Zadatak 8 iz dodatnog materijala.}
 186 \end{exmp}
 187 
 188 Prvo je potrebno definisati funkciju koja opisuje levu stranu ovog izraza.
 189 Postoji više načina da definišemo funkciju koja računa zbir kvadrata od 1 do n. 
 190 Prvi način je da koristimo primitivnu rekurziju, drugi način je da koristimo 
 191 bibliotečke funkcije za rad sa listama.
 192 
 193 \paragraph{Primitivna rekurzija:}
 194 Prvo definišemo primitivnom rekurzijom funkciju koja izračunava zbir kvadrata:
 195 ›
 196 
 197 primrec zbir_kvadrata :: "nat ⇒ nat" where 
 198 "zbir_kvadrata 0 = 0" |
 199 "zbir_kvadrata (Suc n) = zbir_kvadrata n + (Suc n) ^ 2"
 200 
 201 value "zbir_kvadrata 1"
 202 value "zbir_kvadrata 2"
 203 value "zbir_kvadrata 3"
 204 
 205 text‹
 206 \paragraph{Ugrađene funkcije za rad sa listama:}
 207 Korišćenjem ugrađene podrške za liste brojeva, možemo slično kao na prošlom času 
 208 zapisati izraz za zbir kvadrata. Listu elemenata od 0 do 4, odnosno njihov zbir, 
 209 možemo dobiti narednim dvema naredbama:›
 210 
 211 value "[0..<5]"
 212 value "sum_list [0..<5]"
 213 
 214 text‹Možemo umesto 0 napisati 1 i dobiti upravo ono što nam treba u postavci ovog 
 215 zadatka, listu brojeva od 1 do n, odnosno zbir brojeva od 1 do n (iako je u ovom 
 216 slučaju svejedno jer 0 ne utiče na vrednost izraza):›
 217 
 218 value "[1..<5]"
 219 value "sum_list [1..<5]"
 220 
 221 text‹Međutim, nama treba zbir kvadrata pa uvodimo elemente \emph{funkcionalnog 
 222 programiranja}. Isabelle je funkcionalni programski jezik i postoji funkcional 
 223 višeg reda \emph{map} koji datu funkciju primenjuje na svaki element liste. Prvo 
 224 ćemo ključnom rečju @{text ‹definition›} definisati novu funkciju koja kvadrira 
 225 vrednost svog argumenta:›
 226 
 227 definition kvadrat :: "nat ⇒ nat" where 
 228 "kvadrat x = x * x"
 229 
 230 text‹Naredna naredba prikazuje korišćenje funkcionala @{text ‹map›} i primenjuje 
 231 funkciju kvadriranja na elemente liste. Rezultat te naredbe je nova lista čiji 
 232 elementi su jednaki kvadratima elemenata polazne liste. Funkcija @{text 
 233 ‹sum_list›} sumira elemente tako dobijene liste.›
 234 
 235 value "map kvadrat [1..<5]" 
 236 value "sum_list (map kvadrat [1..<5])"
 237 
 238 text‹Isti efekat se može dobiti i bez definicije, ali sada primenjujemo 
 239 \emph{anonimnu funkciju} definisanu pomoću lambda @{text ‹(λ)›} izraza:›
 240 
 241 value "sum_list (map (λ x. x ^ 2) [1..<5])"
 242 
 243 text‹Lambda izraz predstavlja anonimnu funkciju čiji se parametar navodi odmah 
 244 iza @{text ‹λ›}, a nakon tačke se nalazi telo funkcije. Sada funkciju koja 
 245 izračunava zbir kvadrata možemo definisati i direktno bez primitivne rekurzije:›
 246 
 247 definition zbir_kvadrata' :: "nat ⇒ nat" where
 248 "zbir_kvadrata' n = sum_list (map (λ x. x ^ 2) [1..<Suc n])"
 249 
 250 text‹U Isabelle-u postoji skraćeni zapis (blizak matematičkom zapisu na koji smo 
 251 navikli). @{text ‹∑›} se zapisuje kao \verb!\!\verb!<Sum>!, @{text ‹←›} se 
 252 zapisuje kao \verb!\!\verb!<leftarrow>!. Leva strana (pre tačke) navodi opseg 
 253 vrednosti za x, a desna strana (posle tačke) navodi na koji način se te vrednosti 
 254 transformišu:›
 255 
 256 value "∑ x ← [1..<5]. x ^ 2"
 257 
 258 text‹Ako bismo ovu istu funkciju prosledili kao parametar funkciji @{text ‹term›} 
 259 možemo videti da u pozadini sistem ipak koristi raspisani oblik koji smo malopre 
 260 pokazali @{term ‹∑ x ← [1..<5]. x ^ 2›}. Jedina razlika je što sistem koristi 
 261 već ugrađenu funkciju @{text ‹power2›} koja izračunava kvadrat broja.›
 262 
 263 term "∑ x ← [1..<5]. x ^ 2"
 264 
 265 text‹
 266 \begin{exmp}
 267 Pokazati da su ove definicije ekvivalentne, odnosno pokazati da važi: 
 268 \verb!zbir_kvadrata n = zbir_kvadrata' n!.
 269 \end{exmp}
 270 
 271 Prvo pokušavamo sa indukcijom, što očekivano rezultuje sa dva cilja. Nakon toga 
 272 pokušavamo sa auto, ali automatski alati ne prolaze. Razlog za to je što funkcije 
 273 definisane primitivnom rekurzijom automatski ulaze u simplifikator i njihova 
 274 pravila se automatski primenjuju, ali funkcije definisane pomoću ključne reči 
 275 \emph{definition} nisu deo simplifikatora i moramo ih eksplicitno dodati.›
 276 
 277 thm zbir_kvadrata.simps  ―‹ove teoreme su automatski ukljucene u proces simplifikacije›
 278 thm zbir_kvadrata'_def  ―‹ova teorema nije automatski ukljucena u proces simplifikacije›
 279 
 280 lemma "zbir_kvadrata n = zbir_kvadrata' n"
 281 apply (induction n)
 282 ―‹apply auto›
 283 apply (auto simp add: zbir_kvadrata'_def)
 284 done
 285 ―‹ili skraćeno @{text ‹by (induction n) (auto simp add: zbir_kvadrata'_def)›}›
 286 
 287 text‹Drugi način na koji možemo zapisati ovu lemu je bez uvođenja definicije, i 
 288 sada nema potrebe za dodavanjem dodatne leme (zato što smo već raspisali 
 289 definiciju sami):›
 290 
 291 lemma "zbir_kvadrata n = (∑ x ← [1..<Suc n]. x ^ 2)"
 292 by (induction n) auto
 293   
 294 text‹
 295 \begin{exmp}
 296 Dokazati da važi: $1 + 2^2 + ... + n^2 = n * (n+1) * (2*n+1) div 6$
 297 \end{exmp}
 298 
 299 Ovaj dokaz neće proci korišćenjem samo automatskih metoda već moramo da 
 300 simuliramo dokaz koji je naveden u matematičkom udžbeniku.›
 301 
 302 text‹Pogledajmo prvo kako izgleda princip indukcije za prirodne brojeve. Postoji 
 303 ugrađena teorema indukcije koja se zove @{text ‹nat.induct›}, 
 304 @{thm nat.induct [no_vars]}, koja je već dokazana u sistemu i deo je biblioteke 
 305 teorema koje mi možemo koristiti:›
 306 
 307 thm nat.induct
 308 
 309 text‹I po njoj vidimo: da bismo dokazali da svojstvo P važi za proizvoljan 
 310 prirodan broj, dovoljno je da dokažemo da to svojstvo P važi za nulu, i kada 
 311 fiksiramo proizvoljni prirodni broj, ako pretpostavimo da upravo za taj broj važi 
 312 svojstvo P i iz toga uspemo da izvedemo da i njegov sledbenik ima svojstvo P.›
 313 
 314 lemma "zbir_kvadrata n = (n * (n + 1) * (2*n + 1)) div 6"
 315 proof (induction n)
 316   case 0
 317   then show ?case 
 318   by auto
 319 next
 320   case (Suc n)
 321   have "zbir_kvadrata (Suc n) = zbir_kvadrata n + (Suc n) ^ 2"
 322     by simp ―‹na osnovu @{text ‹zbir_kvadrata.simps›}›
 323   also have "... = zbir_kvadrata n + (n+1)*(n+1)"
 324     by (simp add: power2_eq_square) ―‹neophodna nam je ova lema @{thm power2_eq_square [no_vars]}›
 325   also have "... = (n * (n + 1) * (2*n + 1)) div 6 + (n+1)*(n+1)"
 326     using Suc
 327     by simp ―‹na osnovu induktivne hipoteze›
 328   also have "... = (n * (n + 1) * (2*n + 1) + 6 * (n+1) * (n+1)) div 6"
 329     by (simp add: algebra_simps) ―‹za algebarske manipulacije koristimo skup teorema›
 330   also have "... = ((n + 1) * (n + 2) * (2*n + 3)) div 6"
 331     by (simp add: algebra_simps)
 332   finally 
 333   show ?case 
 334     by (simp add: algebra_simps)
 335 qed
 336 
 337 text‹U ovim dokazima možemo korisititi ili samo \emph{simp} ili \emph{auto} koji 
 338 je malo moćniji. On svakako prvo poziva \emph{simp} ali ima još neke dodatne 
 339 mogućnosti koje nekada mogu biti korisne.›
 340 
 341 subsection‹Rad sa matricama›
 342 
 343 text‹U narednom primeru ćemo pokazati množenje matrica u isabelle-u. Prvo moramo 
 344 matricu zapisati na neki način, u ovom primeru nam olakšava to što je dimenzija 
 345 matrice fiksna pa je najjednostavnije da matricu predstavimo uređenom četvorkom 
 346 njenih elemenata. Elemente pišemo po vrstama i eksplicitno navodimo tip ove 
 347 matrice i koristimo operator @{text ‹×›} (koji se zapisuje sa 
 348 \verb!\!\verb!<times>!) pomoću kog kreiramo tip uređenog para, odnosno uređene 
 349 n-torke.›
 350 
 351 term "(1, 1, 0, 1) :: nat × nat × nat × nat"
 352 
 353 text‹Da ne bismo stalno navodili ovu četvorku, možemo koristiti sinonime 
 354 (skraćenice) za već postojeće tipove. Oni se raspisuju nakon parsiranja teksta i 
 355 nisu deo interne reprezentacije niti ispisa. Sinonimi služe udobnosti zapisa 
 356 korisnika. Matricu ćemo navesti na sledeći način:›
 357 
 358 type_synonym mat2 = "nat × nat × nat × nat"
 359 term "(1, 1, 0, 1) :: mat2"
 360 
 361 
 362 text‹
 363 \begin{exmp}
 364 Dokazati da važi $(1,1,0,1)^n = (1,n,0,1)$.
 365 \footnote{Zadatak 3 iz dodatnog materijala.}
 366 \end{exmp}
 367 
 368 Sledeći korak je da definišemo sve pojmove koji su nam se javljali u
 369 dokazu iz udžbenika: jediničnu matricu, množenje matrica, stepenovanje matrica. 
 370 
 371 Jediničnu matricu uvodimo narednom definicijom:›
 372 
 373 definition eye :: mat2 where
 374 "eye = (1, 0, 0, 1)"
 375 
 376 text‹Nakon ovoga definišemo proizvod dve matrice i uvodimo novi način definisanja 
 377 objekata. Definicija (odnosno ključna reč @{text ‹definition›}) ne može da se 
 378 koristi na ovom mestu zato što argument funkcije koja se uvodi definicijom mora 
 379 biti jedna promenljiva (na primer @{text ‹mat_mul m1 m2›}, nakon čega bi bilo 
 380 potrebno da mi sami nekim novim operatorima vadimo element po element). Zbog toga 
 381 ovde koristimo ključnu reč @{text ‹fun›} koja koristi uklapanje šablona 
 382 \emph{(pattern matching)}. Sada umesto da sa leve strane imamo samo imena 
 383 promenljivih, imamo mogućnost da na tom mestu zadamo stukturu vrednosti koje 
 384 te promenljive predstavljaju.›
 385 
 386 fun mat_mul :: "mat2 ⇒ mat2 ⇒ mat2" where
 387   "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)"
 388 
 389 text‹U buduće ćemo @{text ‹fun›} koristiti za definisanje funkcija običnom 
 390 rekurzijom.
 391 
 392 Sada definišemo stepenovanje matrica korišćenjem primitivne rekurzije. I 
 393 korišćenjem funkcije @{text ‹value›} proveravamo da li je definicija dobra.
 394 ›
 395 
 396 primrec mat_pow :: "mat2 ⇒ nat ⇒ mat2" where
 397 "mat_pow A 0 = eye" |
 398 "mat_pow A (Suc n) = mat_mul A (mat_pow A n)"
 399 
 400 value "mat_pow (1, 1, 0, 1) 3"
 401 
 402 thm mat_pow.simps 
 403 
 404 lemma "mat_pow (1, 1, 0, 1) n = (1, n, 0, 1)"
 405   by (induction n, auto simp add: eye_def) ― ‹dodajemo zato što se definicije ne raspliću automatski›
 406 
 407 lemma "mat_pow (1, 1, 0, 1) n = (1, n, 0, 1)"
 408 proof (induct n)
 409   case 0
 410   show ?case
 411     by (simp add: eye_def)
 412 next
 413   case (Suc n)
 414   show ?case
 415   proof-
 416     have "mat_pow (1, 1, 0, 1) (Suc n) = mat_mul (1, 1, 0, 1) (mat_pow (1, 1, 0, 1) n)"
 417       by simp 
 418     also have "... = mat_mul (1, 1, 0, 1) (1, n, 0, 1)"
 419       using Suc
 420       by simp 
 421     also have "... = (1*1+n*0, 1*1+n*1, 0*1+1*0, 0*1+1*1)"
 422       by simp
 423     finally show ?thesis
 424       by simp
 425   qed
 426 qed 
 427 
 428 subsection ‹Deljivost›
 429 
 430 text‹Neke teoreme vezane za deljivost možemo dobiti pretragom skupa teorema:›
 431 
 432 find_theorems "_ dvd _"
 433 find_theorems "_ dvd _ * _"
 434 find_theorems "_ dvd _ + _"
 435 find_theorems "_ ⟹  _ dvd _ + _"
 436 
 437 thm nat_induct
 438 thm dvd_def
 439 thm dvd_add
 440 
 441 thm dvd_refl
 442 find_theorems "_ ^ _"
 443 thm power_0
 444 thm power_one_right
 445 
 446 text‹\begin{exmp}
 447 Dokazati da za svaki prirodan broj n važi: $6 | n * (n + 1) * (2n + 1)$.
 448 \footnote{Zadatak 9 iz dodatnog materijala.}
 449 \end{exmp}
 450 
 451 U postavci ovog zadatka mora biti naglašeno da je u pitanju prirodan broj. U 
 452 dokazima teorema sa celim brojevima, tipovi su često problem, pa se može 
 453 iskoristiti nareda @{text ‹using [[show_types]]›} koja može da otkrije potrebu za 
 454 uvođenjem tipova u teoremi. Nakon utvrđivanja tipova, naredba može da se 
 455 obriše.
 456 
 457 Ako bismo prvo pokušali da formulišemo teoremu na sledeći način (namerno menjamo 
 458 tvrđenje teoreme da ne bi zbunili sledgehammer kasnije sa identičnim tvrđenjem), 
 459 i pokušali sa pravilom indukcije dobili bismo poruku o grešci: \emph{Unable to 
 460 figure out induct rule}. Ako sada dodamo naredbu @{text ‹using [[show_types]]›}, 
 461 odmah nakon tvrđenja teoreme (pre poziva indukcije), vidimo da isabelle nije u 
 462 stanju da ustanovi kog tipa su vrednost 6 i 2. Pa dodajemo sa @{text ‹fixes›} 
 463 informaciju da je n prirodan broj. Sada ako ponovo pogledamo izlaz nakon naredbe 
 464 @{text ‹using [[show_types]]›} možemo primetiti da isabelle sada može da zaključi 
 465 tip i za vrednosti 6 i 2.›
 466 
 467 declare [[quick_and_dirty=true]]
 468 
 469 lemma deljivost_primer:
 470 shows "6 dvd 2*3*n" 
 471 using [[show_types]]  
 472 ―‹@{text ‹proof (induction n)›}›
 473   sorry
 474 
 475 lemma deljivost_sa_6:
 476 fixes n :: nat 
 477 shows "6 dvd n*(n+1)*(2*n+1)" 
 478 ― ‹@{text ‹using [[show_types]]›}›
 479 proof (induction n)
 480   case 0
 481   then show ?case
 482     by simp 
 483 next
 484   case (Suc n)
 485   then show ?case 
 486   proof - 
 487     have "Suc n * (Suc n + 1) * (2 * Suc n + 1) = (n+1)*(n+2)*(2*n+3)" 
 488       by (simp add: algebra_simps)
 489     also have "... = n*(n+1)*(2*n+3) + 2*(n+1)*(2*n+3)" 
 490       by (simp add: algebra_simps)
 491     also have "... = n*(n+1)*(2*n+1) + 2*n*(n+1) + 2*(n+1)*(2*n+3)"
 492       by (simp add: algebra_simps)
 493     also have "... = n*(n+1)*(2*n+1) + 2*(n+1)*(3*n+3)"
 494       by (simp add: algebra_simps)
 495     also have "... = n*(n+1)*(2*n+1) + 6*(n+1)*(n+1)"
 496       by (simp add: algebra_simps)
 497     finally show ?thesis
 498       using Suc
 499       ―‹na ovakvom mestu mozemo pokusati i sledgehammer›
 500       thm One_nat_def
 501 ― ‹a možemo pokušati i @{text ‹using [[simp_trace]] by simp›} i dobijamo 
 502 poruku: "Term does not become smaller". Ovaj izlaz nam prikazuje šta je tačno 
 503 primenjivano tokom simplifikacije. Ako krene pogrešnim putem onda se može 
 504 obrisati teorema koja u stvari nije potrebna za ispravan dokaz. Ovde je to 
 505 teorema @{text ‹One_nat_def:›} @{thm One_nat_def [no_vars]}.›
 506   by (simp del: One_nat_def)   
 507   qed
 508   qed
 509 
 510 
 511 text‹
 512 \begin{exmp}
 513 Dokazati da za svaki prirodan broj n važi: $3 | 5^n + 2^{n+1}$.
 514 \footnote{Zadatak 10 iz dodatnog materijala.}
 515 \end{exmp}
 516 ›
 517 
 518 lemma deljivost_sa_3:
 519 fixes n :: nat 
 520 shows "(3::nat) dvd 5^n + 2^(n+1)" 
 521 (* using [[show_types]] *)
 522 proof (induct n)
 523   case 0
 524   thus ?case
 525 ―‹sledgehammer daje slično rešenje›
 526 ―‹drugi način je da pokušamo sa automatskim dokazivačima sami, i naredba 
 527 @{text ‹apply simp›} sugeriše da je potrebno koristiti pravilo narednog tipa 
 528 @{thm numeral_3_eq_3 [no_vars]}›
 529   (* apply simp 
 530   find_theorems "3 = _"
 531   thm numeral_3_eq_3 *)
 532     by (simp add: numeral_3_eq_3)
 533 next
 534   case (Suc n)
 535 ― ‹u narednom redu se koristi konvertovanje u tip nat. Konvertovanje je neophodno 
 536 kada iz konteksta nije moguće zaključiti tip. Operator stepenovanja @{text ‹(^)›} 
 537 je polimorfan i primenjuje se na objekte različitih tipova. U situaciji kada ne 
 538 prolazi dokaz koji deluje da bi trebalo da prođe automatski moguće je da tipovi 
 539 nisu u redu i da se moraju precizirati.›
 540      
 541   have "(5::nat) ^ Suc n + 2 ^ (Suc n + 1) = 5 * 5 ^ n + 2 * 2 ^ (n + 1)"
 542   using[[show_types]] ― ‹pokrenite ovu naredbu bez ::nat u prethodnom redu›
 543   by simp
 544   
 545   also have "... = 3 * 5 ^ n + 2 * (5 ^ n + 2 ^ (n + 1))"
 546     by simp
 547   finally 
 548   show ?case
 549 ―‹ovde se može iskoristiti sledgehammer, ili možemo pogledati sam oblik koji 
 550 nam treba i napakovati sledeći korak:›
 551 ―‹ispis teorema koje se koriste: ›
 552   thm Suc
 553   thm dvd_triv_left
 554   thm dvd_mult
 555   thm dvd_add 
 556     using dvd_add[OF dvd_triv_left[of "3::nat" "5^n"] dvd_mult[OF Suc, of 2]]
 557     by simp
 558 qed
 559 
 560 text‹Objašnjenje korišćenih naredbi:
 561 
 562 @{text ‹dvd_triv_left[of...]›} - \verb!of! služi da instanciramo promenljive u 
 563 lemi, navodimo ih onim redom kojim se javljaju u njoj.
 564         
 565 @{text ‹dvd_add[OF...]›} nam omogućava da zadamo premise teoreme 
 566 @{text ‹dvd_add›}, premise su u stvari dve činjenice koje dobijamo uz pomoć 
 567 teorema @{text ‹dvd_triv_left›} i @{text ‹dvd_mult›}.
 568 
 569 @{text ‹dvd_mult[OF Suc, of 2]›} - \verb!OF! omogućava nam da zadamo premisu 
 570 našoj lemi, ovako istovremeno zadajemo i premisu i instanciramo jednu 
 571 promenljivu (sa \verb!of!).
 572 ›
 573 
 574 
 575 subsection‹Nejednakosti sa celim brojevima›
 576 
 577 text‹
 578 \begin{exmp}
 579 Dokazati da za svaki prirodan broj $n \geq 5$ važi $n^2 < 2^n$.
 580 \footnote{Zadatak 11 iz dodatnog materijala.}
 581 \end{exmp}
 582 
 583 U udžbeniku možemo da primetimo da se u dokazu ovog tvrđenja koristi pomoćno 
 584 tvrđenje koje prvo moramo dokazati. Prilikom formulisanja ovih tvrđenja moramo 
 585 naglasiti da je n prirodan broj, zato što to ne može da se zaključi iz konteksta 
 586 a ta informacija nam je neophodna da bismo mogli u dokazima da koristimo princip 
 587 matematičke indukcije. To radimo ključnom rečju @{text ‹fixes›}.
 588 
 589 Ključna reč @{text ‹fixes›} nam omogućava da navedemo tip promenljivih unapred, 
 590 pre navođenja tvrđenja teoreme (naspram korišćenja @{text ‹n::nat›} negde u 
 591 zapisu teoreme). Pored toga ovde nam znači da koristimo struktuirani zapis 
 592 tvrđenja i ključne reči @{text ‹assumes›} i @{text ‹shows›} koje nam dozvoljavaju 
 593 da imenujemo pretpostavke teoreme (ako imamo više različitih pretpostavki možemo 
 594 ih razdvojiti ključnom rečju @{text ‹and›}) i sa @{text ‹shows›} da izdvojimo 
 595 cilj teoreme.
 596 
 597 Sledeći detalj koji moramo naglasiti jeste da nam je u ovom dokazu neophodno da 
 598 uključimo pretpostavke pre pozivanja indukcije. To radimo korišćenjem ključnih 
 599 reči @{text ‹using assms›} i sada je uslov $n > 2$ uključen i u princip 
 600 indukcije. U ovakvim dokazima induktivni korak se sastoji iz dva dela, prvi deo 
 601 je standardni (da tvrđenje važi za n), a drugi deo se sastoji od tvrđenja da 
 602 sledbenik broja n zadovoljava pretpostavke koje se nalaze medju @{text ‹assms›}.
 603 
 604 Sada moramo obratiti pažnju na dva nivoa baze indukcije, prvi obrađuje šta se 
 605 dešava sa nulom (automatski je ispunjen uslov zato što nula ne zadovoljava 
 606 pretpostavke teoreme), a drugi nivo obrađuje šta se stvarno dešava sa minimalnim 
 607 brojem n za koji je ispunjen preduslov našeg tvrđenja. U ovom primeru to je broj 
 608 3. Pa sada treba na neki način posebno obraditi slučaj trojke, i slučaj 
 609 sledbenika.
 610 
 611 Ovakva induktivna hipoteza je uslovna, uslov koji mora da važi je da je 
 612 @{text ‹Sled n ≥ 3›}, odnosno @{text ‹n ≥ 2›}. Dakle razlikujemo slučaj kada je 
 613 @{text ‹Sled n = 3›} i slučaj kada je @{text ‹Sled n > 3›}. Slučaj kada je 
 614 @{text ‹Sled n = 3›}, je stvarna baza indukcije. I moramo da izvršimo analizu 
 615 slučajeva prema ova dva slučaja.
 616 
 617 \emph{Rezonovanje po slučajevima} se dobija metodom @{text ‹cases›} i u ovom 
 618 slučaju poziva se naredbom @{text ‹proof (cases "Suc n = 3")›}. Dobijamo dva 
 619 slučaja @{text ‹case True›} i @{text ‹case False›}. U ovom dokazu takođe moramo 
 620 naglasiti da je \emph{also have} rezonovanje pogodno za operator @{text ‹≤›} ali 
 621 nije pogodan za lanac koji u sebi ima @{text ‹≥›} (kao što je navedeno u dokazu u 
 622 udžbeniku), pa se vodi računa o smeru u kom izvodimo formule.›
 623 
 624 thm power2_eq_square
 625 
 626 lemma n2_2np1:
 627   fixes n::nat
 628   assumes "n > 2"
 629   shows "n^2 > 2*n + 1"
 630   using assms
 631 proof (induction n)
 632   case 0
 633   thus ?case ― ‹slučaj 0 se lako dokazuje zato što leva strana nije zadovoljena 
 634 pa je i desna automatski tačna, šta god pisalo na tom mestu›
 635   by simp
 636 next
 637   case (Suc n) 
 638   thm Suc
 639   show ?case
 640   proof (cases "n = 2")
 641     case True
 642     thus ?thesis
 643       by simp
 644   next
 645     case False
 646     (*from this and Suc
 647     have "n > 2" 
 648     by simp*)
 649     hence "n > 2"  
 650       using Suc(2)
 651       by simp
 652 
 653     have "2 * (Suc n) + 1 < 2 * (Suc n) + 2 * n"
 654       using `n > 2`
 655       by simp
 656     also have "... = 2 * n + 1 + 2 * n + 1"
 657       by simp
 658     also have "... < n^2 + 2 * n + 1"
 659       using Suc(1) `n > 2`
 660       by simp
 661     also have "... = (Suc n)^2"
 662       by (simp add: power2_eq_square)
 663     finally
 664     show ?thesis
 665       .
 666   qed
 667 qed
 668 
 669 text‹Sada prelazimio na dokaz glavnog tvrđenja koji je slične strukture. Jedina 
 670 nova stvar u ovom dokazu je instanciranje promenljive iz leme uz pomoć naredbe 
 671 @{text ‹[of n]›}. U uglastim zagradama se navodi ime promenljive.›
 672 
 673 lemma 
 674   assumes "n ≥ 5"
 675   shows "2^n > n^2"
 676   using assms
 677 proof (induction n)
 678   case 0
 679   thus ?case
 680     by simp
 681 next
 682   case (Suc n)
 683   show ?case
 684   proof (cases "n = 4") ― ‹suštinska baza indukcije›
 685     case True
 686     thus ?thesis
 687       by simp
 688   next
 689     case False
 690     hence "n ≥ 5"
 691       using Suc(2)
 692       by simp
 693 
 694     have "(Suc n)^2 = n^2 + 2*n + 1"
 695       by (simp add: power2_eq_square algebra_simps)
 696     also have "... < n^2 + n^2"
 697       using Suc(2) n2_2np1[of n] ― ‹instanciranje promenljive›
 698       by simp 
 699     also have "... = 2 * n^2"
 700       by simp
 701     also have "... < 2 * 2^n"
 702       using Suc(1) `n ≥ 5`
 703       by simp
 704     also have "... = 2^(n+1)"
 705       by simp
 706     finally
 707     show ?thesis
 708       by simp
 709   qed
 710 qed
 711 
 712 subsection ‹Pravilo indukcije koje počinje pozitivnim brojem›
 713 
 714 text ‹Pravilo indukcije koje zadovoljava uslov $n \geq m$ zove se @{text 
 715 ‹nat_induct_at_least:›} @{thm[mode=Proof] nat_induct_at_least [no_vars]} i ovako 
 716 se zapisuje u Isabelle-u. Zahvaljujući ovom pravilu možemo zapisati prethodne 
 717 dokaze tako da više liče na dokaze iz udžbenika.›
 718 
 719 thm nat_induct_at_least
 720 
 721 (* Zadatak 11 - pomocno tvrdjenje *)
 722 
 723 lemma n2_2np1_at_least:
 724   fixes n::nat
 725   assumes "n ≥ 3"
 726   shows "n^2 > 2*n + 1"
 727   using assms
 728 proof (induction n rule: nat_induct_at_least)
 729 ―‹bazni slučaj›
 730   case base
 731   thus ?case
 732     by simp
 733 next
 734   case (Suc n)
 735   have "2 * (Suc n) + 1 < 2 * (Suc n) + 2 * n"
 736     using `n ≥ 3`
 737     by simp
 738   also have "... = 2 * n + 1 + 2 * n + 1"
 739     by simp
 740   also have "... < n^2 + 2 * n + 1"
 741     using Suc
 742     by simp
 743   also have "... = (Suc n)^2"
 744     by (simp add: power2_eq_square)
 745   finally
 746   show ?case
 747   .
 748 qed
 749 
 750 subsection ‹Princip jake indukcije›
 751 
 752 text‹Postoje dva metoda: \verb!less_induct:! @{thm less_induct [no_vars]} i 
 753 \verb!nat_less_induct:! @{thm nat_less_induct}. 
 754 Prvi je opštiji (i radi za bilo koje potpuno uređenje), ali drugi je specifičniji 
 755 i zadovoljava naše potrebe za sada.›
 756 
 757 thm less_induct (* (⋀x. (⋀y. y < x ⟹ ?P y) ⟹ ?P x) ⟹ ?P ?a *)
 758 thm nat_less_induct (* (⋀n. ∀m<n. ?P m ⟹ ?P n) ⟹ ?P ?n *)
 759 
 760 text‹
 761 \begin{exmp}
 762 Niz fibonačijevih brojeva zadat je jednačinama: $f_1 = 1$, $f_2 = 1$, 
 763 $f_n = f_{n-1} + f_{n-2}$, za $n>2$. 
 764 
 765 Dokazati da važi nejednakost:
 766 $$f_n \leq \varphi ^ {n-1}$$
 767 za svaki prirodan broj n, gde je $\varphi = \frac{1 + \sqrt{5}}{2}$.
 768 \footnote{Zadatak 6 iz dodatnog materijala.}
 769 \end{exmp}›
 770 
 771 definition gm where
 772  "gm = (1 + sqrt 5) / 2"
 773 
 774 fun fib :: "nat ⇒ nat" where
 775 "fib 0 = 0" |
 776 "fib (Suc 0) = 1" |
 777 "fib (Suc (Suc n)) = fib (Suc n) + fib n"
 778 
 779 lemma fibonaci:
 780 shows "fib (n + 1) ≤ gm ^ n"
 781 proof (induction n rule: nat_less_induct)
 782 case (1 n)
 783 thm 1
 784   show ?case
 785   proof (cases "n = 0")
 786     case True
 787     thus ?thesis
 788       by simp
 789   next
 790     case False
 791     show ?thesis
 792     proof (cases "n = 1")
 793       case True
 794       have "fib 2 = 1"
 795         by (simp add: numeral_2_eq_2)
 796         thus ?thesis
 797         using `n = 1`
 798         by (simp add: gm_def)
 799     next
 800       case False
 801       show ?thesis
 802       proof-
 803         obtain m where "m = n - 2"
 804           by auto
 805           have "n > 1" using `n ≠ 0` `n ≠ 1`
 806           by simp
 807         have "fib (m + 3) = fib (m + 2) + fib (m + 1)"
 808           by (simp add: numeral_3_eq_3)             
 809         also have "... ≤ gm ^ (m + 1) + gm ^ m"
 810 ―‹modifikator @{text ‹[rule_format]›} od $\forall x. P x$ pravi "P ?x" 
 811 na koji onda možemo dalje da primenimo of da bi ubacili vrednost za x. 
 812 Obično se koristi kada imamo premisu sa univerzalnim kvantifikatorom 
 813 koju hoćemo da instanciramo prilikom primene.›
 814           using 1[rule_format, of "m+1"] 1[rule_format, of m] `m = n - 2` `n > 1`
 815           by force
 816         also have "... = gm ^ m * (gm + 1)"       
 817           by (simp add: algebra_simps)
 818         also have "... = gm ^ m * (gm ^ 2)"
 819           by (simp add: power2_eq_square algebra_simps gm_def) 
 820         also have "... = gm ^ (m + 2)"
 821           by (simp add: power_add power2_eq_square)
 822         finally
 823         show ?thesis
 824           using `m = n - 2` `n > 1`
 825           by (simp add: numeral_2_eq_2 Suc_diff_Suc)
 826       qed
 827     qed
 828   qed
 829 qed
 830 
 831 
 832 
 833 section ‹ Primeri sa realnim brojevima ›
 834 
 835 text‹Realni brojevi nisu uključeni u teoriju @{text ‹Main›}. Da bi mogli da 
 836 radimo sa realnim brojevima potrebno je da uključimo @{text ‹HOL.Real›} a ako 
 837 želimo da radimo i sa kompleksnim brojevima potrebno je da uključimo @{text 
 838 ‹MainComplex_Main›}
 839 
 840 \begin{exmp}
 841 Dokazati da važi Bernulijeva nejednakost $(1 + x)^n \geq 1 + nx$, za $x > -1$.
 842 \footnote{Zadatak 4 iz dodatnog materijala.}
 843 \end{exmp}
 844 
 845 U narednom dokazu, nećemo koristiti @{text ‹using assms›} da bi bili 
 846 jednostavniji dokazi, pa ćemo se pozivati na pretpostavku samo na onim mestima u 
 847 dokazu gde ćemo je eksplicitno koristiti.
 848 
 849 ›
 850 
 851 lemma bernulijeva_nejednakost:
 852   fixes x::real and n::nat
 853   assumes "x > -1"
 854   shows "(1 + x)^n ≥ 1 + n * x"
 855 proof (induction n)
 856   case 0
 857   show ?case
 858     by simp
 859 next
 860   case (Suc n)
 861   show ?case
 862   proof-
 863     have "1 + (n + 1) * x ≤ 1 + (n + 1) * x + n * x^2"
 864       by simp
 865     also have "... = (1 + x) * (1 + n * x)"
 866       by (simp add: algebra_simps power2_eq_square)
 867     also have "... ≤ (1 + x) * (1 + x) ^ n"
 868       using Suc `x > -1` ― ‹ovde se pozivamo na pretpostavku›
 869       by simp
 870     also have "... = (1 + x) ^ (Suc n)"
 871       by simp
 872     finally
 873     show ?thesis
 874       by simp
 875   qed
 876 qed                                            
 877 
 878 text‹ Funkcije za kastovanje izmedju razlicitih tipova se mogu naci narednim 
 879 naredbama. Funkcije se zovu @{text "int"}, @{text ‹real›}, 
 880 @{text ‹real_of_nat›},...›
 881 
 882 find_consts "nat ⇒ int"
 883 find_consts "nat ⇒ real"
 884 find_consts "real ⇒ complex"                                 
 885 
 886 text‹Primer funkcije @{text ‹int›}. Tip i funkcija mogu imati isto ime. Ovde int 
 887 predstavlja funkciju koja slika tip @{typ nat} u tip @{typ int}. ›
 888 
 889 term "3::nat"
 890 term "int (3::nat)"
 891 term "int 3"
 892 
 893 text‹Poziv \verb!@!\verb!{term t}! štampa dobro definisan term t. Poziv funkcije 
 894 \verb!@!\verb!{value t}! računa vrednost terma t i štampa rezultat.›
 895 
 896 value "int (3::nat)"
 897 term "3::nat"
 898 value "3::nat"
 899 
 900 thm Re_complex_of_real
 901 thm Im_complex_of_real
 902 thm complex_of_real_def
 903 
 904 text‹
 905 \begin{exmp}
 906 Dokazati Moavrovu formulu: neka je dat kompleksan broj u trigonometrijskom obliku
 907 $z = r (\cos \theta + i* \sin \theta)$. Tada se $n$-ti stepen broja $z$ računa po 
 908 formuli:
 909 
 910 $$z^n = r^n (\cos n \theta + i \sin n \theta)$$
 911 \footnote{Zadatak 12 iz dodatnog materijala. }
 912 \end{exmp}›
 913 
 914 lemma moavrova_formula:
 915   fixes r φ :: real and n :: nat
 916   shows "(r * (cos φ + \ * sin φ))^n = r^n * (cos (n * φ) + \ * sin(n * φ))"
 917 proof (induction n)
 918   case 0
 919   show ?case
 920     by simp
 921 next
 922   case (Suc n)
 923   show ?case
 924   proof-
 925     have "(r * (cos φ + \ * sin φ)) ^ Suc n = 
 926           (r * (cos φ + \ * sin φ)) ^ n * r * (cos φ + \ * sin φ)"
 927       by simp
 928     also have "... = r^n * (cos (n * φ) + \ * sin (n * φ)) * r * (cos φ + \ * sin φ)"
 929       using Suc
 930       by simp
 931     also have "... = r^(Suc n) * ((cos (n * φ) * cos φ - sin (n * φ) * sin φ) + \ * (sin(n * φ) * cos φ + cos (n * φ) * sin φ))"
 932       by (simp add: algebra_simps)
 933       also have "... = r^(Suc n) * (cos (n * φ + φ) + \ * sin (n * φ + φ))"
 934       thm cos_add
 935       thm sin_add
 936     using cos_add[of "n * φ" φ, symmetric] sin_add[of "n * φ" φ, symmetric]
 937     by simp
 938     finally
 939     show ?thesis
 940       by (simp add: algebra_simps)
 941   qed
 942 qed
 943 
 944 end