1 section‹Dokazi po slučajevima› 2 3 theory Cas7_vezbe_resenja 4 imports Main 5 begin 6 7 subsection ‹The Drinker's principle› 8 9 text‹ 10 \begin{exmp} 11 Paradoks pijanca: postoji osoba za koju važi, ako je on pijanac onda su i svi 12 ostali pijanci. 13 \end{exmp} 14 › 15 16 17 text‹Prvo ćemo dokazati klasični deo de-Morganovog zakona› 18 19 lemma de_Morgan: "(¬ (∀ x. P x)) ⟶ (∃ x. ¬ P x)" 20 apply (rule impI) 21 apply (rule classical) ―‹prebacujemo negaciju zaključka na levu stranu› 22 apply (erule notE) 23 apply (rule allI) 24 apply (rule classical) 25 apply (erule notE) 26 apply (rule_tac x = "x" in exI) 27 apply assumption 28 done 29 30 text‹Dokaz iste leme u Isar-u:› 31 32 lemma de_Morgan1: 33 assumes "¬ (∀ x. P x)" 34 shows "∃ x. ¬ P x" 35 proof (rule classical) ―‹isto pravilo primenjujemo kao malopre› 36 assume "¬ (∃ x. ¬ P x)" ―‹imitiramo gornji dokaz i dodajemo među korak› 37 have "∀ x. P x" 38 proof 39 ―‹ostavljamo bez crtice pošto dobijamo oblik koji nam treba: fix... show...› 40 fix x show "P x" 41 proof (rule classical) ―‹isti korak kao u prethodnom dokazu› 42 assume "¬ P x" 43 then have "∃ x. ¬ P x" by auto 44 from this `¬ (∃ x. ¬ P x)` 45 show "P x" by auto 46 qed 47 qed 48 from this `¬ (∀ x. P x)` 49 show "∃ x. ¬ P x" by auto 50 qed 51 52 text‹Sada ćemo pogledati dokaz samog paradoksa pijanca. Prvo ćemo prikazati dokaz u Isar-u. 53 U njemu ćemo koristiti naredbu 54 @{text "proof cases"} koja nam omogućava dokazivanje po slučajevima u okviru 55 samog dokaza. Odnosi se na pravilo: @{text "(A ==> C) ==> (¬ A ==> C) ==> C"}, 56 pa se nakon naredbe \emph{proof cases} dokaz deli na dva 57 poddokaza, odnosno na dve grane razdvojene sa \emph{next}. 58 Lokalne pretpostavke @{text A} (u prvoj grani), odnosno @{text "¬ A"} (u drugoj grani), 59 se uvode ključnom rečju \emph{assume}.› 60 61 text‹U narednom dokazu koristi se skraćenica @{text "?thesis"} koja se implicitno povezuje 62 sa tekućim ciljem (koji je prethodno bio naveden pod \emph{lemma} ili \emph{show}).› 63 64 lemma Drinker's_Principle: "∃ x. (drunk x ⟶ (∀ x. drunk x))" 65 proof cases 66 ―‹Narednom naredbom možemo videti šta je tekući cilj. Skraćenica @{text "?thesis"} 67 može biti korišćena nadalje u dokazu uz naredbu @{text show} umesto navođenja formule 68 koja se dokazuje.› 69 term ?thesis ―‹ova naredba nije deo dokaza, može se obrisati, dodata je zbog ispisa› 70 assume "∀ x. drunk x" 71 fix a ―‹uvešćemo proizvoljno a, bez ikakvih dodatnih pretpostavki o njemu› 72 ―‹sada bez obzira na to da li važi @{text "drunk a"} ili @{text "¬ drunk a"}, 73 važiće naredna formula; 74 na osnovu teoreme @{text "A ⟶ B ⟷ ¬ A ∨ B"}; odnosno na osnovu leme 75 @{text "B ⟶ (A ⟶ B)"}› 76 from `∀ x. drunk x` have "drunk a ⟶ (∀ x. drunk x)" by auto 77 then show ?thesis by auto ―‹kraj dokaza prve grane› 78 next 79 assume "¬ (∀ x. drunk x)" 80 then have "∃ x. ¬ drunk x" by (auto simp add: de_Morgan) 81 then obtain a where "¬ drunk a" by auto 82 ―‹sada pokazujemo da važi naredna implikacija, posto važi @{text "¬ A"}, važiće i 83 @{text "A ⟶ B"} na osnovu leme @{text "¬ A ⟶ (A ⟶ B)"}› 84 have "drunk a ⟶ (∀ x. drunk x)" 85 proof 86 assume "drunk a" 87 with `¬ drunk a` show "∀ x. drunk x" by auto 88 qed 89 then show ?thesis by auto 90 qed 91 92 text‹Sada ćemo videti tri verzije dokaza uz pomoć pravila prirodne dedukcije. Prve dve 93 verzije će u sebi koristiti već dokazanu lemu, a treća verzija će prikazati direktan dokaz. 94 95 Videćemo i razliku između primene lema @{text de_Morgan} (zapisane sa @{text "⟶"}) i 96 @{text de_Morgan1} (zapisane sa @{text "⟹"}). 97 98 Naredba @{text "[rule_format]"} naglašava Isabelle-u da se svako @{text "⟶"} zameni sa 99 @{text "⟹"} pre čuvanja ili primene dokazane leme. 100 101 Ako bi se prilikom navođenja leme @{text de_Morgan} navela naredba @{text "[rule_format]"}, 102 ova razlika bi nestala. Drugi način za primenu ove naredbe jeste prilikom samog pozivanja 103 leme, što će biti urađeno u narednom dokazu.› 104 105 lemma Drinker's_Principle1: 106 "∃ x. (drunk x ⟶ (∀ x. drunk x))" 107 apply (cases "∀ x. drunk x") 108 ―‹prva grana, ako je ova pretpostavka tacna onda nam nije bitan svedok› 109 apply (rule exI) 110 apply (rule impI) 111 apply assumption 112 ―‹druga grana› 113 ―‹Koristimo pravilo @{text subgoal_tac} da bismo dodali novu pretpostavku koji ćemo koristiti 114 u dokazu konačnog cilja. Tek nakon dokazivanja konačnog cilja se dokazuje ovaj medjukorak, 115 tj. pretpostavka koja je korišćena.› 116 apply (subgoal_tac "∃ x. ¬ drunk x") 117 apply (erule exE) 118 apply (rule_tac x = "x" in exI) 119 apply (rule impI) 120 ―‹sada u pretpostavkama imamo @{text "¬ drunk x"} i @{text "drunk x"}, pa želimo da primenimo 121 pravilo notE upravo na @{text "¬ drunk x"}. Zbog toga nam treba back. › 122 apply (erule notE) back 123 apply assumption 124 ―‹sada je dokazan konačni cilj. Ostaje nam da dokažemo medjukorak direktnom primenom 125 leme @{text "de_Morgan1"} ili leme @{text "de_Morgan"} nakon što je transformišemo u 126 odgovarajući oblik naredbom @{text "[rule_format]"}.› 127 apply (rule de_Morgan[rule_format]) ―‹ili @{text "apply (rule de_Morgan1)"}› 128 apply assumption 129 done 130 131 132 text‹Drugi način: U narednom dokazu koristimo frule pravilo. Ono je nalik erule pravilu (označava 133 forward-resolution) s tim što se pravilo pre primenjivanja transformiše u kanonski oblik. 134 Pored toga, pretpostavka na koju je pravilo primenjeno se ne briše iz skupa pretpostavki.› 135 136 lemma Drinker's_Principle2: 137 "∃ x. (drunk x ⟶ (∀ x. drunk x))" 138 apply (cases "∀ x. drunk x") 139 apply (rule exI) 140 apply (rule impI) 141 apply assumption 142 ―‹druga grana› 143 apply (frule de_Morgan[rule_format]) 144 apply (erule exE) 145 apply (rule_tac x=x in exI) 146 apply (rule impI) 147 apply (erule notE) 148 back 149 apply assumption 150 done 151 152 text‹Treći način: direktan dokaz:› 153 154 lemma Drinker's_Principle3: 155 "∃ x. (drunk x ⟶ (∀ x. drunk x))" 156 apply (cases "∀ x. drunk x") 157 ―‹prva grana, ako je ova pretpostavka tacna onda nam nije bitan svedok› 158 apply (rule exI) 159 apply (rule impI) 160 apply assumption 161 ―‹druga grana --- drugi način, direktni dokaz› 162 apply (rule ccontr) 163 apply (erule notE) 164 apply (rule allI) 165 apply (rule ccontr) 166 apply (erule notE) 167 apply (rule_tac x = "x" in exI) 168 apply (rule impI) 169 apply (erule notE) 170 apply assumption 171 done 172 173 subsection‹Smullyan - Logical Labirinths› 174 175 text‹Dokazi u iskaznoj, predikatskoj logici: 176 Raymond M. Smullyan, Logical Labyrinths 177 @{url "http://logic-books.info/sites/default/files/logical_labirints.pdf"} 178 › 179 180 text‹Sada ćemo se podsetiti primera sa početka kursa: 181 Edgar Abercrombie was an anthropologist who was particularly interested in the logic and 182 sociology of lying and truth-telling. One day he decided to visit a cluster of islands 183 where a lot of lying and truth-telling activity was going on! The first island of his 184 visit was the Island of Knights and Knaves in which those called knights always tell 185 the truth and knaves always lie. Furthermore, each inhabitant is either a knight or a knave. 186 187 Formule koje ćemo koristiti za zapisivanje tvrđenja: 188 \begin{itemize} 189 \item @{text kA} - Osoba A je vitez 190 \item @{text "¬ kA"} - Osoba A je podanik 191 \item @{text "kA ⟷ B"} - Osoba A je rekla činjenicu B 192 \item @{text "kA ⟷ (Q ⟷ yes)"} - Osoba A je odgovorila sa yes na yes/no pitanje Q 193 \end{itemize} 194 › 195 196 text‹Kada želimo da unapred naglasimo po kojim pretpostavkama ćemo granati dokaz 197 (ili ako su same pretpostavke previše dugačke pa ne želimo da ih prepisujemo - kao što bismo 198 morali sa prethodnim metodom), možemo na sledeći način koristiti metod 199 @{text "proof cases"}: \emph{proof (cases "A")}. Ovakav zapis se suštinski ne razlikuje 200 od prethodnog dokaza, samo je razlika u sintaksi.› 201 202 text‹ 203 \begin{exmp} 204 Every person answers @{text yes} to the question "Are you a knight?" 205 \end{exmp} 206 › 207 208 text‹Kada se postavi pitanje proizvoljnom stanovniku ostrva "Da li si ti vitez?", imamo 209 dve mogućnosti. Osoba je ili vitez ili podanik. Ako je osoba vitez ona će odgovoriti iskreno 210 i dobićemo odgovor Da, sa druge strane ako je osoba podanik, ona će lagati i daće nam isti 211 odgovor Da. Pitanje "Da li je k vitez?" se kodira sa @{text "(k ⟷ yes)"}, a pošto pitanje 212 postavljamo upravo osobi k, u kombinaciji sa formulama za zapisivanje tvrđenja sa prethodne 213 strane, možemo da formulišemo narednu lemu:› 214 215 lemma no_one_admits_knave: 216 assumes "k ⟷ (k ⟷ yes)" 217 shows "yes" 218 proof (cases "k") 219 ―‹sada se dokaz razbija u dve grane, jedna koja odgovara slučaju @{text True} (odnosno kada 220 je pretpostavka tačna i važi @{text k}) i drugu koja odgovara slučaju @{text False} (kada je 221 pretpostavka netačna, odnosno važi @{text "¬ k"}). Kao i ranije, ovakve grane su razdvojene 222 ključnom rečju next.› 223 ―‹Isabelle automatski nudi kostur ovakvog dokaza koji možemo automatski preuzeti kada 224 kliknemo na njega (u donjem delu ekrana), ili možemo sami izabrati koji deo tog kostura 225 nam treba pa prepisati.› 226 case True 227 from this assms have "k ⟷ yes" by auto 228 from this `k` show "yes" by auto 229 next 230 case False 231 from this assms have "¬ (k ⟷ yes)" by auto 232 from this have "¬ k ⟶ yes" by auto ―‹dodajemo među korak, koji se dokazuje sa by auto› 233 from this `¬ k` show "yes" by auto 234 qed 235 236 text‹ 237 \begin{exmp} 238 [Problem 1.1.] On the day of his arrival, Abercrombie came across three inhabitants, 239 whom we will call A, B and C. He asked A: Are you a knight or a knave? A answered, 240 but so indistinctly that Abercrombie could not understand what he said. He then asked B: 241 What did he say? B replied: He said that he is a knave. At this point, C piped up and said: 242 Don't believe that; it's a lie! Was C a knight or a knave? 243 \end{exmp} 244 › 245 246 lemma Smullyan_1_1: 247 assumes "kA ⟷ (kA ⟷ yesA)" 248 assumes "kB ⟷ ¬ yesA" 249 assumes "kC ⟷ ¬ kB" 250 shows "kC" 251 ―‹sledgehammer --- prvo pokušavamo sa sledgehammer i on daje sledeće rešenje: 252 @{text "using assms(1) assms(2) assms(3) by auto"}› 253 ―‹Takođe može se pokušati sa drugačijim zaključkom: @{text "shows ¬ kC"} u kom slučaju 254 sledgehammer neće naći rešenje u zadatom vremenskom ograničenju.› 255 256 proof - 257 ―‹izvešćemo nekoliko međukoraka› 258 from assms(1) have "yesA" by (auto simp add: no_one_admits_knave) 259 from this assms(2) have "¬ kB" by auto 260 from this assms(3) show "kC" by auto 261 qed 262 263 text‹ 264 \begin{exmp} 265 [Problem 1.2.] According to another version of the story, Abercrombie didn't ask A whether 266 he was a knight or a knave (because he would have known in advance what answer he would 267 get), but instead asked A how many of the three were knaves. Again A answered indistinctly, 268 so Abercrombie asked B what A had said. B then said that A had said that exactly two of 269 them were knaves. Then, as before, C claimed that B was lying. Is it now possible to 270 determine whether C is a knight or a knave? 271 \end{exmp} 272 › 273 274 text‹Pošto sada u postavci zadatka figuriše izjava oblika: Tačno dva od tri zadovoljavaju 275 neko svojstvo, potrebno je uvesti narednu definiciju (koja je tačna samo ako su tačno dve 276 od tri logičke vrednosti tačne):› 277 278 definition exactly_two where 279 "exactly_two A B C ⟷ ((A ∧ B) ∨ (A ∧ C) ∨ (B ∧ C)) ∧ ¬ (A ∧ B ∧ C)" 280 281 text‹Sada je lako formulisati traženo tvrđenje:› 282 283 lemma Smullyan_1_2: 284 assumes "kA ⟷ (exactly_two (¬ kA) (¬ kB) (¬ kC) ⟷ yesA)" 285 assumes "kB ⟷ yesA" 286 assumes "kC ⟷ ¬ kB" 287 shows "kC" 288 ―‹Isto kao i ranije, prvo testiramo sa sledgehammer i dobijamo: 289 @{text "using assms(1) assms(2) exactly_two_def by auto"}› 290 proof (rule ccontr) 291 assume "¬ kC" 292 from this assms have "kB" "yesA" by auto 293 show False 294 proof (cases "kA") 295 case True 296 from this assms(1) `yesA` have "exactly_two (¬ kA) (¬ kB) (¬ kC)" by auto 297 from this `kA` `kB` `¬ kC` show False unfolding exactly_two_def by auto 298 next 299 case False 300 from this assms(1) `yesA` have "¬ exactly_two (¬ kA) (¬ kB) (¬ kC)" by auto 301 from this `¬ kA` `kB` `¬ kC` show False unfolding exactly_two_def by auto 302 qed 303 qed 304 305 306 text‹ 307 \begin{exmp} 308 B said that exactly two of them were knights. Does this change the conclusion? 309 \end{exmp}› 310 311 lemma Smullyan_1_2': 312 assumes "kA ⟷ (exactly_two kA kB kC ⟷ yesA)" 313 assumes "kB ⟷ yesA" 314 assumes "kC ⟷ ¬ kB" 315 shows "¬ kC" 316 ―‹isto kao i ranije, prvo testiramo sa sledgehammer i dobijamo 317 @{text "using assms(1) assms(2) exactly_two_def by auto"}› 318 proof (rule ccontr) 319 ―‹ovaj dokaz je mogao biti napisan i samo sa proof i assume "kC" - pokušajte› 320 assume "¬ ¬ kC" 321 from this assms have "kC" "¬ kB" "¬ yesA" by auto 322 show False 323 proof (cases "kA") 324 case True 325 from this `¬ yesA` assms(1) have "¬ exactly_two kA kB kC" by auto 326 from this `kA` `¬ kB` `kC` show False unfolding exactly_two_def by auto 327 next 328 case False 329 from this `¬ yesA` assms(1) have "exactly_two kA kB kC" by auto 330 from this `¬ kA` `¬ kB` `kC` show False unfolding exactly_two_def by auto 331 qed 332 qed 333 334 text‹\begin{exmp} 335 Problem 1.3. Next, Abercrombie met just two inhabitants, A and B. A made the following 336 statement: "Both of us are knaves." What is A and what is B? 337 \end{exmp}› 338 339 lemma Smullyan_1_3: 340 assumes "kA ⟷ ¬ kA ∧ ¬ kB" 341 shows "¬ kA ∧ kB" 342 ―‹using assms 343 by auto› 344 proof (cases kA) 345 case True 346 from this assms have "¬ kA ∧ ¬ kB" by auto 347 from this `kA` have False by auto 348 from this show ?thesis by auto 349 next 350 case False 351 from this assms have "¬ (¬ kA ∧ ¬ kB)" by auto 352 from this have "kA ∨ kB" by auto 353 from this `¬ kA` have "kB" by auto 354 from this `¬ kA` show ?thesis by auto 355 qed 356 357 text‹\begin{exmp} 358 Problem 1.4. According to another version of the story, A didn't say "Both of us are knaves." 359 All he said was "At least one of us is a knave." If this version is correct, what are A and B? 360 \end{exmp}› 361 362 lemma Smullyan_1_4: 363 assumes "kA ⟷ ¬ kA ∨ ¬ kB" 364 shows "kA ∧ ¬ kB" 365 ―‹using assms 366 by auto› 367 proof (cases kA) 368 case True 369 from this assms have "¬ kA ∨ ¬ kB" by auto 370 from this `kA` have "¬ kB" by auto 371 from this `kA` show ?thesis by auto 372 next 373 case False 374 from this assms have "¬ (¬ kA ∨ ¬ kB)" by auto 375 from this have "kA ∧ kB" by auto 376 from this `¬ kA` have False by auto 377 from this show ?thesis by auto 378 qed 379 380 text‹\begin{exmp} 381 Problem 1.5. According to still another version, what A actually said was 382 "We are of the same type: that is, we are either both knights or both knaves." 383 If this version is correct, then what can be deduced about A and B? 384 \end{exmp}› 385 386 lemma Smullyan_1_5: 387 assumes "kA ⟷ (kA ⟷ kB)" 388 shows "kB" ―‹u ovom primeru je zanimljivo da ništa ne mozemo da zaključimo o A. Pokušajte 389 da vidite zašto, logički, i uz pomoć Isabelle.› 390 ―‹using assms 391 by blast› 392 proof (cases kA) 393 case True 394 from this assms have "kA ⟷ kB" by auto 395 from this `kA` show ?thesis by auto 396 next 397 case False 398 from this assms have "¬ (kA ⟷ kB)" by auto 399 from this `¬ kA` show ?thesis by auto 400 qed 401 402 text‹\begin{exmp} 403 Problem 1.6. On one occasion, Abercrombie came across two natives who were lazily lying 404 in the sun. He asked one of them whether the other one was a knight and got an answer 405 (yes or no). He then asked the other native whether the first one was a knight, and got 406 an answer (yes or no). Were the two answers necessarily the same? 407 \end{exmp}› 408 409 text‹Odgovore ćemo označiti sa yesA i yesB i provera da li su odgovori isti se svodi na 410 @{text "yesA ⟷ yesB"}.› 411 412 lemma Smullyan_1_6: 413 assumes "kA ⟷ (kB ⟷ yesA)" 414 assumes "kB ⟷ (kA ⟷ yesB)" 415 shows "yesA ⟷ yesB" 416 ―‹using assms 417 by auto› 418 proof (cases kA) 419 case True 420 from this assms(1) have "kB ⟷ yesA" by auto 421 show ?thesis 422 proof (cases kB) 423 case True 424 from this `kB ⟷ yesA` have "yesA" by auto 425 from `kB` assms(2) have "kA ⟷ yesB" by auto 426 from this `kA` have "yesB" by auto 427 from this `yesA` show ?thesis by auto 428 next 429 case False 430 from this `kB ⟷ yesA` have "¬ yesA" by auto 431 from `¬ kB` assms(2) have "¬ (kA ⟷ yesB)" by auto 432 from this `kA` have "¬ yesB" by auto 433 from this `¬ yesA` show ?thesis by auto 434 qed 435 next 436 case False 437 from this assms(1) have "¬ (kB ⟷ yesA)" by auto 438 show ?thesis 439 proof (cases kB) 440 case True 441 from this `¬ (kB ⟷ yesA)` have "¬ yesA" by auto 442 from `kB` assms(2) have "kA ⟷ yesB" by auto 443 from this `¬ kA` have "¬ yesB" by auto 444 from this `¬ yesA` show ?thesis by auto 445 next 446 case False 447 from this `¬ (kB ⟷ yesA)` have "yesA" by auto 448 from `¬ kB` assms(2) have "¬ (kA ⟷ yesB)" by auto 449 from this `¬ kA` have "yesB" by auto 450 from this `yesA` show ?thesis by auto 451 qed 452 qed 453 454 text‹\begin{exmp} 455 Problem 1.9. In the next incident, Abercrombie came across three natives, A, B, and C, 456 who made the following statements: 457 458 A: Exactly one of us is a knave. 459 460 B: Exactly two of us are knaves. 461 462 C: All of us are knaves. 463 464 What type is each? 465 \end{exmp}› 466 467 definition exactly_one where 468 "exactly_one A B C ⟷ (A ∨ B ∨ C) ∧ ¬((A ∧ B) ∨ (A ∧ C) ∨ (B ∧ C))" 469 470 lemma Smullyan_1_9: 471 assumes "kA ⟷ exactly_one (¬kA) (¬kB) (¬kC)" 472 assumes "kB ⟷ exactly_two (¬kA) (¬kB) (¬kC)" 473 assumes "kC ⟷ ¬ kA ∧ ¬ kB ∧ ¬ kC" 474 shows "¬ kC ∧ kB ∧ ¬ kA" 475 ―‹@{text "using assms unfolding exactly_one_def exactly_two_def by auto"}› 476 proof (cases kC) 477 case True 478 from this assms(3) have "¬ kA" "¬ kB" "¬ kC" by auto 479 from this `kC` have False by auto 480 from this show ?thesis by auto 481 next 482 case False 483 from this assms(3) have "¬ (¬ kA ∧ ¬ kB ∧ ¬ kC)" by auto 484 from this have "kA ∨ kB ∨ kC" by auto 485 from this `¬ kC` have "kA ∨ kB" by auto 486 from this show ?thesis 487 proof 488 assume "kA" 489 from this assms(1) have "exactly_one (¬kA) (¬kB) (¬kC)" by auto 490 from this `¬ kC` have "kB" unfolding exactly_one_def by auto 491 from this assms(2) have "exactly_two (¬kA) (¬kB) (¬kC)" by auto 492 from this `¬ kC` `kA` `kB` have False unfolding exactly_two_def by auto 493 from this show ?thesis by auto 494 next 495 assume "kB" 496 from this assms(2) have "exactly_two (¬kA) (¬kB) (¬kC)" by auto 497 from this `¬ kC` `kB` have "¬ kA" unfolding exactly_two_def by auto 498 from this `kB` `¬ kC` show ?thesis by auto 499 qed 500 qed 501 502 text‹\begin{exmp} 503 Problem 1.10. Abercrombie knew that the island had a chief and was curious to find him. 504 He finally narrowed his search down to two brothers named Og and Bog, and knew that one 505 of the two was the chief, but didn't know which one until they made the following 506 statements: 507 508 Og: Bog is the chief and he is a knave! 509 510 Bog: Og is not the chief, but he is a knight. 511 512 Which one is the chief? 513 \end{exmp}› 514 515 text‹Pošto je poglavica ili Og ili Bog i ne mogu biti poglavica istovremeno, možemo izjavu 516 "Bog is the chief" zapisati kao "Og is not the chief".› 517 518 lemma Smullyan_1_10: 519 assumes "Og ⟷ ¬ chief_Og ∧ ¬ Bog" 520 assumes "Bog ⟷ ¬ chief_Og ∧ Og" 521 shows "chief_Og" "¬ Og" "¬ Bog" 522 oops 523 524 text‹Zbog bržeg zapisivanja preimenovaćemo promenljive u ovom dokazu i koristićemo naredni 525 zapis umesto originalnog:› 526 527 lemma Smullyan_1_10': 528 assumes "A ⟷ ¬ C ∧ ¬ B" 529 assumes "B ⟷ ¬ C ∧ A" 530 shows "C ∧ ¬ A ∧ ¬ B" 531 proof (cases A) 532 case True 533 from this assms(1) have "¬ C ∧ ¬ B" by auto 534 from this have "¬ C" "¬ B" by auto 535 from this assms(2) have "¬ (¬ C ∧ A)" by auto 536 from this have "C ∨ ¬ A" by auto 537 from this `A` have "C" by auto 538 from this `¬ C` have False by auto 539 from this show ?thesis by auto 540 next 541 case False 542 from this assms(1) have "¬ (¬ C ∧ ¬ B)" by auto 543 from this have "C ∨ B" by auto 544 from this show ?thesis 545 proof 546 assume "C" 547 from this `¬ A` assms(2) have "¬ B" by auto 548 from this `¬ A` `C` show ?thesis by auto 549 next 550 assume "B" 551 from this assms(2) have "¬ C ∧ A" by auto 552 from this have "¬ C" "A" by auto 553 from this `¬ A` have False by auto 554 from this show ?thesis by auto 555 qed 556 qed 557 558 text‹\begin{exmp} 559 (Problem 1.11.) Suppose that you visit the Island of Knights and Knaves because you have 560 heard a rumor that there is gold buried there. You meet a native and you wish to find out 561 from him whether there really is gold there, but you don't know whether he is a knight or 562 a knave. You are allowed to ask him only one question answerable by yes or no. 563 \end{exmp}› 564 565 text‹The question is @{text "k ⟷ g"} i.e. are you a knight iff there is gold.› 566 567 lemma NelsonGoodman: 568 shows "(k ⟷ (k ⟷ g)) ⟷ g" 569 by auto 570 571 lemma Smullyan_1_11: 572 assumes "k ⟷ ((k ⟷ g) ⟷ yes)" 573 shows "yes ⟷ g" 574 ―‹ using assms 575 by auto› 576 proof (cases k) 577 case True 578 from this assms have "(k ⟷ g) ⟷ yes" by auto 579 show ?thesis 580 proof (cases g) 581 case True 582 from this `k` `(k ⟷ g) ⟷ yes` have "yes" by auto 583 from this `g` show ?thesis by auto 584 next 585 case False 586 from this `k` `(k ⟷ g) ⟷ yes` have "¬ yes" by auto 587 from this `¬ g` show ?thesis by auto 588 qed 589 next 590 case False 591 from this assms have "¬ ((k ⟷ g) ⟷ yes)" by auto 592 show ?thesis 593 proof (cases g) 594 case True 595 from this `¬ k` `¬ ((k ⟷ g) ⟷ yes)` have "yes" by auto 596 from this `g` show ?thesis by auto 597 next 598 case False 599 from this `¬ k` `¬ ((k ⟷ g) ⟷ yes)` have "¬ yes" by auto 600 from this `¬ g` show ?thesis by auto 601 qed 602 qed 603 604 text‹\begin{exmp} 605 (Problem 1.12.) There is an old problem in which it is said that the knights all live in 606 one village and the knaves all live in another. You are standing at a fork in the road and 607 one road leads to the village of knights, and the other to the village of knaves. You wish 608 to go to the village of knights, but you don't know which road is the right one. A native 609 is standing at the fork and you may ask him only one yes/no question. Of course, you could 610 use the Nelson Goodman principle and ask: "Are you a knight if and only if the left road 611 leads to the village of knights?" There is a much simpler and more natural-sounding 612 question, however, that would do the job: a question using only eight words. 613 Can you find such a question? 614 \end{exmp}› 615 616 text‹Question: does the left road lead to your village. 617 618 Suppose he answers yes. If he is a knight, then the left road really does lead to his 619 village, which is the village of knights. If he is a knave, then the left road doesn’t 620 lead to his village, which is the village of knaves, hence again, it leads to the village 621 of knights. So in either case, a yes answer indicates that you should take the left road. 622 623 Suppose he answers no. If he is a knight, then the left road really doesn’t lead to his 624 village, so the right road leads to his village, which is the village of knights. If he is 625 a knave, then the left road does lead to his village (since he indicates that it doesn’t), 626 which is the village of knaves, so again it is the right road that leads to the village of 627 knights. Thus, a no answer indicates that you should take the right road. 628 › 629 630 lemma Smullyan_1_12: 631 assumes "k ⟷ (((k ∧ l) ∨ (¬ k ∧ ¬ l)) ⟷ yes)" 632 shows "yes ⟷ l" 633 ―‹ using assms 634 by auto› 635 proof (cases k) 636 case True 637 from this assms have *: "((k ∧ l) ∨ (¬ k ∧ ¬ l)) ⟷ yes" by auto 638 from `k` have **: "k ∧ l ⟷ l" by auto 639 from `k` have "¬ (¬ k ∧ ¬ l)" by auto 640 from this * have "k ∧ l ⟷ yes" by auto 641 from this ** show ?thesis by auto 642 next 643 case False 644 from this assms have *: "¬ (((k ∧ l) ∨ (¬ k ∧ ¬ l)) ⟷ yes)" by auto 645 from `¬ k` have **: "¬ k ∧ ¬ l ⟷ ¬ l" by auto 646 from `¬ k` have "¬ (k ∧ l)" by auto 647 from this * have "¬ ((¬ k ∧ ¬ l) ⟷ yes)" by auto 648 from this ** have "¬ ((¬ l) ⟷ yes)" by auto 649 from this have "(¬ l ∧ ¬ yes) ∨ (l ∧ yes)" by auto 650 from this show ?thesis by auto 651 qed 652 653 text‹ 654 The next island visited by Abercrombie was a curious one in which women were also 655 classified as knights or knaves! And the most curious part of all is that while male 656 knights told the truth and male knaves lied, the females did the opposite: The female 657 knaves told the truth and the female knights lied! 658 › 659 660 text‹ 661 \begin{exmp} 662 [Problem 2.1.] Abercrombie was led into an auditorium, and an inhabitant of the island 663 came on the stage wearing a mask. Abercrombie was to determine whether the inhabitant 664 was male or female. He was allowed to ask only one yes/no question, and the inhabitant 665 would then write his or her answer on the blackboard (so as not to be betrayed by his 666 or her voice). 667 \end{exmp} 668 › 669 670 text‹ Odgovarajuće pitanje: Da li si ti vitez?› 671 672 text‹Svaka muška osoba bi odgovorila yes, na osnovu leme @{text no_one_admits_knave}: 673 @{text "assumes k ⟷ (k ⟷ yes) shows yes"}, koju smo već dokazali. 674 675 Svaka ženska osoba bi odgovorila no. Svaka ženska osoba može biti ili vitez ili 676 podanik. Ako je ženska osoba vitez ona će lagati i dobićemo odgovor Ne, sa druge strane 677 ako je osoba podanik, ona će govoriti istinu i daće nam odgovor Ne. 678 679 Otuda odgovor yes na ovo pitanje znači da je u 680 pitanju male (zadovoljeno m); odgovor no, znaci da je u pitanju female (nije zadovoljeno m); 681 Otuda možemo da zaključimo da važi ekvivalencija @{text "yes ⟷ m"}. 682 › 683 684 text‹ 685 Sada kada k može biti muško i žensko, dodajemo u lemu @{text no_one_admits_knave} i tu 686 pretpostavku, da je k upravo muško: 687 @{text "assumes (k ∧ m) ⟷ (k ⟷ yes) shows yes"}. 688 689 Napomena: samostalno, ovo nije valjana lema, već samo opis kako od već postojećih tvrđenja 690 možemo doći do formule koja nam treba za opis početnog problema. 691 › 692 693 text‹ 694 Svaka ženska osoba, analogno, na ovo pitanje bi odgovorila sa ne, tj. @{text "¬ yes"}. Prvo 695 možemo zameniti k sa leve strane sa @{text "¬ k"} (sa desne strane ostaje k zato što je to odgovor 696 na pitanje "da li si ti vitez"). A nakon toga možemo dodati pretpostavku da je u pitanju 697 ženska osoba (odnosno @{text "¬ m"}): 698 @{text "assumes (¬ k ∧ ¬ m) ⟷ (k ⟷ yes) shows ¬ yes"} 699 › 700 701 text‹Sada možemo spojiti ova dva tvrđenja u jedno:› 702 703 lemma Smullyan_2_1: 704 assumes "(m ∧ k) ∨ (¬ m ∧ ¬ k) ⟷ (k ⟷ yes)" (* or "(m ⟷ k) ⟷ (k ⟷ yes)" *) 705 shows "yes ⟷ m" 706 proof (cases "m") 707 case True 708 show "yes ⟷ m" 709 proof (cases "k") ―‹musko i vitez - govori istinu› 710 case True 711 from `k` `m` assms have "k ⟷ yes" by auto 712 from this `k` `m` show "yes ⟷ m" by auto 713 next 714 case False ―‹musko i nije vitez - laze› 715 from `¬ k` `m` assms have "¬ (k ⟷ yes)" by auto 716 from this `¬ k` have "yes" by auto 717 from this `m` show "yes ⟷ m" by auto 718 qed 719 next 720 case False ―‹zensko› 721 show "yes ⟷ m" 722 proof (cases "k") ―‹zensko i vitez - laze› 723 case True 724 from `k` `¬ m` assms have "¬ (k ⟷ yes)" by auto 725 from this `k` have "¬ yes" by auto 726 from this `¬ m` show "yes ⟷ m" by auto 727 next 728 case False ―‹zensko i nije vitez - govori istinu› 729 from `¬ k` `¬ m` assms have "k ⟷ yes" by auto 730 from this `¬ k` have "¬ yes" by auto 731 from this `¬ m` show "yes ⟷ m" by auto 732 qed 733 qed 734 735 text‹ 736 \begin{exmp} 737 Problem 2.2. The inhabitant then left the stage and a new masked inhabitant appeared. 738 This time Abercrombie's task was to find out, not the sex of the inhabitant, but whether 739 the inhabitant was a knight or a knave. 740 \end{exmp} 741 › 742 743 text‹ Question: are you male › 744 745 lemma Smullyan_2_2: 746 assumes "(m ⟷ k) ⟷ (m ⟷ yes)" 747 shows "yes ⟷ k" 748 using assms 749 by blast 750 751 text‹ 752 \begin{exmp} 753 (Problem 2.3.) Next, a new inhabitant appeared on the stage, and Abercrombie was to 754 determine whether or not the inhabitant was married, but he could ask only one yes/no 755 question. What question should he ask? 756 \end{exmp} 757 › 758 759 lemma Smullyan_2_3: 760 assumes "(m ⟷ k) ⟷ (((m ⟷ k) ⟷ married) ⟷ yes)" 761 shows "yes ⟷ married" 762 using assms 763 by blast 764 765 text‹ 766 \begin{exmp} 767 (Problem 2.4.) In the next test, an inhabitant wrote a sentence from which Abercrombie 768 could deduce that the inhabitant must be a female knight. What sentence could do this? 769 \end{exmp} 770 › 771 772 text‹ Question: are you a male knave › 773 lemma Smullyan_2_4: 774 assumes "(m ⟷ k) ⟷ ((m ∧ ¬k) ⟷ yes)" 775 shows "yes ⟷ ¬ m ∧ k" 776 using assms 777 by blast 778 779 text‹ 780 \begin{exmp} 781 Problem 2.5. Next, a sentence was written from which Abercrombie could deduce that the writer must 782 be a male knight. What could this sentence have been? 783 \end{exmp} 784 › 785 786 text‹ Question: are you a male or a knight› 787 lemma Smullyan_2_5: 788 assumes "(m ⟷ k) ⟷ ((m ∨ k) ⟷ yes)" 789 shows "yes ⟷ m ∧ k" 790 using assms 791 by blast 792 793 794 text‹ 795 \begin{exmp} 796 [Problem 8.1.] You meet a native and ask him whether there is gold on the island. All he 797 replies is: If I am a knight, then there is gold on the island. From this, is it possible 798 to tell whether there is gold, and whether he is a knight or a knave? 799 \end{exmp} 800 › 801 802 text‹U ovakvim zadacima, ako niste sigurni kako zapisati tvrđenje možete koristiti 803 sledgehammer. › 804 805 lemma Smullyan_8_1: 806 assumes "k ⟷ (k ⟶ g)" 807 shows "g ∧ k" 808 proof (cases k) 809 case True 810 from this assms have "k ⟶ g" by auto 811 from this `k` show "g ∧ k" by auto 812 next 813 case False 814 from this assms have "¬ (k ⟶ g)" by auto 815 from this have "¬ (¬ k ∨ g)" by auto 816 from this have "k ∧ ¬ g" by auto 817 from this `¬ k` have False by auto 818 from this show "g ∧ k" by auto 819 qed 820 821 822 text‹ 823 \begin{exmp} 824 (Problem 8.3.) Suppose that the native had instead said: "I am a knave and there is no 825 gold on the island." What can be deduced? 826 \end{exmp} 827 › 828 829 text‹U zapisu ovog tvrđenja, slično kao i ranije, možemo ili sami shvatiti šta je traženi 830 zaključak, ili nasumice ređati razne zaključke pa videti koje možemo da elimišemo. U ovom 831 slučaju, ako pokušamo da izvedemo samo @{text k} Isabelle će naći kontraprimer, što znači 832 da mora važiti @{text "¬ k"}. Slično možemo zaključiti ako pokušamo da izvedemo @{text "¬ g"}. 833 Otuda vidimo da je ispravna sledeća formulacija:› 834 835 lemma Smullyan_8_3: 836 assumes "k ⟷ (¬ k ∧ ¬ g)" 837 shows "¬ k ∧ g" 838 ―‹using assms 839 by auto - ovo bi bio automatski dokaz, a sada ga treba raspisati u Isar-u› 840 proof (cases k) 841 case True 842 from this assms have "¬ k ∧ ¬ g" by auto 843 from this have "¬ k" by auto 844 from this `k` have False by auto ―‹nakon sto izvedemo kontradikciju, možemo izvesti bilo koji zaključak› 845 from this show ?thesis by auto 846 next 847 case False 848 from this assms have "¬ (¬ k ∧ ¬ g)" by auto 849 from this have "k ∨ g" by auto 850 from this `¬ k` have "g" by auto 851 from this `¬ k` show ?thesis by auto 852 qed 853 854 subsubsection ‹Logika prvog reda› 855 856 857 text‹ 858 \begin{exmp} 859 If all say the same, then they are all of a same kind. 860 \end{exmp} 861 › 862 lemma all_say_the_same: 863 assumes "∀ x. k x ⟷ P" 864 shows "(∀ x. k x) ∨ (∀ x. ¬ k x)" 865 proof (rule ccontr) 866 assume "¬ ?thesis" 867 from this have "(∃ x. k x) ∧ (∃ x. ¬ k x)" by auto 868 from this obtain kv kn where "k kn" "¬ k kv" by auto 869 from this assms have "P" "¬ P" by auto 870 from this show False by auto 871 qed 872 873 text‹ 874 \begin{exmp} 875 [Problem 12.1.] On the first island he visited, all the inhabitants said the 876 same thing: All of us here are of the same type. What can be deduced about the 877 inhabitants of that island? 878 \end{exmp} 879 › 880 881 lemma Smullyan_12_1: 882 assumes "∀ x. (k x ⟷ (∀ x. k x) ∨ (∀ x. ¬ k x))" 883 shows "∀ x. k x" 884 ―‹sledgehammer 885 @{text "using assms by blast"}› 886 proof (rule ccontr) 887 assume "¬ ?thesis" 888 from this have "∃ x. ¬ k x" by auto 889 from this obtain kx1 where "¬ k kx1" by auto 890 from this assms have *: "¬ ((∀ x. k x) ∨ (∀ x. ¬ k x))" by blast 891 from this have "∃ x. k x" by auto 892 from this obtain kx2 where "k kx2" by auto 893 from this assms have **: "(∀ x. k x) ∨ (∀ x. ¬ k x)" by blast 894 from * ** show False by auto 895 qed 896 897 898 text‹ 899 \begin{exmp} 900 (Problem 12.2.) On the next island, all the inhabitants said: "Some of us 901 are knights and some are knaves." 902 \end{exmp} 903 › 904 905 lemma Smullyan_12_2: 906 assumes "∀ x. (k x ⟷ (∃ x. k x) ∧ (∃ x. ¬ k x))" 907 shows "∀ x. ¬ k x" 908 ―‹ 909 sledgehammer 910 using assms by blast› 911 proof (rule ccontr) 912 assume "¬ ?thesis" 913 from this have "∃ x. ¬ ¬ k x" by auto 914 from this obtain kx where "k kx" by auto 915 from this assms have *: "(∃ x. k x) ∧ (∃ x. ¬ k x)" by blast ―‹by auto ne prolazi› 916 from this have "∃ x. k x" "∃ x. ¬ k x" by auto 917 from this obtain kx1 kx2 where "k kx1" "¬ k kx2" by auto 918 from this assms have **: "¬ ((∃ x. k x) ∧ (∃ x. ¬ k x))" by blast 919 from * ** show False by auto 920 qed 921 922 text‹ 923 \begin{exmp} 924 [Problem 12.3.] On the next island, Abercrombie one day interviewed all the inhabitants 925 but one, who was asleep. They all said: All of us are knaves. The next day, Abercrombie 926 met the inhabitant who was asleep the day before, and asked him: Is it true that all 927 the inhabitants of this island are knaves? The inhabitant then answered (yes or no). 928 What answer did he give? 929 \end{exmp} 930 › 931 932 lemma Smullyan_12_3: 933 assumes "∀ x. x ≠ sleepy ⟶ (k x ⟷ (∀ x. ¬ k x))" 934 assumes "k sleepy ⟷ ((∀ x. ¬ k x) ⟷ yes)" 935 shows "¬ yes" 936 ―‹ sledgehammer 937 @{text "using assms(1) assms(2) by auto"}› 938 proof (rule ccontr) 939 assume "¬ ¬ yes" 940 from this have "yes" by auto 941 from this show False 942 proof (cases "k sleepy") 943 case True 944 from this assms(2) `yes` have "∀ x. ¬ k x" by auto 945 from this have "¬ k sleepy" by auto 946 from this True show False by auto 947 next 948 case False 949 from this assms(2) `yes` have "¬ (∀ x. ¬ k x)" by auto 950 from this have "∃ x. k x" by auto 951 from this obtain kx where "k kx" by auto 952 from this False have "kx ≠ sleepy" by auto 953 from this assms(1) `k kx` have "∀ x. ¬ k x" by auto 954 from this `k kx` show False by auto 955 qed 956 qed 957 958 end