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 text‹Do 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 text‹Vež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 text‹Ovaj 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 text‹Nakon 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 text‹Dokazi 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 ― ‹@{text‹using [[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 ― ‹@{text‹by (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 text‹U 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 text‹Pa 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 text‹Ova 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 text‹Alternativa 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 text‹sada 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 text‹Drugi 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 text‹Ili 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 text‹Ovaj 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 @{text‹nzd_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 text‹Primetite 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 text‹Dokazati 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 text‹Pokazati 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 text‹Dokazati 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 text‹Pokazati 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 text‹Dokazati 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 text‹Slič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 subsection‹Deljenje 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 text‹Dokazati 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 ― ‹@{text‹by (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 section‹Materijal za vežbanje› 928 929 text‹Napomena: 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 subsection‹Sortiranje umetanjem› 934 935 text‹Napisati 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 text‹Napisati 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 text‹Nakon š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 text‹Dokazati 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 text‹Dokazati da su funkcije @{text ‹ubaci›}, @{text ‹insertion_sort_fold›}, 992 @{text ‹insertion_sort_rek›} dobro definisane u odnosu na multiskup:› 993 994 text‹Drugi 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 text‹Dokazati 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 subsection‹Celobrojno deljenje› 1034 1035 1036 text‹Opš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 text‹Ranije 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 text‹Napisati 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 text‹Pomoć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 text‹Ili kraće: \verb!by (induction m) (auto simp add: itadd_Suc)!› 1085 1086 subsection‹Pretraga 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 text‹Dokazati 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 text‹Napisati 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 text‹Sada 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 text‹Dokazati 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 text‹Kada 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 text‹Sada ć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 text‹Sada 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