1 sectionDokazi 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 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 
 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 textPoš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 textSada 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 textOdgovore ć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 textPoš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   textZbog 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 textThe 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 textQuestion: 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 textSvaka 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 textSada 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 textU 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 textU 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