1 theory Cas10_vezbe_resenja
   2 imports Main
   3 begin
   4 
   5 section‹Liste›
   6 
   7 text‹Isabelle ima ugrađeni tip @{text list}, čiji elementi se navode između 
   8 uglastih zagrada @{text ‹[›} i @{text ‹]›}. Ako bismo naveli samo elemente 
   9 @{text ‹[1,2,3]›} isabelle ne bi znao da odredi tip elementa tako da je potrebno 
  10 da navedemo tip za makar jedan element liste (i onda svi ostali elementi moraju 
  11 da budu istog tipa). Prazna lista se označava sa @{text ‹[]›}. Tip liste se može 
  12 navesti i nakon navođenja elemenata liste. ›
  13 
  14 term "[1,2,3]"
  15 term "[1::nat,2,3]"
  16 term "[1,2,3] :: nat list"
  17 term "[] :: nat list"
  18 
  19 text‹Neprazna lista se može navesti i svojim prvim elementom (glavom liste) iza 
  20 koga sledi rep liste. Oznaka operacije nadopisivanja elementa na početak liste je 
  21 @{text ‹#›}. Zapis u sledećem redu je skraćeni zapis za 
  22 @{text ‹(1 :: nat) # (2 # (3 # []))›}.›
  23 
  24 term "(1 :: nat) # [2,3]"
  25 
  26 subsection‹Predefinisan tip listi›
  27 
  28 text ‹
  29 Slično kao što smo radili sa tipom prirodnih brojeva, u isabelle-u imamo 
  30 mogućnost da definišemo novi tip podataka koji odgovara tipu listi, sa svim 
  31 potrebnim funkcijama i njihovim osobinama. Za razliku od ugrađenog tipa, za koji 
  32 su ova svojstva već dokazana, kada se radi sa ugrađenim tipovima na nama je da ta 
  33 svojstva formulišemo i dokažemo potrebna tvrđenja koja će obezbediti da sva 
  34 željena svojstva važe.
  35 
  36 Uvođenje novog algebarskog tipa podataka za definisanje listi se izvodi ključnom 
  37 rečju @{text ‹datatype›}. U narednom primeru listu definišemo ili kao praznu 
  38 listu ili kao listu kojoj na početak dodamo prirodan broj. Ovako definisana lista 
  39 može da sadrži samo prirodne brojeve:
  40 
  41 \begin{verbatim}
  42 datatype lista = Prazna | Dodaj nat lista
  43 term "Dodaj 1 (Dodaj 2 (Dodaj 3 Prazna))"
  44 \end{verbatim}
  45 ›
  46 
  47 text‹Ako bismo želeli da tip liste bude šablonski tip (slično generičkim klasama 
  48 u jeziku Java) a ne sa fiksiranim elementima (tipa @{typ nat}), lista se uvodi na 
  49 sledeći način. Moramo prvo navesti da je u pitanju lista elemenata tipa 
  50 @{text "'a"} (svi elementi liste moraju biti istog tipa). ›
  51 
  52 datatype 'a lista = Prazna | Dodaj 'a "'a lista" ― ‹lista koja može da sadrži 
  53 elemente proizvoljnog tipa›
  54 
  55 term "Dodaj (1 :: nat) (Dodaj 2 (Dodaj 3 Prazna))" ― ‹kreiranje liste, ovaj put 
  56 moramo (kao i sa ugrađenim listama) navesti tip makar jednog elementa liste›
  57 
  58 text‹Ugrađene liste su uvedene na isti način, sa tom razlikom što su dodate 
  59 skraćenice i notacije koje smo videli da se koriste sa listama uglaste zagrade 
  60 @{text ‹([])›} za zapisivanje prazne liste, taraba @{text ‹(#)›} za nadovezivanje 
  61 elementa na početak liste i skraćeni zapis za nadovezivanje više elemenata 
  62 @{text ‹[1,2,3]›}. Ovakve skraćenice je moguće dodati i za predefinisani tip 
  63 liste, na sličan način kao što je urađeno sa predefinisanim tipom prirodnih 
  64 brojeva.
  65 
  66 \textbf{Napomena}: Sve funkcije koje definišemo za predefinisane liste, možemo 
  67 definisati i za ugrađene liste i obratno. Zbog udobnosti zapisa, većinu lema koje 
  68 se tiču svojstava tih funkcija dokazivaćemo nad ugrađenim listama (iako bi dokazi 
  69 za predefinisane liste bili identični - njih možete uraditi za vežbu).
  70 
  71 \begin{exmp}
  72 Definisati funkciju koja računa dužinu liste. 
  73 \end{exmp}
  74 
  75 Kada je definisan algebarski tip podataka, funkcije za rad sa njim se definišu 
  76 primitivnom rekurzijom.
  77 
  78 \textbf{Napomena}: funkcije definisane nad predefinisanim tipom ćemo označiti 
  79 apostrofom nakon naziva funkcije (da bismo ih razlikovali od funkcija nad 
  80 ugrađenim tipom listi koje ćemo kasnije uvesti).›
  81 
  82 primrec duzina' :: "'a lista ⇒ nat" where 
  83 "duzina' Prazna = 0" |
  84 "duzina' (Dodaj x xs) = 1 + duzina' xs"
  85 
  86 value "duzina' (Dodaj (1 :: nat) (Dodaj 2 (Dodaj 3 Prazna)))" ― ‹izlaz: 3::nat›
  87 
  88 text‹\begin{exmp}
  89 Definisati funkciju koja formira novu listu nadovezivanjem dveju listi jedne na 
  90 drugu.
  91 \end{exmp}›
  92 
  93 primrec nadovezi' :: "'a lista ⇒ 'a lista ⇒ 'a lista" where
  94 "nadovezi' Prazna ys = ys" | 
  95 "nadovezi' (Dodaj x xs) ys = (Dodaj x (nadovezi' xs ys))"
  96 
  97 text‹\begin{exmp}
  98 Definisati funkciju koja formira novu listu obrtanjem elemenata date liste.
  99 \end{exmp}
 100 
 101 U definiciji ove funkcije možemo koristiti samo funkcije koje su do sada 
 102 definisane. Funkcija nadovezi' kao argumente prima dve liste, pa dodavanje 
 103 elementa x na kraj liste koja se dobija rekurzivnim pozivom 
 104 @{text ‹(obrni' xs)›}, se izvršava tako što se prvo formira lista koja sadrži 
 105 samo jedan element x dodavanjem elementa x na praznu listu 
 106 @{text ‹(Dodaj x Prazna)›}.›
 107 
 108 primrec obrni' :: "'a lista ⇒ 'a lista" where 
 109 "obrni' Prazna = Prazna" | 
 110 "obrni' (Dodaj x xs) = nadovezi' (obrni' xs) (Dodaj x Prazna)"
 111 
 112 term "Dodaj (1 :: nat) (Dodaj 2 (Dodaj 3 Prazna))"
 113 value "obrni' (Dodaj (1 :: nat) (Dodaj 2 (Dodaj 3 Prazna)))"
 114 
 115 subsection‹Definisanje funkcija nad ugrađenim tipom listi›
 116 
 117 text‹Na sličan način kao što smo definisali funkcije nad predefinisanim tipom 
 118 listi, možemo definisati nove funkcije i nad ugrađenim tipom listi (skoro 
 119 identično). Konstruktori se zovu @{text ‹Nil›} - prazna lista i @{text ‹Cons›} - 
 120 dodavanje elementa na početak liste. Svaka lista je onda oblika: @{text ‹Nil›}, 
 121 @{text ‹Cons x Nil›}, @{text ‹Cons y (Cons x Nil)›}, itd.
 122 
 123 \textbf{Napomena}: Većina svojstava će biti dokazana i automatski i u isar-u. 
 124 Tamo gde nedostaje isar dokaz možete ga sami raspisati za vežbu.
 125 
 126 \begin{exmp}
 127 Definisati funkciju koja računa dužinu liste i dokazati da je definisana funkcija 
 128 ista kao ugrađena funkcija.
 129 \end{exmp}›
 130 
 131 primrec duzina :: "'a list ⇒ nat" where 
 132 "duzina [] = 0" |
 133 "duzina (x # xs) = 1 + duzina xs"
 134 
 135 value "duzina ((1::nat) # (2 # (3 # [])))"
 136 value "duzina [1::nat, 2, 3]"
 137 
 138 text‹Ugrađena funkcija koja računa dužinu liste naziva se @{text ‹length›}.›
 139 
 140 value "length [1::nat, 2, 3]"
 141 
 142 text‹Dokaz standardno ide indukcijom, kao i za sve tipove i funkcije koje su 
 143 definisane primitivnom rekurzijom i pokušavamo prvo automatski, a nakon toga 
 144 raspisujemo dokaz u Isar-u.›
 145 
 146 lemma duzina_length:
 147   shows "duzina xs = length xs"
 148   by (induction xs) auto
 149 
 150 text ‹Dokaz u Isar-u koji počinje indukcijom se suštinski izvršava po dužini 
 151 liste, iako je dužina liste unapred nepoznata. Dokaz se automatski raspisuje na 
 152 dva slučaja @{text ‹Nil›} i @{text ‹Cons›}. Prvo razmatramo bazni slučaj prazne 
 153 liste i nakon toga listu koja ima makar jedan element. Da bismo dokazali da neko 
 154 svojstvo "P" važi za sve liste potrebno je da dokažemo:
 155 
 156 \begin{enumerate}
 157 \item bazni slučaj "P Nil" i 
 158 \item korak indukcije "P (Cons x xs)" pod pretpostavkom da važi "P xs", 
 159 za neke proizvoljne ali fiksirane x i xs.
 160 \end{enumerate}
 161 ›
 162 
 163 lemma duzina_length_isar:
 164   shows "duzina xs = length xs"
 165 proof (induction xs)
 166   case Nil 
 167   then show ?case 
 168     by simp ―‹prolazi automatski na osnovu definicije›
 169 next
 170   case (Cons a xs) ―‹induktivna hipoteza pretpostavlja da tvrđenje važi za xs, i 
 171 pokušavamo da dokažemo da važi za @{text ‹(a # xs)›}›
 172   have "duzina (a # xs) = 1 + duzina xs" ― ‹na osnovu definicije funkcije duzina›
 173     by simp
 174   also have "... = 1 + length xs" ―‹na osnovu induktivne hipoteze›
 175     using Cons by simp
 176   also have "... = length (a # xs)" ―‹na osnovu bibliotečke definicije length›
 177     by simp
 178   finally show ?case 
 179     .
 180 qed
 181 
 182 text‹\begin{exmp}
 183 Definisati funkciju @{text ‹prebroj›} koja prebrojava koliko puta se 
 184 traženi element nalazi u listi i dokazati da važi da je broj pojavljivanja 
 185 elementa u listi manji ili jednak od dužine cele liste.
 186 \end{exmp}
 187 
 188 U ovoj definiciji se koristi @{text ‹if-then-else›} konstrukt. On se navodi u 
 189 okviru običnih zagrada, i unutar samog izraza zagrade nisu neophodne.›
 190 
 191 primrec prebroj :: "'a list ⇒ 'a ⇒ nat" where 
 192 "prebroj [] a = 0" |
 193 "prebroj (x # xs) a = (if x = a then 1 + prebroj xs a else prebroj xs a)"
 194 
 195 lemma prebroj_duzina:
 196   shows "prebroj xs x ≤ duzina xs"
 197   by (induction xs) auto
 198 
 199 lemma prebroj_duzina_isar:
 200   shows "prebroj xs x ≤ duzina xs"
 201 proof (induction xs)
 202   case Nil
 203   then show ?case by simp
 204 next
 205   case (Cons a xs)
 206   show ?case 
 207   proof (cases "x = a") ― ‹razmatramo dokaz po slučajevima›
 208     case True
 209     then have "prebroj (a # xs) x = 1 + prebroj xs x" 
 210       by simp ― ‹definicija prebroj›
 211     also have "... ≤ 1 + duzina xs" 
 212       using Cons
 213       by simp ― ‹induktivna hipoteza›
 214     also have "... ≤ duzina (a # xs)"
 215       by simp ― ‹definicija duzine›
 216     finally show ?thesis
 217       .
 218   next
 219     case False
 220     then have "prebroj (a # xs) x = prebroj xs x" 
 221       by simp ― ‹definicija prebroj›
 222     also have "... ≤ duzina xs" 
 223       using Cons
 224       by simp ― ‹induktivna hipoteza›
 225     also have "... ≤ duzina (a # xs)"
 226       by simp ― ‹definicija duzine›
 227     finally show ?thesis
 228       .
 229   qed
 230 qed
 231 
 232 text‹\begin{exmp}
 233 Dokazati da je funkcija @{text ‹prebroj›} ekvivalentna ugrađenoj funkciji 
 234 koja broji koliko puta se element nalazi u listi @{text ‹count_list›}.
 235 \end{exmp}›
 236 
 237 value "count_list [1::nat, 2, 3, 1] 1"
 238 
 239 lemma prebroj_count_list:
 240   shows "prebroj xs x = count_list xs x"
 241   by (induction xs) auto
 242 
 243 text‹
 244 \begin{exmp}
 245 Definisati funkciju koja proverava da li data lista sadrži traženi element.
 246 Pokazati da odgovara ugrađenom mehanizmu koji je definisan u isabelle-u.
 247 \end{exmp}
 248 
 249 Definisaćemo je primitivnom rekurzijom na sledeći način.›
 250 
 251 primrec sadrzi :: "'a list ⇒ 'a ⇒ bool" where 
 252 "sadrzi [] a ⟷ False" |
 253 "sadrzi (x # xs) a ⟷ x = a ∨ sadrzi xs a"
 254 
 255 text‹Umesto uobičajenog znaka jednakosti koji smo do sada koristili stavićemo 
 256 simbol @{text ‹⟷›}. Kada radimo nad tipom @{typ bool} između ova dva simbola 
 257 (jednakost nad tipom bool i logicka ekvivalencija) nema razlike osim u prioritetu 
 258 operatora. Operator logičke ekvivalencije je operator najmanjeg prioriteta pa ne 
 259 zahteva zagrade sa desne strane druge jednakosti.›
 260 
 261 value "sadrzi [1::nat, 2, 3, 5] 3"
 262 value "sadrzi [1::nat, 2, 3, 5] 4"
 263 
 264 text‹Ne postoji ugrađena funkcija koja proverava da li data lista sadrži traženi 
 265 element. U isabelle-u ova provera se vrši tako što se napravi skup korišćenjem 
 266 funkcije @{text ‹set›} (koja za datu listu vraća skup njenih elemenata), a onda 
 267 se proveri pripadnost skupu:›
 268 
 269 value "5 ∈ set [1::nat, 2, 3, 5]"
 270 
 271 text‹Sada ćemo pokazati da funkcija koju smo mi definisali odgovara ovom mehanizmu.›
 272 
 273 lemma sadrzi_in_set:
 274   shows "sadrzi xs a ⟷ a ∈ set xs"
 275   by (induction xs) auto
 276 
 277 text‹
 278 \begin{exmp}
 279 Definisati funkciju koja vraća skup elemenata liste i pokazati da je ekvivalentna 
 280 ugrađenoj funkciji set.
 281 \end{exmp}›
 282 
 283 primrec skup :: "'a list ⇒ 'a set" where
 284 "skup [] = {}" |
 285 "skup (x # xs) = {x} ∪ skup xs"
 286 
 287 lemma skup_set:
 288   shows "skup xs = set xs"
 289   by (induction xs) auto
 290 
 291 text‹
 292 \begin{exmp}
 293 Definisati funkciju nadovezivanja dve liste i pokazati da je ekvivalentna 
 294 ugrađenoj funkciji @{text ‹append›} koja postoji u isabelle-u.
 295 \end{exmp}
 296 
 297 Biramo da primitivna rekurzija ide po prvom argumentu.
 298 ›
 299 
 300 primrec nadovezi :: "'a list ⇒ 'a list ⇒ 'a list" where
 301 "nadovezi [] ys = ys" | 
 302 "nadovezi (x # xs) ys = x # (nadovezi xs ys)"
 303 
 304 value "nadovezi [1::nat, 2, 3] [4, 5, 6]"
 305 
 306 text‹Funkcija @{text ‹append›} se zapisuje uz pomoć oznake @{text ‹@›}.›
 307 
 308 lemma nadovezi_append:
 309   shows "nadovezi xs ys = xs @ ys"
 310   by (induction xs) auto
 311 
 312 text‹Uopšteno gledano, nema smisla definisati funkcije koje već postoje u 
 313 biblioteci. Bolje je koristiti bibliotečke funkcije jer postoji već dosta lema 
 314 dokazanih o njima.›
 315 
 316 find_theorems "_ @ _"
 317 
 318 text‹Kada uvedemo naše funkcije, moramo dokazati da se dobro slažu sa već 
 319 ugrađenim funkcijama. 
 320 
 321 \begin{exmp}
 322 Dokazati da je dužina nadovezane liste jednaka zbiru dužina originalnih listi. 
 323 Prvo automatski pa onda u isar-u.
 324 \end{exmp}›
 325 
 326 lemma duzina_nadovezi:
 327   shows "duzina (nadovezi xs ys) = duzina xs + duzina ys"
 328   by (induction xs) auto
 329 
 330 lemma duzina_nadovezi_isar:
 331   shows "duzina (nadovezi xs ys) = duzina xs + duzina ys"
 332 proof (induction xs)
 333   case Nil ― ‹raspisaćemo korak po korak›
 334   have "duzina (nadovezi [] ys) = duzina ys" 
 335     by simp ―‹na osnovu definicije koja je automatski uključena u simp›
 336   also have "... = 0 + duzina ys" 
 337     by simp
 338   also have "... = duzina [] + duzina ys" 
 339     by simp ― ‹na osnovu definicije›
 340   finally show ?case 
 341     .
 342 next
 343   case (Cons a xs) ―‹krećemo od leve strane›
 344   have "duzina (nadovezi (a # xs) ys) = duzina (a # nadovezi xs ys)" 
 345     by simp ―‹na osnovu definicije nadovezi›
 346   also have "... = 1 + duzina (nadovezi xs ys)" 
 347     by simp ―‹na osnovu definicije duzina›
 348   also have "... = 1 + duzina xs + duzina ys"
 349     using Cons
 350     by simp ―‹na osnovu induktivne hipoteze›
 351   also have "... = duzina (a # xs) + duzina ys"
 352     by simp ―‹na osnovu definicije duzina›
 353   finally show ?case 
 354     .
 355 qed
 356 
 357 text‹
 358 \begin{exmp}
 359 Dokazati da je skup elemenata nadovezanih listi jednak uniji skupova elemenata 
 360 originalnih listi.
 361 \end{exmp}›
 362 
 363 lemma skup_nadovezi:
 364   shows "skup (nadovezi xs ys) = skup xs ∪ skup ys"
 365   by (induction xs) auto
 366 
 367 text‹
 368 \begin{exmp}
 369 Dokazati da se element nalazi u nadovezanoj listi ako i samo ako se nalazi makar 
 370 u jednoj od originalnih listi.
 371 \end{exmp}›
 372 
 373 lemma sadrzi_nadovezi:
 374   shows "sadrzi (nadovezi xs ys) a ⟷ sadrzi xs a ∨ sadrzi ys a"
 375   by (induction xs) auto
 376 
 377 text‹
 378 \begin{exmp}
 379 Prvi i poslednji element liste se dobijaju funkcijama @{text ‹hd›} i 
 380 @{text ‹last›}. Dokazati da važi @{text ‹hd (rev xs) = last xs›}
 381 \end{exmp}
 382 
 383 Prilikom formulisanja ove leme, neophodna je pretpostavka da je lista neprazna
 384 zato što je glava liste parcijalno definisana funkcija samo za neprazne liste.›
 385 
 386 lemma "xs ≠ [] ⟶ hd (rev xs) = last xs"
 387   by (induction xs) auto
 388 
 389 subsubsection ‹Obrtanje liste›
 390 
 391 text‹Definisati primitivnom rekurzijom funkciju koja obrće elemente liste. Ovu 
 392 funkciju definišemo pomoću funkcije @{text ‹nadovezi›} koja prima kao argumente 
 393 dve liste, pa se prvi element liste (koji se sada dodaje na kraj nove liste) mora 
 394 pretvoriti u listu (koja sadrži samo taj jedan element) @{text ‹[x]›}.›
 395 
 396 primrec obrni :: "'a list ⇒ 'a list" where 
 397 "obrni [] = []" | 
 398 "obrni (x # xs) = nadovezi (obrni xs) [x]"
 399 
 400 value "obrni [1::nat, 2, 3, 4]"
 401 
 402 text ‹Bibliotečka funkcija koja obrće listu zove se @{text ‹rev›}›
 403 
 404 value "rev [1::nat, 2, 3, 4]"
 405 
 406 text‹
 407 \begin{exmp}
 408 Dokazati da je definisana funkcija @{text ‹obrni›} ekvivalentna bibliotečkoj 
 409 funkciji obrni. 
 410 
 411 Sa ovom lemom automatski dokaz ne prolazi pa odmah pišemo raspisani isar dokaz.
 412 \end{exmp}›
 413 
 414 lemma obrni_rev:
 415   shows "obrni xs = rev xs"
 416 proof (induction xs)
 417   case Nil
 418   show ?case
 419     by simp
 420 next
 421   case (Cons a xs)
 422   then show ?case
 423 ― ‹apply simp›
 424 ― ‹kada pokušamo sa simp vidimo da nam je potrebna lema koja tvrdi da su funkcije 
 425 nadovezi i append jednake›
 426     by (simp add: nadovezi_append)
 427 qed
 428 
 429 text‹
 430 \begin{exmp}
 431 Dokazati da važi da se dvostrukim obrtanjem liste dobija početna lista
 432 \end{exmp}
 433 
 434 Prvi korak u dokazu (1.1) je svakako primena indukcije. Nakon toga pokušavamo sa 
 435 primenom automatskih metoda, ali vidimo da je u dokazu potrebna dodatna lema koju 
 436 formulišemo i pokusavamo da dokažemo (1.2). 
 437 
 438 Pratite brojeve lema u dokazu. Dokaz se ne čita linearno odozgo na dole, već 
 439 obratno.
 440 ›
 441 
 442 ― ‹1.4 dokaz ove leme prolazi automatski i vraćamo se na dokaz leme 
 443 @{text ‹obrni_nadovezi›} u kom sada dodajemo ovu lemu (nakon čega i taj dokaz 
 444 prolazi)›
 445 lemma nadovezi_desno_prazno:
 446   "nadovezi xs [] = xs"
 447   apply (induction xs)
 448   apply auto
 449   done
 450 
 451 ― ‹1.3 - dodajemo asocijativnost operacije nadoveži, čiji dokaz prolazi 
 452 automatski. Sada se vraćamo na dokaz leme @{text ‹obrni_nadovezi›} i posmatramo 
 453 šta se dešava sa automatskim dokazivačem kada mu damo na raspolaganje i ovu novu 
 454 lemu›
 455 lemma nadovezi_asoc:
 456   shows "nadovezi xs (nadovezi ys zs) = nadovezi (nadovezi xs ys) zs"
 457   apply (induction xs)
 458    apply auto
 459   done
 460 
 461 ―‹1.2 levu stranu leme dobijamo iz stanja u kom se automatski dokazivač nije 
 462 snašao, a desnu stranu sami formulišemo u skladu sa konkretnim funkcijama koje 
 463 koristimo›
 464 lemma obrni_nadovezi:
 465   shows "obrni (nadovezi xs ys) = nadovezi (obrni ys) (obrni xs)"
 466   apply (induction xs)
 467 ― ‹apply auto›
 468 ― ‹kada pokušamo sa auto vidimo da dokazivaču nedostaje informacija o tome da li 
 469 je operacija nadovezi asocijativna, pa formulišemo i dodajemo još jednu novu lemu 
 470 1.3›
 471    apply (auto simp add: nadovezi_asoc)
 472 ― ‹sada vidimo da je dokazivač stao na mestu kada funkcija nadovezi ima praznu 
 473 listu kao svoj drugi argument. Posto je funkcija nadovezi definisana rekurzivno 
 474 po prvom argumentu, dokazivač sam ne može da se snađe sa ovom situacijom pa 
 475 dodajemo novu lemu 1.4›
 476   apply (auto simp add: nadovezi_desno_prazno)
 477 ― ‹sada se vraćamo na dokaz leme @{text ‹obrni_obrni›}, koji nakon svih ovih 
 478 dodatih lema prolazi automatski›
 479   done
 480 
 481 ― ‹Odavde krećemo: 1.0›
 482 lemma obrni_obrni:
 483   shows "obrni (obrni xs) = xs"
 484   apply (induction xs) ― ‹1.1›
 485 ― ‹apply auto›
 486 ― ‹vidimo da dobijamo nešto oblika @{text ‹obrni (nadovezi _ _)›} pa formulisemo 
 487 i dodajemo novu lemu @{text ‹obrni_nadovezi›} 1.2›
 488    apply (auto simp add: obrni_nadovezi)
 489   done
 490 
 491 text‹Napomena: Kada bismo obrisali sav nepotreban tekst korišćen za potrebe 
 492 objašnjavanja dobili bismo naredni blok dokaza:
 493 
 494 \begin{footnotesize}
 495 \begin{verbatim}
 496 lemma nadovezi_desno_prazno:
 497   "nadovezi xs [] = xs"
 498   by (induction xs) auto
 499 
 500 lemma nadovezi_asoc:
 501   shows "nadovezi xs (nadovezi ys zs) = nadovezi (nadovezi xs ys) zs"
 502   by (induction xs) auto
 503 
 504 lemma obrni_nadovezi:
 505   shows "obrni (nadovezi xs ys) = nadovezi (obrni ys) (obrni xs)"
 506   by (induction xs) (auto simp add: nadovezi_asoc nadovezi_desno_prazno)
 507 
 508 lemma obrni_obrni:
 509   shows "obrni (obrni xs) = xs"
 510   by (induction xs) (auto simp add: obrni_nadovezi)
 511 \end{verbatim}
 512 \end{footnotesize}
 513 
 514 Alternativa korišćenju @{text ‹simp add›}, odnosno alternativa eksplicitnom 
 515 naglašavanju u svakom koraku koju lemu koristimo, jeste da koristimo operator 
 516 @{text ‹[simp]›} nakon imena lema koje se koriste u narednim dokazima i na taj 
 517 način dobijamo sledeći blok dokaza. 
 518 
 519 Ovako nešto možete koristiti na ispitu, i kada radite u svojim teorijama ali nije 
 520 preporučljivo koristiti u velikim fajlovima koji se koriste za pokazivanje 
 521 velikog skupa lema koje nisu sve obavezno iz iste grupe (kao što je ovaj 
 522 materijal koji se koristi kao deo skripte).
 523 
 524 \begin{footnotesize}
 525 \begin{verbatim}
 526 lemma nadovezi_desno_prazno [simp]:
 527   "nadovezi xs [] = xs"
 528   by (induction xs) auto
 529 
 530 lemma nadovezi_asoc [simp]:
 531   shows "nadovezi xs (nadovezi ys zs) = nadovezi (nadovezi xs ys) zs"
 532   by (induction xs) auto
 533 
 534 lemma obrni_nadovezi [simp]:
 535   shows "obrni (nadovezi xs ys) = nadovezi (obrni ys) (obrni xs)"
 536   by (induction xs) auto
 537 
 538 lemma obrni_obrni:
 539   shows "obrni (obrni xs) = xs"
 540   by (induction xs) auto 
 541 \end{verbatim}
 542 \end{footnotesize}
 543 ›
 544 
 545 subsubsection ‹Dodavanje elementa na kraj liste i obrtanje liste dodavanjem na kraj›
 546 
 547 text‹Definisati funkciju @{text ‹snoc›} koja dodaje element na kraj liste, i 
 548 rekurzivnu funkciju @{text ‹rev_snoc›} koja uz pomoć funkcije @{text ‹snoc›} 
 549 obrće elemente liste.›
 550 
 551 primrec snoc:: "'a list ⇒ 'a ⇒ 'a list" where
 552 "snoc [] x = (x # [])" |
 553 "snoc (x1 # xs) x = x1 # (snoc xs x)"
 554 
 555 primrec rev_snoc :: "'a list ⇒ 'a list" where
 556 "rev_snoc [] = [] " |
 557 "rev_snoc (x1 # xs) = snoc (rev_snoc xs) x1"
 558 
 559 text‹
 560 \begin{exmp}
 561 Pokazati da dvostrukim obrtanjem liste ovom funkcijom dobijamo originalnu listu.
 562 \end{exmp}›
 563 
 564 ― ‹2.1 leva strana ove leme se dobija iz dokazivača (na mestu gde je zablokirao) 
 565 a desnu stranu sami pokušavamo da formulisemo. Ovaj dokaz prolazi automatski.›
 566 lemma rev_snoc_snoc:
 567   shows "rev_snoc (snoc xs y) = y # rev_snoc xs"
 568   apply (induction xs)
 569    apply auto
 570   done
 571 
 572 ― ‹Krećemo odavde 2.0›
 573 lemma rev_snoc_rev_snoc:
 574   shows "rev_snoc (rev_snoc xs) = xs"
 575   apply (induction xs)
 576 ― ‹apply auto›
 577 ― ‹kada primenimo auto vidimo da dokazivač ne zna šta da radi sa kombinacijom 
 578 @{text ‹rev_snoc (snoc _ _)›} pa formulisemo lemu 2.1. Nakon njenog dodavanja, 
 579 dokaz prolazi.›
 580    apply (auto simp add: rev_snoc_snoc)
 581   done
 582 
 583 text‹Dokaz iste leme u isar-u:›
 584 
 585 lemma rev_snoc_rev_snoc_isar: "rev_snoc (rev_snoc xs) = xs" 
 586 proof (induction xs)
 587   case Nil
 588   then show ?case by simp
 589 next
 590   case (Cons x1 xs)
 591   have "rev_snoc (rev_snoc (x1 # xs)) = rev_snoc (snoc (rev_snoc xs) x1)"
 592     by (simp only: rev_snoc.simps)
 593   also have "... = x1 # rev_snoc (rev_snoc xs)" 
 594     by (simp only: rev_snoc_snoc)
 595   also have "... = x1 # xs" 
 596     using Cons 
 597     by simp
 598   finally show ?case .
 599 qed
 600 
 601 subsubsection ‹Obrtanje liste u linearnom vremenu›
 602 
 603 text ‹
 604 \begin{exmp}
 605 Definisati funkciju za obrtanje liste koja radi u linearnom vremenu i dokazati da 
 606 je ekvivalentna ugrađenoj funkciji @{text ‹rev›}.
 607 \end{exmp}
 608 
 609 Ugrađena funkcija obrtanja liste @{text ‹rev›} (kao i funkcija obrtanja
 610 liste koju smo mi definisali) ima kvadratnu složenost po dužini liste zato što 
 611 za svaki element liste ta funkcija poziva funkciju @{text ‹append›} koja je 
 612 linearna po prvom argumentu.
 613 
 614 Postoji mogućnost da se kreira linearna funkcija koja obrće datu listu, ali je 
 615 neophodno koristiti dodatni argument u kome će se postepeno akumulirati 
 616 rezultujuća lista.›
 617 
 618 fun itrev :: "'a list ⇒ 'a list ⇒ 'a list" where
 619 "itrev [] ys = ys" |
 620 "itrev (x # xs) ys = itrev xs (x # ys)"
 621 
 622 text‹Ova funkcija je definisana repnom rekurzijom, uzima jedan po jedan element 
 623 liste sa početka i dodaje ga na početak liste u kojoj se rezultat akumulira. U 
 624 slučaju kada se ova funkcija pozove sa praznom akumulacionom listom, dobićemo 
 625 listu sa istim elementima ali u obrnutom redosledu što ćemo i naknadno dokazati.
 626 
 627 Prvo moramo primetiti da dokaz te leme ne prolazi automatski. Razlog za to je što
 628 se u dokazu te leme javlja fiksirana promenljiva, tj. prazna lista, pa moramo 
 629 formulisati takvu istu teoremu ali sada sa opštom promenljivom.
 630 
 631 Problem koji se sada javlja jeste da automatski dokazivač ima potrebu da u dokazu 
 632 teoreme promeni drugi argument funkcije @{text ‹itrev›}. Da bi to bilo moguće 
 633 potrebno je dodati ključnu reč @{text ‹arbitrary›} ispred imena promenljive čiju
 634 promenu vrednosti želimo da dozvolimo. Sada će oba dokaza proći automatski.
 635 (notacija @{text ‹arbitrary: vars›} univerzalno kvantifikuje promenljive pre 
 636 primene indukcije).›
 637 
 638 lemma itrev_rev_append':
 639   shows "itrev xs ys = rev xs @ ys"
 640 ― ‹apply (induction xs) 
 641     apply auto›
 642 ― ‹prvo pokušamo ovako i ovo ne prolazi zato što je funkcija itrev definisana 
 643 tako da menja svoj drugi argument, a u indukciji je promenljiva ys fiksirana a 
 644 treba nam @{text ‹a # ys›}. Neophodno je koristiti generalizaciju tako da ovo 
 645 važi za svako ys. Ovakav efekat se postiže naredbom: ›
 646   apply (induction xs arbitrary: ys) 
 647   apply auto
 648   done
 649 
 650 text‹ili kraće:›
 651 
 652 lemma itrev_rev_append:
 653   shows "itrev xs ys = rev xs @ ys"
 654   by (induction xs arbitrary: ys) auto
 655 
 656 lemma "itrev xs [] = rev xs"
 657   by (induction xs) (auto simp add: itrev_rev_append)
 658 
 659 subsubsection ‹Funkcionali nad listama›
 660 
 661 text ‹Tri osnovna funkcionala nad listama u funkcionalnom programiranju su 
 662 @{text ‹map›}, @{text ‹filter›} i @{text ‹fold›}.›
 663 
 664 text‹\paragraph{Funkcija map}
 665 
 666 Funkcija @{text ‹map f xs ›} proizvodi listu koja se dobija kada se funkcija 
 667 @{text ‹f›} primeni na sve elemente liste @{text ‹xs›}: 
 668 @{text ‹map f [x1,...,xn] = [f x1,...,f xn]›} i definisana je na sledeći način:
 669 
 670 \begin{footnotesize}
 671 \begin{verbatim}
 672 fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
 673 "map f Nil = Nil" |
 674 "map f (Cons x xs) = Cons (f x ) (map f xs)"
 675 \end{verbatim}
 676 \end{footnotesize}
 677 
 678 \begin{exmp}
 679 Definisati funkciju @{text ‹preslikaj›} i dokazati da je ekvivalentna ugrađenoj funkciji.
 680 \end{exmp}
 681 ›
 682 
 683 term map
 684 value "map (λ x. x ^ 2) [1::nat, 2, 3, 4]"
 685 
 686 primrec preslikaj :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
 687 "preslikaj f [] = []" | 
 688 "preslikaj f (x # xs) = f x # preslikaj f xs"
 689 
 690 lemma preslikaj_map:
 691   shows "preslikaj f xs = map f xs"
 692   by (induction xs) auto
 693 
 694 text‹
 695 \begin{exmp}
 696 Definisati funkciju @{text ‹intersperse›} koja raspoređuje dati element iza 
 697 svakog elementa liste: 
 698 @{text ‹intersperse a [x1,...,xn] = [x1,a,x2,a,...,a,xn,a]›} i dokazati da važi 
 699 @{text ‹map f (intersperse a xs) = intersperse (f a) (map f xs)›}
 700 \end{exmp}›
 701 
 702 primrec intersperse :: "'a ⇒ 'a list ⇒ 'a list" where
 703 "intersperse x [] = []" |
 704 "intersperse x (x1 # xs) = x1 # x # intersperse x xs"
 705 
 706 value "intersperse (1::nat)(2 # 3 # 4 # [])"
 707 value "intersperse (1::nat)([])"
 708 value "intersperse (1::nat)(2 # [])"
 709 
 710 lemma "map f (intersperse x xs) = intersperse (f x) (map f xs)"
 711   by (induction xs) auto
 712 
 713 lemma map_isar: "map f (intersperse x xs) = intersperse (f x) (map f xs)"
 714 proof (induction xs)
 715   case Nil
 716   then show ?case by simp
 717 next
 718   case (Cons x1 xs)
 719   have "map f (intersperse x (x1 # xs)) = map f (x1 # x # intersperse x xs)" 
 720     by simp ― ‹definicija intersperse›
 721   also have "... = (f x1) # (f x) # map f (intersperse x xs)" 
 722     by simp ― ‹definicija map›
 723   also have "... = (f x1) # (f x) # intersperse (f x) (map f xs)" 
 724     using Cons by simp
 725   also have "... = intersperse (f x) ((f x1) # map f xs)" 
 726     by (simp only: intersperse.simps)
 727   also have "... = intersperse (f x) (map f (x1 # xs))"
 728     by simp ― ‹definicija map›
 729   finally show ?case .
 730 qed
 731 
 732 text‹
 733 \begin{exmp}
 734 Definisati funkciju @{text ‹intersperse_inside›} koja raspoređuje dati element 
 735 između elemenata liste: 
 736 @{text ‹intersperse_inside a [x1,...,xn] = [x1,a,x2,a,...,a,xn]›} i dokazati da važi 
 737 @{text ‹map f (intersperse_inside a xs) = intersperse_inside (f a) (map f xs)›}
 738 \end{exmp}
 739 
 740 Ova funkcija je za nijansu komplikovanija zato što moramo da vodimo računa o 
 741 specijalnom slučaju kada lista ima samo jedan element - u tom slučaju se lista 
 742 ne menja primenom ove funkcije. Proveru da li lista ima samo jedan element 
 743 ćemo izvršiti primenom @{text ‹if-then-else›} bloka u kom ćemo ispitati da li je
 744 rep liste prazan.›
 745 
 746 primrec intersperse_inside :: "'a ⇒ 'a list ⇒ 'a list" where
 747 "intersperse_inside a [] = []" |
 748 "intersperse_inside a (x1 # xs) = (if xs = [] then (x1 # []) else (x1 # a # (intersperse_inside a xs)))"
 749 
 750 value "intersperse_inside (1::nat)(2 # 3 # 4 # [])"
 751 value "intersperse_inside (1::nat)([])"
 752 value "intersperse_inside (1::nat)(2 # [])"
 753 
 754 lemma "map f (intersperse_inside x xs) = intersperse_inside (f x) (map f xs)"
 755   apply (induction xs)
 756 apply auto (* vidimo da se javlja map f xs = [] pa uvodimo dodatnu lemu --- iznad *)
 757 done
 758 
 759 text‹Iako smo dokazali da su @{text ‹map›} i @{text ‹preslikaj›} ekvivalentne 
 760 funkcije, pogledajmo šta bi se desilo ako bismo zamenili jednu sa drugom i dobili 
 761 lemu 3.0.
 762 
 763 Kada primenimo metod auto, nakon indukcije, vidimo da je dokazivač stao kod 
 764 koraka oblika \verb!f _ = []! pa formulišemu lemu sa premisom koja odgovara 
 765 tom šablonu i dodajemo narednu lemu. Pokušaćemo dokaz da granamo po slučajevima 
 766 i vidimo da automatski dokazivač uspeva da je dokaže.›
 767 
 768 ― ‹3.1›
 769 lemma preslikaj_u_praznu:
 770   shows "preslikaj f xs = [] ⟶ xs = []"
 771 apply (cases xs)
 772 apply auto
 773 done
 774 
 775 ― ‹ Krace zapisano:›
 776 lemma preslikaj_u_praznu': "map f xs = [] ⟹ xs = []"
 777 by (cases xs) auto
 778 
 779 ― ‹Odavde krećemo 3.0›
 780 lemma "preslikaj f (intersperse_inside x xs) = intersperse_inside (f x) (preslikaj f xs)"
 781   apply (induction xs)
 782 ― ‹apply auto›
 783 ― ‹vidimo da se javlja @{text ‹preslikaj f _ = []›} pa uvodimo dodatnu lemu 3.1 
 784 kada nju dodamo dokaz prolazi do kraja›
 785   apply (auto simp add: preslikaj_u_praznu)
 786 done
 787 
 788 text‹Ovo se desilo zato što, kao što smo ranije rekli, ugrađeni predikati imaju 
 789 veliki skup već dokazanih lema koje možemo koristiti praktično i ne znajući da 
 790 one postoje. U ovom dokazu smo istakli koja lema je korišćena i u prethodnom 
 791 primeru (sa @{text ‹map›}) iako je eksplicitno nismo videli.
 792 
 793 Dokaz početne leme, sa map, zapisan u Isar-u:›
 794 
 795 lemma map_inside_isar: "map f (intersperse_inside x xs) = intersperse_inside (f x) (map f xs)"
 796 proof (induction xs)
 797   case Nil
 798   show ?case by simp
 799 next
 800   case (Cons x1 xs)
 801   show ?case
 802   proof (cases "xs = []")
 803     case True
 804     thus ?thesis by simp
 805   next
 806     case False
 807     then have "map f (intersperse_inside x (x1 # xs)) = map f (x1 # x # intersperse_inside x xs)"
 808       by simp
 809     also have "... = f x1 # (map f (x # intersperse_inside x xs))" by simp
 810     also have "... = f x1 # (f x # (map f (intersperse_inside x xs)))" by simp
 811     also have "... = f x1 # (f x # (intersperse_inside (f x) (map f xs)))" 
 812       using Cons by simp
 813     also have "... = intersperse_inside (f x) (f x1 # (map f xs))" 
 814       using `xs ≠ []` by auto
 815     also have "... = intersperse_inside (f x) (map f (x1 # xs))" by simp
 816     finally show ?thesis .
 817   qed
 818 qed
 819 
 820 text‹\paragraph{Funkcija filter}
 821 
 822 Funkcija @{text ‹filter›} izdvaja sve elemente liste koji zadovoljavaju traženo svojstvo.
 823 Definiše se na sledeći način:
 824 
 825 \begin{footnotesize}
 826 \begin{verbatim}
 827 primrec filter:: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
 828 "filter P [] = []" |
 829 "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
 830 \end{verbatim}
 831 \end{footnotesize}
 832 ›
 833 
 834 term filter
 835 value "filter (λ x. x > 0) [-3::int, 4, 2, 0, 6, -1, 2]"
 836 
 837 text‹
 838 \begin{exmp}
 839 Definisati funkciju @{text ‹izdvoj›} i dokazati da je ekvivalentna ugrađenoj 
 840 funkciji.
 841 \end{exmp}
 842 ›
 843 
 844 primrec izdvoj :: "('a ⇒ bool) ⇒ 'a list ⇒ 'a list" where
 845 "izdvoj P [] = []" | 
 846 "izdvoj P (x # xs) = (if P x then x # izdvoj P xs else izdvoj P xs)"
 847 
 848 lemma izdvoj_filter:
 849   shows "izdvoj P xs = filter P xs"
 850   by (induction xs) auto
 851 
 852 text‹\paragraph{Familija funkcija fold}
 853 
 854 Funkcije tipa @{text ‹fold›} obrađuju dati skup podataka (elemente liste) u 
 855 određenom redosledu i kao rezultat vraćaju jedinstvenu vrednost. Kao argument im 
 856 se prosleđuje funkcija koja se primenjuje, lista nad čijim elementima 
 857 primenjujemo funkciju i početna vrednost. Funkcija koja se primenjuje ima dva 
 858 argumenta. U opštem slučaju takva funkcija nije asocijativna, tako da redosled 
 859 primene operacije može da utiče na konačni rezultat. Takođe, u opštem slučaju 
 860 tipovi argumenata takve funkcije ne moraju biti isti. 
 861 
 862 Ako operaciju primenimo na prvi element liste zajedno sa rezultatom koji se 
 863 dobije kada se operacija primeni na ostatak liste dobijamo desni fold 
 864 (\emph{foldr});
 865 
 866 ako operaciju primenimo na sve elemente liste sem poslednjeg pa je onda 
 867 iskombinujemo sa poslednjim elementom dobijamo levi fold (\emph{foldl});
 868 
 869 a ako operaciju prvo primenimo na prvi element liste, pa taj rezultat 
 870 iskombinujemo sa drugim elementom liste, pa taj rezultat iskombinujemo sa trećim
 871 elementom liste, itd. dobijamo običan fold (\emph{fold}).
 872 
 873 Inicijalna vrednost koja se zadaje uz ove funkcije se koristi za kombinovanje 
 874 sa prvim ili poslednjim elementom liste (u zavisnosti koji tip fold funkcije 
 875 se odabere.
 876 
 877 U slučaju funkcije sabiranja koja je asocijativna i ima isti tip svojih 
 878 argumenata, nema razlike u ponašanju ovih funkcija. Rezultat sve tri naredne 
 879 operacije je isti i iznosi 6.›
 880 
 881 term fold
 882 value "fold (+) [1, 2, 3::nat] 0"
 883 term foldl
 884 value "foldl (+) 0 [1, 2, 3::nat]"
 885 term foldr
 886 value "foldr (+) [1, 2, 3::nat] 0"
 887 
 888 text‹Kada ne znamo kako je definisana funkcija možemo videti kako isabelle
 889 tretira naredne izraze:›
 890 
 891 value "fold f [1::nat, 2, 3] a"   ― ‹f 3 (f 2 (f 1 a))›
 892 value "foldl f a [1::nat, 2, 3]"  ― ‹f (f (f a 1) 2) 3›
 893 value "foldr f [1::nat, 2, 3] a"  ― ‹f 1 (f 2 (f 3 a))›
 894 
 895 text‹Što se može i videti kroz neke od ugrađenih lema vezanih za ove funkcije:›
 896 
 897 lemma "fold f [a,b,c] x = f c (f b (f a x))" 
 898   by simp
 899 
 900 lemma "foldr f [a,b,c] x = f a (f b (f c x))"
 901   by simp
 902 
 903 lemma "foldl f x [a,b,c] = f (f (f x a) b) c"
 904   by simp
 905 
 906 text‹
 907 \begin{exmp}
 908 Definisati odgovarajuće korisničke funkcije i dokazati da su ekvivalentne 
 909 ugrađenim funkcijama.
 910 \end{exmp}
 911 ›
 912 
 913 primrec agregiraj :: "('a ⇒ 'b ⇒ 'b) ⇒ 'a list ⇒ 'b ⇒ 'b" where
 914 "agregiraj f [] b = b" | 
 915 "agregiraj f (x # xs) b = agregiraj f xs (f x b)"
 916 
 917 lemma agregiraj_fold:
 918   shows "agregiraj f xs b = fold f xs b"
 919   by (induction xs arbitrary: b) auto
 920 
 921 primrec agregirajl :: "('a ⇒ 'b ⇒ 'a) ⇒ 'a ⇒ 'b list ⇒ 'a" where
 922 "agregirajl f b [] = b" | 
 923 "agregirajl f b (x # xs) = agregirajl f (f b x) xs"
 924 
 925 lemma agregirajl_foldl:
 926   shows "agregirajl f b xs = foldl f b xs"
 927   by (induction xs arbitrary: b) auto
 928 
 929 primrec agregirajr :: "('a ⇒ 'b ⇒ 'b) ⇒ 'a list ⇒ 'b ⇒ 'b" where
 930 "agregirajr f [] b = b" | 
 931 "agregirajr f (x # xs) b = f x (foldr f xs b)"
 932 
 933 lemma
 934   shows "agregirajr f xs b = foldr f xs b"
 935   by (induction xs) auto
 936 
 937 
 938 end