1 theory Cas8_vezbe_resenja
2 imports Main
3 begin
4
5 section ‹Prirodni brojevi i matematička indukcija›
6
7 subsection ‹Ponavljanje sa predavanja›
8
9 text‹Tip prirodnih brojeva se označava sa @{typ nat}. Ključnu reč @{text term} možemo
10 koristiti da proverimo koji je tip određenog izraza. Na primer, ako zapišemo samo 3 -
11 to je vrednost 3 proizvoljnog, nepoznatog tipa; ako zapišemo 3::nat - to je vrednost 3
12 koja pripada skupu prirodnih brojeva. Treba napomenuti da i nula 0::nat spada u skup
13 prirodnih brojeva u Isabelle-u. Sa @{typ int} označavamo tip celih brojeva. I celi i
14 prirodni brojevi su u Isabelle-u kodirani tako da nemaju ograničenje.›
15
16 typ nat
17
18 term 3
19 term "3::nat"
20 term "0::nat"
21 term "-3::int"
22
23 text‹Operacije nad prirodnim brojevima se zapisuju na uobičajeni način: +, -, *, div, mod.
24 Pored ovih operacija bitna je i operacija @{text Suc} koja nam daje sledbenik prirodnog
25 broja i biće korišćena kod indukcije.›
26
27 text‹Primer dokaza u Isabelle-u nad prirodnim brojevima se može videti u nastavku
28 teksta. Prilikom definisanja leme, komandom @{text "fixes"} se može naglasiti da se lema
29 odnosi samo na prirodne brojeve. Bez te pretpostavke, naredni dokaz ne bi bio uspešan.›
30
31 lemma
32 fixes a b c d :: nat
33 shows "a * ((b + c) + d) = (a * b + a * d) + a * c"
34 proof-
35 have "a * ((b + c) + d) = a * (b + c) + a * d"
36 by (rule distrib_left)
37 also have "... = (a * b + a * c) + a * d"
38 by (simp add: add_mult_distrib2)
39 also have "... = a * b + (a * c + a * d)"
40 by simp
41 also have "... = a * b + (a * d + a * c)"
42 by simp
43 also have "... = (a * b + a * d) + a * c"
44 by simp
45 finally
46 show ?thesis
47 by simp
48 qed
49
50 text‹U nastavku, prilikom pisanja Isar dokaza, od automatskih alata koristicemo samo
51 \emph{simp} kada radimo sa brojevima. Ako želimo da pored simplifikatora koristimo još
52 i pravilo A, to ćemo naglasiti naredbom @{text "by simp add rule A"}. Ako želimo da
53 simplifikator koristi iskučivo pravilo A (i ni jedno drugo pravilo), to ćemo naglasiti
54 naredbom @{text "by simp only rule A"}.›
55
56 text‹Naredni dokaz će prikazati način korišćenja matematičke indukcije. U zapisu ove leme
57 koristimo operator @{text "..<"} koji kreira listu i funkciju za sumiranje elemenata liste
58 @{text "sum_list"}.›
59
60 value "[0..<5]" ―‹lista brojeva strogo manjih od 5›
61 value "sum_list [0..<5]" ―‹suma brojeva strogo manjih od 5›
62
63 text‹Dokazati da važi: $0 + 1 + 2 + ... + (n-1) = n * (n - 1) / 2$.›
64
65 lemma
66 "sum_list [0..<n] = n*(n-1) div 2"
67 proof (induction n)
68 case 0
69 then show ?case
70 by simp
71 next
72 case (Suc n)
73 note ih = this
74 have "sum_list [0..<Suc n] = sum_list [0..<n] + n"
75 by simp
76 also have "... = (n * (n - 1)) div 2 + n"
77 using ih
78 by simp
79 also have "(n * (n - 1)) div 2 + n = n * (n + 1) div 2"
80 by (metis Suc_eq_plus1 atLeastLessThanSuc_atLeastAtMost calculation distinct_sum_list_conv_Sum distinct_upt gauss_sum_nat set_upt)
81 finally
82 show ?case
83 by simp
84 qed
85
86 text‹U okviru dokaza koji koriste matematičku indukciju moramo razlikovati funkciju, odnosno
87 @{text "term Suc"} koji se koristi za zapisivanje sledbenika celog broja, od induktivne
88 pretpostavke koja se zapisuje istim imenom @{text "thm Suc"}. Otuda @{text "term Suc"}
89 može da se pojavi kao deo formula koje se javljaju u dokazu, dok teorema @{text "thm Suc"}
90 može da se pojavi kao deo metoda koji se koristi za dokazivanje tekućeg koraka. Otuda
91 se naredba @{text "using Suc"} odnosi na korišćenje induktivne hipoteze.›
92
93 text‹Mnogi dokazi nad prirodnim brojevima se mogu dokazati samo koristeći metod matematičke
94 indukcije. Tako da se lema sa početka ovog poglavlja može dokazati i kraće, uz pomoć
95 automatskih metoda na sledeći način. Pored automatskog dokazivača @{text "auto"} koristi
96 se i metod matematičke indukcije @{text "induction"} koji se mora eksplicitno pozvati i
97 za koji moramo navesti po kojoj promenljivoj izvodimo taj dokaz.›
98
99 lemma "sum_list [0..<n+1] = n * (n + 1) div 2"
100 by (induction n) auto
101
102 text‹U ovom dokazu se "krije" tip liste, funkcija za kreiranje liste i funkcija za
103 računanje sume elemenata liste. Ovo nam može dati uvid u to šta nam je sve potrebno
104 da bismo jedno ovakvo tvrđenje mi sami mogli da definišemo i dokažemo.
105
106 Za početak ćemo samostalno definisati funkciju koja računa sumu brojeva od 0 do n.
107 Vrednosti te funkcije redom za vrednosti 0, 1, 2, 3, i 4 su brojevi 0, 1, 3, 6, 10,....
108 Ovi brojevi se nazivaju trougaoni brojevi. ›
109
110 text‹Koristićemo rekurzivnu definiciju za zapis ove funkcije. Rekurzivne definicije nad
111 tipom prirodnih brojeva su direktno povezane sa načinom na koji su prirodni brojevi
112 definisani. Svaki prirodni broj je ili 0 ili je sledbenik nekog drugog prirodnog broja.
113
114 Kada se definišu rekurzivne funkcije moramo voditi računa o dve stvari: izlaz iz rekurzije
115 (za prirodne brojeve to će biti broj 0) i rekurzivni poziv koji se ovde definiše za
116 parametar koji je nečiji sledbenik.
117
118 Za definiciju se koristi ključna rec @{text "primrec"} i odnosi se na primitivnu rekurziju i
119 razlikuje dva slučaja, slučaj nule i slučaj sledbenika. Nakon imena funkcije zadaje se
120 njen tip, ključna reč @{text "where"} i nakon toga definicija funkcije.›
121
122 primrec trougaoni :: "nat ⇒ nat" where
123 "trougaoni 0 = 0" |
124 "trougaoni (Suc n) = trougaoni n + Suc n"
125 ―‹sa leve strane oko Suc n je neophodna zagrada, a sa desne strane nije›
126
127 text‹Ista lema zapisana na ovom novom jeziku se dokazuje na isti način.›
128
129 lemma "trougaoni n = n * (n + 1) div 2"
130 by (induction n) auto
131
132 value "trougaoni 5"
133
134 text‹Sada ćemo definisati faktorijel broja na sličan način.›
135
136 primrec fact :: "nat ⇒ nat" where
137 "fact 0 = 1" |
138 "fact (Suc n) = fact n * (n + 1)"
139
140 value "fact 3"
141
142 subsubsection ‹Građenje skupa prirodnih brojeva›
143
144 text‹U ovom poglavlju ćemo videti kako možemo sami da definišemo tip prirodnih brojeva.
145 Uopšteno gledano naučićemo kako da definišemo novi tip podataka, operacije nad tim tipom i
146 da definišemo i dokažemo njihova svojstva. ›
147
148 text‹Gradimo skup prirodnih brojeva od početka. Prirodni brojevi se definišu kao
149 najmanji skup koji sadrži 0 i koji za svaki broj koji već pripada tom skupu, sadrži i
150 njegovog sledbenika - to je induktivni skup (najmanji skup zatvoren za određen skup
151 operacija).
152
153 Isabelle nudi definisanje novih algebarskih tipova podataka kroz konstrukciju
154 @{text "datatype"}. Nakon toga se definiše konstanta @{text "nula"} (koja predstavlja
155 osnovni term od koga se polazi) i konstruktor koji kreira nove termove (na osnovu datih
156 elemenata ovog tipa konstruiše nove elemente ovog tipa) @{text "Sled"}:
157
158 \verb"datatype prirodni = nula | Sled prirodni"
159
160 Sada ga Isabelle prepoznaje kao novi tip, što mozemo videti naredbom: \verb|typ prirodni1|.
161
162 Prirodni brojevi se sada zapisuju u Isabelle-u kao: nula, Sled nula, Sled (Sled nula).
163 Da ne bismo morali da u svim narednim dokazima vučemo konstantu nula, možemo u
164 definiciji osnovne konstante zameniti nekim simbolom, npr. zadebljana nula
165 koja se zapisuje \verb|\ < zero >|. Sada je svejedno koji ćemo zapis koristiti.
166
167 Napomena: ubacite sami naredni kod u Isabelle da biste istestirali. Html fajl ne prikazuje
168 lepo ovako zapisanu nulu pa postoji razlika između html fajla i thy fajla.›
169
170 (* datatype prirodni = nula ("\") | Sled prirodni *)
171 datatype prirodni = nula | Sled prirodni
172
173 typ prirodni
174
175 term "nula"
176 term "Sled nula"
177 term "Sled (Sled nula)"
178
179 text‹Možemo navoditi i nove definicije, i npr. možemo definisati konstantu jedan, dva itd. ›
180
181 definition jedan_def :: "prirodni" where
182 "jedan_def = Sled nula"
183
184 definition dva_def :: "prirodni" where
185 "dva_def = Sled jedan_def"
186
187 text‹Sada ćemo definisati neke funkcije nad skupom prirodnih brojeva korišćenjem
188 primitivne rekurzije. Primitivna rekurzija je specijalni oblik rekurzije koji direktno
189 prati definiciju tipa podataka i slučajeve koji odgovaraju tipu.
190
191 Definicija sabiranja: funkcija koja za dva prirodna broja vraća treći prirodni broj koji
192 je jednak njihovom zbiru. Kada funkcija ima dva argumenta, možemo birati da li želimo da
193 rekurzija ide po prvom ili po drugom argumentu, ovde ćemo izabrati da bude po prvom
194 argumentu. ›
195
196 text‹Ako želimo da umesto imena @{text "saberi"} koristimo operator, njega uvodimo u
197 zagradama između tipa i ključne reci @{text "where"}. Običan simbol + ne možemo koristiti
198 zato što je rezervisan (isto kao i što ne koristimo običan simbol nula - 0).
199 Koristimo simbol \verb|⊕|, broj 100 oznacava prioritet operatora, l (na kraju ključne
200 reči @{text "infixl"}) označava levo asocijativni operator tj. a + b + c = (a + b) + c.
201 Funkcionalnost je ista sa ili bez operatora, samo je notacija malo udobnija za čitanje.›
202
203 primrec saberi :: "prirodni ⇒ prirodni ⇒ prirodni" (infixl "⊕" 100) where
204 "nula ⊕ y = y" |
205 "(Sled x) ⊕ y = Sled (x ⊕ y)"
206
207 text‹Kada se definicija navede primitivnom rekurzijom, automatski se formule koje su navedene
208 u okviru nje smatraju dokazanim teoremama sto možemo videti narednom naredbom. ›
209
210 print_theorems
211
212 text‹Dobijene teoreme se zovu saberi.simps i automatski su na raspolaganju simplifikatoru,
213 što ćemo videti u narednim dokazima.›
214
215 thm saberi.simps(1)
216 thm saberi.simps(2)
217
218 text‹
219 @{thm [display] saberi.simps(1) [no_vars]}
220 @{thm [display] saberi.simps(2) [no_vars]}
221 ›
222
223 text‹Sledećom naredbom dobijamo kao rezultat dva ali nije ispisana vrednost dva.
224 Definicije koje navodimo nam služe da mi možemo da koristimo pojmove koje smo uveli,
225 ali kada Isabelle dobije rezultat koji je jednak desnoj strani nekog pojma, on ne
226 redukuje to i ne prikazuje u obliku leve strane.›
227
228 value "saberi jedan_def jedan_def"
229
230 text‹Umesto definicije mogli smo da koristimo skraćenice @{text "abbreviations"} kao u
231 narednoj naredbi (simbol ekvivalencije se dobija kada otkucamo \verb|= =|):›
232
233 abbreviation jedan :: "prirodni" where
234 "jedan ≡ Sled nula"
235
236 abbreviation dva :: "prirodni" where
237 "dva ≡ Sled jedan"
238
239 text‹Sada kada Isabelle primeti da je našao desnu stranu neke skraćenice, on će je
240 automatski prikazati u obliku leve strane te skraćenice:›
241
242 value "saberi jedan jedan"
243
244 text‹Skraćenice ima smisla koristiti kada se uvodi koncept koji je jednostavna varijacija
245 već postojećeg koncepta. One se automatski raspisuju, pa nisu pogodne da se koriste nad
246 velikim skupom već postojećih koncepta. Nisu ekvivalentne definicijama i ne mogu ih
247 zameniti.›
248
249 text‹Sada možemo preći na dokazivanje nekih svojstava sabiranja. Pravilo kojeg se često
250 pridržavamo: kad god je funkcija definisana induktivno po nekom parametru, dokaz njene
251 korektnosti se izvodi indukcijom upravo po tom parametru.›
252
253 text‹Napomena: u ovim dokazima automatski dokazivači ne pomažu zato što ne rade sa
254 indukcijom, i to se odnosi i na @{text "sledgehammer"}, i oni uopšte ne pokušavaju da
255 izvedu dokaze nad indukcijom. Tako da ako se u dokazu koristi inducija korisnik mora
256 naglasiti da želi da je koristi, što ćemo mi u ovom dokazu i uraditi. Nakon što se
257 primeni indukcija @{text "sledgehammer"} ima šanse da dokaže cilj ali problem je što ako
258 imamo više podciljeva u dokazu, @{text "sledgehammer"} dokazuje samo prvi cilj, tako da
259 treba birati trenutak kada se poziva.›
260
261 text‹\begin{exmp}
262 Dokazati da je sabiranje asocijativna operacija.
263 \end{exmp}›
264
265 text‹Kada u narednom dokazu primenimo induciju, naredbom @{text "apply (induction a)"},
266 vidimo da Isabelle deli dokaz na dva cilja - bazu indukcije kada je @{text "a = 0"} i
267 induktivni korak gde pretpostavljamo da tvrđenje važi za proizvoljno @{text "a"} i iz
268 te pretpostavke dokazujemo da tvrđenje važi za @{text "Sled a"}.
269
270 Pravilo koje se implicitno primenjuje na ovom mestu je pravilo indukcije definisano samim
271 tipom prirodnih brojeva koje se zove @{text "prirodni.induct"} i u Isabelle-u izgleda ovako:
272 @{thm [display] prirodni.induct [no_vars]}›
273
274 thm prirodni.induct
275
276 text‹Nakon toga pokušavamo sa @{text "apply auto"} što u ovom slučaju prolazi zato što auto
277 pokušava da dokaže sve preostale ciljeve i uspeva. Kada se dokaz raspisuje na ovaj
278 način, potrebno je na kraju navesti done kao ranije što smo radili u dokazima sa prirodnom
279 dedukcijom.›
280
281 lemma saberi_asoc':
282 shows "a ⊕ (b ⊕ c) = (a ⊕ b) ⊕ c"
283 apply (induction a)
284 apply auto
285 done
286
287 text‹Ovaj dokaz je mogao kraće da se zapiše sa @{text "by (induction a) auto"}.
288 Naredba @{text "by"} daje mogućnost da se navedu jedan ili dva metoda (ali ne i više
289 od dva).›
290
291 lemma saberi_asoc:
292 shows "a ⊕ (b ⊕ c) = (a ⊕ b) ⊕ c"
293 by (induction a) auto
294
295 text‹\begin{exmp}
296 Dokazati da je sabiranje komutativna operacija.
297 \end{exmp}›
298
299 text‹Dokaz svakako kreće primenom indukcije @{text "apply (induction a)"} na prvi parametar,
300 čime se cilj razbija na dva cilja. Nakon toga naredbom @{text "apply auto"} pokušavamo
301 da dokažemo oba cilja istovremeno, ali ni jedan cilj ne uspeva.
302
303 Napomena: u Isabelle-u skinuti komentare pa pokrenuti kod i videćete izlaz.›
304
305 (*
306 lemma saberi_kom:
307 shows "a ⊕ b = b ⊕ a"
308 apply (induction a)
309 apply auto
310 sorry
311 *)
312
313 text‹Pogledajmo zašto ne uspeva prvi cilj: leva strana se uprostila na b (što sledi iz
314 definicije sabiranja - sve te jednakosti se smatraju automatski delom procesa
315 simplifikacije i biće vidljive Isabelle-u), ali sa desne strane imamo b+0 ali pošto ne
316 znamo ništa o sabiranju nule sa desne strane vidimo da je ovde neophodno da definišemo
317 novu lemu kojom cemo dokazati ovo tvrdjenje b + 0 = b.
318
319 Dokaz ove leme @{text "saberi_nula_desno"} automatski prolazi, ali sada ako u originalnom
320 dokazu samo kažemo @{text "apply auto"} ne uspevamo da se oslobodimo prvog cilja pošto ne
321 zna koju lemu treba da iskoristi, pa možemo da mu damo tu informaciju i da na taj način
322 eliminišemo prvi podcilj.›
323
324 declare [[quick_and_dirty=true]]
325 (*
326 lemma saberi_nula_desno:
327 shows "a ⊕ nula = a"
328 by (induction a) auto
329
330 lemma saberi_kom:
331 shows "a ⊕ b = b ⊕ a"
332 apply (induction a)
333 apply (auto simp add: saberi_nula_desno)
334 sorry
335 *)
336
337 text‹Alternativa naredbi @{text "apply (auto simp add: saberi_nula_desno)"} jeste da
338 direktno naglasimo Isabelle-u da određenu lemu želimo da koristimo uvek sa simplifikatorom.
339 To radimo ključnom rečju @{text "[simp]"} koja se navodi nakon imena leme. Sada će i sama
340 naredba @{text "apply auto"} uspeti da pronađe odgovarajuću lemu.›
341
342 (*
343 lemma saberi_nula_desno[simp]:
344 shows "a ⊕ nula = a"
345 by (induction a) auto
346
347 lemma saberi_kom:
348 shows "a ⊕ b = b ⊕ a"
349 apply (induction a)
350 apply auto
351 sorry
352 *)
353
354 text‹Postoje dodatne naredbe za ubacivanje i izbacivanje lema iz simplifikatora: ako
355 želimo neku lemu koja je bila deklarisana kao simp, da izbacimo iz tog skupa koristimo
356 ključnu reč @{text "declare"} i naredbu @{text "simp del"}:
357
358 @{text "declare saberi_nula_desno [simp del]"}
359
360 A ako želimo da lemu vratimo (dodamo) u simplifikator koristimo naredbu @{text "simp"}.
361
362 @{text "declare saberi_nula_desno [simp]"}›
363
364 text‹Sada se bavimo drugim podciljem i vidimo da u drugom podcilju sa desne strane imamo
365 nešto oblika $b + Sled a$, a to ne znamo na koji način treba da transformišemo i još jednom
366 dodajemo novu pomoćnu lemu @{text "saberi_Sled_desno"}. Prilikom navođenja ove leme, odmah
367 dodajemo opciju @{text "[simp]"} nakon njenog imena. Njen dokaz prolazi automatski i
368 vraćamo se na dokaz početne leme koji takođe sada prolazi automatski.
369
370 Kompletan skup lema i njihovih dokaza izgleda ovako:›
371
372 ―‹1.2›
373 lemma saberi_nula_desno[simp]:
374 shows "a ⊕ nula = a"
375 by (induction a) auto ―‹sada se vraćamo na 1.3›
376
377 ―‹1.4.›
378 lemma saberi_Sled_desno[simp]:
379 shows "a ⊕ Sled b = Sled (a ⊕ b)"
380 by (induction a) auto
381
382 ―‹1.0 --- odavde krećemo›
383 lemma saberi_kom:
384 shows "a ⊕ b = b ⊕ a"
385 apply (induction a)
386 apply auto
387 done
388
389 text‹Sada ovaj dokaz može da se skrati na @{text "by (induction a) auto"}.›
390
391 lemma saberi_kom':
392 shows "a ⊕ b = b ⊕ a"
393 by (induction a) auto
394
395 text‹Napomena: voditi računa o korišćenju @{text "[simp]"} prilikom dokazivanja teorema. U
396 nekim situacijama (kao u prethodnom primeru) nam to koristi, ali to neće važiti uvek.
397 Na primer, za komutativnost ne stavljamo @{text "[simp]"} da ne bismo napravili beskonačnu
398 petlju u simplifikatoru. Opšte pravilo kojeg se treba držati je da se leme ubacuju u
399 simplifikator ako je desna strana teoreme na neki način jednostavnija od leve strane (što
400 važi u teoremama iz prethodnog primera koje smo ubacivali u simplifikator).›
401
402 text‹Prikazaćemo dokaz komutativnosti u Isar-u. Prvi korak dokaza biće svakako indukcija i
403 Isabelle odmah nudi opštu školjku dokaza koju možemo iskopirati (klikom na taj dokaz u
404 donjem delu ekrana). ›
405
406 lemma saberi_kom1:
407 shows "a ⊕ b = b ⊕ a"
408 proof (induction a)
409 case nula ―‹baza indukcije›
410 then show ?case sorry
411 next
412 case (Sled a) ―‹induktivni korak›
413 then show ?case sorry
414 qed
415
416 ―‹kada raspisemo prvi slucaj dobijamo ›
417
418 lemma saberi_kom2:
419 shows "a ⊕ b = b ⊕ a"
420 proof (induction a)
421 case nula ―‹baza indukcije›
422 have "nula ⊕ b = b" by simp
423 also have "b = b ⊕ nula" by simp
424 finally show ?case . ―‹also... finally nam daje tranzitivnost›
425 ―‹. je skraceno za assumption, moze i by simp›
426 next
427 case (Sled a) ―‹induktivni korak›
428 then show ?case sorry
429 qed
430
431 ―‹a mozemo biti i precizniji i umesto by simp navesti specificno koje teoreme koristimo:›
432
433 lemma saberi_kom3:
434 shows "a ⊕ b = b ⊕ a"
435 proof (induction a)
436 case nula ―‹baza indukcije›
437 have "nula ⊕ b = b"
438 ―‹ by (simp only: saberi.simps(1))›
439 by (rule saberi.simps(1)) ―‹ili ovako bez ikakve automatizacije›
440 also have "b = b ⊕ nula"
441 ―‹@{text "by (simp only: saberi_nula_desno)"}›
442 ―‹@{text "by (rule saberi_nula_desno)"} ne prolazi zato sto nama treba b = b + 0, a
443 lema tvrdi da je a + 0 = a, pa moramo da obrnemo jednakost atributom symmetric›
444 thm saberi_nula_desno
445 thm saberi_nula_desno[symmetric]
446 by (rule saberi_nula_desno[symmetric])
447 finally show ?case .
448 next
449 case (Sled a) ―‹induktivni korak›
450 then show ?case sorry
451 qed
452
453
454 ―‹sada prelazimo na induktivni korak›
455
456 lemma saberi_kom4:
457 shows "a ⊕ b = b ⊕ a"
458 proof (induction a)
459 case nula ―‹baza indukcije›
460 have "nula ⊕ b = b"
461 by (rule saberi.simps(1))
462 also have "b = b ⊕ nula"
463 by (rule saberi_nula_desno[symmetric])
464 finally show ?case .
465 next
466 case (Sled a) ―‹induktivna hipoteza je a + b = b + a,
467 i treba da dokazemo da je Sled a + b = b + Sled a›
468 thm Sled
469 have "Sled a ⊕ b = Sled (a ⊕ b)" ―‹na osnovu definicije sabiranja›
470 by (rule saberi.simps(2))
471 also have "... = Sled (b ⊕ a)" ―‹posledica induktivne hipoteze koja na ovom mestu
472 ima ime Sled pa pozivanje na ih se zapisuje ovako›
473 ―‹ili @{text "by (subst Sed, rule refl)"}›
474 using Sled by simp
475 also have "... = b ⊕ Sled a"
476 thm saberi_Sled_desno ―‹nama treba simetrican oblik›
477 thm saberi_Sled_desno[symmetric]
478 by (rule saberi_Sled_desno[symmetric])
479 finally show ?case .
480 qed
481
482 text‹Napomena: ovi dokazi su previše detaljni, dovoljno nam je @{text "by simp"} u
483 ovakvim dokazima.›
484
485 text‹
486 \begin{exmp}
487 Primitivnom rekurzijom definisati operaciju mnozenja.
488 \end{exmp}›
489
490 text‹Odmah ćemo dodati i notaciju sa većim prioritetom nego sabiranje što je imalo.›
491
492 primrec pomnozi :: "prirodni ⇒ prirodni ⇒ prirodni" (infixl "⊗" 101) where
493 "nula ⊗ y = nula" |
494 "(Sled x) ⊗ y = x ⊗ y ⊕ y"
495
496 (* Mozemo zapisati i ovako:
497 "pomnozi nula y = nula" |
498 "pomnozi (Sled x) y = saberi (pomnozi x y) y" ―‹(x + 1) * y = x * y + y›
499 *)
500
501 value "pomnozi dva dva"
502 value "pomnozi dva (Sled dva)"
503
504 value "dva ⊗ dva"
505
506 text‹\begin{exmp}
507 Dokazati komutativnost množenja. Krećemo od 2.0.
508 \end{exmp}
509
510 Napomena: kada se testira naredni kod, sve između ovog teksta i leme označene sa 2.0
511 treba staviti pod komentar i onda deo pod deo koristiti.›
512
513 ―‹2.1.›
514 lemma pomnozi_nula_desno[simp]:
515 shows "a ⊗ nula = nula"
516 by (induction a) auto
517
518 ―‹2.2›
519 lemma pomnozi_Sled_desno[simp]:
520 shows "a ⊗ (Sled b) = a ⊕ a ⊗ b" ―‹posto smo vec dokazali komutativnost sabiranja manje
521 vise je svejedno kako cemo zapisati›
522 apply (induction a)
523 apply auto ―‹uspeo je prvi cilj ali drugi cilj ne, ako pogledamo drugi cilj vidimo
524 da je razlika u zagradama, posto je sabiranje levo asocijativno zagrade koje se ne vide
525 stoje sa leve strane --- pa nam treba lema koja dokazuje asocijativnost sabiranja›
526 apply (auto simp add: saberi_asoc)
527 done
528
529 ―‹ili krace zapisano:›
530 lemma pomnozi_Sled_desno':
531 shows "a ⊗ (Sled b) = a ⊕ a ⊗ b"
532 by (induction a) (auto simp add: saberi_asoc)
533
534 ―‹2.0 --- odavde krecemo›
535 lemma pomnozi_kom:
536 shows "a ⊗ b = b ⊗ a"
537 apply (induction a)
538 apply auto
539 ―‹ne prolazi, slicno kao za sabiranje zato sto ne znamo cemu je jednako b + 0;
540 dodajemo lemu 2.1›
541 ―‹posle dodavanja 2.1 - sada prolazi prvi cilj›
542 ―‹drugi cilj je transformisan sa leve strane ali ne zna da transformise desnu stranu pa
543 dodajemo novu lemu 2.2›
544 ―‹sada se transformise cilj i vidimo da mu nedostaje komutativnost sabiranja i
545 dodajemo ga uz auto›
546 apply (auto simp add: saberi_kom)
547 done
548
549 text‹Ovi dokazi se formiraju korak po korak, ovako kako je opisano u teksu iznad, ali
550 kada se jednom kreira dokaz i dodaju sve potrebne leme finalni dokaz može biti kraće
551 zapisan: @{text "by (induction a) (auto simp add: saberi_kom)"}›
552
553 text‹
554 \begin{exmp}
555 Dokazati da je množenje asocijativno. Krećemo od 3.0.
556 \end{exmp}›
557
558
559 ―‹3.1 distributivnost mnozenja prema sabiranju sa desne strane›
560 lemma pomnozi_saberi_distrib_desno:
561 shows "(a ⊕ b) ⊗ c = (a ⊗ c) ⊕ (b ⊗ c)"
562 apply (induction a)
563 (* apply auto *) ―‹prvi cilj prolazi›
564 ―‹drugi cilj ne prolazi i dobijamo da nam fali komutativnost i asocijativnost sabiranja
565 koje možemo eksplicitno dodati›
566 apply (auto simp add: pomnozi_kom saberi_asoc)
567 ―‹a mogli smo i pozvati sledgehammer i videti šta on nudi›
568 done
569
570 ―‹3.0›
571 lemma pomnozi_asoc:
572 shows "(a ⊗ b) ⊗ c = a ⊗ (b ⊗ c)"
573 apply (induction a) ―‹dobijamo dva cilja›
574 apply auto
575 ―‹prvi cilj prolazi ali drugi cilj ne prolazi;
576 i mozemo videti da nam nedostaje distributivnost mnozenja u odnosu na sabiranje pa
577 dodajemo lemu 3.1. Nakon što je formulišemo i dokažemo potrebno je eksplicitno dodati je
578 u metod koji se primenjuje.›
579 apply (auto simp add: pomnozi_saberi_distrib_desno)
580 done
581
582
583 text‹Ovakve dokaze dobijamo kada ga raspisujemo i sami pokušavamo da dokažemo, ali kada
584 jednom znamo kako dokaz izgleda možemo ga zapisati i kraće:›
585
586 lemma pomnozi_saberi_distrib_desno':
587 shows "(a ⊕ b) ⊗ c = (a ⊗ c) ⊕ (b ⊗ c)"
588 by (induction a) (auto simp add: pomnozi_kom saberi_asoc)
589
590 lemma pomnozi_asoc':
591 shows "(a ⊗ b) ⊗ c = a ⊗ (b ⊗ c)"
592 by (induction a) (auto simp add: pomnozi_saberi_distrib_desno)
593
594 text‹\begin{exmp}
595 Definisati operaciju stepenovanja prirodnih brojeva
596 \end{exmp}›
597
598 text‹Zbog prirodnog načina definisanja stepenovanja, rekurzija se mora izvesti po drugom
599 argumentu ($x^0 = 1$, $x^(y+1) = x^y * x$). Pošto se u rekurzivnoj definiciji javlja
600 jedinica, a videli smo da se broj jedan može uvesti i pomoću definicije i pomoću skraćenice,
601 u narednom kodu je potrebno da stoji jedinica uvedena pomoću skraćenice (\emph{abbreviation}).›
602
603 primrec stepenuj :: "prirodni ⇒ prirodni ⇒ prirodni" (infixl "△" 102) where
604 "x △ nula = jedan" |
605 "x △ (Sled y) = x △ y ⊗ x"
606
607 thm stepenuj.simps(1)
608 thm stepenuj.simps(2)
609
610 text‹Sa funkcijom @{text "value"} proveravamo da li smo dobro definisali našu novu funkciju:›
611
612 value "stepenuj dvojka dvojka"
613 value "stepenuj dvojka (Sled dvojka)"
614
615 ―‹Sada cemo pokusati da dokazemo neke osobine koje vaze za stepenovanje. ›
616
617 text‹\begin{exmp}
618 Dokazati da vazi: $a^1 = a$.
619 \end{exmp}›
620
621 lemma "a △ jedan = a"
622 by auto
623
624 text‹Ova lema se dokazuje automatski, @{term jedan} je skraćenica za @{term "Sled nula"},
625 a druga jednakost se automatski izračunava iz definicije stepenovanja.›
626
627 text‹\begin{exmp}
628 Dokazati da važi: $a ^ (b + c) = a ^ b + a ^ c$
629 \end{exmp}›
630
631 text‹Pošto je stepenovanje definisano rekurzivno po drugom parametru, treba i indukciju da
632 sprovedemo po drugom parametru, ali sabiranje je definisano rekurzivno po prvom parametru
633 pa ovde biramo zbog toga indukciju po b.›
634
635 ―‹4.0›
636 lemma stepenuj_na_zbir:
637 shows "a △ (b ⊕ c) = a △ b ⊗ a △ c"
638 apply (induction b)
639 (* apply auto *)
640 ―‹prvi slucaj prolazi automatski, ali drugi slucaj ne prolazi, vidimo da fali
641 komutativnost mnozenja (a mozda i asocijativnost)›
642 (* sledgehammer *)
643 using pomnozi_asoc pomnozi_kom by auto
644
645 ―‹krace zapisano›
646 lemma "a △ (b ⊕ c) = a △ b ⊗ a △ c"
647 using pomnozi_asoc pomnozi_kom by (induction b) auto
648
649
650 text‹U ovom dokazu možemo da primetimo da dosadašnji način dodavanja informacija
651 automatskom dokazivaču (sa naredbom @{text "auto simp add"}) ne uspeva da dokaže našu lemu.
652 Ali dokaz prolazi kada se koristi naredba @{text "Using"}. Razlika je u tom da kada se
653 teoreme zadaju pomoću \emph{Using}, tokom procesa simplifikacije one se uprošćavaju i
654 koriste u svom uprošćenom obliku, naspram naredbe @{text "auto simp add"} koji ih ne
655 uprošćava i koristi ih u izvornom obliku. Ove sitne razlike nekada mogu uticati na uspešnost
656 našeg dokaza pa ima smisla pokušati sa obema verzijama i videti koja prolazi.›
657
658 text‹\begin{exmp}
659 Dokazati da važi: $a^(b*c) = (a^b)^c$. Krećemo od 5.0.
660 \end{exmp}›
661
662 ―‹5.1›
663 lemma stepenuj_jedan:
664 shows "jedan △ a = jedan"
665 by (induction a) auto
666
667 ―‹5.2›
668 lemma stepenuj_proizvod:
669 shows "(a ⊗ b) △ c = a △ c ⊗ b △ c"
670 apply (induction c)
671 apply auto ―‹prvi cilj nestaje›
672 ―‹ostaje drugi cilj koji koristi komutativnost i asocijativnost mnozenja›
673 (* sledgehammer *)
674 by (metis pomnozi_asoc pomnozi_kom)
675
676 ―‹5.0›
677 lemma stepenuj_na_proizvod:
678 "a △ (b ⊗ c) = (a △ b) △ c"
679 apply (induction b)
680 (* apply auto *)
681 ―‹ni prvi podcilj ne prolazi, stao je kod jedan = jedan ^ c, pa uvodimo novu lemu 5.1›
682 apply (auto simp add: stepenuj_jedan)
683 ―‹sada nam ostaje drugi cilj, u njegovoj levoj strani imamo _^(_+_), a desno (_*_)^_
684 tj. stepenovanje na zbir (nju imamo) i kako se stepenuje proizvod (nju moramo da dodamo)
685 5.2›
686 apply (auto simp add: stepenuj_proizvod stepenuj_na_zbir)
687 done
688
689 subsection ‹ Zadaci za vežbanje ›
690
691 text‹Dokazati sve leme sa predavanja u Isar-u:›
692
693 text‹\begin{exmp}
694 "a + 0 = a"
695 \end{exmp}›
696
697 lemma saberi_nula_desno_isar:
698 shows "a ⊕ nula = a"
699 proof (induction a)
700 case nula
701 show ?case
702 by (simp only: saberi.simps(1))
703 next
704 case (Sled a)
705 show ?case
706 proof-
707 have "Sled a ⊕ nula = Sled (a ⊕ nula)"
708 by (simp only: saberi.simps(2))
709 also have "... = Sled a"
710 using Sled
711 by simp
712 finally
713 show ?thesis
714 .
715 qed
716 qed
717
718 text‹\begin{exmp}
719 @{text "a ⊕ Sled b = Sled (a ⊕ b)"}
720 \end{exmp}›
721
722 lemma saberi_Sled_desno_isar:
723 shows "a ⊕ Sled b = Sled (a ⊕ b)"
724 proof (induction a)
725 case nula
726 show ?case
727 by (simp only: saberi.simps(1))
728 next
729 case (Sled a)
730 show ?case
731 proof-
732 have "Sled a ⊕ Sled b = Sled (a ⊕ Sled b)"
733 by (simp only: saberi.simps(2))
734 also have "... = Sled (Sled (a ⊕ b))"
735 using Sled
736 by simp
737 finally
738 show ?thesis
739 by (simp only: saberi.simps(2))
740 qed
741 qed
742
743 text‹\begin{exmp}
744 @{text "a ⊕ (b ⊕ c) = (a ⊕ b) ⊕ c"}
745 \end{exmp}›
746
747 lemma saberi_asoc_isar:
748 shows "a ⊕ (b ⊕ c) = (a ⊕ b) ⊕ c"
749 proof (induction a)
750 case nula
751 then
752 show ?case
753 by (simp only:saberi.simps(1))
754 next
755 case (Sled a)
756 then show ?case
757 proof -
758 have "(Sled a ⊕ b) ⊕ c = Sled (a ⊕ b) ⊕ c" by (simp only: saberi.simps(2))
759 also have "... = Sled ((a ⊕ b) ⊕ c)" by (simp only: saberi.simps(2))
760 also have "... = Sled (a ⊕ (b ⊕ c))" using Sled by simp
761 (*
762 also have "... = Sled a ⊕ (b ⊕ c)" by (simp only: saberi.simps(2))
763 finally show ?thesis .
764 *)
765 finally show ?thesis by (simp only: saberi.simps(2))
766 qed
767 qed
768
769 text‹\begin{exmp}
770 @{text "a ⊕ b = b ⊕ a"}
771 \end{exmp}›
772
773 lemma saberi_kom_isar:
774 shows "a ⊕ b = b ⊕ a"
775 proof (induction a)
776 case nula
777 then show ?case by (simp only: saberi.simps(1) saberi_nula_desno)
778 next
779 case (Sled a)
780 then show ?case
781 proof -
782 have "Sled a ⊕ b = Sled(a ⊕ b)" by (simp only: saberi.simps(2))
783 also have "... = Sled(b ⊕ a)" using Sled by simp
784 also have "... = b ⊕ Sled a" by (simp only: saberi_Sled_desno)
785 finally show ?thesis .
786 qed
787 qed
788
789 text‹\begin{exmp}
790 Definisati funkciju @{text "duplo"} koja računa dvostruku vrednost broja.
791 \end{exmp}›
792
793 primrec duplo :: "prirodni ⇒ prirodni" where
794 "duplo nula = nula" |
795 "duplo (Sled n) = Sled (Sled (duplo n))"
796
797 value "(duplo (Sled (Sled nula)))"
798
799 text‹\begin{exmp}
800 Dokazati da je vrednost funkcije duplo jednaka sabiranju broja sa samim sobom. Napisati
801 i dokaz uz pomoć automatskih alata i dokaz u Isar-u.
802 \end{exmp}›
803
804 lemma duplo_zbir: "duplo n = n ⊕ n"
805 apply (induction n)
806 apply (auto)
807 done
808
809 lemma duplo_zbir_isar: "duplo n = n ⊕ n"
810 proof (induction n)
811 case nula
812 then show ?case by (simp only: duplo.simps(1) saberi.simps(1))
813 next
814 case (Sled a)
815 then show ?case
816 proof -
817 have "duplo(Sled a) = Sled(Sled(duplo a))" by (simp only: duplo.simps(2))
818 also have "... = Sled(Sled(a ⊕ a))" using Sled by simp
819 also have "... = Sled(Sled a ⊕ a)" by (simp only: saberi.simps(2))
820 finally show ?thesis by (simp only: saberi_Sled_desno)
821 qed
822 qed
823
824 text‹\begin{exmp}
825 Definisati funkciju koja računa zbir brojeva od 1 do n.
826 \end{exmp}›
827
828 primrec zbir_do :: "prirodni ⇒ prirodni" where
829 "zbir_do nula = nula"
830 | "zbir_do (Sled n) = (Sled n) ⊕ (zbir_do n)"
831
832 text‹\begin{exmp}
833 Dokazati da vazi @{text "duplo(a ⊕ b) = duplo a ⊕ duplo b"}, uz automatske alate i u Isar-u.
834
835 Napomena: Ova lema se koristi u dokazu narednog zadatka pa je zato dodata ovde. Inače bio
836 bi zadat samo naredni zadatak a na studentima bi bilo da otkriju da je ova lema potrebna.
837 \end{exmp}›
838
839 lemma duplo_od_zbira:
840 "duplo (a ⊕ b) = duplo a ⊕ duplo b"
841 by (induction a) auto
842
843 lemma duplo_od_zbira_isar:
844 "duplo (a ⊕ b) = duplo a ⊕ duplo b"
845 proof (induction a)
846 case nula
847 then show ?case by (simp only: duplo.simps(1) saberi.simps(1))
848 next
849 case (Sled a)
850 then show ?case
851 proof -
852 have "duplo (Sled a ⊕ b) = duplo (Sled (a ⊕ b))" by (simp only: saberi.simps(2))
853 also have "... = Sled (Sled (duplo (a ⊕ b)))" by (simp only: duplo.simps(2))
854 also have "... = Sled (Sled (duplo a ⊕ duplo b))" using Sled by simp
855 also have "... = Sled (Sled (duplo a) ⊕ duplo b)" by (simp only: saberi.simps(2))
856 also have "... = Sled (Sled (duplo a)) ⊕ duplo b" by (simp only: saberi.simps(2))
857 also have "... = duplo (Sled a) ⊕ duplo b" by (simp only: duplo.simps(2))
858 finally show ?thesis .
859 qed
860 qed
861
862 text‹\begin{exmp}
863 Dokazati da vazi @{text "duplo(zbir_do n) = n ⊗ Sled n"}, uz automatske alate i u Isar-u.
864 \end{exmp}›
865
866 thm pomnozi.simps(1)
867 thm zbir_do.simps(1)
868 thm duplo.simps(1)
869
870 lemma suma_do: "duplo(zbir_do n) = n ⊗ Sled n"
871 apply (induction n)
872 apply auto
873 apply (auto simp add: duplo_od_zbira)
874 by (metis duplo_zbir pomnozi.simps(2) pomnozi_kom saberi_asoc saberi_kom)
875
876 lemma suma_do_isar: "duplo(zbir_do n) = n ⊗ Sled n"
877 proof (induction n)
878 case nula
879 then show ?case by (simp only: pomnozi.simps(1) zbir_do.simps(1) duplo.simps(1))
880 next
881 case (Sled n)
882 show ?case
883 thm Sled
884 proof -
885 have "duplo (zbir_do (Sled n)) = duplo ((Sled n) ⊕ (zbir_do n))"
886 by (simp only: zbir_do.simps(2))
887 also have "... = duplo(Sled n) ⊕ duplo(zbir_do n)" by (simp only: duplo_od_zbira)
888 also have "... = duplo(Sled n) ⊕ (n ⊗ (Sled n))" using Sled by simp
889 also have "... = Sled n ⊕ Sled n ⊕ n ⊗ (Sled n)" by (simp only: duplo_zbir)
890 also have "... = Sled n ⊕ (Sled n) ⊗ (Sled n)" by (simp add: pomnozi_kom saberi_asoc_isar)
891 also have "... = Sled (Sled n) ⊗ (Sled n)" by (simp add: pomnozi_kom saberi_asoc_isar)
892 also have "... = (Sled n) ⊗ Sled (Sled n)" by (simp add: pomnozi_kom)
893 finally show ?thesis .
894 qed
895 qed
896
897 text‹Sve naredne leme dokazati u Isar-u:›
898
899 lemma "a ⊗ nula = nula" sorry
900
901 lemma "a ⊗ (Sled b) = a ⊗ b ⊕ a" sorry
902
903 lemma "(a ⊕ b) ⊗ c = a ⊗ c ⊕ b ⊗ c" sorry
904
905 lemma "(a ⊗ b) ⊗ c = a ⊗ (b ⊗ c)" sorry
906
907 lemma "a ⊗ b = b ⊗ a" sorry
908
909 lemma "a ⊗ (b ⊕ c) = a ⊗ b ⊕ a ⊗ c" sorry
910
911 end
912