1 sectionDefinisanje 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 textAko 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 textPrimeri 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 textDa 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 textSada 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 textSada ć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 textVeza 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 textRaspisać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 (@{textsadrzi 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 subsectionImplementacija obilaska stabla
 143 
 144 textRedosled 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 subsubsectionNeefikasna 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 textNa 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 subsubsectionDokaz korektnosti
 177 
 178 textDa 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 textDokazati 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 textPrimetimo 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 textNapisati 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 textDokazati 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 subsubsectionEfikasna implementacija obilaska stabla
 213 
 214 textPokuš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 textPrincip 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 textPrimetimo 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 textOva 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 textDokaze 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 textU 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 textProvere 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 textNakon š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 subsectionPretrazivačko (sortirano) drvo
 426 
 427 textPrecizna 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 textTestirać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 textNapomena, 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 textNakon š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 textDokazati 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 textDokazati da je ovako kreirano drvo pretraživačko drvo.
 624 
 625 lemma [simp]: "sortirano (listaUDrvo xs)"
 626   by (induction xs) auto
 627 
 628 textSve 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 textDokazati 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 textDokazati 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 textNapisati 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 sectionZadaci za vežbanje
 695 
 696 subsectionProvera da li je lista sortirana
 697 
 698 textDefinisać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 textDrugi 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 textSada ć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 textPogledajmo 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 textPotrebno 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 textMož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 textSada 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 textI 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 textPod 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 textRaspisati 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