1 theory Cas12_vezbe_resenja
   2 imports Main "~/Downloads/Isabelle2019/src/HOL/Library/Code_Target_Nat"
   3 "~/Downloads/Isabelle2019/src/HOL/Library/Multiset"
   4 
   5 
   6 begin
   7 
   8 section Opšta rekurzija i algoritmi sortiranja
   9 
  10 textDo sada smo samo videli funkcije definisane primitivnom rekurzijom u kojima 
  11 rekurzija direktno prati strukturu tipa podataka po kome se rekurzija definiše:
  12 
  13  Kod prirodnih brojeva razlikuju se slučaj 0 i sledbenika (Suc n)
  14  Kod lista se razlikuje slučaj prazne liste ([]) i nadovezanog elementa na 
  15 početak liste @{text (x # xs)}
  16  Kod drveta (koje smo sami definisali) razlikuje se slučaj praznog drveta (Null) 
  17 i nepraznog čvora koji se sastoji od levog postabla, korena i desnog podstabla 
  18 (Cvor l k d)
  19 
  20 
  21 text
  22 \begin{exmp}
  23 Definisati funkciju stepenovanja.
  24 \end{exmp}
  25 
  26 Prvo ćemo napisati verziju uz pomoć primitivne rekurzije i njeno izvršavanje je 
  27 relativno neefikasno i sporo se izvršava. Razlog za to je pre svega u internoj 
  28 reprezentaciji prirodnih brojeva jer se oni predstavljaju kao 0, Suc 0, 
  29 Suc (Suc 0),... pa vidimo da nam već sama ta interna reprezentacija ne odgovara u 
  30 situaciji kada dobijamo velike vrednosti brojeva jer će funkcija Suc biti pozvana 
  31 veliki broj puta. Rešenje je da koristimo drugačiju reprezentaciju prirodnih 
  32 brojeva i koristimo mašinske tipove podataka. Uključujemo teoriju 
  33 @{text "HOL-Library.Code_Target_Nat"} i koristimo reprezentaciju prirodnih 
  34 brojeva koja se koristi i u ciljnom jeziku. Isabelle je programiran u ML-u i 
  35 korišćenjem ove reprezentacije znatno brže se izvršava ova ista funkcija. U 
  36 isabelle-u nemamo prekoračenje tipa, pa o tome ne moramo da vodimo računa.
  37 
  38 Napomena: dokazi nekih lema će se malo razlikovati u odnosu na dokaze sa 
  39 profesorovog sajta, na par mesta kod profesora leme su dodate u simplifikator a u 
  40 ovom dokumentu smo to najčešće izbegavali. Takođe par definicija imaju promenjene 
  41 nazive. Sve ovo nisu suštinske promene.
  42 
  43 primrec pow' :: "nat ⇒ nat ⇒ nat" where
  44 "pow' x 0 = 1" | 
  45 "pow' x (Suc n) = x * pow' x n"
  46 
  47 value "pow' 2 15" 
  48 
  49 textVežbe radi, dokazaćemo da je ova funkcija dobro definisana, odnosno da 
  50 stvarno računa stepen broja. Dokaz pokušavamo standardno indukcijom i automatskim 
  51 dokazivačem što prolazi.
  52 
  53 lemma pow'_stepen:
  54   "pow' x n = x ^ n"
  55   by (induction n) auto
  56 
  57 text U realnom programiranju javljaju se i mnogo bogatiji oblici rekurzije.
  58 Ilustujmo ih kroz nekoliko primera. Za početak ćemo napisati efikasniju verziju 
  59 iste funkcije.
  60 
  61 subsection Efikasno stepenovanje
  62 
  63 text Razmotrimo narednu definiciju efikasnog stepenovanja. U njoj koristimo 
  64 definiciju opšte rekurzije i koristimo ključnu reč @{text fun}. Koristićemo 
  65 matematičko tvrđenje po kome, za paran broj n važi $x^n = (x^2)^{n div 2}$. 
  66 Otuda, u rekurzivnom pozivu \verb!pow (x*x) (n div 2)! svođenje nije sa 
  67 sledbenika na prethodnika pa stoga nije mogla biti upotrebljena primitivna 
  68 rekurzija. Opšta (generalna) rekurzija se u sistemu Isabelle uvodi pomoću 
  69 ključnih reči @{text fun} i @{text function} (razlika će naknadno biti 
  70 objašnjena).
  71 
  72 fun pow'' :: "nat ⇒ nat ⇒ nat" where 
  73 "pow'' x 0 = 1" |
  74 "pow'' x n = (if n mod 2 = 0 then pow'' (x*x) (n div 2) else x * pow'' x (n-1))"
  75 
  76 textOvaj oblik podseća izgledom na definiciju primitivne rekurzije, ali nije 
  77 potrebno koristiti tako nešto već možemo preći skroz na if-then-else konstrukciju 
  78 i dobiti narednu funkciju.
  79 
  80 fun pow :: "nat ⇒ nat ⇒ nat" where
  81   "pow x n = 
  82      (if n = 0 then 1
  83       else if n mod 2 = 0 then
  84          pow (x * x) (n div 2) 
  85       else
  86          x * pow x (n - 1))"
  87 
  88 value "pow 2 10"
  89 
  90 thm pow.induct
  91 
  92 textNakon definisanja funkcije u isabelle-u, u pozadini se automatski dokazuje 
  93 teorema indukcije koja odgovara toj funkciji i koja se može koristiti u dokazu 
  94 korektnosti te funkcije. Teorema se dobija kada se na ime funkcije nadoveže 
  95 \verb!.induct! i u ovom konretnom slučaju ona se zove @{text pow.induct}, i 
  96 izgleda ovako: @{thm[display] pow.induct [no_vars]}
  97 
  98 Ova teorema suštinski tvrdi da ako pretpostavimo da svaki rekurzivni poziv (imamo 
  99 ih dva) računa stepen korektno, da će onda i tekući rekurzivni poziv korektno 
 100 izračunati stepen funkcije. Ova teorema se mora eksplicitno navesti u dokazu 
 101 teoreme ako želimo da je koristimo, kao što ćemo videti malo kasnije.
 102 
 103 Kada se radi sa opšte rekurzivnim funkcijama, mora se voditi računa o još jednom 
 104 pravilu koje se automatski generiše i koje se automatski prosleđuje 
 105 simplifikatoru. Ime tog pravila se dobija kada se na ime rekurzivne funkcije 
 106 dopiše \verb!.simps! i glasi @{text thm pow.simps}. Može se desiti da 
 107 postajanje ovakvih pravila dovede simplifikator u beskonačnu petlju. Ako se tako 
 108 nešto desi potrebno je izbaciti to pravilo iz procesa simplifikacije naredbom 
 109 \verb!declare pow.simps [simp del]!. Prilikom ovakvog menjanja znanja koje 
 110 poseduje simplifikator treba voditi računa da ovo može uticati na neke korake 
 111 koji su ranije bili trivijalni zato što je simplifikator posedovao više znanja.
 112 Ovo pravilo, u ovom slučaju, izgleda ovako: @{thm[display] pow.simps [no_vars]}
 113 
 114 thm pow.simps
 115 declare pow.simps [simp del]
 116 
 117 textDokazi svojstava primitivno-rekurzivnih podataka se dokazuju strukturnom 
 118 indukcijom po odgovarajućem tipu podataka. Na sličan način se dokazi 
 119 generalno-rekurzivnih funkcija izvode specijalnim oblikom indukcije koji je 
 120 prilagođen toj rekurzivnoj funkciji. Korektnost tako definisanog tvrđenja se 
 121 svodi na to da se iz pretpostavki da svaki rekurzivni poziv radi korektno dokaže 
 122 da glavni poziv radi korektno. Ilustrujmo ovo na primeru dokazivanja korektnosti 
 123 efikasne funkcije stepenovanja.
 124 
 125 text Napomena: prvo se dokazuje naredno tvrđenje, pa ako sami pokušavate da 
 126 dokažete, krenite od naredne leme.
 127 
 128 U ovom pasusu je izdvojen dokaz matematičkog tvrđenja koje stoji iza definicije 
 129 koju smo već dali. Ovo je centralni argument korektnosti definicije i zasniva se 
 130 na narednoj lemi koju dokazujemo zasebno. 
 131 
 132 Napomenimo da je ovde neophodno navesti tip za promenljive koje se javljaju u 
 133 tvrđenju. Ovo možemo zaključiti korišćenjem naredbe \verb!using [[show_types]]! 
 134 koju pokrećemo pre dokaza teoreme koja bi ispisala (pre nego što dodamo red koji 
 135 počinje sa ključnom rečju fixes) da ne može da odredi tip promenljive x. Sada 
 136 možemo pozvati sledgehammer i dobiti izdvojen dokaz ovog matematičkog tvrđenja.
 137 
 138 lemma pow_div2:
 139   fixes x n :: nat 
 140   assumes "n mod 2 = 0"
 141   shows "(x * x) ^ (n div 2) = x ^ n"
 142  @{textusing [[show_types]]}
 143   using assms
 144   by (metis dvd_div_mult_self minus_mod_eq_div_mult minus_mod_eq_mult_div mod_0_imp_dvd power_mult_distrib semiring_normalization_rules(36))
 145 
 146 text Dokazati da naša generalno-rekurzivna funkcija pow zaista izračunava stepen 
 147 prirodnog broja. Ako bismo sada primenili običnu indukciju dobili bismo kao 
 148 rezultat dva slučaja koja standardno odgovaraju nuli, i sledbeniku prirodnog 
 149 broja. Ali ovakav oblik indukcije ne odgovara definiciji tipa i želimo da 
 150 primenimo drugačiji tip indukcije što nam isabelle i omogućava korišćenjem samog 
 151 tipa. Koristimo naredbu \verb!proof (induction x n rule: pow.induct)!.
 152 
 153 Pošto funkcija ima dva argumenta, moramo sve argumente te funkcije navesti (onim 
 154 redosledom kojim se javljaju u definiciji), nakon čega sledi ime teoreme 
 155 indukcije koja odgovara ovoj funkciji. Pošto je cela struktura ove funkcije malo 
 156 komplikovanija, ovaj dokaz ne prolazi automatski pa ćemo odmah raspisati dokaz u 
 157 Isar-u.
 158 
 159 Prvi deo dokaza prolazi relativno jednostavno dok ne dođemo do slučaja kada je n 
 160 paran broj (pogledajte dokaz do tog koraka). Pogledajmo šta se dešava kada sada 
 161 primenimo simplifikator (ali postupamo kao u automatskom dokazivanju i koristimo 
 162 ključnu reč @{text apply} umesto @{text by}). Izdvojićemo nekoliko zaključaka 
 163 do kojih možemo doći (nastavite kroz dokaz korak po korak i najbolje da pokušate 
 164 sami da ga napišete prateći uputstva iz teksta):
 165 
 166 (1) Primećujemo da simplifikator ne vidi činjenicu da n nije jednako 0 pa tu 
 167 činjenicu eksplicitno dodajemo naredbom @{text using}.
 168 
 169 (2) Na ovom mestu možemo da primetimo da (pre brisanja pow.simps iz 
 170 simplifikatora), možemo da dobijemo beskonačnu petlju rekurzivnih poziva. Nakon 
 171 brisanja pow.simps simplifikator ne može ništa da uradi pa inicijalizujemo 
 172 tvrđenje za konkretne promenljive koje se trenutno javljaju u dokazu.
 173 
 174 (3) Nakon toga primećujemo da smo sveli slučaj na rekurzivni poziv i pozivamo se 
 175 na induktivnu pretpostavku i to na njen prvi deo. Ovde se induktivna hipoteza 
 176 zove 1 i njen prvi deo se dobija sa 1(1).
 177 
 178 (4) Sada smo došli do čisto matematičkog tvrđenja: kada $(x^2)^{n mod 2} = x^n$, 
 179 pa možemo ili upotrebiti sledgehammer 
 180 
 181 (5) ili formulisati našu novu lemu u kojoj ćemo dokaz tog matematičkog tvrđenja 
 182 izvaditi iz dokaza ove glavne leme - pogledajte dokaz prethodne teoreme.
 183 
 184 lemma pow_stepen:
 185   "pow x n = x ^ n"
 186 proof (induction x n rule: pow.induct) 
 187  ovo je način da primenimo rekurzivno pravilo specifično za funkciju pow
 188   case (1 x n)  ovako je označena induktivna hipoteza
 189   show ?case 
 190  glavni deo dokaza analizira jedan po jedan slučaj koji se javlja u definiciji 
 191 funkcije i granamo isto kao što smo granali u definiciji
 192   proof (cases "n = 0")
 193     case True
 194  slučaj kada je n = 0 je trivijalan dok je pow.simps tvrđenje uključeno u 
 195 simplifikator, kada ga izbacimo ovaj korak više ne prolazi samo sa simp pa 
 196 tvrđenje koje se koristi moramo eksplicitno dodati
 197     thus ?thesis
 198       by (simp add: pow.simps)
 199   next
 200     case False
 201  ako n nije 0 onda opet granamo prema tome da li je n parno ili neparno
 202     show ?thesis
 203     proof (cases "n mod 2 = 0")
 204       case True
 205       then show ?thesis
 206  pre brisanja:
 207  ako bismo na ovom mestu pokušali samo sa simp (pre brisanja pow.simps), videli 
 208 bismo da je simplifikator upao u beskonačnu petlju rekurzivnih poziva
 209  nakon brisanja:
 210  nakon što obrišemo pow.simps simplifikator ne može ništa da uradi pa nam treba 
 211 rešenje između ova dva ekstrema, i to rešenje dobijamo kada inicijalizujemo 
 212 tvrđenje za konkretne promenljive koje se trenutno javljaju u dokazu.
 213         using `n ≠ 0`
 214         using pow.simps[of x n]
 215         using 1(1)
 216  apply simp
 217  sledgehammer
 218  @{textby (metis div_mult_self1_is_m mod_eq_0D power2_eq_square power_mult zero_less_numeral)}
 219         by (simp add: pow_div2)
 220     next
 221       case False
 222  ako je n neparno pokusavamo slično, sada ćemo koristiti drugi deo induktivne 
 223 hipoteze i opet pokušavamo sa sledgehammerom koji nalazi teoremu 
 224 @{text power_eq_if} koja je već dokazana u isabelle-u pa nema potrebe da je 
 225 dodajemo i sami dokazujemo
 226       then show ?thesis
 227         using `n ≠ 0`
 228         using pow.simps[of x n]
 229         using 1(2)
 230          sledgehammer
 231         by (simp add: power_eq_if)
 232     qed
 233   qed
 234 qed
 235 
 236 textU ovakvim dokazima može se desiti da automatski dokaz ne možemo da 
 237 formulišemo, odnosno ako pokušamo da kreiramo kraći automatski dokaz sa 
 238 informacijama do kojih smo došli dobili bismo dokaz narednog oblika koji iz nekog 
 239 razloga ulazi u beskonačnu petlju. Na ovaj način možemo da vidimo neophodnost 
 240 interaktivnih dokaza u situacijama kada automatski dokazivači ne znaju da se 
 241 snađu sa informacijama koje su im neophodne za kreiranje dokaza.
 242 
 243 \begin{footnotesize}
 244 \begin{verbatim}
 245 lemma pow_stepen_auto:
 246   "pow x n = x ^ n"
 247   using pow.simps[of x n]
 248   apply (induction x n rule: pow.induct, auto simp: pow_div2 power_eq_if)
 249 \end{verbatim}
 250 \end{footnotesize}
 251 
 252 
 253 subsection NZD
 254 
 255 text U ovom poglavlju ćemo videti kako možemo da isprogramiramo Euklidov 
 256 algoritam za nalaženje najvećeg zajedničkog delioca dva broja.
 257 
 258 \begin{exmp}
 259 Definisati osnovnu varijantu Euklidovog algoritma preko oduzimanja.
 260 \end{exmp}
 261 
 262 Ponovo koristimo opštu rekurziju. Kada koristimo ključnu reč @{text fun} sistem 
 263 pokušava automatski da dokaže zaustavljanje za sve moguće ulaze. Kod primitivne 
 264 rekurzije ovako nešto nije neophodno (jedini rekurzivni poziv u tom slučaju je 
 265 bilo svođenje na prethodnika, što znači da smo automatski imali smanjivanje 
 266 argumenta funkcije dok ne stignemo do nule što je izlaz iz rekurzije). Kada 
 267 radimo sa opštom rekurzijom moramo biti veoma obazrivi zato što je moguće 
 268 napraviti beskonačne cikluse. Neophodno je da se automatski može dokazati 
 269 zaustavljanje ove funkcije.
 270 
 271 Pogledajmo prvo kako izgleda nepotpuna definicija ove funkcije (dodaćemo 
 272 apostrofe nakon naziva funkcije da bismo je razlikovali od konačne funkcije). Ako 
 273 koristimo ključnu reč @{text fun} isabelle će ispisati grešku "Could not find 
 274 lexicographic termination order" što znači da nije uspeo da dokaže zaustavljanje. 
 275 Sada možemo pokušati sami da ga ubedimo da se naša funkcija zaustavlja, ali za to 
 276 je potrebno da koristimo ključnu reč @{text function} i naredbu 
 277 \verb!by pat_completeness auto!. Nakon toga potrebno je identifikovati jednu 
 278 vrednost koja će se smanjivati kroz rekurzivne pozive ove naše definicije. Ako 
 279 pogledamo definiciju, vrednost koja se smanjuje u svakom pozivu neće biti posebno 
 280 ni prvi ni drugi argument (zato što se oni naizmenično smanjuju), ali njihov zbir 
 281 se konstantno smanjuje (bez obzira na to koji argument se smanjio) i njega ćemo 
 282 koristiti. 
 283 
 284 Nakon toga ključnom rečju @{text termination} ulazimo u proces dokazivanja da 
 285 se ova funkcija zaustavlja (možemo da primetimo da isabelle formira cilj koji 
 286 treba da se dokaže) i koristimo isti princip koji smo koristili ranije i 
 287 pokušavamo uz pomoć automatskih dokazivača. Korišćenjem naredbe 
 288 \verb!apply (relation "measure (λ (a, b). a + b)")! koristimo automatski 
 289 dokazivač \emph{auto}, metod \emph{relation}, ključnu reč \emph{measure} i nakon 
 290 nje anonimnu funkciju koja od para argumenata dobijenih ovom funkcijom kreira 
 291 vrednost za koju tvrdimo da ona konstantno opada.
 292 
 293 Nakon toga pokušavamo sa automatskim dokazivačem, samo auto i primećujemo da 
 294 isabelle traži da pokažemo da su i a i b pozitivni. Ako pogledamo samu definiciju 
 295 funkcije vidimo da nula kao argument može da dovede do beskonačne petlje (po 
 296 definiciji nzd''(5,0) = nzd''(5,0) zato što je 5 veće od 0). To znači da trenutna 
 297 defincija nije dobra i da ne pokriva adekvatno slučaj kada je b = 0. Slično za 
 298 nzd''(0,5) = nzd''(0,5) daje beskonačnu petlju. 
 299 
 300 Ovo je primer kako automatski dokazivač može da nam pomogne i pronađe greške koje 
 301 postoje u našem kodu. 
 302 
 303 Napomena: naredni kod odkomentarišite da biste ga istestirali.
 304 
 305 \begin{footnotesize}
 306 \begin{verbatim}
 307 (* fun nzd'' :: "nat ⇒ nat ⇒ nat" where *)
 308 function nzd'' :: "nat ⇒ nat ⇒ nat" where
 309   "nzd'' a b = 
 310      (if a > b then 
 311         nzd'' (a - b) b
 312       else if b > a then 
 313         nzd'' a (b - a)
 314       else 
 315         a)"
 316   by pat_completeness auto
 317 termination  
 318   apply (relation "measure (λ (a, b). a + b)")
 319   apply auto
 320 
 321 (* value "nzd'' 8 4" *)
 322 \end{verbatim}
 323 \end{footnotesize}
 324 
 325 
 326 textPa sada proširujemo definiciju funkcije za slučajeve kada je jedan od 
 327 argumenata jednak nuli i sada auto prolazi.
 328 
 329 function nzd'' :: "nat ⇒ nat ⇒ nat" where
 330   "nzd'' a b = 
 331      (if a = 0 then b
 332       else if b = 0 then a
 333       else if a > b then nzd'' (a - b) b
 334       else if b > a then nzd'' a (b - a)
 335       else a)"
 336   by pat_completeness auto
 337 termination  
 338   apply (relation "measure (λ (a, b). a + b)")
 339   apply auto
 340   done
 341 
 342 text ili kraće \verb!by (relation "measure (λ (a, b). a + b)", auto)!
 343 
 344 Sada možemo pokušati da vratimo ključnu reč @{text fun} i vidimo da isabelle 
 345 sada uspeva sam da potvrdi da je ova definicija dobra (što nam potvrđuje ispisana 
 346 poruka: "Found termination order") tako što je pronašao neku relaciju poretka nad 
 347 ovim argumentima koja se tokom rekurzivnih poziva smanjuje i koja je dobro 
 348 zasnovana odnosno nema beskonačnih lanaca (u ovom slučaju, leksikografsko 
 349 poređenje uređenih parova).
 350 
 351 fun nzd' :: "nat ⇒ nat ⇒ nat" where
 352   "nzd' a b = 
 353      (if a = 0 then b
 354       else if b = 0 then a
 355       else if a > b then nzd' (a - b) b
 356       else if b > a then nzd' a (b - a)
 357       else a)"
 358 
 359 textOva definicija bi se mogla zapisati i kraće bez poslednje else grane, tako 
 360 što bi se ona uvukla u slučaj @{text a  b}.
 361 
 362 text 
 363 \begin{exmp}
 364 Dokažati da je naša funkcija dobro definisana, odnosno da izračunava nzd tako što 
 365 ćemo pokazati da je ekvivalentna sa bibliotečkom funkcijom gcd.
 366 \end{exmp}
 367 
 368 Kao i u prethodnom primeru koristi se specifično pravilo indukcije koje je 
 369 dodeljeno ovoj funkciji i navode se dva argumenta. Ovde možemo prikazati kako 
 370 izgled same definicije funkcije utiče na izgled dokaza koji se dobija u 
 371 isabelle-u. Ako bismo koristili gore navedeni oblik koji koristi samo 
 372 if-then-else konstrukciju dobili bismo dokaz koji ima samo jednu granu i onda je 
 373 na nama da u okviru te grane raspišemo sve moguće slučajeve koji su navedeni u 
 374 okviru if-then-else naredbi (kao što smo videli u prethodnom primeru) i dobijamo 
 375 naredni dokaz. Prvo izbacujemo rekurzivnu funkciju iz simplifikatora i dodaćemo 
 376 je u slučajevima kada nam je potrebna:
 377 
 378 declare nzd'.simps [simp del]
 379 
 380 lemma nzd'_gcd:
 381   shows "nzd' a b = gcd a b"
 382 proof (induction a b rule: nzd'.induct)
 383   case (1 a b)
 384   show ?case
 385   proof (cases "b = 0")
 386     case True
 387     thus ?thesis
 388       by (simp add: nzd'.simps)
 389   next
 390     case False
 391     show ?thesis
 392     proof (cases "a = 0")
 393       case True
 394       thus ?thesis
 395         using `b ≠ 0`
 396         by (simp add: nzd'.simps)
 397     next
 398       case False
 399       show ?thesis
 400       proof (cases "a > b")
 401         case True
 402         thus ?thesis
 403           using `a ≠ 0` `b ≠ 0` 1(1)
 404           by (simp add: nzd'.simps[of a b] gcd_diff1_nat)
 405       next
 406         case False
 407         show ?thesis
 408         proof (cases "a < b")
 409           case True
 410           thus ?thesis
 411             using `a ≠ 0` `b ≠ 0` `¬ (a > b)` 1(2)
 412             using nzd'.simps[of a b]
 413             by (metis gcd.commute gcd_diff1_nat less_imp_le)
 414         next
 415           case False
 416           thus ?thesis
 417             using `a ≠ 0` `b ≠ 0` `¬ (a > b)`
 418             using nzd'.simps[of a b]
 419             by simp
 420         qed
 421       qed
 422     qed
 423   qed
 424 qed
 425 
 426 
 427 textAlternativa je da promenimo izgled same definicije i da je zapišemo na 
 428 sledeći način:
 429 
 430 fun nzd :: "nat ⇒ nat ⇒ nat" where
 431 "nzd 0 b = b" |
 432 "nzd a 0 = a" |
 433 "nzd a b = (if a ≥ b then nzd (a - b) b
 434             else nzd a (b - a))"
 435 
 436 
 437 textsada dobijamo tri slučaja u automatski generisanom dokazu koji odgovaraju 
 438 ovim trima slučajevima iz definicije. Za razliku od prethodnog oblika definicije 
 439 i dokaza koji smo tada kreirali (kada smo morali da eksplicitno navodimo da 
 440 prethodni slučajevi grananja nisu ispunjeni, konkretno da a i b nisu jednaki 
 441 nuli), ovako definisani šabloni ne zahtevaju to. Ovako kreirana funkcija 
 442 automatski vuče kroz dokaz informaciju da svi prethodni slučajevi nisu ispunjeni.
 443 
 444 Da bi se izbeglo "zaglavljivanje" simplifikatora, ponovo rekurzivnu definiciju 
 445 izbacujemo iz procesa automatske simplifikacije:
 446 
 447 declare nzd.simps [simp del]
 448 
 449 text Slično kao i ranije glavna lema @{text nzd_gcd} će se svesti na 
 450 matematičku formulu koju treba dokazati i za to možemo upotrebiti sledgehammer.
 451 
 452 lemma nzd_gcd:
 453   shows "nzd a b = gcd a b"
 454 proof (induction a b rule: nzd.induct)
 455   case (1 b)
 456   then show ?case 
 457     by (simp add: nzd.simps)
 458 next
 459   case (2 v)
 460   then show ?case 
 461     by (simp add: nzd.simps)
 462 next
 463   case (3 a' b')  promenićemo imena na a' i b'
 464  ovo je mesto gde ćemo se pozivati na rekurzivne pozive i prvo ćemo pokušati 
 465 automatski i dobićemo matematičku formulu koju treba dokazati i za to možemo 
 466 upotrebiti sledgehammer ili izdvojiti dve matematičke formule kao nezavisne 
 467 leme.
 468   then show ?case 
 469     apply (auto simp add: nzd.simps)
 470  sledgehammer
 471     using gcd_diff1_nat apply force
 472   sledgehammer
 473     by (metis Suc_le_mono diff_Suc_Suc gcd.commute gcd_diff1_nat nat_le_linear)
 474 qed
 475 
 476 textDrugi način na koji možemo zapisati dokaz ove leme jeste da izdvojimo leme 
 477 koje se tiču čisto matematičkih svojstava najvećeg zajedničkog delioca:
 478 
 479 lemma gcd_math1:
 480   fixes a b :: nat
 481   assumes "a ≥ b"
 482   shows "gcd a b = gcd (a - b) b"
 483   using assms
 484   by (simp add: gcd_diff1_nat)
 485 
 486 lemma gcd_math2:
 487   fixes a b :: nat
 488   assumes "a < b"
 489   shows "gcd a b = gcd a (b - a)"
 490   using assms
 491   by (metis gcd.commute gcd_diff1_nat less_imp_le)
 492 
 493 lemma nzd_gcd_shorter:
 494   shows "nzd a b = gcd a b"
 495 proof (induction a b rule: nzd.induct)
 496   case (1 b)
 497   then show ?case 
 498     by (simp add: nzd.simps)
 499 next
 500   case (2 v)
 501   then show ?case 
 502     by (simp add: nzd.simps)
 503 next
 504   case (3 a' b') 
 505   then show ?case 
 506     by (auto simp add: nzd.simps gcd_math1 gcd_math2)
 507 qed
 508 
 509 textIli najkraće zapisano: 
 510 
 511 lemma nzd_gcd_shortest:
 512   shows "nzd a b = gcd a b"
 513   by (induction a b rule: nzd.induct, auto simp add: nzd.simps gcd_math1 gcd_math2)
 514 
 515 
 516 text 
 517 \begin{exmp}
 518 Definisati efikasniju verziju Euklidovog algoritma koja koristi celobrojno 
 519 deljenje i dokazati da je ekvivalentna bibliotečkoj funkciji.
 520 \end{exmp}
 521 
 522 fun nzd_ef :: "nat ⇒ nat ⇒ nat" where
 523   "nzd_ef a b = 
 524     (if b = 0 then a
 525      else nzd_ef b (a mod b))"
 526 
 527 value "nzd_ef 120 48"
 528 
 529 declare nzd_ef.simps[simp del]
 530 
 531 text Prvo ćemo pokušati automatski da dokažemo pa krećemo od indukcije za novu 
 532 definiciju. Nakon toga pokušavamo samo auto i vidimo da smo stigli do čisto 
 533 matematičkog tvrđenja pa sada možemo da pokušamo sa sledgehammer-om:
 534 
 535 lemma nzd_ef_gcd:
 536   "nzd_ef a b = gcd a b"
 537   apply (induction a b rule: nzd_ef.induct)
 538   apply (auto simp add: nzd_ef.simps)
 539   using gcd_red_nat by auto
 540 
 541 textOvaj dokaz bi se kraće mogao zapisati na naredni način:
 542 
 543 \begin{footnotesize}
 544 \begin{verbatim}
 545 lemma nzd_ef_gcd:
 546   "nzd_ef a b = gcd a b"
 547   using gcd_red_nat
 548   by (induction a b rule: nzd_ef.induct, auto simp add: nzd_ef.simps)
 549 \end{verbatim}
 550 \end{footnotesize}
 551 
 552 Isar dokaz:
 553 
 554 lemma nzd_ef_gcd_isar:
 555   "nzd_ef a b = gcd a b"
 556 proof (induction a b rule: nzd_ef.induct)
 557   case (1 a b)
 558   show ?case
 559   proof (cases "b = 0")
 560     case True
 561     thus ?thesis
 562       by (simp add: nzd_ef.simps)
 563   next
 564     case False
 565     thus ?thesis
 566       using 1 nzd_ef.simps[of a b]
 567       using gcd_red_nat
 568       by auto
 569   qed
 570 qed
 571 
 572 text U realnim situacijama nemamo na raspolaganju bibliotečku funkciju. Jer ako 
 573 bismo je imali, onda ne bi imali potrebe da definišemo svoju funkciju. Tada 
 574 direktno dokazujemo svojstva naše funkcije. Pokušaćemo sada to da uradimo, npr. 
 575 dokažimo direktno da @{textnzd_ef} izračunava najveći zajednički delioc dva 
 576 broja. 
 577 
 578 Specifikacija: NZD je broj koji deli i prvi i drugi argument i ujedno je i 
 579 najveći broj sa tim svojstvom. Ovo tvrđenje ćemo formulisati kao dve odvojene 
 580 leme.
 581 
 582 lemma nzd_ef_deli_oba:
 583   "nzd_ef a b dvd a ∧ nzd_ef a b dvd b"
 584 proof (induction a b rule: nzd_ef.induct)
 585   case (1 a b)
 586   show ?case
 587   proof (cases "b = 0")
 588     case True
 589     thus ?thesis
 590       by (simp add: nzd_ef.simps)
 591   next
 592     case False
 593     thus ?thesis
 594       using nzd_ef.simps[of a b] 1
 595        sledgehammer
 596       using dvd_mod_iff
 597       by auto
 598   qed
 599 qed
 600 
 601 text Sada ćemo formulisati drugu lemu koja glasi: Ako bilo koji broj deli oba 
 602 argumenta, onda on mora da deli i rezultat (rezultat je, dakle, najveći u 
 603 relaciji deljivosti dvd). Nezavisno možemo pokazati i da je nzd najveći i u 
 604 smislu relacije manje jednako.
 605 
 606 lemma delioc_deli_nzd_ef:
 607   assumes "c dvd a" "c dvd b" 
 608   shows "c dvd nzd_ef a b"
 609   using assms
 610 proof (induction a b rule: nzd_ef.induct)
 611   case (1 a b)
 612   show ?case
 613   proof (cases "b = 0")
 614     case True
 615     then show ?thesis
 616       using 1(2)
 617       by (simp add: nzd_ef.simps)
 618   next
 619     case False
 620     then show ?thesis
 621       using nzd_ef.simps[of a b]
 622       using 1
 623       using dvd_mod_iff
 624       by auto
 625   qed
 626 qed
 627 
 628 
 629 subsection Brzo sortiranje 
 630 
 631 text 
 632 \begin{exmp}
 633 Definišimo i dokažimo korektnost funkcije brzog sortiranja.
 634 \end{exmp}
 635 
 636 text Ukratko opisano, quick-sort se izvodi tako što prvi element liste uzimamo 
 637 za pivot, pa: 
 638    izvajamo i sortiramo manje ili jednake od pivota,
 639    zatim na rezultat nadovezujemo pivot, 
 640    izdvajamo i sortiramo veće ili jednake od pivota.
 641 
 642 Bibliotečka funkcija filter izdvaja elemente koji zadovoljavaju dati uslov.
 643 Uslov se često zadaje u obliku lambda izraza (anonimne funkcije). 
 644 
 645 value "filter (λ x. x < 5) [1::nat, 3, 8, 4, 2, 5, 6, 3]"
 646 value "filter (λ x. x ≥ 5) [1::nat, 3, 8, 4, 2, 5, 6, 3]"
 647 
 648 
 649 fun qsort :: "nat list ⇒ nat list" where
 650 "qsort [] = []" | 
 651 "qsort (x # xs) = 
 652      qsort (filter (λ y. y ≤ x) xs) @ [x] @ qsort (filter (λ y. y > x) xs)" 
 653 
 654 textPrimetite da je prva podlista dobijena od elemenata koji su manji ili 
 655 jednaki početnom elementu liste x, ali pošto se filtrira rep liste nećemo dobiti 
 656 ponavljanje elementa x.
 657 
 658 textDokazati da ovakvo filtriranje skupa elemenata liste čuva skup elemenata i 
 659 multiskup elemenata početne liste:
 660 
 661 lemma mset_filter_leq_filter_gt:
 662   fixes xs :: "nat list" 
 663   shows "mset (filter (λy. y ≤ x) xs) + mset (filter (λ y. y > x) xs) =
 664          mset xs"
 665   by (induction xs) auto
 666 
 667 lemma set_filter_leq_filter_gt:
 668   fixes xs :: "nat list"
 669   shows "set (filter (λy. y ≤ x) xs) ∪ set (filter (λ y. y > x) xs) =
 670          set xs"
 671   by auto
 672 
 673 text Dokazati da se multiskup elemenata originalne liste ne menja nakon 
 674 sortiranja:
 675 
 676 lemma mset_qsort:
 677   "mset (qsort xs) = mset xs"
 678   by (induction xs rule: qsort.induct) (auto simp add: not_less)
 679 
 680 text Samim tim se ne menja ni skup elemenata:
 681 
 682 lemma set_qsort:
 683   "set (qsort xs) = set xs"
 684   by (metis mset_qsort set_mset_mset)
 685 
 686 text Dokazati da je dobijena lista nakon sortiranja sortirana:
 687 
 688 Napomena: u narednom dokazu, obratite pažnju na to da su sve leme koje se koriste 
 689 u dokazu već ranije formulisane i dokazane. Ako to ne bi bio slučaj, na nama je 
 690 da prepoznamo koji format treba da imaju nove leme, da ih formulišemo i dokažemo. 
 691 
 692 Za vežbu možete pokušati da u nezavisnom dokumentu izdvojite samo definicije i 
 693 glavne leme i da vidite da li možete da prepoznate šta je sve potrebno dodatno 
 694 formulisati.
 695 
 696 lemma qsort_sorted:
 697   "sorted (qsort xs)"
 698   apply (induction xs rule: qsort.induct) 
 699   apply auto
 700   apply (auto simp add: sorted_append)
 701     apply (auto simp add: set_qsort)
 702   done
 703 
 704 subsection Sortiranje objedinjavanjem
 705 
 706 text 
 707 \begin{exmp}Definisati i analizirati funkciju koja spaja dve sortirane liste tako 
 708 da formira novu sortiranu listu.
 709 \end{exmp}
 710 
 711 fun spoji :: "nat list ⇒ nat list ⇒ nat list" where
 712 "spoji [] ys = ys" | 
 713 "spoji xs [] = xs" | 
 714 "spoji (x # xs) (y # ys) = 
 715     (if x ≤ y then
 716         x # spoji xs (y # ys)
 717      else
 718         y # spoji (x # xs) ys)"
 719 
 720 textPokazati da je multiskup (i skup) liste dobijene objedinjavanjem jednak 
 721 uniji multiskupova (odnosno skupova) originalnih listi. Ove leme bismo mogli 
 722 dodati u simplifikator (ključnom reči simp nakon imena leme) ali nećemo 
 723 iskoristiti tu opciju sada da bismo videli da su neophodne za dokazivanje glavne 
 724 leme.
 725 
 726 Napomena: kada radite na manjem skupu lema u jednoj teoriji slobodno možete 
 727 dodati leme ovog tipa u simplifikator, ali u opštem slučaju treba biti obazriv 
 728 pošto previše lema može opteretiti simplifikator do te mere da postane 
 729 neupotrebljiv.
 730 
 731 lemma mset_spoji:
 732   shows "mset (spoji xs ys) = mset xs + mset ys"
 733   by (induction xs ys rule: spoji.induct, auto)
 734 
 735 lemma set_spoji:
 736   shows "set (spoji xs ys) = set xs ∪ set ys"
 737   apply (induction xs ys rule: spoji.induct)
 738     apply auto
 739   done
 740 
 741 textDokazati da se funkcijom spoji od dve sortirane liste dobija sortirana lista:
 742 
 743 lemma spoji_sorted:
 744   assumes "sorted xs" "sorted ys"
 745   shows "sorted (spoji xs ys)"
 746   using assms
 747   apply (induction xs ys rule: spoji.induct) 
 748   apply auto 
 749  vidimo da je automatski dokazivač došao do skupova, javlja se izraz oblika 
 750 @{text set (spoji _ _)} pa dodajemo lemu @{text set_spoji}.
 751 Napomena, da ova lema nije već bila formulisana morali bismo sami da prepoznamo 
 752 da je ovakva lema potrebna i formulisali bismo je i dokazali.
 753    apply (auto simp add: set_spoji)
 754   done
 755 
 756 text
 757 \begin{exmp}
 758 Napisati funkciju koja sortira listu objedinjavanjem i dokazati da je dobro definisana.
 759 \end{exmp}
 760 
 761 fun mergesort :: "nat list ⇒ nat list" where
 762 "mergesort [] = []" | 
 763 "mergesort [x] = [x]" | 
 764 "mergesort xs = 
 765     (let n = length xs div 2
 766       in spoji (mergesort (take n xs)) (mergesort (drop n xs)))"
 767 
 768 value "mergesort [3, 5, 1, 4, 8, 2]"
 769 
 770 textPokazati da je lista dobijena funkcijom mergesort sortirana:
 771 
 772 lemma mergesort_sortirano:
 773   shows "sorted (mergesort xs)"
 774   apply (induction xs rule: mergesort.induct)
 775   apply auto 
 776  vidimo da je dokazivač stao kod oblika @{text sorted (spoji _ _)} pa se 
 777 pozivamo na lemu @{text spoji_sorted}
 778   apply (auto simp add: spoji_sorted)
 779   done
 780 
 781 textDokazati da je skup elemenata i multiskup elemenata ostao nepromenjen nakon 
 782 poziva funkcije mergesort:
 783 
 784 lemma mset_take_drop:
 785   shows "mset (take n xs) + mset (drop n xs) = mset xs"
 786  sledgehammer
 787   by (metis append_take_drop_id mset_append)
 788 
 789 lemma mset_mergesort:
 790   shows "mset (mergesort xs) = mset xs"
 791   apply (induction xs rule: mergesort.induct)
 792     apply auto 
 793  možemo sami, korak po korak doći do ovog zaključka ili upotrebiti sledgehammer
 794  primetimo da u zaključku dokazivač ima izraz oblika @{text "mset (spoji _ _)"} 
 795 pa pokušavamo da dodamo lemu tog oblika (koju smo već dokazali)
 796   apply (auto simp add: mset_spoji)
 797  sada možemo da primetimo da u zaključku imamo izraz oblika 
 798 @{text mset (take _ _) + mset (drop _ _)} pa sada formulišemo novu lemu tog 
 799 oblika koju ćemo nazvati @{text mset_take_drop}.
 800   apply (auto simp add: mset_take_drop)
 801   done
 802 
 803 textSlično za set:
 804 
 805 lemma set_take_drop:
 806   shows "set (take n xs) ∪ set (drop n xs) = set xs"
 807  sledgehammer
 808   by (metis append_take_drop_id set_append)
 809 
 810 lemma set_mergesort:
 811   shows "set (mergesort xs) = set xs"
 812   apply (induction xs rule: mergesort.induct)
 813   apply auto
 814   apply (metis Un_iff in_set_dropD in_set_takeD list.simps(15) set_ConsD set_spoji)
 815   apply (auto simp add: set_spoji)
 816    apply (metis drop_Cons' list.set_intros(1) take_Cons')
 817  sledgehammer sam ne uspeva pa dodajemo novu lemu, slično kao za mset i onda ponovo sledgehammer
 818   by (metis Un_iff insertI2 list.simps(15) set_take_drop)
 819 
 820 
 821 subsectionDeljenje liste
 822 
 823 text Definisaćemo funkciju mergesort sada na malo drugačiji način:
 824 
 825 \begin{exmp}
 826 Definisati funkciju koja deli listu na dve liste približno jednake dužine.
 827 \end{exmp}
 828 
 829 Ovakva funkcija vraća uređeni par listi. U njenoj implementaciji koristićemo 
 830 funkcije @{text take} i @{text drop} koje izdvajaju, odnosno izbacuju, prvih 
 831 k elemenata liste.
 832 
 833 value "length [3::nat, 1, 4, 2, 5]"  duzina liste
 834 value "take 2 [3::nat, 1, 4, 2, 5]"  uzimanje prvih k elemenata liste
 835 value "drop 2 [3::nat, 1, 4, 2, 5]"  izbacivanje prvih k elemenata liste
 836 
 837 definition split :: "'a list ⇒ 'a list × 'a list" where
 838   "split xs = (let k = length xs div 2 in (take k xs, drop k xs))"  
 839 
 840 text Dokazati da nakon poziva funkcije split, dobijamo kraće liste: 
 841 
 842 lemma split_length:
 843   assumes "length xs > 1" "(ys, zs) = split xs"
 844   shows "length ys < length xs" "length zs < length xs"
 845   using assms
 846   unfolding split_def Let_def
 847   by auto
 848 
 849 textDokazati da je multiskup elemenata podeljen u dve rezultujuće liste:
 850 
 851 lemma split_mset:
 852   assumes "(ys, zs) = split xs"
 853   shows "mset xs = mset ys + mset zs"
 854   using assms
 855   unfolding split_def Let_def
 856   by (simp add: union_code)
 857 
 858 text Da bi se moglo nešto zaključivati o vrednosti generalno-rekurzivne 
 859 funkcije, potrebno je dokazati da se ona zaustavlja. Kada se upotrebi ključna reč 
 860 fun, sistem Isabelle automatski pokušava da dokaže zaustavljanje. To nekada uspe, 
 861 a nekada ne. Kada ne uspe, onda je potrebno da korisnik sam dokaže zaustavljanje 
 862 i tada koristi kombinaciju function-termination i možemo koristiti sledgehammer 
 863 za dokazivanje zaustavljanja. 
 864 
 865 Potrebno je ponovo definisati funkciju f i koristiti naredbu oblika 
 866 \verb!relation "measure f"! kojom ćemo dokazati da se u svakom koraku rekurzije 
 867 vrednost funkcije f smanjuje. U našem primeru tvrdimo da se kroz rekuzivne pozive 
 868 smanjuje dužina liste. Nakon toga koristimo sledgehammer da bismo to i dokazali.
 869 
 870 function (sequential) mergesort_split :: "nat list ⇒ nat list" where
 871 "mergesort_split [] = []" | 
 872 "mergesort_split [x] = [x]" | 
 873 "mergesort_split xs = 
 874     (let (ys, zs) = split xs 
 875       in spoji (mergesort_split ys) (mergesort_split zs))"
 876   by pat_completeness auto
 877 termination
 878   apply (relation "measure (λ xs. length xs)")
 879     apply simp
 880    apply (metis One_nat_def in_measure length_Cons lessI linorder_not_less list.size(4) split_length(1) trans_le_add2)
 881   apply (metis One_nat_def impossible_Cons in_measure linorder_not_less list.size(4) split_length(2) trans_le_add2)
 882   done
 883 
 884 
 885 text Funkcija je definisana preko tri "šablona" (engl. pattern). Opcija 
 886 (sequential) znači da se šabloni ispituju jedan po jedan (tj. da se šablon 
 887 primenjuje samo ako prethodni nisu uklopljeni). Ovo je podrazumevano ponašanje u 
 888 većini funkcionalnih jezika (npr. u Haskell-u), pa ćemo stoga praktično uvek 
 889 navoditi tu opciju. 
 890 
 891 U narednom dokazu koristićemo naredbu \verb!apply (simp split: prod.split)!. 
 892 Pošto funkcija @{text mergesort_split} prvo kreira uređeni par 
 893 @{text let (ys, zs) = split xs}, potrebno nam je da upotrebimo @{text split} 
 894 pravilo @{text prod.split} koje će izdvojiti elemente odgovarajućeg uređenog 
 895 para. 
 896 
 897 Napomena: ovde se @{text split} koristi kao ključna reč i nema veze sa imenom 
 898 funkcije split koje smo ranije koristili.
 899 
 900 lemma mset_mergesort_split:
 901   "mset (mergesort_split xs) = mset xs"
 902 proof (induction xs rule: mergesort_split.induct) 
 903   case 1
 904   then show ?case
 905     by simp
 906 next
 907   case (2 x)
 908   then show ?case
 909     by simp
 910 next
 911   case (3 x0 x1 xs)
 912   then show ?case
 913     apply (simp split: prod.split)
 914  sledgehammer
 915     by (metis mset.simps(2) mset_spoji split_mset)
 916  ili kraće:
 917  @{textby (simp split: prod.split) (metis mset.simps(2) mset_spoji split_mset)}
 918 qed
 919 
 920 lemma
 921   "sorted (mergesort_split xs)"
 922   apply (induction xs rule: mergesort_split.induct) 
 923     apply (auto split: prod.split)
 924  sledgehammer
 925   by (simp add: spoji_sorted)
 926 
 927 sectionMaterijal za vežbanje
 928 
 929 textNapomena: odavde pa nadalje se nalazi materijal za vežbanje. Pokušajte sami 
 930 da formulišete sve definicije i leme ili makar da napišete dokaze lema nakon što 
 931 vidite njihovu formulaciju.
 932 
 933 subsectionSortiranje umetanjem
 934 
 935 textNapisati funkciju koja ubacuje element u sortiranu listu prirodnih brojeva 
 936 tako da ona ostane i dalje sortirana.
 937 
 938 primrec ubaci :: "nat ⇒ nat list ⇒ nat list" where
 939 "ubaci a [] = [a]" |
 940 "ubaci a (x # xs) = (if a ≤ x then a # x # xs else x # ubaci a xs)"
 941 
 942 value "ubaci 5 [1,3,4,9]"
 943 
 944 textNapisati funkciju koja sortira listu umetanjem, prvo uz pomoć rekurzije a 
 945 onda uz pomoć funkcije fold. 
 946 
 947 primrec insertion_sort_rek :: "nat list ⇒ nat list" where
 948 "insertion_sort_rek [] = []" |
 949 "insertion_sort_rek (x # xs) = ubaci x (insertion_sort_rek xs)"
 950 
 951 textNakon što smo definisali funkciju ubaci, možemo iskoristiti funkciju fold da 
 952 ubacimo sve elemente liste u praznu listu.
 953 
 954 definition insertion_sort_fold :: "nat list ⇒ nat list" where
 955 "insertion_sort_fold xs = fold ubaci xs []"
 956 
 957 value "insertion_sort_fold [3,1,5,4]"
 958 value "insertion_sort_fold []"
 959 
 960 term sorted
 961 value "sorted [3,1,2::nat]"
 962 
 963 textDokazati da su funkcije @{text ubaci}, @{text insertion_sort_fold}, 
 964 @{text insertion_sort_rek} dobro definisane u odnosu na skup:
 965 
 966 lemma [simp]:
 967   "set (ubaci a xs) = {a} ∪ set xs"
 968   by (induction xs) auto
 969 
 970 lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp
 971 lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp
 972 lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp
 973 
 974 
 975 text Koristi se desni fold pa nam treba indukcija sa desna, odnosno indukcija 
 976 kada se novi element dodaje na kraj liste @{thm[mode=Proof] rev_induct [no_vars]}.
 977 
 978 @{url https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Doc/How_to_Prove_it/How_to_Prove_it.html}
 979 
 980 
 981 thm rev_induct  
 982 
 983 lemma "set (insertion_sort_fold xs) = set xs"
 984 unfolding insertion_sort_fold_def
 985   by (induction xs rule: rev_induct) auto 
 986 
 987 lemma "set (insertion_sort_rek xs) = set xs"
 988   unfolding insertion_sort_rek_def
 989   by (induction xs) auto
 990 
 991 textDokazati da su funkcije @{text ubaci}, @{text insertion_sort_fold}, 
 992 @{text insertion_sort_rek} dobro definisane u odnosu na multiskup:
 993 
 994 textDrugi način da ubacimo element u multiskup (osim @{text {#a#} + mset xs}) 
 995 je korišćenjem funkcije @{text add_mset}:
 996 
 997 term mset
 998 term add_mset
 999 
1000 lemma [simp]:
1001   "mset (ubaci a xs) = add_mset a (mset xs)"
1002   by (induction xs) auto
1003 
1004 lemma [simp]:
1005   "mset (insertion_sort_fold xs) = mset xs"
1006   unfolding insertion_sort_fold_def
1007   by (induction xs rule: rev_induct) auto
1008 
1009 lemma [simp]:
1010   "mset (insertion_sort_rek xs) = mset xs"
1011   unfolding insertion_sort_rek_def
1012   by (induction xs) auto
1013 
1014 textDokazati da funkcije @{text ubaci}, @{text insertion_sort_fold}, 
1015 @{text insertion_sort_rek} generišu sortirane liste:
1016 
1017 lemma [simp]:
1018   assumes "sorted xs"
1019   shows "sorted (ubaci a xs)"
1020   using assms
1021   by (induction xs) auto
1022 
1023 lemma
1024   "sorted (insertion_sort_fold xs)"
1025   by (induction xs rule: rev_induct) (auto simp add: insertion_sort_fold_def)
1026 
1027 lemma
1028   "sorted (insertion_sort_rek xs)"
1029   by (induction xs) auto
1030 
1031 
1032 
1033 subsectionCelobrojno deljenje
1034 
1035 
1036 textOpštom rekurzijom definisati funkciju div2 koja izračunava celobrojnu 
1037 vrednost n/2 i dokazati da je dobro definisana.
1038 
1039 fun div2 :: "nat ⇒ nat" where
1040 "div2 0 = 0" |
1041 "div2 (Suc 0) = 0" |
1042 "div2 (Suc(Suc n)) = Suc (div2 n)"
1043 
1044 thm div2.induct
1045 
1046 lemma "div2 n = n div 2"
1047   apply (induction n rule: div2.induct)
1048     apply auto
1049 done
1050 
1051 textRanije smo već definisali sabiranje nad prirodnim brojevima na sledeći način:
1052 
1053 primrec add :: "nat ⇒ nat ⇒ nat" where
1054 "add 0 n = n" |
1055 "add (Suc m) n = Suc (add m n)"
1056 
1057 textNapisati funkciju itadd koristeći repnu rekurziju, odnosno napisati 
1058 rekurzivni poziv tako da funkcija itadd poziva samu sebe direktno:
1059 @{text itadd (Suc m) n = itadd...}. Dokazati da je ekvivalentna operaciji 
1060 sabiranja koju smo malopre uveli.
1061 
1062 primrec itadd :: "nat ⇒ nat ⇒ nat" where
1063 "itadd 0 n = n" |
1064 "itadd (Suc m) n = itadd m (Suc n)"
1065 
1066 textPomoćna lema:
1067 
1068 lemma itadd_Suc:
1069   shows "itadd m (Suc n) = Suc (itadd m n)"
1070   apply (induction m arbitrary: n)  
1071   posto funkcija itadd menja drugi argument, moramo dodati ključnu reč arbitrary
1072    apply auto
1073 done 
1074 
1075 lemma "itadd m n = add m n"
1076   apply (induction m)
1077    apply auto 
1078  vidimo da je dokazivač stao kod tvrđenja oblika 
1079 @{text itadd m (Suc n) = Suc (add m n)} pa formulišemo pomoćnu lemu 
1080 @{text itadd_Suc}koja odgovara tom tvrđenju
1081   apply (auto simp add: itadd_Suc)
1082   done
1083 
1084 textIli kraće: \verb!by (induction m) (auto simp add: itadd_Suc)!
1085 
1086 subsectionPretraga za parom brojeva
1087 
1088 text Napisati funkciju koja proverava da li u sortiranoj listi prirodnih brojeva 
1089 postoji par brojeva čiji zbir je jednak traženom broju s. Funkcija vraća True ili 
1090 False.
1091 
1092 Pošto se u rekurzivnim pozivima ove funkcije menjaju indeksi granica liste 
1093 (odnosno dela liste koji pretražujemo) funkcija mora da ima dva početna parametra 
1094 koji će odgovarati levoj i desnoj granici - lo i hi.
1095 
1096 U ovoj funkciji koristimo operator @{text "xs!i"} kojim pristupamo elementu liste 
1097 xs koji se nalazi na poziciji $i$.
1098 
1099 
1100 function par :: "nat ⇒ nat ⇒ nat list ⇒ nat ⇒ bool" where
1101   "par lo hi xs s = (
1102     if lo ≥ hi then 
1103        False
1104     else if xs ! lo + xs ! hi < s then
1105        par (lo + 1) hi xs s
1106     else if xs ! lo + xs ! hi > s then
1107        par lo (hi - 1) xs s
1108     else
1109        True)"
1110   by pat_completeness auto
1111 termination by (relation "measure (λ (lo, hi, xs, x). hi - lo)") auto
1112 
1113 declare par.simps [simp del]
1114 
1115 textDokazati da ako je lista sortirana, funkcija par vraća True ako i samo ako u 
1116 listi postoje dva prirodna broja na pozicijama $i$ i $j$ čiji zbir je jednak 
1117 traženom broju $s$.
1118 
1119 Dokaz počinjemo indukcijom, samo moramo voditi računa da navedemo sve parametre 
1120 funkcije par onim redom kojim se pojavljuju u definiciji. Nakon toga dokaz 
1121 granamo onim redom kojim se pojavljuju grananja u definiciji. Počinjemo sa 
1122 grananjem @{text lo  hi}, pa uvodimo redom sva grananja koja se javljaju u 
1123 definiciji.
1124 
1125 Za vežbu: pokušajte sami da napišete ovaj dokaz.
1126 
1127 lemma sorted_par:
1128   assumes "sorted xs" "0 ≤ lo" "hi < length xs"
1129   shows "par lo hi xs s ⟷ 
1130          (∃ i j. lo ≤ i ∧ i < j ∧ j ≤ hi ∧ xs ! i + xs ! j = s)"
1131   using assms
1132 proof (induction lo hi xs s rule: par.induct)
1133   case (1 lo hi xs s)
1134   show ?case 
1135   proof (cases "lo ≥ hi")
1136     case True
1137     thus ?thesis
1138       by (simp add: par.simps)
1139   next            
1140     case False
1141     show ?thesis
1142     proof (cases "xs ! lo + xs ! hi < s")
1143       case True
1144       have "(∃i≥Suc lo. ∃j>i. j ≤ hi ∧ xs ! i + xs ! j = s) ⟷
1145             (∃i≥lo. ∃j>i. j ≤ hi ∧ xs ! i + xs ! j = s)" (is "?lhs ⟷ ?rhs")
1146       proof
1147         assume "?lhs"
1148         then obtain i j where *: "Suc lo ≤ i" "i < j" "j ≤ hi" "xs ! i + xs ! j = s"
1149           by auto
1150         hence "lo ≤ i" 
1151           by simp
1152         thus ?rhs
1153           using *
1154           by blast
1155       next
1156         assume "?rhs"
1157         then obtain i j where *: "lo ≤ i" "i < j" "j ≤ hi" "xs ! i + xs ! j = s"
1158           by auto
1159         show "?lhs"
1160         proof (cases "Suc lo ≤ i")
1161           case True
1162           thus ?thesis
1163             using *
1164             by blast
1165         next
1166           case False
1167           hence "i = lo"
1168             using *
1169             by simp
1170           hence "xs ! lo + xs ! j = s"
1171             using *
1172             by simp
1173           hence "xs ! lo + xs ! hi ≥ s"
1174             using `sorted xs` `j ≤ hi` `hi < length xs`
1175             using sorted_nth_mono[of xs j hi]
1176             by auto
1177           hence False
1178             using `xs ! lo + xs ! hi < s`
1179             by simp
1180           thus ?thesis
1181             by simp
1182         qed
1183       qed
1184       thus ?thesis
1185         using `¬ lo ≥ hi` par.simps[of lo hi xs s]
1186         using `xs ! lo + xs ! hi < s` 1(1) 1(3-5)
1187         by simp
1188     next
1189       case False
1190       show ?thesis
1191       proof (cases "xs ! lo + xs ! hi > s")
1192         case True
1193         have "(∃i≥lo. ∃j>i. j ≤ hi - 1 ∧ xs ! i + xs ! j = s) ⟷
1194               (∃i≥lo. ∃j>i. j ≤ hi ∧ xs ! i + xs ! j = s)" (is "?lhs ⟷ ?rhs")
1195         proof
1196           assume "?lhs"
1197           then obtain i j where *: "lo ≤ i" "i < j" "j ≤ hi - 1" "xs ! i + xs ! j = s"
1198             by auto
1199           hence "j ≤ hi"
1200             by simp
1201           thus "?rhs"
1202             using *
1203             by blast
1204         next
1205           assume "?rhs"
1206           then obtain i j where *: "lo ≤ i" "i < j" "j ≤ hi" "xs ! i + xs ! j = s"
1207             by auto
1208           show ?lhs
1209           proof (cases "j ≤ hi - 1")
1210             case True
1211             thus ?thesis
1212               using *
1213               by blast
1214           next
1215             case False
1216             hence "j = hi"
1217               using *
1218               by simp
1219             hence "xs ! i + xs ! hi = s"
1220               using *
1221               by simp
1222             hence "xs ! lo + xs ! hi ≤ s"
1223               using `sorted xs` * `hi < length xs`
1224               using sorted_nth_mono[of xs lo i]
1225               by simp
1226             hence False
1227               using `xs ! lo + xs ! hi > s`
1228               by simp
1229             thus ?thesis
1230               by simp
1231           qed          
1232         qed
1233         thus ?thesis 
1234           using `¬ lo ≥ hi` par.simps[of lo hi xs s]
1235           using `xs ! lo + xs ! hi > s` 1(2) 1(3-5)
1236           by simp
1237       next
1238         case False
1239         thus ?thesis 
1240           using par.simps[of lo hi xs s] `¬ lo ≥ hi`
1241           using `¬ xs ! lo + xs ! hi < s` `¬ xs ! lo + xs ! hi > s`
1242           by auto (rule_tac x="lo" in exI, simp, rule_tac x="hi" in exI, simp)          
1243       qed
1244     qed
1245   qed
1246 qed
1247 
1248 
1249 subsection Binarna pretraga
1250 
1251 textNapisati funkciju koja izvodi binarnu pretragu nad sortiranom listom.
1252 
1253 Prvo ćemo definisati pomoćnu funkciju bsearch' koja će imati dodatna dva 
1254 argumenta koji će određivati opseg liste koji pretražujemo.
1255 
1256 Primetimo da naredna funkcija mora biti deklarisana sa celim brojevima, zato što 
1257 ovakva definicija dodeljuje promenljivoj mid tip celog broja, a ta promenljiva se 
1258 prosleđuje narednim rekurzivnim pozivima (pogledajte šta se dešava kada promenite 
1259 tip u funkciji sa int na nat).
1260 
1261 function bsearch' :: "int ⇒ int ⇒ nat list ⇒ nat ⇒ bool" where
1262   "bsearch' lo hi xs x = 
1263     (if lo > hi then 
1264        False
1265      else                 
1266        let mid = lo + (hi - lo) div 2
1267         in if x > xs ! nat mid then 
1268              bsearch' (mid+1) hi xs x
1269            else if x < xs ! nat mid then
1270              bsearch' lo (mid-1) xs x
1271            else
1272              True
1273     )"
1274   by pat_completeness auto
1275 termination
1276 by (relation "measure (λ (lo, hi, xs, x). nat (hi - lo + 1))") auto
1277 
1278 declare bsearch'.simps [simp del]
1279 
1280 textSada možemo definisati funkciju bsearch koja prima samo sortiranu listu i broj koji se traži:
1281 
1282 definition bsearch :: "nat list ⇒ nat ⇒ bool" where
1283   "bsearch xs x = bsearch' 0 (int (length xs) - 1) xs x" 
1284 
1285 textDokazati da je funkcija bsearch dobro definisana.
1286 
1287 Razmotrimo šta to znači u ovom slučaju. Lista koje se pretražuje mora biti 
1288 sortirana, i funkcija bsearch će vratiti vrednost True ako i samo ako se traženi 
1289 element nalazi u listi. Proveru da li se element nalazi u listi izvodimo uz pomoć 
1290 funkcije set i dobijamo narednu formulaciju:
1291 
1292 \begin{footnotesize}
1293 \begin{verbatim}
1294 lemma sorted_bsearch:
1295   assumes "sorted xs"
1296   shows "bsearch xs x ⟷ x ∈ set xs"
1297 \end{verbatim}
1298 \end{footnotesize}
1299 
1300 Pošto funkcija bsearch poziva funkciju bsearch' koja radi nad segmentima liste, 
1301 primećujemo da nam odgovara da uvedemo pojam segmenta liste - elementi liste koji 
1302 se nalaze između indeksa lo i hi na sledeći način. Koristićemo lambda funkciju i 
1303 operaciju map:
1304 
1305 definition segment where
1306   "segment lo hi xs = map (λ i. xs ! (nat i)) [lo..hi]"
1307 
1308 textKada budemo radili sa listom, krećemo od cele liste tako da je na početku 
1309 segment određen pozicijom 0 i poslednjim elementom liste koji je na poziciji 
1310 @{text length xs - 1}. Ovo ćemo dokazati kao izdvojenu lemu i nazvaćemo je 
1311 @{text ceo_segment}. 
1312 
1313 U narednom dokazu koristićemo lemu @{text map_nth} koja glasi: 
1314 @{thm[mode=Proof] map_nth [no_vars]} i tvrdi da funkcija ! može biti korišćena da 
1315 mapiramo sve elemente liste kada prođemo kroz sve indekse od prvog do poslednjeg 
1316 elementa.
1317 
1318 thm map_nth
1319 
1320 lemma ceo_segment:
1321   shows "segment 0 (int (length xs) - 1) xs = xs"
1322 proof-
1323   have "[0..<length xs] = map nat [0..int(length xs) - 1]"
1324 (*    apply (induction xs)
1325      apply auto
1326     sledgehammer
1327     by (simp add: upto_rec2)
1328 *)  by (induction xs, simp_all add: upto_rec2)
1329   thus ?thesis
1330     using map_nth[of xs, symmetric]
1331     unfolding segment_def
1332  možemo da iskoristimo sledgehammer a možemo i da primenimo samo auto i da 
1333 vidimo da se pojavljuje kompozicija funkcija
1334     by (auto simp add: comp_def)
1335 qed
1336 
1337 
1338 textSada ćemo ponovo dodati opštiju lemu koja će se ticati funkcije bsearch'. 
1339 Ekvivalent našoj finalnoj lemi, samo primenjena na segment lo hi.
1340 
1341 U narednom dokazu, isto kao i ranije, moramo pratiti definiciju same funkcije i u 
1342 ovom slučaju u definiciji imamo naredbu \verb!let mid = lo + (hi - lo) div 2! 
1343 koju koristimo u dokazu. Nadalje granamo isto kao i u ranijim dokazima.
1344 
1345 lemma bsearch'_segment:
1346   assumes "0 ≤ lo" "lo ≤ hi" "hi < int (length xs)" "sorted xs"
1347   shows "bsearch' lo hi xs x ⟷ x ∈ set (segment lo hi xs)"
1348   using assms
1349 proof (induction lo hi xs x rule: bsearch'.induct)
1350   case (1 lo hi xs x)
1351   let ?mid = "lo + (hi - lo) div 2"
1352 
1353   have "lo ≤ ?mid" "?mid ≤ hi"
1354     using `lo ≤ hi`
1355     by auto
1356 
1357   show ?case
1358   proof (cases "x > xs ! (nat ?mid)")
1359     case True
1360     hence *: "bsearch' lo hi xs x = bsearch' (?mid + 1) hi xs x"
1361       using `lo ≤ hi` bsearch'.simps[of lo hi xs x]
1362       by simp
1363 
1364     have "x ∉ set (segment lo ?mid xs)"
1365     proof (rule ccontr)
1366       assume "¬ ?thesis"
1367       then obtain i where "lo ≤ i" "i ≤ ?mid" "xs ! nat i = x"
1368         by (auto simp add: segment_def)
1369       hence "xs ! nat i > xs ! nat ?mid"
1370         using `x > xs ! nat ?mid`
1371         by simp
1372       moreover
1373       have "nat i ≤ nat ?mid"
1374         using `i ≤ ?mid`
1375         by simp
1376       moreover
1377       have "?mid < int (length xs)"
1378         using `?mid ≤ hi` `hi < int (length xs)`
1379         by simp
1380       hence "nat ?mid < length xs"
1381         using `0 ≤ lo` `lo ≤ ?mid`
1382         by simp
1383       ultimately
1384       show False
1385         using `sorted xs`
1386         using sorted_nth_mono[of xs "nat i" "nat ?mid"]
1387         by simp
1388     qed
1389 
1390     have "[lo..hi] = [lo..?mid] @ [?mid+1..hi]"
1391       using `lo ≤ ?mid` `?mid ≤ hi`
1392       using upto_split2
1393       by blast
1394     hence "segment lo hi xs = segment lo ?mid xs @ segment (?mid + 1) hi xs"
1395       unfolding segment_def
1396       by simp
1397     hence **: "x ∈ set (segment lo hi xs) ⟷ x ∈ set (segment (?mid + 1) hi xs)"
1398       using `x ∉ set (segment lo ?mid xs)`
1399       by simp
1400 
1401     show ?thesis
1402     proof (cases "?mid + 1 ≤ hi")
1403       case False
1404       have "segment (?mid + 1) hi xs = []"
1405         using False `0 ≤ lo` `lo ≤ hi`
1406         unfolding segment_def
1407         by simp
1408       moreover
1409       have "bsearch' (?mid + 1) hi xs x = False"
1410         using False bsearch'.simps[of "?mid + 1" hi xs x]
1411         by simp
1412       ultimately
1413       show ?thesis
1414         using * **
1415         by simp
1416     next
1417       case True
1418       thus ?thesis
1419         using 1(1)[of ?mid] `lo ≤ hi` `0 ≤ lo` `hi < int (length xs)` `sorted xs`
1420         using `x > xs ! nat ?mid` * **
1421         by simp
1422     qed
1423   next
1424     case False
1425     show ?thesis
1426     proof (cases "x < xs ! nat ?mid")
1427       case True
1428       hence *: "bsearch' lo hi xs x = bsearch' lo (?mid - 1) xs x"
1429         using `lo ≤ hi` bsearch'.simps[of lo hi xs x]
1430         by simp
1431 
1432       have "x ∉ set (segment ?mid hi xs)"
1433       proof (rule ccontr)
1434         assume "¬ ?thesis"
1435         then obtain i where "?mid ≤ i" "i ≤ hi" "xs ! nat i = x"
1436           by (auto simp add: segment_def)
1437         hence "xs ! nat i < xs ! nat ?mid"
1438           using `x < xs ! nat ?mid`
1439           by simp
1440         moreover
1441         have "nat i ≥ nat ?mid"
1442           using `i ≥ ?mid`
1443           by simp
1444         moreover
1445         have "nat i < length xs"
1446           using `0 ≤ lo` `lo ≤ hi` `hi < int (length xs)` `i ≤ hi`
1447           by simp
1448         ultimately
1449         show False
1450           using `sorted xs`
1451           using sorted_nth_mono[of xs "nat ?mid" "nat i"]
1452           by simp
1453       qed
1454 
1455       have "[lo..hi] = [lo..?mid-1] @ [?mid..hi]"
1456         using `lo ≤ ?mid` `?mid ≤ hi`
1457         using upto_split1 
1458         by blast
1459       hence "segment lo hi xs = segment lo (?mid - 1) xs @ segment ?mid hi xs"
1460         unfolding segment_def
1461         by simp
1462       hence **: "x ∈ set (segment lo hi xs) ⟷ x ∈ set (segment lo (?mid - 1) xs)"
1463         using `x ∉ set (segment ?mid hi xs)`
1464         by simp
1465 
1466       show ?thesis
1467       proof (cases "lo ≤ ?mid - 1")
1468         case False
1469         have "segment lo (?mid - 1) xs = []"
1470           using False `0 ≤ lo` `lo ≤ hi`
1471           unfolding segment_def
1472           by simp
1473         moreover
1474         have "bsearch' lo (?mid - 1) xs x = False"
1475           using False bsearch'.simps[of lo "?mid - 1" xs x]
1476           by simp
1477         ultimately
1478         show ?thesis
1479           using * **
1480           by simp
1481       next
1482         case True
1483         thus ?thesis
1484           using 1(2)[of ?mid] `lo ≤ hi` `0 ≤ lo` `hi < int (length xs)` `sorted xs`
1485           using `x < xs ! nat ?mid` * **
1486           by simp
1487       qed
1488     next
1489       case False
1490       have "bsearch' lo hi xs x = True"
1491         using bsearch'.simps[of lo hi xs x]
1492         using `¬ x > xs ! nat ?mid` `¬ x < xs ! nat ?mid` `lo ≤ hi`
1493         by simp
1494       moreover
1495       have "x = xs ! nat ?mid"
1496         using `¬ x > xs ! nat ?mid` `¬ x < xs ! nat ?mid`
1497         by simp
1498       hence "x ∈ set (segment lo hi xs)"
1499         using `lo ≤ ?mid` `?mid ≤ hi`
1500         unfolding segment_def
1501         by simp
1502       ultimately
1503       show ?thesis
1504         by simp
1505     qed
1506   qed
1507 qed
1508 
1509 textSada prelazimo na glavnu lemu. Težinu dokaza smo prebacili na prethodne leme 
1510 tako da je dokaz ove leme kratak.
1511 
1512 lemma sorted_bsearch:
1513   assumes "sorted xs"
1514   shows "bsearch xs x ⟷ x ∈ set xs"
1515 proof (cases "xs = []")
1516   case True
1517   thus ?thesis
1518     unfolding bsearch_def
1519     by (simp add: bsearch'.simps)
1520 next
1521   case False  
1522   hence "segment 0 (int (length xs) - 1) xs = xs"
1523     by (auto simp add: ceo_segment)
1524   thus ?thesis                
1525     unfolding bsearch_def
1526     using assms `xs ≠ []`
1527     using bsearch'_segment[of 0 "int (length xs) - 1" xs x]
1528     by simp
1529 qed  
1530 
1531 end