(*
    $Id: sol.thy,v 1.2 2004/11/23 15:14:35 webertj Exp $
    Original Author: Tjark Weber
    Updated to Isabelle 2016 and additions by Jacques Fleuriot
    Updated to Isabelle 2020 ({**} to \<open>\<close>) by Jake Palmer
*)

section \<open>A Riddle: Rich Grandfather\<close>

theory riddle_solution imports Main begin

text \<open>
  First prove the following formula, which is valid in classical predicate
  logic, informally with pen and paper.  Use case distinctions and/or proof by
  contradiction.

  "If every poor man has a rich father,
   then there is a rich man who has a rich grandfather"
\<close>


text \<open>
Proof
(1) We first show: "\<exists>x. rich x".
Proof by contradiction.
    Assume "\<not> (\<exists>x. rich x)"
      Then "\<forall>x. \<not> rich x"
      We consider an arbitrary "y" with "\<not> rich y"
      Then "rich (father y)"

(2) Now we show the theorem.
Proof by cases.
    Case 1:  "rich (father (father x))"
             We are done.
    Case 2: "\<not> rich (father (father x))"
            Then "rich (father (father (father x)))
            Also "rich (father x)"
            because otherwise "rich (father (father x))"
qed
\<close>

text \<open>
  Now prove the formula in Isabelle using a sequence of rule applications
  (i.e. only using the methods rule, erule and assumption).
\<close>

theorem
  "\<forall>x. \<not> rich x \<longrightarrow> rich (father x) \<Longrightarrow>
  \<exists>x. rich (father (father x)) \<and> rich x"
apply (rule classical)
apply (rule exI)
apply (rule conjI)
  
  apply (rule classical)
  apply (rule allE) apply assumption
  apply (erule impE) apply assumption
  apply (erule notE) 
  apply (rule exI)
  apply (rule conjI) apply assumption
  apply (rule classical)
  apply (erule allE)
  apply (erule notE)
  apply (erule impE) apply assumption
  apply assumption

apply (rule classical)
apply (rule allE) apply assumption
apply (erule impE) apply assumption
apply (erule notE)
apply (rule exI)
apply (rule conjI) apply assumption
apply (rule classical)
apply (erule allE)
apply (erule notE)
apply (erule impE) apply assumption
apply assumption
done


text \<open>An alternative proof of the above that does not rely on meta variables and uses additional
      tactics/methods such as drule and cut_tac. Note the use of rule exCI too.

      Note also that the order in which the subgoals are tackled are dictated by Isabelle but
      there are ways of doing the proof in a way closer to the informal one e.g. using "prefer"
      to change the order of the goals (although this makes the proof potentially more "brittle"
      to changes in future versions of Isabelle\<close>

theorem
  "\<forall>x. \<not> rich x \<longrightarrow> rich (father x) \<Longrightarrow>
  \<exists>x. rich (father (father x)) \<and> rich x"
apply (subgoal_tac "\<exists>x. rich x")
apply (erule exE)
(* Tackling (2) first *)
apply (cut_tac P="rich (father (father x))" in excluded_middle)
apply (erule disjE)
(* Case 2 *)
apply (subgoal_tac "rich (father x)")
apply (drule_tac x="father (father x)" in spec)
apply (drule mp, assumption)
apply (rule_tac x="father x" in exI)
apply (rule conjI)
apply assumption
apply assumption
apply (rule ccontr)
apply (drule_tac x="father x" in spec)
apply (drule mp, assumption)
apply (erule notE, assumption)
(* Case 1*)
apply (rule_tac x=x in exI)
apply (rule conjI)
apply assumption
apply assumption
(* Tackling (1) now *)
apply (rule_tac a="father x" in exCI)
apply (drule_tac x=x in spec)
apply (drule_tac x=x in spec)
apply (drule mp, assumption)
apply assumption
done


text \<open>
  Here is a proof in Isar that resembles the informal reasoning above:
\<close>

theorem rich_grandfather: "\<forall>x. \<not> rich x \<longrightarrow> rich (father x) \<Longrightarrow> 
  \<exists>x. rich x \<and> rich (father (father x))"
proof -
  assume a: "\<forall>x. \<not> rich x \<longrightarrow> rich (father x)"
  have "\<exists>x. rich x"
  proof (rule classical)
    fix y 
    assume "\<not> (\<exists>x. rich x)"
    then have "\<forall>x. \<not> rich x" by simp 
    then have "\<not> rich y" by simp
    with a have "rich (father y)" by simp
    then show ?thesis by rule 
  qed
  then obtain x where x: "rich x" by auto
  show ?thesis
  proof cases
    assume "rich (father (father x))"
    with x show ?thesis by auto
  next
    assume b: "\<not> rich (father (father x))"
    with a have "rich (father (father (father x)))" by simp
    moreover have "rich (father x)" 
    proof (rule classical)
      assume "\<not> rich (father x)" 
      with a have "rich (father (father x))" by simp
      with b show ?thesis by contradiction 
    qed
    ultimately show ?thesis by auto
  qed
qed

text \<open>
  An slightly modified proof of the above, with a named assumption right from the beginning:
\<close>


theorem rich_grandfather2: 
  assumes a: "\<forall>x. \<not> rich x \<longrightarrow> rich (father x)" 
  shows "\<exists>x. rich x \<and> rich (father (father x))"
proof -
  have "\<exists>x. rich x"
  proof (rule classical)
    fix y 
    assume "\<not> (\<exists>x. rich x)"
    then have "\<forall>x. \<not> rich x" by simp 
    then have "\<not> rich y" by simp
    with a have "rich (father y)" by simp
    then show ?thesis by rule 
  qed
  then obtain x where x: "rich x" by auto
  show ?thesis
  proof cases
    assume "rich (father (father x))"
    with x show ?thesis by auto
  next
    assume b: "\<not> rich (father (father x))"
    with a have "rich (father (father (father x)))" by simp
    moreover have "rich (father x)" 
    proof (rule classical)
      assume "\<not> rich (father x)" 
      with a have "rich (father (father x))" by simp
      with b show ?thesis by contradiction 
    qed
    ultimately show ?thesis by auto
  qed
qed


 end