1 section‹Dokazi po slučajevima› 2 3 theory Cas7_vezbe_postavke 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 proof - 256 ―‹izvešćemo nekoliko međukoraka› 257 from assms(1) have "yesA" by (auto simp add: no_one_admits_knave) 258 from this assms(2) have "¬ kB" by auto 259 from this assms(3) show "kC" by auto 260 qed 261 262 text‹ 263 \begin{exmp} 264 [Problem 1.2.] According to another version of the story, Abercrombie didn't ask A whether 265 he was a knight or a knave (because he would have known in advance what answer he would 266 get), but instead asked A how many of the three were knaves. Again A answered indistinctly, 267 so Abercrombie asked B what A had said. B then said that A had said that exactly two of 268 them were knaves. Then, as before, C claimed that B was lying. Is it now possible to 269 determine whether C is a knight or a knave? 270 \end{exmp} 271 › 272 273 text‹Pošto sada u postavci zadatka figuriše izjava oblika: Tačno dva od tri zadovoljavaju 274 neko svojstvo, potrebno je uvesti narednu definiciju (koja je tačna samo ako su tačno dve 275 od tri logičke vrednosti tačne):› 276 277 definition exactly_two where 278 "exactly_two A B C ⟷ ((A ∧ B) ∨ (A ∧ C) ∨ (B ∧ C)) ∧ ¬ (A ∧ B ∧ C)" 279 280 text‹Sada je lako formulisati traženo tvrđenje:› 281 282 lemma Smullyan_1_2: 283 assumes "kA ⟷ (exactly_two (¬ kA) (¬ kB) (¬ kC) ⟷ yesA)" 284 assumes "kB ⟷ yesA" 285 assumes "kC ⟷ ¬ kB" 286 shows "kC" 287 ―‹Isto kao i ranije, prvo testiramo sa sledgehammer i dobijamo: 288 @{text "using assms(1) assms(2) exactly_two_def by auto"}› 289 proof (rule ccontr) 290 assume "¬ kC" 291 from this assms have "kB" "yesA" by auto 292 show False 293 proof (cases "kA") 294 case True 295 from this assms(1) `yesA` have "exactly_two (¬ kA) (¬ kB) (¬ kC)" by auto 296 from this `kA` `kB` `¬ kC` show False unfolding exactly_two_def by auto 297 next 298 case False 299 from this assms(1) `yesA` have "¬ exactly_two (¬ kA) (¬ kB) (¬ kC)" by auto 300 from this `¬ kA` `kB` `¬ kC` show False unfolding exactly_two_def by auto 301 qed 302 qed 303 304 subsection‹Zadaci za vežbanje› 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 using assms(1) assms(2) exactly_two_def by auto 317 318 text‹\begin{exmp} 319 Problem 1.3. Next, Abercrombie met just two inhabitants, A and B. A made the following 320 statement: "Both of us are knaves." What is A and what is B? 321 \end{exmp}› 322 323 lemma Smullyan_1_3: 324 assumes "kA ⟷ ¬ kA ∧ ¬ kB" 325 shows "¬ kA ∧ kB" 326 using assms 327 by auto 328 329 text‹\begin{exmp} 330 Problem 1.4. According to another version of the story, A didn't say "Both of us are knaves." 331 All he said was "At least one of us is a knave." If this version is correct, what are A and B? 332 \end{exmp}› 333 334 lemma Smullyan_1_4: 335 assumes "kA ⟷ ¬ kA ∨ ¬ kB" 336 shows "kA ∧ ¬ kB" 337 using assms 338 by auto 339 340 text‹\begin{exmp} 341 Problem 1.5. According to still another version, what A actually said was 342 "We are of the same type: that is, we are either both knights or both knaves." 343 If this version is correct, then what can be deduced about A and B? 344 \end{exmp}› 345 346 lemma Smullyan_1_5: 347 assumes "kA ⟷ (kA ⟷ kB)" 348 shows "kB" ―‹u ovom primeru je zanimljivo da ništa ne mozemo da zaključimo o A. Pokušajte 349 da vidite zašto, logički, i uz pomoć Isabelle.› 350 using assms 351 by blast 352 353 text‹\begin{exmp} 354 Problem 1.6. On one occasion, Abercrombie came across two natives who were lazily lying 355 in the sun. He asked one of them whether the other one was a knight and got an answer 356 (yes or no). He then asked the other native whether the first one was a knight, and got 357 an answer (yes or no). Were the two answers necessarily the same? 358 \end{exmp}› 359 360 text‹Odgovore ćemo označiti sa yesA i yesB i provera da li su odgovori isti se svodi na 361 @{text "yesA ⟷ yesB"}.› 362 363 lemma Smullyan_1_6: 364 assumes "kA ⟷ (kB ⟷ yesA)" 365 assumes "kB ⟷ (kA ⟷ yesB)" 366 shows "yesA ⟷ yesB" 367 using assms 368 by auto 369 370 text‹\begin{exmp} 371 Problem 1.9. In the next incident, Abercrombie came across three natives, A, B, and C, 372 who made the following statements: 373 374 A: Exactly one of us is a knave. 375 376 B: Exactly two of us are knaves. 377 378 C: All of us are knaves. 379 380 What type is each? 381 \end{exmp}› 382 383 definition exactly_one where 384 "exactly_one A B C ⟷ (A ∨ B ∨ C) ∧ ¬((A ∧ B) ∨ (A ∧ C) ∨ (B ∧ C))" 385 386 lemma Smullyan_1_9: 387 assumes "kA ⟷ exactly_one (¬kA) (¬kB) (¬kC)" 388 assumes "kB ⟷ exactly_two (¬kA) (¬kB) (¬kC)" 389 assumes "kC ⟷ ¬ kA ∧ ¬ kB ∧ ¬ kC" 390 shows "¬ kC ∧ kB ∧ ¬ kA" 391 using assms unfolding exactly_one_def exactly_two_def by auto 392 393 text‹\begin{exmp} 394 Problem 1.10. Abercrombie knew that the island had a chief and was curious to find him. 395 He finally narrowed his search down to two brothers named Og and Bog, and knew that one 396 of the two was the chief, but didn't know which one until they made the following 397 statements: 398 399 Og: Bog is the chief and he is a knave! 400 401 Bog: Og is not the chief, but he is a knight. 402 403 Which one is the chief? 404 \end{exmp}› 405 406 text‹Pošto je poglavica ili Og ili Bog i ne mogu biti poglavica istovremeno, možemo izjavu 407 "Bog is the chief" zapisati kao "Og is not the chief".› 408 409 lemma Smullyan_1_10: 410 assumes "Og ⟷ ¬ chief_Og ∧ ¬ Bog" 411 assumes "Bog ⟷ ¬ chief_Og ∧ Og" 412 shows "chief_Og" "¬ Og" "¬ Bog" 413 oops 414 415 text‹Zbog bržeg zapisivanja preimenovaćemo promenljive u ovom dokazu i koristićemo naredni 416 zapis umesto originalnog:› 417 418 lemma Smullyan_1_10': 419 assumes "A ⟷ ¬ C ∧ ¬ B" 420 assumes "B ⟷ ¬ C ∧ A" 421 shows "C ∧ ¬ A ∧ ¬ B" 422 using assms(1) assms(2) by blast 423 424 text‹\begin{exmp} 425 (Problem 1.11.) Suppose that you visit the Island of Knights and Knaves because you have 426 heard a rumor that there is gold buried there. You meet a native and you wish to find out 427 from him whether there really is gold there, but you don't know whether he is a knight or 428 a knave. You are allowed to ask him only one question answerable by yes or no. 429 \end{exmp}› 430 431 text‹The question is @{text "k ⟷ g"} i.e. are you a knight iff there is gold.› 432 433 lemma NelsonGoodman: 434 shows "(k ⟷ (k ⟷ g)) ⟷ g" 435 by auto 436 437 lemma Smullyan_1_11: 438 assumes "k ⟷ ((k ⟷ g) ⟷ yes)" 439 shows "yes ⟷ g" 440 using assms 441 by auto 442 443 text‹\begin{exmp} 444 (Problem 1.12.) There is an old problem in which it is said that the knights all live in 445 one village and the knaves all live in another. You are standing at a fork in the road and 446 one road leads to the village of knights, and the other to the village of knaves. You wish 447 to go to the village of knights, but you don't know which road is the right one. A native 448 is standing at the fork and you may ask him only one yes/no question. Of course, you could 449 use the Nelson Goodman principle and ask: "Are you a knight if and only if the left road 450 leads to the village of knights?" There is a much simpler and more natural-sounding 451 question, however, that would do the job: a question using only eight words. 452 Can you find such a question? 453 \end{exmp}› 454 455 text‹Question: does the left road lead to your village. 456 457 Suppose he answers yes. If he is a knight, then the left road really does lead to his 458 village, which is the village of knights. If he is a knave, then the left road doesn’t 459 lead to his village, which is the village of knaves, hence again, it leads to the village 460 of knights. So in either case, a yes answer indicates that you should take the left road. 461 462 Suppose he answers no. If he is a knight, then the left road really doesn’t lead to his 463 village, so the right road leads to his village, which is the village of knights. If he is 464 a knave, then the left road does lead to his village (since he indicates that it doesn’t), 465 which is the village of knaves, so again it is the right road that leads to the village of 466 knights. Thus, a no answer indicates that you should take the right road. 467 › 468 469 lemma Smullyan_1_12: 470 assumes "k ⟷ (((k ∧ l) ∨ (¬ k ∧ ¬ l)) ⟷ yes)" 471 shows "yes ⟷ l" 472 using assms 473 by auto 474 475 text‹ 476 The next island visited by Abercrombie was a curious one in which women were also 477 classified as knights or knaves! And the most curious part of all is that while male 478 knights told the truth and male knaves lied, the females did the opposite: The female 479 knaves told the truth and the female knights lied! 480 › 481 482 text‹ 483 \begin{exmp} 484 [Problem 2.1.] Abercrombie was led into an auditorium, and an inhabitant of the island 485 came on the stage wearing a mask. Abercrombie was to determine whether the inhabitant 486 was male or female. He was allowed to ask only one yes/no question, and the inhabitant 487 would then write his or her answer on the blackboard (so as not to be betrayed by his 488 or her voice). 489 \end{exmp} 490 › 491 492 text‹ Odgovarajuće pitanje: Da li si ti vitez?› 493 494 text‹Svaka muška osoba bi odgovorila yes, na osnovu leme @{text no_one_admits_knave}: 495 @{text "assumes k ⟷ (k ⟷ yes) shows yes"}, koju smo već dokazali. 496 497 Svaka ženska osoba bi odgovorila no. Svaka ženska osoba može biti ili vitez ili 498 podanik. Ako je ženska osoba vitez ona će lagati i dobićemo odgovor Ne, sa druge strane 499 ako je osoba podanik, ona će govoriti istinu i daće nam odgovor Ne. 500 501 Otuda odgovor yes na ovo pitanje znači da je u 502 pitanju male (zadovoljeno m); odgovor no, znaci da je u pitanju female (nije zadovoljeno m); 503 Otuda možemo da zaključimo da važi ekvivalencija @{text "yes ⟷ m"}. 504 › 505 506 text‹ 507 Sada kada k može biti muško i žensko, dodajemo u lemu @{text no_one_admits_knave} i tu 508 pretpostavku, da je k upravo muško: 509 @{text "assumes (k ∧ m) ⟷ (k ⟷ yes) shows yes"}. 510 511 Napomena: samostalno, ovo nije valjana lema, već samo opis kako od već postojećih tvrđenja 512 možemo doći do formule koja nam treba za opis početnog problema. 513 › 514 515 text‹ 516 Svaka ženska osoba, analogno, na ovo pitanje bi odgovorila sa ne, tj. @{text "¬ yes"}. Prvo 517 možemo zameniti k sa leve strane sa @{text "¬ k"} (sa desne strane ostaje k zato što je to odgovor 518 na pitanje "da li si ti vitez"). A nakon toga možemo dodati pretpostavku da je u pitanju 519 ženska osoba (odnosno @{text "¬ m"}): 520 @{text "assumes (¬ k ∧ ¬ m) ⟷ (k ⟷ yes) shows ¬ yes"} 521 › 522 523 text‹Sada možemo spojiti ova dva tvrđenja u jedno:› 524 525 lemma Smullyan_2_1: 526 assumes "(m ∧ k) ∨ (¬ m ∧ ¬ k) ⟷ (k ⟷ yes)" (* or "(m ⟷ k) ⟷ (k ⟷ yes)" *) 527 shows "yes ⟷ m" 528 using assms by auto 529 530 text‹ 531 \begin{exmp} 532 Problem 2.2. The inhabitant then left the stage and a new masked inhabitant appeared. 533 This time Abercrombie's task was to find out, not the sex of the inhabitant, but whether 534 the inhabitant was a knight or a knave. 535 \end{exmp} 536 › 537 538 text‹ Question: are you male › 539 540 lemma Smullyan_2_2: 541 assumes "(m ⟷ k) ⟷ (m ⟷ yes)" 542 shows "yes ⟷ k" 543 using assms 544 by blast 545 546 text‹ 547 \begin{exmp} 548 (Problem 2.3.) Next, a new inhabitant appeared on the stage, and Abercrombie was to 549 determine whether or not the inhabitant was married, but he could ask only one yes/no 550 question. What question should he ask? 551 \end{exmp} 552 › 553 554 lemma Smullyan_2_3: 555 assumes "(m ⟷ k) ⟷ (((m ⟷ k) ⟷ married) ⟷ yes)" 556 shows "yes ⟷ married" 557 using assms 558 by blast 559 560 text‹ 561 \begin{exmp} 562 (Problem 2.4.) In the next test, an inhabitant wrote a sentence from which Abercrombie 563 could deduce that the inhabitant must be a female knight. What sentence could do this? 564 \end{exmp} 565 › 566 567 text‹ Question: are you a male knave › 568 lemma Smullyan_2_4: 569 assumes "(m ⟷ k) ⟷ ((m ∧ ¬k) ⟷ yes)" 570 shows "yes ⟷ ¬ m ∧ k" 571 using assms 572 by blast 573 574 text‹ 575 \begin{exmp} 576 Problem 2.5. Next, a sentence was written from which Abercrombie could deduce that the writer must 577 be a male knight. What could this sentence have been? 578 \end{exmp} 579 › 580 581 text‹ Question: are you a male or a knight› 582 lemma Smullyan_2_5: 583 assumes "(m ⟷ k) ⟷ ((m ∨ k) ⟷ yes)" 584 shows "yes ⟷ m ∧ k" 585 using assms 586 by blast 587 588 589 text‹ 590 \begin{exmp} 591 [Problem 8.1.] You meet a native and ask him whether there is gold on the island. All he 592 replies is: If I am a knight, then there is gold on the island. From this, is it possible 593 to tell whether there is gold, and whether he is a knight or a knave? 594 \end{exmp} 595 › 596 597 text‹U ovakvim zadacima, ako niste sigurni kako zapisati tvrđenje možete koristiti 598 sledgehammer. › 599 600 lemma Smullyan_8_1: 601 assumes "k ⟷ (k ⟶ g)" 602 shows "g ∧ k" 603 using assms by blast 604 605 text‹ 606 \begin{exmp} 607 (Problem 8.3.) Suppose that the native had instead said: "I am a knave and there is no 608 gold on the island." What can be deduced? 609 \end{exmp} 610 › 611 612 text‹U zapisu ovog tvrđenja, slično kao i ranije, možemo ili sami shvatiti šta je traženi 613 zaključak, ili nasumice ređati razne zaključke pa videti koje možemo da elimišemo. U ovom 614 slučaju, ako pokušamo da izvedemo samo @{text k} Isabelle će naći kontraprimer, što znači 615 da mora važiti @{text "¬ k"}. Slično možemo zaključiti ako pokušamo da izvedemo @{text "¬ g"}. 616 Otuda vidimo da je ispravna sledeća formulacija:› 617 618 lemma Smullyan_8_3: 619 assumes "k ⟷ (¬ k ∧ ¬ g)" 620 shows "¬ k ∧ g" 621 using assms by auto 622 623 subsubsection ‹Logika prvog reda› 624 625 626 text‹ 627 \begin{exmp} 628 If all say the same, then they are all of a same kind. 629 \end{exmp} 630 › 631 lemma all_say_the_same: 632 assumes "∀ x. k x ⟷ P" 633 shows "(∀ x. k x) ∨ (∀ x. ¬ k x)" 634 using assms by blast 635 636 text‹ 637 \begin{exmp} 638 [Problem 12.1.] On the first island he visited, all the inhabitants said the 639 same thing: All of us here are of the same type. What can be deduced about the 640 inhabitants of that island? 641 \end{exmp} 642 › 643 644 lemma Smullyan_12_1: 645 assumes "∀ x. (k x ⟷ (∀ x. k x) ∨ (∀ x. ¬ k x))" 646 shows "∀ x. k x" 647 using assms by blast 648 649 text‹ 650 \begin{exmp} 651 (Problem 12.2.) On the next island, all the inhabitants said: "Some of us 652 are knights and some are knaves." 653 \end{exmp} 654 › 655 656 lemma Smullyan_12_2: 657 assumes "∀ x. (k x ⟷ (∃ x. k x) ∧ (∃ x. ¬ k x))" 658 shows "∀ x. ¬ k x" 659 using assms by blast 660 661 text‹ 662 \begin{exmp} 663 [Problem 12.3.] On the next island, Abercrombie one day interviewed all the inhabitants 664 but one, who was asleep. They all said: All of us are knaves. The next day, Abercrombie 665 met the inhabitant who was asleep the day before, and asked him: Is it true that all 666 the inhabitants of this island are knaves? The inhabitant then answered (yes or no). 667 What answer did he give? 668 \end{exmp} 669 › 670 671 lemma Smullyan_12_3: 672 assumes "∀ x. x ≠ sleepy ⟶ (k x ⟷ (∀ x. ¬ k x))" 673 assumes "k sleepy ⟷ ((∀ x. ¬ k x) ⟷ yes)" 674 shows "¬ yes" 675 using assms(1) assms(2) by auto 676 677 end