1 theory Cas14_vezbe_resenja
   2   imports Complex_Main "HOL-Library.Code_Target_Nat" "HOL-Library.Multiset"
   3 
   4 begin
   5 
   6 section ‹Aksiomatsko zasnivanje teorija, korišćenje lokala›
   7 
   8 text ‹Aksiomatsko rezonovanje, koje smo navikli da viđamo u matematici, ima
   9 svoje primene i u verifikaciji softvera. Jedan deo formalne semantike
  10 programskih jezika se obrađuje aksiomatskim pristupom. Pod ovim se podrazumeva
  11 definisanje svojstava funkcije, odnosno \emph{dovoljnih uslova} koje funkcija
  12 treba da ispunjava i nezavisno dokazivanje teorema koje opisuju ta svojstva uz
  13 pomoć interaktivnih i automatskih dokazivača teorema.›
  14 
  15 text ‹U ovom poglavlju ćemo prikazati primenu aksiomatskog metoda u razvoju
  16 formalno verifikovanog softvera. Korektnost sofvera je lakše dokazati ako se
  17 razvija korak po korak, umesto odjednom. Prvo kreiramo specifikaciju programa i
  18 program koji neke detalje ostavlja nerazrešenim i ostavljamo njihovu
  19 implementaciju za kasnije dok ne dođemo do konačne izvršive verzije.
  20 
  21 Ovaj pristup se naziva razvoj softvera profinjavanjem \emph{eng: refinement}
  22 (izučava se od 70-tih godina), i nije ograničen na formalno verifikovanje
  23 softvera. Krećemo od glavne funkcije na veoma apstraktnom nivou i specifikujemo
  24 sve više i više detalja softvera dok ne dođemo do konačne verzije.
  25 
  26 Pogledaćemo kako izgleda ovaj pristup na primeru implementacije funkcije
  27 sortiranja objedinjavanjem koji je obrađen u materijalu iz (pretprošlog)
  28 poglavlja \ref{rekurzija}.›
  29 
  30 subsection ‹Sortiranje objedinjavanjem›
  31 
  32 text ‹Ponovimo prvo definiciju funkciju objedinjavanja dve sortirane liste, i
  33 svojstva koja ta funkcija mora da zadovoljava:›
  34 
  35 fun spoji :: "nat list ⇒ nat list ⇒ nat list" where
  36 "spoji [] ys = ys" | 
  37 "spoji xs [] = xs" | 
  38 "spoji (x # xs) (y # ys) = 
  39     (if x ≤ y then
  40         x # spoji xs (y # ys)
  41      else
  42         y # spoji (x # xs) ys)"
  43 
  44 value "spoji [2, 5, 8, 13] [1, 3, 9, 34, 40]"
  45 
  46 text‹Ponavljamo dokaze da su multiskup i skup očuvani, kao i da je rezultujuća
  47 lista sortirana. Pošto smo prve dve leme dodali u simplifikator, treća lema
  48 prolazi automatski.›
  49 
  50 lemma mset_spoji[simp]:
  51   shows "mset (spoji xs ys) = mset xs + mset ys"
  52   by (induction xs ys rule: spoji.induct, auto)
  53 
  54 lemma set_spoji[simp]:
  55   shows "set (spoji xs ys) = set xs ∪ set ys"
  56   by (induction xs ys rule: spoji.induct, auto)
  57   
  58 lemma sorted_spoji [simp]:
  59   assumes "sorted xs" "sorted ys"
  60   shows "sorted (spoji xs ys)"
  61   using assms
  62   by (induction xs ys rule: spoji.induct) auto
  63 
  64 text‹Prilikom implementacije sortiranja objedinjavanjem koristiće se ova
  65 funkcija. Međutim, u funkciji sortiranja prvi korak je deljenje liste na dva
  66 dela, nakon čega sledi rekurzivno sortiranje ta dva dela i nakon toga sledi
  67 objedinjavanje funkcijom koja spaja dve sortirane liste.
  68 
  69 Zbog efikasnosti koda, ta dva dela liste bi trebala da budu jednake dužine. Ali,
  70 primetimo da je ova pretpostavka o dužinama ta dva dela liste vezana samo za
  71 efikasnost sortiranja ali ne i za korektnost funkcije sortiranja.
  72 
  73 Sada je na redu korak u kome treba da implementiramo neki algoritam deljenja
  74 originalne liste na dve liste. Postoji više načina kako to možemo da uradimo:
  75 npr. prva polovina liste i druga polovina liste, ili elementi na neparnim i
  76 elementi na parnim pozicijama i slično. Međutim, ispostavlja se da pitanje
  77 deljenja liste na dve liste, odnosno sam izbor algoritma za deljenje na dve
  78 liste možemo ostaviti za kasnije. Za sada je potrebno da primetimo da je
  79 neophodno da algoritam deljenja liste ima naredne dve osobine:
  80 
  81 ▪ korektnost - da je podela na dve liste urađena tako da su tačno svi elementi
  82 liste raspoređeni u njih i,
  83 
  84 ▪ zaustavljanje - da su obe nove liste kraće od polazne liste.›
  85 
  86 text‹Ove osobine deljenja liste ćemo nadalje nazivati aksiome.
  87 
  88 Pre nego što preciziramo algoritam deljenja, možemo dokazati malo jači oblik
  89 funkcije sortiranja objedinjavanjem. Dokazaćemo korektnost funkcije
  90 objedinjavanja u odnosu na apstraktnu funkciju podele liste na dva dela.
  91 Funkciju podele na dve liste ćemo zadati apstraktno pomoću njene specifikacije.
  92 
  93 Koristimo nov koncept \emph{lokala} (engl. locale) - to je skup konstanti,
  94 odnosno skup pojedinačnih elemenata nekog tipa ili funkcije. Prilikom zadavanja
  95 lokala, prvo se fiksiraju određeni elementi nakon čega se navode njihove osobine
  96 kroz navođenje nekih aksioma. U narednom lokalu ćemo fiksirati funkciju
  97 \emph{split} (ključnom rečju \verb!fixes!) koja od date liste pravi uređeni par
  98 listi. Nakon ovoga zadajemo aksiome (ključnom rečju \verb!assumes!) koje moraju
  99 da važe da bi algoritam sortiranja objedinjavanjem koji koristi ovu funkciju
 100 \emph{split} mogao da se isprogramira. To su aksiome koje obezbeđuju korektnost
 101 algoritma i njegovo zaustavljanje.
 102 
 103 Umesto običnog univerzalnog kvantifikatora @{text ‹(∀)›}, implikacije @{text
 104 ‹(⟶)›} i konjunkcije @{text ‹(∧)›} koristimo veznike meta-logike i Isabelle
 105 sintaksa zapisa @{text ‹(⋀)›}, @{text ‹(⟹)›} i @{text ‹(⟦, ⟧)›}, zbog kasnijeg
 106 lakšeg instanciranja ovih aksioma.
 107 
 108 Pošto se lista deli na polovine samo ako ima više od jednog elementa, dovoljno
 109 je zahtevati da ove aksiome važe samo za takve liste, pa uslov da je dužina
 110 liste veća od 1 stavljamo u premise obe aksiome.
 111 
 112 Nakon navođenja aksioma, između ključnih reči \verb!begin! i \verb!end! navodi
 113 se blok koji sadrži lokalne definicije i teoreme i u kome smemo da koristimo
 114 aksiome koje su uvedene. Na ovom mestu se definiše algoritam sortiranja
 115 objedinjavanjem. Kako nam u algoritmu treba poređenje elemenata, da bismo
 116 pojednostavili primer zapisaćemo definiciju za liste prirodnih brojeva. Ova
 117 definicija i dokaz korektnosti je isti kao u prošlom poglavlju pa ga nećemo
 118 ponovo objašnjavati.›
 119 
 120 
 121 locale MergeSort = 
 122 ― ‹prvo se navode konstante›
 123   fixes split :: "nat list ⇒ nat list × nat list"
 124 ― ‹pa onda aksiome›
 125   assumes split_length:
 126      "⋀ xs ys zs. ⟦length xs > 1; (ys, zs) = split xs⟧ ⟹ 
 127                      length ys < length xs ∧ length zs < length xs"
 128   assumes split_mset: 
 129      "⋀ xs ys zs. ⟦length xs > 1; (ys, zs) = split xs⟧ ⟹ 
 130                      mset xs = mset ys + mset zs"
 131 
 132 ― ‹Između begin i end uvode se lokalne definicije i dokazuju se lokalna tvrđenja
 133 (u njima mogu da se koriste konstante i aksiome lokala).› 
 134 
 135 begin
 136 
 137 function (sequential) mergesort :: "nat list ⇒ nat list" where
 138 "mergesort [] = []" | 
 139 "mergesort [x] = [x]" | 
 140 "mergesort xs = 
 141     (let (ys, zs) = split xs 
 142       in spoji (mergesort ys) (mergesort zs))"
 143   by pat_completeness auto
 144 termination
 145   apply (relation "measure (λ xs. length xs)")
 146     apply simp
 147    apply (metis One_nat_def in_measure length_Cons lessI linorder_not_less list.size(4) split_length trans_le_add2)
 148   apply (metis One_nat_def impossible_Cons in_measure linorder_not_less list.size(4) split_length trans_le_add2)
 149   done
 150 
 151 ―‹Unutar lokala ne možemo pozvati funkciju \emph{mergesort} jer funkcija
 152 \emph{split} nije definisana. Ali možemo pokazati da važe još neke osobine te
 153 funkcije: da se mset ne menja i da je rezultujuća lista sortirana:›
 154 
 155 lemma mset_mergesort_auto:
 156   "mset (mergesort xs) = mset xs"
 157   apply (induction xs rule: mergesort.induct) 
 158   apply simp
 159    apply simp
 160     apply (auto split: prod.split)
 161   ― ‹sledgehammer›
 162   by (metis (mono_tags, hide_lams) One_nat_def Suc_eq_plus1 length_Cons 
 163   less_Suc_eq_0_disj mset.simps(2) mset_append split_mset zero_less_Suc)
 164 
 165 lemma mset_mergesort:
 166   "mset (mergesort xs) = mset xs"
 167 proof (induction xs rule: mergesort.induct) 
 168   case 1
 169   then show ?case
 170     by simp
 171 next
 172   case (2 x)
 173   then show ?case
 174     by simp
 175 next
 176   case (3 x0 x1 xs)
 177   then show ?case
 178     using split_mset[of "x0 # x1 # xs"]
 179     by (simp split: prod.split)
 180 qed
 181 
 182 lemma sorted_mergesort:
 183   "sorted (mergesort xs)"
 184   by (induction xs rule: mergesort.induct) (auto split: prod.split)
 185 end
 186 
 187 text‹Dokazali smo da je funkcija mergesort korektna ako funkcija \verb!split!
 188 zadovoljava navedene aksiome koje su ekspliticno navedene u prethodnom lokalu.
 189 Primetimo da je ovo urađeno bez implementacije funkcije \verb!split!. U ovom
 190 trenutku imamo slobodu da razrešimo detalje te implementacije.
 191 
 192 Sada ćemo prikazati dve različite implementacije funkcije \verb!split!.›
 193 
 194 subsubsection ‹Razdvajanje uzimanjem prve i druge polovine niza›
 195 
 196 text‹Naredna funkcija izdvaja, na osnovu dužine liste, prvu polovinu odnosno
 197 drugu polovinu liste.›
 198 
 199 definition split_half :: "nat list ⇒ nat list × nat list" where
 200   "split_half xs = (let n = length xs div 2 in (take n xs, drop n xs))"  
 201 
 202 value "split_half [3::nat, 4, 8, 1, 2, 0, 5]"
 203 
 204 text ‹Sada nam treba način da povežemo ovu konretnu implementaciju sa opštom
 205 implementacijom algoritma za sortiranje koji smo naveli uz pomoć lokala.
 206 
 207 Koristimo interpretaciju lokala i ključnu reč \verb!global_interpretation! nakon
 208 čega navodimo novo ime lokala, pa ime osnovnog lokala iz koga izvodimo novi
 209 lokal, ključnu reč \verb!where! i ime apstraktne funkcije (konstante lokala)
 210 koju sada zamenjujemo konkretnom funkcijom koju smo sada implementirali. Za tu
 211 konkretnu funkciju treba da dokažemo da važe aksiome koje su navedene u lokalu,
 212 odnosno treba da dokažemo da ovakva funkcija podele zadovoljava potrebna
 213 svojstva. Ovaj dokaz se navodi između \verb!proof! i \verb!qed! bloka, pri čemu
 214 su dokazi različitih aksioma razdvojeni ključnom rečju \verb!next!.
 215 
 216 Napomenimo da je red koji počinje sa ključnom rečju \verb!defines! neophodan da
 217 bi funkcija @{text ‹mergesort_half›} mogla da se izvršava. Nakon ključne reči se
 218 navodi ime funkcije (koje ćemo koristiti u nastavku), ime funkcije iz lokala i
 219 konkretnu funkciju za deljenje liste koju ćemo koristiti u ovoj interpretaciji.›
 220 
 221 global_interpretation MergeSort_half: MergeSort where 
 222   split = "split_half"
 223   ― ‹Naredni red je potrebno navesti da bi funkcija mergesort mogla da se izvršava›
 224   defines mergesort_half = "MergeSort.mergesort split_half"
 225 proof
 226   fix xs ys zs :: "nat list"
 227   assume "length xs > 1" "(ys, zs) = split_half xs"
 228   then show "length ys < length xs ∧ length zs < length xs"
 229     unfolding split_half_def Let_def
 230     by auto
 231 next
 232   fix xs ys zs :: "nat list"
 233   assume "length xs > 1" "(ys, zs) = split_half xs"
 234   then show "mset xs = mset ys + mset zs"
 235     unfolding split_half_def Let_def
 236     ― ‹sledgehammer›
 237     by (simp add: union_code)
 238 qed
 239 
 240 text‹Sada možemo pozvati ovako intepretiranu funkciju:›
 241 
 242 value "mergesort_half [3, 8, 4, 2, 1]"
 243 
 244 text‹Ali imamo i dve teoreme dobijene u ovom lokalu. Jedna teorema koja tvrdi da
 245 zaista ova kombinacija sortira listu i druga koja tvrdi da je multiskup
 246 elemenata nepromenjen.›
 247 
 248 thm "MergeSort_half.mset_mergesort"
 249 thm "MergeSort_half.sorted_mergesort"
 250 
 251 text‹Ovako interpretirana funkcija može da se eksportuje u neki drugi programski
 252 jezik:›
 253 
 254 export_code mergesort_half in Haskell
 255 
 256 text‹Ovde ponovo možemo da primetimo problem sa brzinom izvršavanja ovakvog koda
 257 zbog načina na koji su implementirani prirodni brojevi i gubi se puno vremena na
 258 poređenje prirodnih brojeva (koji su predstavljeni preko Suc). Tako da je u
 259 situacijama kada želimo da eksportujemo kod potrebno uključiti na početku fajla
 260 teoriju \verb!Code_Target_Nat!.›
 261 
 262 value "length (mergesort_half [0..<4000])"
 263 
 264 subsubsection ‹Razdvajanje naizmeničnim uzimanjem elemenata›
 265 
 266 text‹Pokazaćemo kako izgleda interpretacija ovog istog lokala sa drugom
 267 funkcijom za deljenje na dve liste, kada uzimamo elemente naizmenično. Funkciju
 268 ćemo nazvati \verb!split_zigzag!, definisaćemo je rekurzijom i dokazi će
 269 koristiti indukciju po pravilu \verb!split_zigzag.induct!.›
 270 
 271 fun split_zigzag :: "nat list ⇒ nat list × nat list" where
 272 "split_zigzag [] = ([], [])" | 
 273 "split_zigzag [x] = ([x], [])" | 
 274 "split_zigzag (x0 # x1 # xs) = 
 275       (let (ys, zs) = split_zigzag xs 
 276         in (x0 # ys, x1 # zs))"
 277 
 278 value "split_zigzag [3::nat, 2, 8, 4, 1, 5, 6]"
 279 
 280 global_interpretation MergeSort_zigzag: MergeSort 
 281   where split = "split_zigzag"
 282   ― ‹Naredni red je potrebno navesti da bi funkcija @{text ‹mergesort_zigzag›} mogla da se izvršava›
 283   defines mergesort_zigzag = "MergeSort.mergesort split_zigzag"
 284 proof
 285   fix xs ys zs :: "nat list"
 286   assume "length xs > 1" "(ys, zs) = split_zigzag xs"
 287   then show "length ys < length xs ∧ length zs < length xs"
 288   proof (induction xs arbitrary: ys zs rule: split_zigzag.induct)
 289     case 1
 290     then show ?case
 291       by simp
 292   next
 293     case (2 x)
 294     then show ?case
 295       by simp
 296   next
 297     case (3 x0 x1 xs)
 298     show ?case
 299     proof (cases "xs = []")
 300       case True
 301       thus ?thesis
 302         using 3(3)
 303         by simp
 304     next
 305       case False
 306       show ?thesis
 307       proof (cases "length xs = 1")
 308         case True
 309         then obtain x where "xs = [x]"
 310           by (metis One_nat_def length_0_conv length_Suc_conv)
 311         thus ?thesis
 312           using 3(3)
 313           by simp
 314       next
 315         case False
 316         then have "length xs > 1"
 317           using `xs ≠ []`
 318           using not_less_iff_gr_or_eq by auto
 319         then obtain ys' zs' where *: "(ys', zs') = split_zigzag xs"
 320           by (metis surj_pair)
 321         then have **: "ys = x0 # ys'" "zs = x1 # zs'"
 322           using 3(3)
 323           by (metis Pair_inject prod.simps(2) split_zigzag.simps(3))+
 324         then have "length ys' < length xs ∧ length zs' < length xs"
 325           using * 3(1) `length xs > 1`
 326           by simp
 327         then show ?thesis
 328           using **
 329           by simp
 330       qed
 331     qed
 332   qed
 333 next
 334   fix xs ys zs :: "nat list"
 335   assume "(ys, zs) = split_zigzag xs"
 336   then show "mset xs = mset ys + mset zs"
 337     by (induction xs arbitrary: ys zs rule: split_zigzag.induct)
 338        (auto split: prod.split_asm)
 339 qed
 340 
 341 text‹Ovako interpretirana funkcija se sada može pozvati:›
 342 
 343 value "mergesort_zigzag [3, 8, 1, 4, 2, 5, 6]"
 344 
 345 text‹I opet imamo dve teoreme koje tvrde da ova funkcija zaista sortira listu i
 346 da je multiskup elemenata nepromenjen:›
 347 
 348 thm "MergeSort_zigzag.mset_mergesort"
 349 thm "MergeSort_zigzag.sorted_mergesort"
 350 
 351 subsection‹Apstrakcija topološkog prostora›
 352 
 353 text‹Sličan pristup, uvođenje apstraktnog modela, dokazivanje određenih
 354 svojstava i naknadno instanciranje se primenjuje i u matematici. Na taj način
 355 možemo izbeći ponavljanje dokaza određenih osobina sličnih struktura.
 356 Detaljnije, ovim postižemo da uvođenjem odgovarajućih apstrakcija i dokazivanjem
 357 teorema u apstraktnom obliku, dobijamo opciju da upotrebimo konkretne instance
 358 dokazanih teorema na strukturama za koje je dokazano da zadovoljavaju osobine
 359 odgovarajuće apstrakcije.
 360 
 361 Na primer, umesto da se zajedničke teoreme dokažu prvo za polje realnih, a zatim
 362 za polje kompleksnih brojeva, teoreme se mogu dokazati na apstraktnom nivou, za
 363 sva polja. Nakon toga, pošto pokažemo da, na primer, realni brojevi čine polje u
 364 odnosu na odgovarajuće operacije, sve teoreme dokazane za polja važiće i u
 365 odgovarajućoj strukturi realnih brojeva.›
 366 
 367 text‹Ilustrujmo ovaj postupak uvođenjem apstrakcije topološkog
 368 prostora.\footnote{Jedna odlična, veoma lako čitljiva knjiga o topologiji: @{url
 369 ‹http://www.topologywithouttears.net/topbook.pdf›}.}\footnote{Malo kraći
 370 materijal o topološkim prostorima može se naći na: @{url
 371 ‹https://www.dmi.uns.ac.rs/site/dmi/download/master/primenjena_matematika/MilijanaMilovanovic.pdf›}}
 372 
 373 \emph{Topološki prostor} (na nekom skupu X) je par @{text ‹(X,τ)›}, gde X
 374 predstavlja dati skup, a @{text ‹τ›} predstavlja familiju podskupova skupa X.
 375 Podskupove koji pripadaju familiji @{text ‹τ›} nazvaćemo otvorenim podskupovima.
 376 Ova familija treba da zadovoljava sledeće uslove:
 377 
 378  ▪ Prazan skup i ceo skup X moraju biti otvoreni skupovi 
 379 ― ‹aksiome @{text ‹empty›} i @{text ‹univ›}›
 380 
 381  ▪ Unija proizvoljnog broja otvorenih skupova je otvoren skup 
 382 ― ‹aksioma @{text ‹union›}›
 383 
 384  ▪ Presek dva otvorena skupa je otvoren skup ― ‹aksioma @{text ‹inter›}›
 385 
 386 Pored ove četiri aksiome potrebno je eksplicitno navesti da elementi skupa
 387 @{text ‹τ›} moraju biti podskupovi skupa X (obrnuto neće važiti), i to tvrđenje
 388 ćemo predstaviti u narednom lokalu aksiomom sa imenom @{text ‹subsets›}.
 389 Napomenimo još sintaksu koju ćemo koristiti. Skup S je element skupa @{text ‹τ›}
 390 pišemo uobičajeno @{text ‹S ∈ τ›}. Zanimljivo je to da proizvoljan broj
 391 otvorenih skupova u stvari predstavlja podskup skupa @{text ‹τ›}, pa ćemo
 392 rečenicu tipa skup @{text ‹τ'›} sadrži proizvoljan broj otvorenih skupova
 393 jednostavno zapisivati sa @{text ‹τ' ⊆ τ›}. A uniju nad tim skupom, odnosno
 394 uniju proizvoljnog broja otvorenih skupova ćemo zapisati sa @{text ‹⋃ τ'›}.
 395 
 396 Formalizacija ovoj pojma vrši se kroz koncept lokala. Lokal uvodi određeni broj
 397 konstanti/funkcija (koje se kasnije konkretizuju) i aksioma koje te
 398 konstante/funkcije moraju da zadovolje. Svaki topološki prostor fiksira
 399 konstantu X (skup nosilac) i konstantu @{text ‹τ›} (skup svih otvorenih
 400 podskupova).
 401 
 402 Ovako definisana familija @{text ‹τ›} se naziva i \emph{topologija} nad skupom X.
 403 
 404 Može se pokazati da je familija @{text ‹τ›} zatvorena u odnosu na konačne
 405 preseke. Ovo tvrđenje ćemo nezavisno formulisati i dokazati kao lemu u narednom
 406 lokalu (lema @{text ‹inter_finite›}). Da bi smo proverili da li je skup konačan
 407 koristićemo funkciju @{text ‹finite :: 'a set ⇒ bool›} koja vraća vrednost
 408 @{text ‹True›} ako je njen argument konačan. Dokaz te leme će se izvoditi
 409 indukcijom nad konačnim skupom @{text ‹τ'›}. Pravilo indukcije na koje se
 410 pozivamo se u ovom slučaju naziva @{text ‹finite.induct:›} @{thm[mode=Proof]
 411 finite.induct [no_vars]} i ovako se zapisuje u Isabelle-u. U dokazu ćemo
 412 razlikovati slučaj praznog skupa i slučaj nepraznog skupa (koji se dobija
 413 ubacivanjem elementa u skup funkcijom @{text ‹insert :: 'a ⇒ 'a set ⇒ 'a set›}).
 414 
 415 Pored pojma otvorenog skupa, koji smo definisali kao elemente familije @{text
 416 ‹τ›}, uvodimo i pojam \emph{zatvorenog skupa} - skup je zatvoren ako i samo ako
 417 je njegov komplement u odnosu na skup X otvoren skup. Ova dva pojma ćemo uvesti
 418 pojedinačno u narednom lokalu.
 419 
 420 Primetimo da se na sličan način može definisati i topologija uz pomoć zatvorenih
 421 skupova. To možemo i dokazati na osnovu već navedenih aksioma za otvorene
 422 skupove i de Morganovih zakona. Tako da ćemo formulisati (i dokazati) dualne
 423 teoreme za zatvorene skupove: prazan skup i ceo prostor su zatvoreni skupovi
 424 (leme @{text ‹closed_empty›} i @{text ‹closed_univ›}), presek dva zatvorena
 425 skupa je zatvoren skup (lema @{text ‹closed_inter›}), presek konačno mnogo
 426 zatvorenih skupova je zatvoren skup (lema @{text ‹closed_inter_finite›}) i unija
 427 konačno mnogo zatvorenih skupova je zatvoren skup (lema @{text
 428 ‹closed_union_finite›}). ›
 429 
 430 locale topological_space =
 431   ― ‹konstante›
 432   fixes X :: "'a set"  ― ‹skup nosilac›
 433   fixes τ :: "'a set set" ― ‹kolekcija otvorenih skupova›
 434 
 435   ― ‹aksiome›
 436   assumes subsets: "⋀ S. S ∈ τ ⟹ S ⊆ X"
 437   assumes univ: "X ∈ τ"
 438   assumes empty: "{} ∈ τ"
 439   assumes inter: "⋀ S1 S2. ⟦S1 ∈ τ; S2 ∈ τ⟧ ⟹ S1 ∩ S2 ∈ τ"
 440   assumes union: "⋀ τ'. ⟦τ' ≠ {}; τ' ⊆ τ⟧ ⟹ ⋃ τ' ∈ τ"
 441 begin
 442 
 443 ― ‹Skup je otvoren ako i samo ako pripada @{text ‹τ›}.›
 444 abbreviation open_set :: "'a set ⇒ bool" where
 445   "open_set S ≡ S ∈ τ"
 446 
 447 ― ‹U narednom dokazu ćemo koristiti pravilo indukcije nad konačnim skupom.›
 448 term finite
 449 thm finite.induct
 450 
 451 ― ‹Dokazujemo da je presek konačno mnogo otvorenih skupova otvoren skup:›
 452 lemma inter_finite:
 453   assumes "finite τ'" "τ' ≠ {}" "∀ S ∈ τ'. open_set S"
 454   shows "open_set (⋂ τ')"
 455   using assms
 456 proof (induction τ' rule: finite.induct)
 457   case emptyI
 458   then show ?case
 459     by simp
 460 next
 461   case (insertI A a)
 462   thm insertI ― ‹obratite pažnju na to kako izgleda korak indukcije u ovakvom dokazu›
 463   term insert ― ‹funkcija koja ubacuje element u skup›
 464   show ?case
 465   proof (cases "A = {}")
 466     case True
 467     then show ?thesis
 468       using insertI
 469       by simp
 470   next
 471     case False
 472     then show ?thesis
 473       using insertI inter ― ‹pozivamo se na induktivnu pretpostavku i aksiomu inter›
 474       by simp
 475   qed
 476 qed
 477 
 478 ― ‹Skup je zatvoren ako i samo ako mu je komplement (u odnosu na X) otvoren:›
 479 definition closed_set :: "'a set ⇒ bool" where
 480   "closed_set S ⟷ open_set (X - S)"
 481 
 482 ― ‹Zatvoreni skupovi takođe definišu topologiju nad skupom X:›
 483 lemma closed_empty:
 484   "closed_set {}"
 485   unfolding closed_set_def
 486   using univ
 487   by simp
 488 
 489 lemma closed_univ:
 490   "closed_set X"
 491   unfolding closed_set_def
 492   using empty
 493   by simp
 494 
 495 lemma closed_inter:
 496   assumes "closed_set S1" "closed_set S2"
 497   shows "closed_set (S1 ∩ S2)"
 498   using assms union[of "{X - S1, X - S2}"]
 499   unfolding closed_set_def
 500   by (simp add: Diff_Int)
 501 
 502 lemma closed_inter_finite:
 503   assumes "finite τ'" "τ' ≠ {}" "∀ S ∈ τ'. closed_set S"
 504   shows "closed_set (⋂ τ')"
 505 proof-
 506   have "X - (⋂ τ') = ⋃ {X - S | S . S ∈ τ'}"
 507     using assms
 508     by auto
 509   thus ?thesis
 510     using assms
 511     unfolding closed_set_def
 512     using union[of "{X - S |S. S ∈ τ'}"]
 513     by auto
 514 qed
 515 
 516 lemma closed_union_finite:
 517   assumes "finite τ'" "τ' ≠ {}" "∀ S ∈ τ'. closed_set S"
 518   shows "closed_set (⋃ τ')"
 519 proof-
 520   have "X - ⋃ τ' = ⋂ {X - S | S . S ∈ τ'}"
 521     using `τ' ≠ {}`
 522     by auto
 523   thus ?thesis
 524     using assms
 525     using inter_finite[of "{X - S | S. S ∈ τ'}"]
 526     unfolding closed_set_def
 527     by auto
 528 qed
 529 
 530 end
 531 
 532 subsubsection ‹Ograničen skup prirodnih brojeva›
 533 
 534 text ‹U nastavku je dat jedan (prilično veštački) primer topološkog prostora:›
 535 
 536 definition X_ex1 :: "nat set" where
 537   "X_ex1 = {0::nat, 1, 2, 3, 4, 5}" 
 538 
 539 definition τ_ex1 :: "nat set set" where
 540   "τ_ex1 = {{0::nat, 1, 2, 3, 4, 5}, {}, {0}, {2, 3}, {0, 2, 3}, {1, 2, 3, 4, 5}}"
 541 
 542 text ‹Komandom \verb!global_interpretation! dokazujemo da neke konkretne
 543 konstante interpretiraju ranije uvedenu apstrakciju. Odnosno, treba da pokažemo
 544 (da ih formalno dokažemo) da važe aksiome koje smo naveli u lokalu.›
 545 
 546 declare [[quick_and_dirty=true]]
 547 
 548 global_interpretation topological_space where
 549   X = "X_ex1" and
 550   τ = "τ_ex1"
 551 proof
 552   fix S
 553   assume "S ∈ τ_ex1"
 554   thus "S ⊆ X_ex1"
 555     unfolding τ_ex1_def X_ex1_def
 556     by auto
 557 next
 558   show "X_ex1 ∈ τ_ex1" "{} ∈ τ_ex1"
 559     unfolding X_ex1_def τ_ex1_def
 560     by auto
 561 next
 562   fix S1 S2
 563   assume "S1 ∈ τ_ex1" "S2 ∈ τ_ex1"
 564   thus "S1 ∩ S2 ∈ τ_ex1"
 565     unfolding τ_ex1_def
 566     ― ‹ovi dokazi su krajnje neinteresantni, a ne mogu se dokazati automatski›
 567     sorry
 568 next
 569   fix τ'
 570   assume "τ' ≠ {}" "τ' ⊆ τ_ex1" 
 571   thus "⋃ τ' ∈ τ_ex1"
 572     unfolding τ_ex1_def
 573     ― ‹ovi dokazi su krajnje neinteresantni, a ne mogu se dokazati automatski›
 574     sorry
 575 qed
 576 
 577 subsubsection‹Skup realnih brojeva›
 578 
 579 text ‹Mnogo interesantniji primer topološkog prostora je skup realnih brojeva sa
 580 tzv. euklidskom topologijom.›
 581 
 582 text ‹Otvoreni interval (a, b) se zadaje na sledeći način:›
 583 
 584 definition open_interval :: "real ⇒ real ⇒ real set" where
 585   "open_interval a b = {x. a < x ∧ x < b}"
 586 
 587 lemma open_interval_empty_iff:
 588   "open_interval a b = {} ⟷ a ≥ b"
 589   unfolding open_interval_def
 590   by (metis (no_types, lifting) dense_le dual_order.strict_implies_order
 591   empty_Collect_eq leD le_less_linear order.strict_trans1)
 592 
 593 text ‹Nakon ovoga ćemo definisati otvoren skup - skup je otvoren ako i samo ako
 594 se svaka njegova tačka može okružiti nekim otvorenim intervalom koji ceo pripada
 595 tom skupu.›
 596 
 597 definition is_real_open_set where 
 598   "is_real_open_set S ⟷ 
 599       (∀ x ∈ S. ∃ a b. x ∈ open_interval a b ∧ open_interval a b ⊆ S)"
 600 
 601 text ‹Dokazujemo da skup realnih brojeva sa ovako uvedenom definicijom otvorenog
 602 skupa zaista predstavlja jedan topološki prostor. 
 603 
 604 U narednoj interpretaciji se koristi UNIV - skup svih elemenata nekog tipa.›
 605 
 606 global_interpretation Euclidean_topology: topological_space where
 607  X = "UNIV :: real set"  and
 608  τ = "{S. is_real_open_set S}"
 609 proof
 610   fix S
 611   assume "S ∈ {S. is_real_open_set S}"
 612   then show "S ⊆ UNIV"
 613     by simp
 614 next
 615   have "∀ x. ∃ a b. x ∈ open_interval a b"
 616   proof-
 617     have "∀ x. x ∈ open_interval (x - 1) (x + 1)"
 618       unfolding open_interval_def
 619       by simp
 620     then show ?thesis
 621       by auto
 622   qed
 623   then show "UNIV ∈ {S. is_real_open_set S}"
 624     unfolding is_real_open_set_def
 625     by auto
 626 next
 627   show "{} ∈ {S. is_real_open_set S}"
 628     unfolding is_real_open_set_def
 629     by simp
 630 next
 631   fix τ'
 632   assume *: "τ' ⊆ {S. is_real_open_set S}"
 633   show "⋃ τ' ∈ {S. is_real_open_set S}"
 634   proof
 635     show "is_real_open_set (⋃ τ')"
 636       unfolding is_real_open_set_def
 637     proof
 638       fix x
 639       assume "x ∈ ⋃ τ'"
 640       then obtain S where "S ∈ τ'" "x ∈ S"
 641         by auto
 642       hence "is_real_open_set S"
 643         using *
 644         by auto
 645       then obtain a b where "x ∈ open_interval a b" "open_interval a b ⊆ S"
 646         using `x ∈ S`
 647         unfolding is_real_open_set_def
 648         by auto
 649       thus "∃a b. x ∈ open_interval a b ∧ open_interval a b ⊆ ⋃ τ'"
 650         using `S ∈ τ'`
 651         by auto
 652     qed
 653   qed
 654 next
 655   fix S1 S2
 656   assume *: "S1 ∈ {S. is_real_open_set S}" "S2 ∈ {S. is_real_open_set S}"
 657   show "S1 ∩ S2 ∈ {S. is_real_open_set S}"
 658   proof
 659     show "is_real_open_set (S1 ∩ S2)"
 660       unfolding is_real_open_set_def
 661     proof
 662       fix x
 663       assume "x ∈ S1 ∩ S2"
 664       then obtain a1 b1 a2 b2 where 
 665       **: "x ∈ open_interval a1 b1" "open_interval a1 b1 ⊆ S1"
 666           "x ∈ open_interval a2 b2" "open_interval a2 b2 ⊆ S2"
 667         using *
 668         unfolding is_real_open_set_def
 669         by blast
 670       let ?a = "max a1 a2" 
 671       let ?b = "min b1 b2"
 672       have "x ∈ open_interval ?a ?b"
 673         using **
 674         unfolding open_interval_def
 675         by auto
 676       moreover
 677       have "open_interval ?a ?b ⊆ S1 ∩ S2"
 678         using **
 679         unfolding open_interval_def
 680         by auto
 681       ultimately
 682       show "∃a b. x ∈ open_interval a b ∧ open_interval a b ⊆ S1 ∩ S2"
 683         by auto
 684     qed
 685   qed
 686 qed
 687 
 688 text ‹Kada smo dokazali da realni brojevi predstavljaju topološki prostor, na
 689 raspolaganju imamo sve definicije i teoreme dokazane o topološkim prostorima.›
 690 
 691 thm Euclidean_topology.closed_set_def
 692 thm Euclidean_topology.closed_inter
 693 thm Euclidean_topology.closed_union_finite
 694 
 695 lemma "Euclidean_topology.open_set A ⟷ is_real_open_set A"
 696   by simp
 697 
 698 
 699 end
 700