1 section‹Definisanje algebarskog tipa drveta i funkcija za rad sa njima› 2 3 theory Cas11_vezbe_resenja 4 imports Main 5 "~/Downloads/Isabelle2019/src/HOL/Library/Multiset" 6 7 begin 8 9 10 text ‹Drvo je ili prazno (sto obeležavamo sa Null) ili sadrži vrednost i levo i 11 desno poddrvo (sto obeležavamo sa Cvor l v d). Ovako definisano drvo može 12 sadržati samo prirodne brojeve. › 13 datatype Drvo_nat = Null_nat | Cvor_nat Drvo_nat nat Drvo_nat 14 15 term "Null" ― ‹prazno drvo› 16 term "Cvor_nat" ― ‹funkcija koja od dva drveta i novog elementa kreira novo drvo› 17 term "Cvor_nat Null 1 Null" ― ‹drvo sa jednim elementom› 18 19 text‹ Primer drveta i njegovo kreiranje u isabelle-u. 20 \begin{verbatim} 21 3 22 1 2 23 . . 4 3 24 . . . . 25 \end{verbatim} 26 › 27 term "Cvor_nat (Cvor_nat Null 1 Null) 3 (Cvor_nat (Cvor_nat Null 4 Null) 2 (Cvor_nat Null 3 Null))" 28 29 text‹Ako bismo želeli da kreiramo drvo sa elementima proizvoljnog tipa koristili 30 bi sledeću naredbu. Sada prilikom navođenja elemenata moramo navesti i tip jednog 31 elementa. Isto kao kod listi, dovoljno je navesti tip za jedan element pošto svi 32 elementi drveta moraju biti istog tipa.› 33 34 datatype 'a Drvo = Null | Cvor "'a Drvo" 'a "'a Drvo" 35 term "Cvor Null (1::nat) Null" 36 term "Cvor (Cvor Null (4::nat) Null) 2 (Cvor Null 3 Null)" 37 38 text‹Primeri koji slede mogu se pisati nad tipom @{text ‹Drvo›} kao i nad tipom 39 @{text ‹Drvo_nat›}. Nema velike razlike u definicijama i funkcijama koje slede.› 40 41 42 text‹ 43 \begin{exmp} 44 Definisati primitivnom rekurzijom funkciju koja računa zbir svih elemenata u 45 drvetu koje sadrži samo prirodne brojeve. 46 \end{exmp} 47 48 Primitivna rekurzija mora da prati definiciju tipa. Posto se računa zbir, 49 ograničili smo ovu funkciju samo na zbir drveta prirodnih brojeva.› 50 51 primrec zbir :: "nat Drvo ⇒ nat" where 52 "zbir Null = 0" | 53 "zbir (Cvor l v d) = zbir l + v + zbir d" 54 55 text‹Da bismo mogli da testiramo vrednosti funkcija na konkretnom drvetu, da ne 56 bismo iznova konstruisali drvo na koje želimo da primenimo tu funkciju, koristimo 57 ključnu reč @{text ‹definition›} i uvodimo narednu definiciju radi lakšeg 58 testiranja. Sada možemo da testiramo funkciju @{text ‹zbir›} primenjujuci je na 59 @{text ‹test_drvo›} koje smo kreirali.› 60 61 definition test_drvo :: "nat Drvo" where 62 "test_drvo = Cvor (Cvor Null 1 Null) 3 (Cvor (Cvor Null 4 Null) 2 (Cvor Null 3 Null))" 63 64 value "zbir test_drvo" 65 66 text‹ 67 \begin{exmp} 68 Napisati funkciju koja proverava da li drvo sadrži dati element. 69 \end{exmp} 70 71 Pošto ovako definisano drvo nije uređeno drvo, pretraga drveta mora da bude 72 iscrpna i da se svaki čvor pregleda. Funkciju definišemo primitivnom rekurzijom. 73 Ova funkcija ne bi morala da bude ograničena samo na tip prirodnih brojeva. Isto 74 bi izgledala i za proizvoljan tip.› 75 76 primrec sadrzi :: "nat Drvo ⇒ nat ⇒ bool" where 77 "sadrzi Null _ ⟷ False" | 78 "sadrzi (Cvor l v d) x ⟷ sadrzi l x ∨ v = x ∨ sadrzi d x" 79 80 text‹Sada testiramo funkciju @{text ‹sadrzi›} nad istim drvetom kao i malopre. Na 81 isti način se može kreirati više različitih drveta pa se testirati funkcija za 82 različitu strukturu drveta.› 83 84 value "test_drvo" 85 value "sadrzi test_drvo 3" 86 value "sadrzi test_drvo 5" 87 88 text‹Sada ćemo, analogno listama kod koje se pripadanje elementa listi proverava 89 preko skupa elemenata koji pripadaju listi, definisati funkciju koja određuje 90 skup svih elemenata u drvetu. 91 92 \begin{exmp} 93 Definisati funkciju @{text ‹skup›} koja odredjuje skup elemenata koji pripadaju 94 drvetu. Dokazati da je dobro definisana u odnosu na funkcije @{text ‹sadrzi›} i 95 @{text ‹pripadnost elementa skupu›}. 96 \end{exmp} 97 98 Kada ne navedemo tip funkcije prilikom kreiranja, isabelle pretpostavlja 99 najopštiji tip tako da će ova funkcija moći da se primeni na drvo proizvoljnog 100 tipa (za razliku od prethodnih, gde bismo morali da promenimo tip drveta u samoj 101 definiciji).› 102 103 primrec skup where 104 "skup Null = {}" | 105 "skup (Cvor l v d) = skup l ∪ {v} ∪ skup d" 106 107 value "skup test_drvo" ―‹testiramo funkciju skup› 108 109 text‹Veza između pretrage i skupa elemenata se formuliše narednom lemom. Ovaj 110 dokaz prolazi automatski primenom indukcije.› 111 112 lemma pripada_skup_sadrzi: 113 shows "a ∈ skup drvo ⟷ sadrzi drvo a" 114 by (induction drvo) auto 115 116 text‹Raspisaćemo i dokaz u isar-u uz pomoć indukcije. Razmatramo dva slučaja, 117 prvo slučaj praznog drveta pa onda slučaj nepraznog drveta. Slučaj praznog drveta 118 ima obe strane koje su netačne pa su samim tim i ekvivalentne 119 (@{text‹sadrzi Null x = (x ∈ skup Null))›}. A induktivni korak ima dve induktivne 120 hipoteze, zato što definicija drveta ima dva rekurzivna poziva, pa induktivne 121 hipoteze odgovaraju pretpostavkama za levo, odnosno za desno poddrvo. › 122 123 lemma pripada_skup_sadrzi_isar: 124 shows "a ∈ skup drvo ⟷ sadrzi drvo a" 125 proof (induction drvo) 126 case Null 127 show ?case by simp ― ‹obe strane su netačne pa su ekvivalentne› 128 next 129 case (Cvor l x d) ― ‹menjamo imena drvo1 i drvo2 sa l i d, zbog čitljivosti› 130 then have "a ∈ skup (Cvor l x d) ⟷ a ∈ skup l ∪ {x} ∪ skup d" 131 by simp ― ‹na osnovu definicije funkcije skup› 132 also have "... ⟷ a ∈ skup l ∨ a = x ∨ a ∈ skup d" 133 by auto ― ‹na osnovu osobine unije› 134 also have "... ⟷ sadrzi l a ∨ a = x ∨ sadrzi d a" 135 using Cvor 136 by simp ― ‹na osnovu induktivne hipoteze› 137 also have "... ⟷ sadrzi (Cvor l x d) a" 138 by auto ― ‹na osnovu definicije funkcije sadrzi› 139 finally show ?case . 140 qed 141 142 subsection‹Implementacija obilaska stabla› 143 144 text‹Redosled obilaska drveta može biti: infiksni redosled (LKD), prefiksni 145 redosled (KLD) i postfiksni redosled (LDK), gde su velikim slovima označena Levo 146 podstablo, Desno podstablo, i Koren stabla.› 147 148 subsubsection‹Neefikasna implementacija› 149 150 text‹ 151 \begin{exmp} 152 Definisati funkciju koja od elemenata drveta kreira listu koja se dobija 153 infiksnim obilaskom drveta. 154 \end{exmp} 155 156 Prilikom kreiranja liste sa desne strane se koristi nadovezivanje listi 157 operatorom @{text ‹append›} tako da se element koji se nalazi u korenu drveta 158 pretvara u listu stavljanjem u okviru uglastih zagrada. Primetimo da funkciju ne 159 možemo nazvati @{text ‹infix›} jer je to rezervisana ključna reč u isabelle-u. I 160 ova funkcija se može napraviti za proizvoljni tip drveta i to bi se uradilo na 161 isti način. › 162 163 primrec infiks :: "nat Drvo ⇒ nat list" where 164 "infiks Null = []" | 165 "infiks (Cvor l v d) = (infiks l) @ [v] @ (infiks d)" 166 167 value "infiks test_drvo" ―‹testiramo funkciju infiks› 168 169 text‹Na efikasnost ove funkcije utiču funkcije koje se javljaju u njenoj 170 definiciji. Pošto se koristi operacija @{text ‹append›} koja je linearna po 171 dužini liste, za svaki element stabla očekujemo kvadratnu složenost ovog 172 algoritma. Postavlja se pitanje da li je moguće napraviti efikasniju 173 implementaciju - što ćemo i uraditi kasnije. Prvo ćemo proveriti neka svojstva 174 ovako definisane funkcije funkcije.› 175 176 subsubsection‹Dokaz korektnosti› 177 178 text‹Da bismo dokazali da je implementacija obilaska stabla koju smo napisali 179 korektna potrebno je dokazati određena svojstva koja važe za tu funkciju.› 180 181 text‹Dokazati da je skup svih elemenata liste koja se dobija infiksnim obilaskom 182 jednak skupu svih elemenata drveta:› 183 184 lemma set_infiks_skup [simp]: 185 "set (infiks drvo) = skup drvo" 186 by (induction drvo) auto 187 188 text‹Primetimo da ovakvo slično tvrđenje važi i ako se koristi 189 @{text ‹multiskup›}. Da bi se koristili multiskupovi potrebno je uključiti 190 biblioteku \emph{Multiset}. Na taj način pored funkcije set dobijamo i funkciju mset:› 191 192 term mset 193 value "mset [1::nat, 3, 1, 2, 1]" 194 195 text‹Napisati funkciju koja određuje multiskup elemenata drveta. I ova funkcija 196 se može zapisati za proizvoljan tip drveta. Ugrađena konstanta koja označava 197 prazan multiskup se zapisuje @{text ‹{#}›}. Simbol unije za multiskup je 198 @{text ‹+›}. Kreiranje jednočlanog multiskupa od korenog elementa v se radi 199 naredbom \verb!{#v#}!.› 200 201 primrec multiskup :: "nat Drvo ⇒ nat multiset" where 202 "multiskup Null = {#}" | 203 "multiskup (Cvor l v d) = multiskup l + {#v#} + multiskup d" 204 205 text‹Dokazati da je multiskup liste dobijene infiksnim obilaskom jednak 206 multiskupu svih elemenata drveta:› 207 208 lemma mset_infiks_multiskup [simp]: 209 "mset (infiks drvo) = multiskup drvo" 210 by (induction drvo) auto 211 212 subsubsection‹Efikasna implementacija obilaska stabla› 213 214 text‹Pokušaćemo da implementiramo optimizovanu verziju funkcije za infiksni 215 obilazak stabla. Želimo da izbegnemo operaciju @{text ‹append›} koja u sebi 216 koristi dodavanje elementa na kraj liste. 217 218 Da bi implementacija bila najefikasnija moguća potrebno je da koristimo samo 219 operaciju dodavanja elementa na početak liste. Operacija dodavanja na početak je 220 efikasna operacija zbog toga što su liste interno u funkcionalnim programskim 221 jezicima implementirane kao jednostruko povezane liste i dodavanje na početak se 222 radi u konstantnom vremenu, za razliku od dodavanja elementa na kraj liste koje 223 se izvršava u linearnom vremenu (i zavisi od dužine liste). 224 225 Da bismo mogli ovu funkciju da implementiramo na ovako opisan način (korišćenjem 226 samo funkcije dodavanja elementa na početak liste) trebaće nam dodatni parametar 227 u kome ćemo malo po malo akumulirati rezultat. Slično kao što smo radili kada smo 228 pisali funkciju za efikasno obrtanje elemenata liste. 229 230 Funkcija @{text ‹infiks_opt›} će imati isti potpis kao funkcija @{text ‹infiks›} 231 i služice kao omotač glavnoj rekurzivnoj funkciji @{text ‹infiks_opt'›} i 232 pozivaće je sa prosleđenom praznom listom kao drugi argument. Naša glavna 233 funkcija neće biti primitivno rekurzivna. Pomoćna funkcija će biti primitivno 234 rekurzivna (i njena struktura će odgovarati strukturi drveta) i imaće kao drugi 235 argument listu u kojoj se akumulira rezultat. 236 237 Ovde moramo da vodimo računa o redosledu kojim se primenjuju operacije. Želimo 238 infiksni obilazak i jedino imamo na raspolaganju operaciju nadovezivanja na 239 početak liste i rekurzivni poziv. Pošto je u pitanju infiksan obilazak stabla, 240 koje odgovara (L)evom podstablu (K)orenu (D)esnom podstablu i sve to treba 241 dopisati na akumuliranu listu $xs$, čitamo rekurzivni poziv zdesna na levo: 242 prvo treba da primenimo rekurzivni poziv na desno podstablo i listu $xs$, nakon 243 toga dopišemo na početak rezultujuće liste koreni element $v$ i tako dobijenu 244 listu prosledimo kao drugi argument drugom rekurzivnom pozivu u kojem će dopisati 245 levo podstablo originalnog drveta na nju.› 246 247 primrec infiks_opt' :: "nat Drvo ⇒ nat list ⇒ nat list" where 248 "infiks_opt' Null xs = xs" | 249 "infiks_opt' (Cvor l v d) xs = infiks_opt' l (v # infiks_opt' d xs)" 250 251 definition infiks_opt :: "nat Drvo ⇒ nat list" where 252 "infiks_opt drvo = infiks_opt' drvo []" 253 254 value "infiks_opt test_drvo" ―‹testiramo optimizovanu verziju› 255 256 subsubsection ‹Dokaz korektnosti optimizovane verzije› 257 258 text‹Princip koji je ovde opisan se često primenjuje kod verifikacije koda. Uvek 259 je lakše definisati jednostavniju neefikasnu verziju, za koju je lakše dokazati 260 potrebna svojstva. Nakon toga, kada definišemo efikasniju implementaciju, 261 dovoljno je pokazati ekvivalentnost sa osnovnom neefikasnom implementacijom i 262 onda znamo da važe sva svojstva koja smo dokazali za neefikasnu implementaciju.› 263 264 text‹ 265 \begin{exmp} 266 Dokazati da su osnovna i optimizovana verzija ekvivalentne. 267 \end{exmp} 268 269 Dokaz kreće od 1.0. Pogledajte ispod. 270 271 Automatski dokaz, indukcijom i auto ne prolazi. Razlog za to je što definicije 272 date primitivnom rekurzijom ulaze u proces simplifikacije ali definicije date 273 ključnom rečju @{text ‹definition›} ne ulaze u proces simplifikacije, pa takve 274 definicije moraju ručno da se raspišu ili makar dodaju simplifikatoru. Naredba 275 @{text ‹unfolding infiks_opt_def›} će raspisati definiciju funkcije @{text 276 ‹infiks_opt›} i pojaviće se funkcija @{text ‹infiks_opt'›}. 277 278 Kada nakon toga ponovo poku[amo da primenimo auto, vidimo da smo stigli do nekih 279 osobina samo funkcije @{text ‹infiks_opt'›} pa moramo da formulišemo pomoćnu lemu 1.1.› 280 281 text‹Primetimo da je formulacija pomoćne leme uopštena, iako se u narednom dokazu 282 koristi funkcija @{text ‹infiks_opt'›} samo sa praznom listom kao drugi argument, 283 formulisaćemo je opštije sa proizvoljnim argumentom xs. Vidimo da primena 284 indukcije i automatskog dokazivača staje u trenutku kada dokazivač menja drugi 285 argument funkcije @{text ‹infiks_opt'›}. Slično kao u primeru sa obrtanjem 286 elemenata liste, da bi bila dozvoljena promena argumenta moramo upotrebiti 287 ključnu reč @{text ‹arbitrary›} i pokušavamo ponovo. 288 289 Primetimo da je u ovom dokazu svejedno da li ćemo navesti i za promenljivu ys da 290 bude proizvoljna jer se njena vrednost ne menja u toku izvršavanja dokaza.› 291 292 ― ‹1.1› 293 lemma infiks_opt'_append: 294 shows "infiks_opt' drvo xs @ ys = infiks_opt' drvo (xs @ ys)" 295 ― ‹apply (induction drvo)› 296 ― ‹apply auto› 297 apply (induction drvo arbitrary: xs) 298 apply auto 299 done 300 301 ― ‹Krećemo odavde 1.0!› 302 ― ‹Prilikom testiranja koda skinite komentare nad svim komandama koje su korišćene› 303 lemma infiks_infiks_opt[code]: 304 ― ‹[code] označava da se prilikom generisanja koda koristi efikasnija verzija› 305 shows "infiks drvo = infiks_opt drvo" 306 apply (induction drvo) 307 ― ‹apply auto› 308 ― ‹ne zna da raspiše definiciju @{text ‹infiks_opt›}, pa je ručno raspetljavamo› 309 unfolding infiks_opt_def 310 ― ‹apply auto› 311 ― ‹automatski dokazivač je stao kod izraza oblika› 312 ― ‹@{text ‹infiks_opt' drvo [] @ _ = infiks_opt' drvo _›} 313 pa formulišemo dodatnu lemu 1.1. koja kombinuje funkciju @{text ‹infiks_opt'›} i 314 funkciju append i dodajemo je automatskom dokazivaču› 315 apply (auto simp add: infiks_opt'_append) 316 done 317 318 319 text‹Ova dva dokaza se mogu kraće zapisati na naredni način: 320 321 \begin{footnotesize} 322 \begin{verbatim} 323 lemma infiks_opt'_append: 324 shows "infiks_opt' drvo xs @ ys = infiks_opt' drvo (xs @ ys)" 325 by (induction drvo arbitrary: xs ys) auto 326 327 lemma infiks_infiks_opt[code]: 328 shows "infiks drvo = infiks_opt drvo" 329 by (induction drvo) (auto simp add: infiks_opt'_append) 330 \end{verbatim} 331 \end{footnotesize} 332 › 333 334 text‹Dokaze ovih dveju lema možemo raspisati i u Isar-u da vidimo šta se tačno 335 dešava u pozadini. 336 337 Kada dođemo do trenutka da želimo da primenimo induktivnu hipotezu, treba da 338 izvučemo nekako ili prvi ili drugi deo induktivne pretpostavke. Za drugi deo bi 339 nam bilo potrebno da nekako izvučemo deo koji se tiče desnog poddrveta (označenog 340 sa d), odnosno @{text ‹infiks_opt' d xs›} iz zagrade; a za prvi deo nam treba 341 @{text ‹infiks_opt' l xs›}, ali levo poddrvo se kombinuje sa drugom listom. 342 343 Možemo da zaključimo da je ovako formulisana induktivna hipoteza preslaba i da ne 344 možemo da primenimo ni jedan korak dalje pa moramo da ojačamo induktivnu hipotezu 345 zato što je ona trenutno tačna za fiksirane xs i ys (u okviru jednog koraka). 346 Preciznije, ono što je nama ovde dovoljno jeste da ova induktivna hipoteza vazi 347 za proizvoljno xs i ys i koristi se ugrađeni mehanizam isabelle-a 348 @{text ‹arbitrary›}. 349 350 Dodavanjem ključne reči @{text ‹arbitrary›} u dokazu teoreme, kada uđemo u korak 351 koji se dokazuje indukcijom, možemo primetiti da su xs i ys proizvoljni (što 352 isabelle označava znakom pitanja ispred naziva promenljive - naspram oznaka za xs 353 i ys u prethodnom dokazu). Sada se moze primeniti prvi deo induktivne hipoteze.› 354 355 lemma infiks_opt'_append_isar: 356 shows "infiks_opt' drvo xs @ ys = infiks_opt' drvo (xs @ ys)" 357 ― ‹proof (induction drvo)› 358 ― ‹prvo pokrenite ovaj dokaz sa običnom indukcijom, pa onda sa narednom naredbom:› 359 proof (induction drvo arbitrary: xs ys) 360 case Null 361 then show ?case by simp 362 next 363 case (Cvor l x d) 364 have "infiks_opt' (Cvor l x d) xs @ ys = infiks_opt' l (x # infiks_opt' d xs) @ ys" 365 by simp ― ‹na osnovu definicije @{text ‹infiks_opt'›}› 366 also have "... = infiks_opt' l (x # infiks_opt' d xs @ ys)" 367 using Cvor(1) 368 by simp ― ‹na osnovu prvog dela induktivne hipoteze, za levo podstablo› 369 also have "... = infiks_opt' l (x # infiks_opt' d (xs @ ys))" 370 using Cvor(2) 371 by simp ― ‹na osnovu drugo dela induktivne hipoteze, za desno podstablo› 372 also have "... = infiks_opt' (Cvor l x d) (xs @ ys)" 373 by simp ― ‹na osnovu definicije @{text ‹infiks_opt'›}› 374 finally show ?case 375 . 376 qed 377 378 text‹U drugom dokazu opet raspisujemo definiciju @{text ‹infiks_opt›}.› 379 380 lemma infiks_infiks_opt_isar: 381 shows "infiks drvo = infiks_opt drvo" 382 unfolding infiks_opt_def 383 proof (induction drvo) 384 case Null 385 then show ?case by simp 386 next 387 case (Cvor l x d) 388 have "infiks (Cvor l x d) = infiks l @ [x] @ infiks d" 389 by simp ― ‹na osnovu definicije funkcije infiks koja je deo simplifikatora› 390 also have "... = infiks_opt' l [] @ [x] @ infiks_opt' d []" 391 using Cvor 392 by simp ― ‹na osnovu oba dela induktivne hipoteze› 393 also have "... = infiks_opt' l [] @ (x # infiks_opt' d [])" 394 by simp ― ‹dodavanje jednočlane liste na početak druge liste se može uraditi tarabicom› 395 also have "... = infiks_opt' l ([] @ x # infiks_opt' d [])" 396 by (simp add: infiks_opt'_append) ― ‹na osnovu teoreme› 397 also have "... = infiks_opt' l (x # infiks_opt' d [])" 398 by simp ― ‹dodavanje prazne liste› 399 also have "... = infiks_opt' (Cvor l x d) []" 400 by simp ― ‹na osnovu definicije @{text ‹infiks_opt'›}› 401 finally show ?case 402 . 403 qed 404 405 406 text‹Provere radi, eksportujemo kod funkcije infiks u Haskell sledećom naredbom. 407 Rezultat se moze videti u fajlu @{text ‹Cas11_vezbe.hs›} koji se dobija kada se u 408 Output prozoru klikne na "See theory exports", i sa leve strane se izlaz može 409 naći u folderu "export1".› 410 411 export_code infiks_opt in Haskell 412 413 text‹Nakon što smo dokazali sve ove leme, mozemo smatrati da imamo verifikovan 414 kod. Ovim eksportovanjem dobijamo definiciju drveta u programskom jeziku Haskel i 415 implementaciju optimizovane funkcije za infiksan ispis. Ono što znamo sigurno 416 jeste da je ova funkcija korektna tj. da zadovoljava svojstva koja smo do sada 417 dokazali. 418 419 Ovo se može uraditi i za druge programske jezike (SML, Scala), i dobijamo 420 verifikovan kod bez bagova koji bezbedno moze da se integriše u neki drugi 421 projekat.› 422 423 export_code infiks_opt in Scala 424 425 subsection‹Pretrazivačko (sortirano) drvo› 426 427 text‹Precizna karakterizacija pretaživačkog (sortiranog) drveta: drvo je 428 sortirano ako i samo ako važi da je i levo i desno poddrvo sortirano i da je 429 koren drveta veći i jednak od svih elemenata iz levog poddrveta i manji ili 430 jednak od svih elemenata desnog poddrveta. 431 432 \begin{exmp} 433 Napisati funkciju koja proverava da li je dato drvo sortirano. 434 \end{exmp}› 435 436 primrec sortirano where 437 "sortirano Null ⟷ True" | 438 "sortirano (Cvor l v d) ⟷ sortirano l ∧ sortirano d ∧ 439 (∀ x ∈ skup l. x ≤ v) ∧ (∀ x ∈ skup d. v ≤ x)" 440 441 text‹Testiraćemo funkciju @{text ‹sortirano›} na starom primeru koji smo 442 koristili od ranije i na drvetu koje ima iste elemente ali raspoređene tako da 443 oblikuju sortirano stablo. 444 445 Primer nesortiranog i sortiranog drveta. 446 \begin{verbatim} 447 3 3 448 1 2 1 4 449 . . 4 3 . 2 3 . 450 . . . . . . . . 451 \end{verbatim} 452 › 453 value "test_drvo" 454 value "sortirano test_drvo" 455 value "infiks test_drvo" 456 457 definition test_drvo_sortirano :: "nat Drvo" where 458 "test_drvo_sortirano = Cvor (Cvor Null 1 (Cvor Null 2 Null)) 3 (Cvor (Cvor Null 3 Null) 4 Null)" 459 460 value "sortirano test_drvo_sortirano" 461 value "infiks test_drvo_sortirano" 462 463 text‹ 464 Možemo primetiti da funkcija @{text ‹sortirano›} dobro radi na ova dva primera 465 ali i da je lista koja se dobija funkcijom @{text ‹infiks›} sortirana, odnosno 466 nesortirana - u zavisnosti od toga kakvo je bilo polazno drvo. Ovo ćemo i 467 dokazati. 468 469 \begin{exmp} 470 Dokazati da se infiksnim obilaskom pretraživačkog drveta dobija sortirana lista. 471 \end{exmp} 472 473 U dokazu ove leme ćemo koristiti @{text ‹sledgehammer›} da nam pomogne da nađemo 474 pomoćne leme koje se koriste u dokazu. Te leme se tiču listi, a o njima već znamo 475 jako puno pa nema potrebe da mi sami dokazujemo nove leme u ovom slučaju. 476 477 Već je ranije rečeno, ali podsetimo se da se @{text ‹sledgehammer›} ne može 478 upotrebiti za pronalaženje dokaza koji koriste indukciju, tako da kao prvi korak 479 mi sami primenimo indukciju. Nakon toga ponovo treba biti obazriv jer ako 480 pozovemo odmah @{text ‹sledgehammer›} on će biti primenjen samo na prvi cilj, 481 odnosno na bazu indukcije što najčešće ne želimo. Tako da ćemo i drugi korak mi 482 sami napisati i pokušati sa automatskim dokazivačem koji uspešno rešava prvi 483 cilj. Nakon toga nam ostaje induktivni korak koji je malo komplikovaniji.› 484 485 lemma sortirano_sorted_infiks: 486 assumes "sortirano drvo" 487 shows "sorted (infiks drvo)" 488 using assms 489 apply (induction drvo) 490 apply auto 491 ― ‹rešava prvi podcilj, ali ne i drugi pa primenjujemo sledgehammer› 492 ― ‹sledgehammer› 493 using sorted_append by fastforce 494 495 text ‹Ovaj dokaz se uspešno završio sa predlogom koji nam je dao 496 @{text ‹sledgehammer›}, ali je korišćen @{text ‹fasforce›}. Vežbe radi, 497 pogledajmo šta se dešava u pozadini i kakav bismo dokaz dobili ako bismo 498 koristili @{text ‹auto›} umesto toga. 499 500 Ponavljamo dokaz iste leme, s tim što smo lemu koju je @{text ‹sledgehammer›} 501 našao prosleđujemo uz @{text ‹auto›}. Nakon toga ćemo opet pokušati sa 502 @{text ‹sledgehammer›}-om i dobiti još jednu lemu koja je korišćena u dokazu.› 503 504 lemma sortirano_sorted_infiks': 505 assumes "sortirano drvo" 506 shows "sorted (infiks drvo)" 507 using assms 508 apply (induction drvo) 509 apply (auto simp add: sorted_append) 510 ― ‹sledgehammer› 511 using le_trans by blast 512 513 text‹Napomena, do ovog zaključka smo mogli i sami da dođemo ako bismo pogledali 514 šta se dešava sa dokazivačem nakom primene automatskog dokazivača @{text ‹auto›}. 515 Sistem se zaustavio na koraku oblika \verb!sorted (_ @ _)! pa možemo iskoristiti 516 naredbu @{text ‹find_theorems›} da pronađemo odgovarajuću teoremu, 517 @{text ‹sorted_append:›} @{thm[mode=Proof] sorted_append [no_vars]}. Nakon toga 518 ako ponovo pogledamo gde se dokazivač zaustavio, vidimo da je u pitanju 519 tranzitivnost operacije poređenja @{text ‹≤›} što je sadržano u lemi 520 @{text ‹le_trans:›} @{thm[mode=Proof] le_trans [no_vars]}.› 521 522 find_theorems "sorted (_ @ _)" 523 thm sorted_append 524 525 thm le_trans 526 527 lemma sortirano_sorted_infiks'': 528 assumes "sortirano drvo" 529 shows "sorted (infiks drvo)" 530 using assms 531 apply (induction drvo) 532 apply (auto simp add: sorted_append) 533 apply (auto simp add: le_trans) 534 done 535 536 text ‹ili skraćeno:› 537 538 lemma sortirano_sorted_infiks''': 539 assumes "sortirano drvo" 540 shows "sorted (infiks drvo)" 541 using assms 542 by (induction drvo) (auto simp add: sorted_append le_trans) 543 544 text‹ 545 \begin{exmp} 546 Napisati funkciju koja ubacuje element u pretraživačko drvo. 547 \end{exmp} › 548 549 primrec ubaci :: "nat ⇒ nat Drvo ⇒ nat Drvo" where 550 "ubaci v Null = (Cvor Null v Null)" | 551 "ubaci v (Cvor l v' d) = 552 (if v ≤ v' then 553 Cvor (ubaci v l) v' d 554 else 555 Cvor l v' (ubaci v d))" 556 557 text‹ 558 \begin{exmp} 559 Dokazati da nakon ubacivanja elementa x drvo sadrži element x. 560 \end{exmp} 561 562 Napomena: U ovim dokazima, alternativa tome da leme klasifikujemo kao 563 simplifikatorske ključnom rečju @{text ‹[simp]›} koju pišemo odmah nakon naziva 564 leme, jeste da ih eksplicitno navodimo kao što smo radili na prethodnim 565 časovima.› 566 567 lemma sadrzi_ubaci [simp]: 568 shows "sadrzi (ubaci x drvo) x" 569 by (induction drvo) auto 570 571 text‹ 572 \begin{exmp} 573 Dokazati da se skup, multiskup i zbir elemenata drveta uvećavaju za element x 574 nakon ubacivanja x u drvo. 575 \end{exmp}› 576 577 lemma skup_ubaci [simp]: 578 shows "skup (ubaci x drvo) = {x} ∪ skup drvo" 579 by (induction drvo) auto 580 581 lemma multiskup_ubaci[simp]: 582 shows "multiskup (ubaci x drvo) = {#x#} + (multiskup drvo)" 583 by (induction drvo) auto 584 585 lemma zbir_ubaci [simp]: 586 shows "zbir (ubaci x drvo) = x + zbir drvo" 587 by (induction drvo) auto 588 589 text‹ 590 \begin{exmp} 591 Dokazati da funkcija @{text ‹ubaci›} očuvava sortiranost drveta. 592 \end{exmp}› 593 594 lemma sortirano_ubaci [simp]: 595 assumes "sortirano drvo" 596 shows "sortirano (ubaci x drvo)" 597 using assms 598 by (induction drvo) auto 599 600 601 text‹Nakon što smo dokazali ovu lemu možemo iskoristiti funkciju @{text ‹ubaci›} 602 za kreiranje sortiranog drveta na osnovu elemenata liste: › 603 604 primrec listaUDrvo :: "nat list ⇒ nat Drvo" where 605 "listaUDrvo [] = Null" | 606 "listaUDrvo (x # xs) = ubaci x (listaUDrvo xs)" 607 608 value "listaUDrvo [3, 4, 7, 2, 1, 6]" ― ‹testiramo funkciju listaUDrvo› 609 610 text‹Dokazati da se skup elemenata nije promenio, tj. da je skup elemenata drveta 611 dobijenog od liste jednak skupu elemenata liste. Isto to pokazati i za multiskup 612 i za zbir.› 613 614 lemma [simp]: "skup (listaUDrvo xs) = set xs" 615 by (induction xs) auto 616 617 lemma [simp]: "multiskup (listaUDrvo xs) = mset xs" 618 by (induction xs) auto 619 620 lemma [simp]: "zbir (listaUDrvo xs) = sum_list xs" 621 by (induction xs) auto 622 623 text‹Dokazati da je ovako kreirano drvo pretraživačko drvo.› 624 625 lemma [simp]: "sortirano (listaUDrvo xs)" 626 by (induction xs) auto 627 628 text‹Sve do sada kreirane funkcije i dokazane leme nam omogućavaju da opišemo 629 \emph{TreeSort} postupak sortiranja lista tako što od elemenata liste formiramo 630 drvo, pa ga infiksno obidjemo.› 631 632 definition sortiraj :: "nat list ⇒ nat list" where 633 "sortiraj xs = infiks (listaUDrvo xs)" 634 635 text‹ Testiramo funkciju sortiraj › 636 value "sortiraj [3, 4, 7, 2, 1, 6]" 637 638 text‹ Eksportujemo kod u Haskell › 639 export_code sortiraj in Haskell 640 641 text‹Dokazati da je ovako kreirana lista sortirana, tj. dokazati da funkcija 642 sortiraj daje sortiranu listu. › 643 644 theorem "sorted (sortiraj xs)" 645 unfolding sortiraj_def 646 by (simp add: sortirano_sorted_infiks) 647 648 text‹Dokazati da funkcija sortiraj čuva skup elemenata liste i multiskup 649 elemenata liste. › 650 theorem "set (sortiraj xs) = set xs" 651 unfolding sortiraj_def 652 by simp 653 654 theorem "mset (sortiraj xs) = mset xs" 655 unfolding sortiraj_def 656 by simp 657 658 text‹Napisati funkciju koja određuje maksimalni element neuređenog drveta - 659 primer funkcije koja nije definisana primitivnom rekurzijom. 660 661 Ako funkcija koju definišemo nema strogo podeljene slučajeve prazne liste 662 @{text ‹([])›} i liste koja ima makar jedan element @{text ‹(x1 # xs)›} onda ne 663 možemo da koristimo primitivnu rekurziju. 664 665 Napomena: U ovom primeru se koristi konstrukcija @{text ‹fun›} koja je mnogo 666 naprednija konstrukcija od @{text ‹primrec›} i podržava generalnu rekurziju. 667 Kod @{text ‹primrec›} zaustavljanje automatski sledi, a kod @{text ‹fun›} se mora 668 dokazati zaustavljanje (i to se najčešće radi automatski, korišćenjem ugrađenog 669 termination checker-a). Pogledajte izlaz u isabelle-u, ispisaće: \emph{Found 670 termination order}. U opštem slučaju, zaustavljanje se dokazuje pokazivanjem da 671 su argumenti rekurzivnih poziva na neki način manji od originalnih argumenata. U 672 ovom poglavlju ćemo se ograničiti na funkcije za koje isabelle može sam 673 automatski da dokaže zaustavljanje.› 674 675 fun maks :: "nat Drvo ⇒ nat" where 676 "maks (Cvor Null v Null) = v" 677 | "maks (Cvor l v Null) = max (maks l) v" 678 | "maks (Cvor Null v d) = max v (maks d)" 679 | "maks (Cvor l v d) = 680 (let maksl = maks l; 681 maksd = maks d 682 in max (max maksl v) maksd)" 683 684 value "maks (listaUDrvo [3, 4, 1, 7, 6, 3, 2])" ―‹ testiramo funkciju maks › 685 686 text‹ Korektnost funkcije maks - dokaz ostavljamo za kasnije › 687 declare [[quick_and_dirty=true]] 688 lemma 689 assumes "sortirano drvo" "drvo ≠ Null" 690 shows "∀ x ∈ skup drvo. maks drvo ≥ x" 691 using assms 692 sorry 693 694 section‹Zadaci za vežbanje› 695 696 subsection‹Provera da li je lista sortirana› 697 698 text‹Definisaćemo slične funkcije za rad sa listama zato što su liste 699 jednostavniji tip podataka i pokazaćemo nekoliko lema čiji dokazi će biti 700 jednostavniji nego sa stablima. 701 702 \begin{exmp} 703 Definisati naše funkcije koje određuju prvi, odnosno poslednji element liste. 704 \end{exmp} 705 › 706 707 primrec glava :: "nat list ⇒ nat" where 708 "glava (x1 # xs) = x1" 709 710 primrec kraj :: "nat list ⇒ nat" where 711 "kraj (x1 # xs) = (if xs = [] then x1 else kraj xs)" 712 713 text‹ 714 \begin{exmp} 715 Definisati našu funkciju koja proverava da li je lista sortirana. 716 \end{exmp} 717 718 Lista je sortirana (rastuce) ako i samo ako je sortiran rep liste i ako je njen 719 prvi element manji ili jednak od svih ostalih elemenata liste. Pošto imamo 720 pretpostavku da je rep liste takođe sortiran onda je dovoljno da prvi element 721 liste bude manji ili jednak od glave repa liste. U ovoj definiciji možemo 722 koristiti našu funkciju:› 723 724 primrec sortirana' :: "nat list ⇒ bool" where 725 "sortirana' [] ⟷ True" | 726 "sortirana' (x1 # xs) ⟷ sortirana' xs ∧ (if xs = [] then True else x1 ≤ glava xs)" 727 728 text‹Drugi način je da koristimo ugrađenu funkciju @{text ‹hd›} koja vraća prvi 729 element liste i kvantifikator kojim ćemo opisati da je prvi element liste manji 730 ili jednak od svih elemenata koji se nalaze u repu:› 731 732 term hd 733 734 primrec sortirana :: "nat list ⇒ bool" where 735 "sortirana [] ⟷ True" | 736 "sortirana (x1 # xs) ⟷ sortirana xs ∧ (∀ x ∈ set xs. x1 ≤ x)" 737 738 value "sortirana [1,2,3]" 739 value "sortirana [2,1,3]" 740 741 text‹Sada ćemo dokazati da je u sortiranoj listi prvi element liste manji ili 742 jednak od svih ostalih elemenata liste. 743 744 Kako glava liste ne postoji za prazne liste, pretpostavka da je lista sa kojom 745 radimo neprazna mora biti eksplicitno dodata prilikom formulisanja naredne leme. 746 Ovaj dokaz automatski prolazi.› 747 748 lemma sortirana_glava_najmanja: 749 assumes "xs ≠ []" "sortirana xs" 750 shows "∀ x ∈ set xs. hd xs ≤ x" 751 using assms 752 apply (induction xs) 753 apply auto 754 done 755 756 text‹Pogledajmo kako bi izgledao dokaz ove leme kada bi se koristila prva 757 definicija, gde se upoređuje prvi element liste. Iskoristićemo sledgehammer i 758 primetimo da je dokaz znatno komplikovaniji zato što više odstupamo od 759 kvantifikatora nego što je neophodno. Tako da nadalje nećemo koristiti prvu 760 definiciju funkcije sortirano nego samo drugu.› 761 762 lemma sortirana_glava_najmanja_def': 763 assumes "xs ≠ []" "sortirana' xs" 764 shows "∀ x ∈ set xs. hd xs ≤ x" 765 using assms 766 apply (induction xs) 767 apply auto 768 by (metis glava.simps le_trans list.discI list.sel(1) list.set_cases) 769 770 text‹Potrebno je dokazati i da su ove dve definicije ekvivalentne (uz pomoć 771 sledgehammer-a:› 772 773 lemma "sortirana xs ⟷ sortirana' xs" 774 apply (induction xs) 775 apply auto 776 apply (metis glava.simps list.collapse list.set_sel(1)) 777 by (metis glava.simps le_trans list.sel(1) list.set_cases sortirana_glava_najmanja_def') 778 779 text‹Možemo sada formulisati sledeće tvrđenje koje se odnosi samo na liste koje 780 imaju makar jedan element:› 781 782 lemma sortirana_Cons: 783 "sortirana (x # xs) ⟷ sortirana xs ∧ (∀ x' ∈ set xs. x ≤ x')" 784 by (induction xs) auto 785 786 text‹Sada ako bismo želeli da dokažemo ovu lemu u isaru, granaćemo po slučajevima 787 da li je xs prazna ili neprazna lista. Iskomentarisaćemo detaljno samo prvu granu 788 dokaza.› 789 790 lemma sortirana_Cons_isar: 791 "sortirana (x # xs) ⟷ sortirana xs ∧ (∀ x' ∈ set xs. x ≤ x')" 792 proof (cases "xs = []") 793 case True 794 thus ?thesis 795 by simp 796 next 797 case False 798 show ?thesis 799 proof ― ‹pustićemo dokazivač da ekvivalenciju razbije na dve implikacije› 800 assume "sortirana (x # xs)" 801 hence "sortirana xs" "x ≤ hd xs" ― ‹na osnovu definicije sortirana, kako je 802 x manji ili jednak od svakog elementa liste xs, biće manji ili jednak od prvog 803 elementa u listi› 804 using `xs ≠ []` 805 by simp_all 806 ― ‹primenjujemo @{text ‹simp_all›} zato što imamo dva cilja u ovom koraku› 807 ― ‹da smo koristili definiciju sa funkcijom @{text ‹glava›} ovaj korak ne bi 808 prošao, lakše je nekada sa kvantifikatorima› 809 hence "∀ x' ∈ set xs. hd xs ≤ x'" 810 ― ‹na osnovu ranije dokazane leme, glava neprazne liste je manja ili jednaka od 811 svih njenih elemenata› 812 using sortirana_glava_najmanja[of xs] `xs ≠ []` 813 ― ‹instanciranje ove leme nije neophodno, dodato je samo zbog čitljivosti› 814 by simp 815 ― ‹sada znamo da je x manji ili jednak od prvog elementa od xs, i da je prvi 816 element od xs manji ili jednak od svih elemenata liste xs; 817 na osnovu tranzitivnosti operacije manje ili jednako možemo da zaključimo da je x 818 manji ili jednak od svih elemenata liste xs› 819 hence "∀ x' ∈ set xs. x ≤ x'" 820 using `x ≤ hd xs` 821 by auto 822 thus "sortirana xs ∧ (∀ x' ∈ set xs. x ≤ x')" 823 using `sortirana xs` 824 by simp 825 next 826 ― ‹druga grana dokaza› 827 assume "sortirana xs ∧ (∀ x' ∈ set xs. x ≤ x')" 828 hence "sortirana xs ∧ x ≤ hd xs" 829 using `xs ≠ []` 830 by simp 831 thus "sortirana (x # xs)" 832 using sortirana_glava_najmanja[of xs] `xs ≠ []` 833 by auto 834 qed 835 qed 836 837 838 text‹ 839 \begin{exmp} 840 Dokazati da se nadovezivanjem dveju sortiranih listi dobija sortirana lista ako i 841 samo ako je svaki element prve liste manji ili jednak od svakog elementa druge liste. 842 \end{exmp}› 843 844 lemma sortirana_append: 845 "sortirana (xs @ ys) ⟷ sortirana xs ∧ sortirana ys ∧ 846 (∀ x ∈ set xs. ∀ y ∈ set ys. x ≤ y)" 847 apply (induction xs) 848 apply auto 849 done 850 851 text‹I odgovarajući dokaz u isar-u:› 852 853 lemma sortirana_append_isar: 854 "sortirana (xs @ ys) ⟷ sortirana xs ∧ sortirana ys ∧ 855 (∀ x ∈ set xs. ∀ y ∈ set ys. x ≤ y)" 856 proof (induction xs) 857 case Nil 858 thus ?case 859 by simp 860 next 861 case (Cons x xs) 862 show ?case 863 proof (cases "xs = []") 864 case True 865 thus ?thesis 866 using sortirana_Cons[of x ys] 867 by simp 868 next 869 case False 870 show ?thesis 871 proof- 872 have "sortirana ((x # xs) @ ys) ⟷ 873 sortirana (x # (xs @ ys))" 874 by simp 875 also have "... ⟷ sortirana (xs @ ys) ∧ (∀ x' ∈ set (xs @ ys). x ≤ x')" 876 using sortirana_Cons[of x "xs @ ys"] 877 by simp 878 also have "... ⟷ sortirana xs ∧ sortirana ys ∧ (∀ x' ∈ set xs. ∀ y ∈ set ys. x' ≤ y) ∧ (∀ x' ∈ set (xs @ ys). x ≤ x')" 879 using Cons 880 by simp 881 also have "... ⟷ (sortirana xs ∧ (∀ x' ∈ set xs. x ≤ x')) ∧ sortirana ys ∧ (∀x∈set (x # xs). ∀y∈set ys. x ≤ y)" 882 by auto 883 also have "... ⟷ sortirana (x # xs) ∧ sortirana ys ∧ (∀x∈set (x # xs). ∀y∈set ys. x ≤ y)" 884 using sortirana_Cons[of x xs] 885 by simp 886 finally 887 show ?thesis 888 . 889 qed 890 qed 891 qed 892 893 subsection ‹Rotiranje drveta› 894 895 text‹Pod rotiranim drvetom podrazevamo drvo sa istim elementima kao polazno drvo, 896 s tim što su elementi u novom drvetu raspoređeni tako da odgovaraju slici u 897 ogledalu početnom drvetu (postavljenom sa strane). 898 899 \begin{exmp} 900 Definisati funkciju koja rotira drvo i dokazati da se dvostrukim rotiranjem 901 dobija originalno drvo. Napisati i automatski i isar dokaz. 902 \end{exmp}› 903 904 primrec mirror :: "'a Drvo ⇒ 'a Drvo" where 905 "mirror Null = Null" | 906 "mirror (Cvor l v d) = Cvor (mirror d) v (mirror l)" 907 908 lemma mirror_id: "mirror (mirror t) = t" 909 apply (induction t) 910 apply auto 911 done 912 913 lemma mirror_id_isar: "mirror (mirror t) = t" 914 proof (induction t) 915 case Null 916 show ?case by simp 917 next 918 case (Cvor t1 x2 t2) 919 have "mirror (mirror (Cvor t1 x2 t2)) = mirror (Cvor (mirror t2) x2 (mirror t1))" by simp 920 also have "... = Cvor (mirror (mirror t1)) x2 (mirror (mirror t2))" by simp 921 also have "... = Cvor t1 x2 t2" using Cvor by simp 922 finally show ?case . 923 qed 924 925 text‹ 926 \begin{exmp} 927 Definisati funkciju koja pravi od drveta listu dobijenu postfiksnim obilaskom 928 drveta i funkciju koja pravi od drveta listu dobijenu prefiksnim obilaskom 929 drveta. 930 931 Dokazati da se prefiksnim obilaskom rotiranog stabla dobija obrnuta lista u 932 odnosu na postfiksni obilazak originalnog stabla. 933 \end{exmp}› 934 935 primrec prefiks :: "nat Drvo ⇒ nat list" where 936 "prefiks Null = []" | 937 "prefiks (Cvor l v d) = [v] @ prefiks l @ prefiks d" 938 939 primrec postfiks :: "nat Drvo ⇒ nat list" where 940 "postfiks Null = []" | 941 "postfiks (Cvor l v d) = postfiks l @ postfiks d @ [v]" 942 943 text‹ 944 \begin{verbatim} 945 3 3 946 1 2 2 1 947 . . 4 3 3 4 . . 948 . . . . . . . . 949 \end{verbatim} 950 › 951 952 value "test_drvo" 953 value "prefiks test_drvo" 954 value "mirror test_drvo" 955 value "prefiks (mirror test_drvo)" 956 value "postfiks test_drvo" 957 value "rev (postfiks test_drvo)" 958 value "rev (postfiks test_drvo) = prefiks (mirror test_drvo)" 959 960 lemma prefiks_mirror_postfiks: 961 shows "prefiks (mirror t) = rev (postfiks t)" 962 apply (induction t) 963 apply auto 964 done 965 966 text‹Raspisati i dokaz u Isar-u.› 967 968 lemma prefiks_mirror_postfiks_isar: 969 shows "prefiks (mirror t) = rev (postfiks t)" 970 proof (induction t) 971 case Null 972 show ?case by simp 973 next 974 case (Cvor l x d) 975 have " prefiks (mirror (Cvor l x d)) = prefiks (Cvor (mirror d) x (mirror l))" 976 by simp ― ‹na osnovu definicije mirror› 977 also have "... = [x] @ prefiks (mirror d) @ prefiks (mirror l)" 978 by simp ― ‹na osnovu definicije prefiks› 979 also have "... = [x] @ rev (postfiks d) @ rev (postfiks l)" 980 using Cvor 981 by simp ― ‹na osnovu induktivne pretpostavke, obe grane se koriste› 982 also have "... = [x] @ rev (postfiks l @ postfiks d)" 983 by simp ― ‹na osnovu osobina listi› 984 also have "... = rev [x] @ rev (postfiks l @ postfiks d)" 985 by simp ― ‹na osnovu osobina listi› 986 also have "... = rev (postfiks l @ postfiks d @ [x])" 987 by simp ― ‹na osnovu osobina listi› 988 also have "... = rev (postfiks (Cvor l x d))" 989 by simp ― ‹na osnovu definicije postfiks› 990 finally show ?case 991 . 992 qed 993 end