theory SmullyanLogicalLabirinths
  imports Main                             
begin

(*
Isabelle/HOL - https://isabelle.in.tum.de/

Dokazi u čistoj logici (iskaznoj, predikatskoj)

Raymond M. Smullyan, Logical Labyrinths
http://logic-books.info/sites/default/files/logical_labirints.pdf
*)

(*
Edgar Abercrombie was an anthropologist who was particularly interested in the logic and sociology
of lying and truth-telling. One day he decided to visit a cluster of islands where a lot of lying
and truth-telling activity was going on! The first island of his visit was the Island of Knights and
Knaves in which those called knights always tell the truth and knaves always lie. Furthermore, each
inhabitant is either a knight or a knave.
*)

(* 
   Encoding:

   kA - the person A is a knight
   \<not> kA - the person A is a knave

   "Person A told the fact B"
   kA \<longleftrightarrow> B
   "Person A answered a yes or no question Q."
   kA \<longleftrightarrow> (Q \<longleftrightarrow> yes)
*)



(* 
  Every person answers YES to the question "Are you a knight?".
*)
lemma no_one_admits_knave:
  assumes "k \<longleftrightarrow> (k \<longleftrightarrow> yes)"
  shows "yes"
  using assms
proof (cases "k")
  case True
  from assms
  have "k \<longleftrightarrow> yes"
    using True
    by blast
  with `k` show "yes"
    by blast
next
  case False
  hence "\<not> (k \<longleftrightarrow> yes)"
    using assms
    by blast
  hence "\<not> k \<longrightarrow> yes"
    by blast
  thus "yes"
    using False
    by blast
qed                                

(*
Problem 1.1. On the day of his arrival, Abercrombie came across three inhabitants, whom we will call
A, B and C. He asked A: “Are you a knight or a knave?” A answered, but so indistinctly that
Abercrombie could not understand what he said. He then asked B: “What did he say?” B replied: “He
said that he is a knave.” At this point, C piped up and said: “Don’t believe that; it’s a lie!” Was
C a knight or a knave?
*)
lemma Smullyan_1_1:
  assumes "kA \<longleftrightarrow> (kA \<longleftrightarrow> yesA)"
  assumes "kB \<longleftrightarrow> \<not> yesA"
  assumes "kC \<longleftrightarrow> \<not> kB"
  shows "kC"
proof-
  have "yesA"
    using assms(1) no_one_admits_knave[of kA yesA]
    by simp
  hence "\<not> kB"        (* from this have "\<not> kB" *)
    using assms(2)
    by blast
  thus "kC"           (* from this show "\<not> kC" *)
    using assms(3)
    by simp
qed

(*
Problem 1.2. According to another version of the story, Abercrombie didn’t ask A whether he was a
knight or a knave (because he would have known in advance what answer he would get), but instead
asked A how many of the three were knaves. Again A answered indistinctly, so Abercrombie asked B
what A had said. B then said that A had said that exactly two of them were knaves. Then, as before,
C claimed that B was lying. Is it now possible to determine whether C is a knight or a knave?
*)

definition exactly_two where
  "exactly_two A B C \<longleftrightarrow> ((A \<and> B) \<or> (A \<and> C) \<or> (B \<and> C)) \<and> \<not> (A \<and> B \<and> C)"

lemma Smullyan_1_2:
  assumes "kA \<longleftrightarrow> (exactly_two (\<not> kA) (\<not> kB) (\<not> kC) \<longleftrightarrow> yesA)"
  assumes "kB \<longleftrightarrow> yesA"
  assumes "kC \<longleftrightarrow> \<not> kB"
  shows "kC"
  using assms
  by (auto simp add: exactly_two_def)

(* B said that exactly two of them were knights. Does this change the conclusion? *)
lemma Smullyan_1_2':
  assumes "kA \<longleftrightarrow> (exactly_two kA kB kC \<longleftrightarrow> yesA)"
  assumes "kB \<longleftrightarrow> yesA"
  assumes "kC \<longleftrightarrow> \<not> kB"
  shows "\<not> kC"
proof (rule ccontr)
  assume "\<not> ?thesis"
  hence "kC" "\<not> kB" "\<not> yesA"
    using assms
    by auto
  hence *: "(kA \<and> \<not> exactly_two kA kB kC) \<or> (\<not> kA \<and> exactly_two kA kB kC)"
    using assms(1)
    by auto
  show False
  proof (cases "kA")
    case True
    hence "\<not> exactly_two kA kB kC"
      using *
      by auto
    thus False
      using `kA` `kC` `\<not> kB`
      unfolding exactly_two_def
      by auto
  next
    case False
    hence "exactly_two kA kB kC"
      using *
      by simp
    thus False
      using `\<not> kA` `\<not> kB` `kC`
      unfolding exactly_two_def
      by simp
  qed
qed

(*
Problem 1.3. Next, Abercrombie met just two inhabitants, A and B. A made the following statement:
“Both of us are knaves.” What is A and what is B?
*)

lemma Smullyan_1_3:
  assumes "kA \<longleftrightarrow> \<not> kA \<and> \<not> kB"
  shows "\<not> kA" "kB"
  using assms
  by auto

(*
Problem 1.4. According to another version of the story, A didn’t say “Both of us are knaves.” All he
said was “At least one of us is a knave.” If this version is correct, what are A and B?
*)
lemma Smullyan_1_4:
  assumes "kA \<longleftrightarrow> \<not> kA \<or> \<not> kB"
  shows "kA" "\<not> kB"
  using assms
  by auto

(*
Problem 1.5. According to still another version, what A actually said was “We are of the same
type—that is, we are either both knights or both knaves.” If this version is correct, then what can
be deduced about A and B?
*)

lemma Smullyan_1_5:
  assumes "kA \<longleftrightarrow> (kA \<longleftrightarrow> kB)"
  shows "kB"
  using assms
  by blast

(*
Problem 1.6. On one occasion, Abercrombie came across two natives who were lazily lying in the sun.
He asked one of them whether the other one was a knight and got an answer (yes or no). He then asked
the other native whether the first one was a knight, and got an answer (yes or no). Were the two
answers necessarily the same?
*)

lemma Smullyan_1_6:
  assumes "kA \<longleftrightarrow> (kB \<longleftrightarrow> yesA)"
  assumes "kB \<longleftrightarrow> (kA \<longleftrightarrow> yesB)"
  shows "yesA \<longleftrightarrow> yesB"
  using assms
  by auto

(*
Problem 1.9. In the next incident, Abercrombie came across three natives, A, B, and C, who made the
following statements:
A: Exactly one of us is a knave.
B: Exactly two of us are knaves.
C: All of us are knaves.
What type is each?
*)

definition exactly_one where
  "exactly_one A B C \<longleftrightarrow> (A \<or> B \<or> C) \<and> \<not>((A \<and> B) \<or> (A \<and> C) \<or> (B \<and> C))"

lemma Smullyan_1_9:
  assumes "kA \<longleftrightarrow> exactly_one (\<not>kA) (\<not>kB) (\<not>kC)"
  assumes "kB \<longleftrightarrow> exactly_two (\<not>kA) (\<not>kB) (\<not>kC)"
  assumes "kC \<longleftrightarrow> \<not> kA \<and> \<not> kB \<and> \<not> kC"
  shows "\<not> kC" "kB" "\<not> kA"
  using assms
  unfolding exactly_one_def exactly_two_def
  by auto

(*
Problem 1.10. Abercrombie knew that the island had a chief and was curious to find him. He finally
narrowed his search down to two brothers named Og and Bog, and knew that one of the two was the
chief, but didn’t know which one until they made the following statements:
Og: Bog is the chief and he is a knave!
Bog: Og is not the chief, but he is a knight.
Which one is the chief?
*)

lemma Smullyan_1_10:
  assumes "Og \<longleftrightarrow> \<not> chief_Og \<and> \<not> Bog"
  assumes "Bog \<longleftrightarrow> \<not> chief_Og \<and> Og"
  shows "chief_Og" "\<not> Og" "\<not> Bog"
proof-
  have "Bog \<longrightarrow> \<not> Bog"
    using assms
    by blast
  thus "\<not> Bog"
    by auto
  hence "Og \<longrightarrow> chief_Og" "Og \<longleftrightarrow> \<not> chief_Og"
    using assms
    by blast+
  thus "\<not> Og"
    by simp
  thus "chief_Og"
    using `Og \<longleftrightarrow> \<not> chief_Og`
    by simp
qed

(*
Problem 1.11. Suppose that you visit the Island of Knights and Knaves because you have heard a rumor
that there is gold buried there. You meet a native and you wish to find out from him whether there
really is gold there, but you don’t know whether he is a knight or a knave. You are allowed to ask
him only one question answerable by yes or no.
*)

lemma NelsonGoodman:
  shows "(k \<longleftrightarrow> (k \<longleftrightarrow> g)) \<longleftrightarrow> g"
  by auto

(* The question is k \<longleftrightarrow> g i.e. are you a knight iff there is gold. *)

lemma Smullyan_1_11:
  assumes "k \<longleftrightarrow> ((k \<longleftrightarrow> g) \<longleftrightarrow> yes)"
  shows "yes \<longleftrightarrow> g"
  using assms
  by auto

(*
Problem 1.12. There is an old problem in which it is said that the knights all live in one village
and the knaves all live in another. You are standing at a fork in the road and one road leads to the
village of knights, and the other to the village of knaves. You wish to go to the village of
knights, but you don’t know which road is the right one. A native is standing at the fork and you
may ask him only one yes/no question. Of course, you could use the Nelson Goodman principle and ask:
“Are you a knight if and only if the left road leads to the village of knights?” There is a much
simpler and more natural-sounding question, however, that would do the job—a question using only
eight words. Can you find such a question?
*)

(* Question: does the left road lead to your village *)
lemma Smullyan_1_12:
  assumes "k \<longleftrightarrow> (((k \<and> l) \<or> (\<not> k \<and> \<not> l)) \<longleftrightarrow> yes)"
  shows "yes \<longleftrightarrow> l"
  using assms
  by auto

(*
The next island visited by Abercrombie was a curious one in which women were also classified as
knights or knaves! And the most curious part of all is that while male knights told the truth and
male knaves lied, the females did the opposite: The female knaves told the truth and the female
knights lied!
*)

(*
Problem 2.1. Abercrombie was led into an auditorium, and an inhabitant of the island came on the
stage wearing a mask. Abercrombie was to determine whether the inhabitant was male or female. He was
allowed to ask only one yes/no question, and the inhabitant would then write his or her answer on
the blackboard (so as not to be betrayed by his or her voice).
*)

(* Question: are you a knight *)
lemma Smullyan_2_1:
  assumes  "(m \<and> k) \<or> (\<not> m \<and> \<not> k) \<longleftrightarrow> (k \<longleftrightarrow> yes)" (* or "(m \<longleftrightarrow> k) \<longleftrightarrow> (k \<longleftrightarrow> yes)" *)
  shows "yes \<longleftrightarrow> m"
proof (cases "m")
  case True
  show "?thesis"
  proof (cases "k")
    case True
    have "k \<longleftrightarrow> yes"
      using `m` `k` assms
      by simp
    thus "?thesis"
      using `k` `m`
      by simp
  next
    case False
    have "\<not> k \<longleftrightarrow> yes"
      using `m` `\<not> k` assms
      by simp
    thus ?thesis
      using `m` `\<not> k` 
      by simp
  qed
next
  case False
  show "?thesis"
  proof (cases "k")
    case True
    have "\<not> k \<longleftrightarrow> yes"
      using `\<not> m` `k` assms
      by simp
    thus "?thesis"
      using `\<not> m` `k`
      by simp
  next
    case False
    have "k \<longleftrightarrow> yes"
      using `\<not> m` `\<not> k` assms
      by auto
    thus ?thesis
      using `\<not> m` `\<not> k`
      by simp
  qed
qed

(* 
Problem 2.2. The inhabitant then left the stage and a new masked inhabitant appeared. This time
Abercrombie’s task was to find out, not the sex of the inhabitant, but whether the inhabitant was a
knight or a knave.
*)

(* Question: are you male *)
lemma Smullyan_2_2:
  assumes  "(m \<longleftrightarrow> k) \<longleftrightarrow> (m \<longleftrightarrow> yes)"
  shows "yes \<longleftrightarrow> k"
  using assms
  by blast

(* 
Problem 2.3. Next, a new inhabitant appeared on the stage, and Abercrombie was to determine whether
or not the inhabitant was married, but he could ask only one yes/no question. What question should
he ask?
*)

lemma Smullyan_2_3:
  assumes  "(m \<longleftrightarrow> k) \<longleftrightarrow> (((m \<longleftrightarrow> k) \<longleftrightarrow> married) \<longleftrightarrow> yes)"
  shows "yes \<longleftrightarrow> married"
  using assms
  by blast

(* 
Problem 2.4. In the next test, an inhabitant wrote a sentence from which Abercrombie could deduce
that the inhabitant must be a female knight. What sentence could do this?
*)

(* Question: are you a male knave *)
lemma Smullyan_2_4:
  assumes "(m \<longleftrightarrow> k) \<longleftrightarrow> ((m \<and> \<not>k) \<longleftrightarrow> yes)"
  shows "yes \<longleftrightarrow> \<not> m \<and> k"
  using assms
  by blast

(*
Problem 2.5. Next, a sentence was written from which Abercrombie could deduce that the writer must
be a male knight. What could this sentence have been?
*)

(* Question: are you a male or a knight *)
lemma Smullyan_2_5:
  assumes "(m \<longleftrightarrow> k) \<longleftrightarrow> ((m \<or> k) \<longleftrightarrow> yes)"
  shows "yes \<longleftrightarrow> m \<and> k"
  using assms
  by blast

(*
Problem 8.1. You meet a native and ask him whether there is gold on the island. All he replies is:
“If I am a knight, then there is gold on the island.” From this, is it possible to tell whether
there is gold, and whether he is a knight or a knave?
*)

lemma Smullyan_8_1:
  assumes "k \<longleftrightarrow> (k \<longrightarrow> g)"
  shows "g \<and> k"                                                                             
proof (cases k)
  case False
  hence "\<not> (k \<longrightarrow> g)"
    using assms
    by simp
  hence "k \<and> \<not> g"
    by simp
  hence False
    using `\<not> k`
    by simp
  thus ?thesis
    by simp
next
  case True
  hence "k \<longrightarrow> g"
    using assms
    by simp
  thus ?thesis
    using `k`
    by simp
qed
                           
(*
Problem 8.3. Suppose that the native had instead said: “I am a knave and there is no gold on the
island.” What can be deduced?
*)

lemma Smullyan_8_3:
  assumes "k \<longleftrightarrow> (\<not> k \<and> \<not> g)"
  shows "\<not> k \<and> g"
  using assms
  by auto


(* First order logic *)

(* If all say the same, then they are all of a same kind *)
lemma all_say_the_same:
  assumes "\<forall> x. k x \<longleftrightarrow> P"                   
  shows "(\<forall> x. k x) \<or> (\<forall> x. \<not> k x)"
proof (rule ccontr)
  assume "\<not> ?thesis"
  hence "(\<exists> x. k x) \<and> (\<exists> x. \<not> k x)"
    by auto
  then obtain Kv Kn where "\<not> k Kv" "k Kn"
    by auto
  hence "P" and "\<not> P"
    using assms
    by auto
  thus False
    by auto
qed

(* 
Problem 12.1. On the first island he visited, all the inhabitants said the
same thing: “All of us here are of the same type.”
*)
lemma Smullyan_12_1:
  assumes "\<forall> x. (k x \<longleftrightarrow> (\<forall> x. k x) \<or> (\<forall> x. \<not> k x))"
  shows "\<forall> x. k x"
proof (rule ccontr)
  assume "\<not> ?thesis"
  then obtain Kv where "~ k Kv"
    by auto
  hence *: "\<not> ((\<forall> x. k x) \<or> (\<forall> x. \<not> k x))"
    using assms
    by blast
  hence "(\<exists> x. k x)"
    by auto
  then obtain Kn where "k Kn"
    by auto
  hence **:"(\<forall> x. k x) \<or> (\<forall> x. \<not> k x)"
    using assms
    by blast
  from * and ** show False
    by auto
qed

(* Problem 12.2. On the next island, all the inhabitants said: “Some of us
are knights and some are knaves.” *)
lemma Smullyan_12_2:
  assumes "\<forall> x. (k x \<longleftrightarrow> (\<exists> x. k x) \<and> (\<exists> x. \<not> k x))"
  shows "\<forall> x. \<not> k x"
  using assms
  by blast

(*
Problem 12.3. On the next island, Abercrombie one day interviewed all the inhabitants but one, who
was asleep. They all said: “All of us are knaves.” The next day, Abercrombie met the inhabitant who
was asleep the day before, and asked him: “Is it true that all the inhabitants of this island are
knaves?” The inhabitant then answered (yes or no). What answer did he give?
*)

lemma Smullyan_12_3:
  assumes "\<forall> x. x \<noteq> sleepy \<longrightarrow> (k x \<longleftrightarrow> (\<forall> x. \<not> k x))"
  assumes "k sleepy \<longleftrightarrow> ((\<forall> x. \<not> k x) \<longleftrightarrow> yes)"
  shows "\<not> yes"
proof (rule ccontr)
  assume "\<not> ?thesis"
  hence "(k sleepy \<and> (\<forall> x. \<not> k x)) \<or> (\<not> k sleepy \<and> \<not> (\<forall> x. \<not> k x))"
    using assms(2)
    by auto
  hence "\<not> k sleepy" "\<exists> x. k x"
    by auto
  then obtain Kn where "k Kn" "Kn \<noteq> sleepy"
    by auto
  hence "\<forall> x. \<not> k x"
    using assms(1)
    by auto
  thus False
    using `k Kn`
    by auto
qed

(*
Problem 12.4. On the next island, Abercrombie was particularly interested in the smoking habits of
the natives. They all said the same thing: “All knights on this island smoke.” What can be deduced
about the knight-knave distributions and the smoking habits of the natives?
*)

lemma Smullyan_12_4:
  assumes "\<forall> x. k x \<longleftrightarrow> (\<forall> x. k x \<longrightarrow> s x)"
  shows "\<forall> x. k x \<and> s x"
  using assms
  by blast

(*
Problem 12.5. On the next island, each one said: “Some knaves on this island smoke.” What can be
deduced from this?
*)

lemma Smullyan_12_5:
  assumes "\<forall> x. k x \<longleftrightarrow> (\<exists> x. \<not> k x \<and> s x)"
  shows "\<forall> x. \<not> k x \<and> \<not> s x"
proof-
  have *: "\<forall> x. \<not> k x"
  proof safe
    fix x
    assume "k x"
    then obtain Kv where "\<not> k Kv" "s Kv"
      using assms
      by blast
    show "False"
      using `k x` `\<not> k Kv` all_say_the_same[OF assms(1)]
      by auto
  qed

  have **: "\<forall> x. \<not> s x"
  proof safe
    fix x
    assume "s x"
    have "\<not> k x"
      using *
      by auto
    hence "\<exists> x. \<not> k x \<and> s x"
      using `s x`
      by auto
    hence "k x"
      using assms(1)
      by blast
    thus False
      using `\<not> k x`
      by auto
  qed

  show ?thesis
    using * **
    by auto
qed

(* 
Problem 12.6. On the next island all were of the same type, and each one said: “If I smoke, then all
the inhabitants of this island smoke.” What can be deduced?
*)

lemma Smullyan_12_6:
  assumes "(\<forall> x. k x) \<or> (\<forall> x. \<not> k x)" 
  assumes "\<forall> x. (k x \<longleftrightarrow> (s x \<longrightarrow> (\<forall> x. s x)))"
  shows "(\<forall> x. k x) \<and> ((\<forall> x. s x) \<or> (\<forall> x. \<not> s x))"
proof
  show "\<forall> x. k x"
  proof (rule ccontr)
    assume "\<not> ?thesis"
    then obtain Kv where "\<not> k Kv"
      by auto
    hence "s Kv" "\<not> (\<forall> x. s x)"
      using assms(2)
      by auto
    then obtain Ns where "\<not> s Ns"
      by auto
    have "\<not> k Ns"
      using assms(1) `\<not> k Kv`
      by auto
    hence "s Ns"
      using assms(2)
      by auto
    thus False
      using `\<not> s Ns`
      by auto
  qed
  hence *: "\<forall> x. s x \<longrightarrow> (\<forall> x. s x)"
    using assms(2)
    by auto
  show "(\<forall> x. s x) \<or> (\<forall> x. \<not> s x)"
  proof (cases "\<forall> x. s x")
    case True
    thus ?thesis
      by simp
  next
    case False
    then obtain Ns where "\<not> s Ns"
      by auto
    have "\<forall> x. \<not> s x"
    proof safe
      fix S
      assume "s S"
      hence "\<forall> x. s x"
        using *
        by auto
      thus False
        using `\<not> s Ns`
        by auto
    qed
    thus ?thesis
      by simp
  qed
qed

(*
Problem 12.7. On the next island again all were of the same type, and each one said: “If any
inhabitant of this island smokes, then I smoke.” What can be deduced?
*)
lemma Smullyan_12_7:
  assumes "(\<forall> x. k x) \<or> (\<forall> x. \<not> k x)" 
  assumes "\<forall> x. (k x \<longleftrightarrow> ((\<exists> x. s x) \<longrightarrow> s x))"
  shows "(\<forall> x. k x) \<and> ((\<forall> x. s x) \<or> (\<forall> x. \<not> s x))"
proof (cases "\<forall> x. k x")
  case True
  have "(\<forall> x. s x) ∨ (\<forall> x. \<not> s x)"
  proof (cases "\<forall> x. s x")
    case True
    thus ?thesis
      by blast
  next
    case False
    hence "\<exists> x. \<not> s x"
      by blast
    from this obtain Pera where "\<not> s Pera"
      by blast
    from assms(2) `\<forall> x. k x`
    have *: "(\<exists> x. s x) \<longrightarrow> s Pera"
      by blast
    show ?thesis
    proof (cases "\<exists> x. s x")
      case True
      hence "s Pera"
        using *
        by blast
      with `\<not> s Pera`
      have False
        by blast
      thus ?thesis
        by blast
    next                   
      case False
      hence "\<forall> x. \<not> s x"
        by blast
      thus ?thesis
        by blast
    qed
  qed
  thus ?thesis
    using `\<forall> x. k x`
    by blast
next
  case False
  hence "\<forall> x. \<not> k x"
    using assms(1)
    by blast
  hence "\<forall> y. (\<exists> x. s x) ∧ \<not> s y"
    using assms(2)                                                             
    by blast
  hence "\<exists> x. s x \<and> (\<forall> y. \<not> s y)"
    by blast
  hence False
    by blast
  thus ?thesis
    by blast
qed


(*
Problem 12.8. On the next island, too, all were of the same type, and each one said: “Some of us
smoke, but I don’t.” What follows?
*)

lemma Smullyan_12_8:
  assumes "(\<forall> x. k x) \<or> (\<forall> x. \<not> k x)" 
  assumes "\<forall> x. (k x \<longleftrightarrow> ((\<exists> x. s x) \<and> \<not> s x))"
  shows "(\<forall> x. \<not> k x) \<and> ((\<forall> x. s x) \<or> (\<forall> x. \<not> s x))"
  using assms
  by auto

(*
Problem 12.9. Suppose that on the same island, instead, each inhabitant made the following two
statements: “Some of us smoke.” “I don’t smoke.” What would you conclude?
*)

lemma Smullyan_12_9:
  assumes "\<forall> x. (k x \<longleftrightarrow> (\<exists> x. s x))"
  assumes "\<forall> x. (k x \<longleftrightarrow> \<not> s x)"
  shows "False"
proof (cases "\<forall> x. k x")
  case True
  hence "\<exists> x. s x" "\<forall> x. \<not> s x"
    using assms
    by auto
  thus False
    by auto
next
  case False
  then obtain x where "\<not> k x"
    by auto
  hence "\<forall> x. \<not> s x" "s x"
    using assms
    by auto
  thus False
    by auto
qed

(*
Problem 12.14. On the next island visited by Abercrombie, he met six natives, named Arthur, Bernard,
Charles, David, Edward, and Frank, who made the following statements:

Arthur: Everyone here smokes cigarettes.
Bernard: Everyone here smokes cigars.
Charles: Everyone here smokes either cigarettes or cigars or both.
David: Arthur and Bernard are not both knaves.
Edward: If Charles is a knight, so is David.
Frank: If David is a knight, so is Charles.

Is is possible to determine of any one of these that he is a knight, and if so, which one or ones?
*)

lemma Smullyan_12_14:
  assumes "A \<longleftrightarrow> (\<forall> x. cigarettes x)"
  assumes "B \<longleftrightarrow> (\<forall> x. cigars x)"
  assumes "C \<longleftrightarrow> (\<forall> x. cigarettes x \<or> cigars x)"
  assumes "D \<longleftrightarrow> A \<or> B"
  assumes "E \<longleftrightarrow> (C \<longrightarrow> D)"
  assumes "F \<longleftrightarrow> (D \<longrightarrow> C)"
  shows F
proof-
  have "A \<or> B \<longrightarrow> C"
    using assms(1-3)
    by auto
  thus ?thesis
    using assms(4, 6)
    by blast
qed

(*
Problem 12.19. On a certain island there is a barber named Jim who shaves all those inhabitants who
don’t shave themselves. Does Jim shave himself or doesn’t he?
*)

lemma Smullyan_12_19:
  assumes "\<forall> x. \<not> shaves x x \<longrightarrow> shaves Jim x"
  shows "shaves Jim Jim"
  using assms
  by auto

(*
Problem 12.20. On another island there is a barber named Bill who shaves only those who don’t shave
themselves. (In other words, he never shaves an inhabitant who shaves himself.) Does Bill shave
himself or doesn’t he?
*)

lemma Smullyan_12_20:
  assumes "\<forall> x. shaves Bil x \<longrightarrow> \<not> shaves x x"
  shows "\<not> shaves Bil Bil"
  using assms
  by auto

(*
What would you say about an island on which there is a barber who shaves all those and only those
inhabitants who don’t shave themselves? (In other words, if an inhabitant shaves himself, the barber
won’t shave him, but if the inhabitant doesn’t shave himself, then the barber shaves him.) Does this
barber shave himself or doesn’t he? What would you say about such a barber? What would you say about
an island on which there is a barber who shaves all those and only those inhabitants who don’t shave
themselves? (In other words, if an inhabitant shaves himself, the barber won’t shave him, but if the
inhabitant doesn’t shave himself, then the barber shaves him.) Does this barber shave himself or
doesn’t he? What would you say about such a barber?
*)
lemma Smullyan_12_21:
  assumes "\<forall> x. shaves Peter x \<longleftrightarrow> \<not> shaves x x"
  shows False
  using assms
  by auto

(* Drinking formula *)

(*
A man at a bar suddenly slammed down his fist and said: “Gimme a drink, and give everyone in the
house a drink, because when I drink, everyone drinks!” So drinks were happily passed around the
house. A few minutes later, the man said: “Gimme another drink, and give everyone else a drink,
because when I take another drink, everyone takes another drink.” So, second drinks were happily
passed around the house. Then the man slammed some money on the counter and said: “And when I pay,
everybody pays!”
*)

lemma "\<exists> x. (drinks x \<longrightarrow> (\<forall> y. drinks y))"
proof (cases "\<forall> y. drinks y")
  case True
  then have "drinks a \<longrightarrow> (\<forall> y. drinks y)" for a ..
  then show ?thesis ..
next
  case False
  then have "\<exists> x. \<not> drinks x"
    by simp
  then obtain a where "\<not> drinks a"
    ..
  have "drinks a \<longrightarrow> (\<forall> y. drinks y)"
  proof
    assume "drinks a"
    hence "False"
      using `\<not> drinks a`
      by contradiction
    thus "\<forall> y. drinks y"
      ..
  qed
  then show ?thesis ..
qed

(*
Problem 13.12 (Another Curious One). Let us define a lover as anyone who loves at least one person.
Now, suppose we are given the following two facts:
(1) Everyone loves a lover.
(2) John loves Mary.
Does it logically follow from (1) and (2) that Iago loves Othello?
*)

lemma Smullyan_13_12:
  assumes "\<forall> x. ((\<exists> y. loves x y) \<longrightarrow> (\<forall> z. loves z x))"
  assumes "loves John Marry"
  shows "loves Iago Othello"
proof-
  have "\<exists> y. loves John y"
    using assms(2)
    by blast
  hence "\<forall> z. loves z John"
    using assms(1)
    by blast
  hence "loves Othello John"
    by blast
  hence "\<exists> y. loves Othello y"
    by blast
  hence "\<forall> z. loves z Othello"
    using assms(1)
    by blast
  thus ?thesis
    by blast
qed

lemma Smullyan_13_13:
  assumes "\<forall> x. \<exists> m. mother m x"
  assumes "\<forall> x m. mother m x \<longrightarrow> parent m x"
  shows "\<forall> x. \<exists> p. parent p x"
proof
  fix x
  obtain m where "mother m x"
    using assms(1)
    by blast
  hence "parent m x"
    using assms(2)
    by blast
  thus "\<exists> p. parent p x"
    by blast
qed

(*
If R is a symmetric and transitive relation on X, and every element x of X is related
to something in X, then R is also a reflexive relation. 
*)

definition
  "reflexive R \<longleftrightarrow> (\<forall> x. R x x)"

definition
  "transitive R \<longleftrightarrow> (\<forall> x y z. R x y \<and> R y z \<longrightarrow> R x z)"

definition
  "symmetric R \<longleftrightarrow> (\<forall> x y. R x y \<longleftrightarrow> R y x)"

lemma 
  assumes "symmetric R"
  assumes "transitive R"
  assumes "\<forall> x. \<exists> y. R x y"
  shows "reflexive R"
  unfolding reflexive_def
proof
  fix x
  obtain y where "R x y" 
    using assms(3)
    by blast
  hence "R y x"
    using `symmetric R`
    unfolding symmetric_def
    by blast
  with `R x y` show "R x x"
    using `transitive R`
    unfolding transitive_def
    by blast
qed


(* Aladin u pećini pronalazi dva kovčega. On zna da se u svakom od njih nalazi
   ili blago ili smrtonosna zamka.
   Na kovčegu A piše: U bar jednom od ova dva kovčega nalazi se blago.
   Na kovčegu B piše: U kovčegu A je smrtonosna zamka.
   Aladin zna da su ili oba natpisa tačna ili su oba pogrešna.
   Koji kovčeg Aladin treba da otvori?
*)

lemma
  (* u bar jednom se nalazi blago *)
  assumes  "nA \<longleftrightarrow> bA \<or> bB"
  (* blago nije u kovcegu A *)
  assumes "nB \<longleftrightarrow> \<not> bA"
  (* ili su oba natpisa tacna ili su oba netacna *)
  assumes "(nA \<and> nB) \<or> (\<not> nA \<and> \<not> nB)"
  shows "\<not> bA \<and> bB"
proof (cases "nA")
  case True
  have "bA \<or> bB"
    using `nA` assms(1)
    by blast
  have "nB"
    using `nA` assms(3)
    by blast
  have "\<not> bA"
    using `nB` assms(2)
    by blast
  have "bB"
    using `\<not> bA` `bA \<or> bB`
    by blast
  show ?thesis
    using `\<not> bA` `bB`
    by blast
next
  case False
  hence "\<not> bA" "\<not> bB"
    using assms(1)
    by auto
  have "\<not> nB"
    using assms(3) `\<not> nA`
    by blast
  hence "bA"
    using assms(2)
    by blast
  have "False"
    using `bA` `\<not> bA`
    by blast
  thus ?thesis
    by blast 
qed


lemma 
  (* u bar jednom se nalazi blago *)
  assumes  "nA \<longleftrightarrow> bA \<or> bB"
  (* blago nije u kovcegu A *)
  assumes "nB \<longleftrightarrow> \<not> bA"
  (* ili su oba natpisa tacna ili su oba netacna *)
  assumes "(nA \<and> nB) \<or> (\<not> nA \<and> \<not> nB)"
  shows "\<not> bA \<and> bB"
proof-
  (* Alternativni dokaz - kontradikcijom *)
  have "nA"
  proof (rule ccontr)
    assume "\<not> ?thesis"
    hence "\<not> bA"
      using assms(1)
      by auto
    have "\<not> nB"
      using assms(3) `\<not> nA`
      by blast
    hence "bA"
      using assms(2)
      by blast
    show "False"
      using `bA` `\<not> bA`
      by blast
  qed
  have "bA \<or> bB"
    using `nA` assms(1)
    by blast
  have "nB"
    using `nA` assms(3)
    by blast
  have "\<not> bA"
    using `nB` assms(2)
    by blast
  have "bB"
    using `\<not> bA` `bA \<or> bB`
    by blast
  show ?thesis
    using `\<not> bA` `bB`
    by blast
qed

lemma 
  assumes  "\<exists> x. macka x \<and> \<not> rep x"
  assumes "\<forall> x. macka x \<longrightarrow> sisar x" 
  shows "\<exists> x. sisar x \<and> \<not> rep x"
proof-
  from assms(1) obtain Garfild where "macka Garfild" "\<not> rep Garfild"
    by auto
  from `macka Garfild` assms(2) have "sisar Garfild"
    by auto
  from `sisar Garfild` `\<not> rep Garfild`
  show ?thesis
    by auto
qed

end