1 sectionDokazi 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 textPrvo ć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 textDokaz 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 textSada ć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 textU 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 textSada ć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 textDrugi 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 textTreć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 subsectionSmullyan - Logical Labirinths
 174 
 175 textDokazi 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 textSada ć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 textKada ž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 textKada 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 textPoš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 textSada 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 subsectionZadaci 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 textOdgovore ć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 textPoš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   textZbog 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 textThe 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 textQuestion: 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 textSvaka 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 textSada 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 textU 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 textU 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