(*<*)
theory Solution
imports Main
begin
(*>*)

section {* Isar *}

subsection {* Propositional Logic *}

text {*
  $\rhd$ Provide Isar proof texts that prove the following lemmas.  You may
  only use the methods @{text rule} and @{text -}.
  \medskip
*}

lemma "(A \<or> A) = (A \<and> A)"
proof
  assume "A \<or> A"
  then have a: "A" by rule
  from a a show "A \<and> A" by rule
next
  assume "A \<and> A"
  then have "A" by rule
  then show "A \<or> A" by rule
qed


text {* Variation, using backticks. *}

lemma "(A \<or> A) = (A \<and> A)"
proof
  assume "A \<or> A"
  then have "A" by rule
  from `A` `A` show "A \<and> A" by rule
next
  assume "A \<and> A"
  then have "A" by rule
  then show "A \<or> A" by rule
qed

lemma "(A \<or> B) \<or> C \<longrightarrow> A \<or> (B \<or> C)"
proof
  assume "(A \<or> B) \<or> C"
  then show "A \<or> (B \<or> C)"
  proof
    assume "A \<or> B"
    then show ?thesis
    proof
      assume "A"
      then show ?thesis by rule
    next
      assume "B"
      then have "B \<or> C" by rule
      then show ?thesis by rule
    qed
  next
    assume "C"
    then have "B \<or> C" by rule
    then show ?thesis by rule
  qed
qed


subsection {* Predicate Logic *}

text {*
  $\rhd$ Provide Isar proof texts that prove the following lemmas.
  Again, you may not use automation.
  \medskip
*}

lemma "((\<forall> x. P x) \<and> (\<forall> x. Q x)) = (\<forall> x. (P x \<and> Q x))"
proof
  assume pq: "(\<forall>x. P x) \<and> (\<forall>x. Q x)"
  from pq have p: "\<forall>x. P x" ..
  from pq have q: "\<forall>x. Q x" ..
  show "\<forall>x. P x \<and> Q x"
  proof
    fix x
    from p have p': "P x" ..
    from q have q': "Q x" ..
    from p' q' show "P x \<and> Q x" ..
  qed
next
  assume pq: "\<forall>x. P x \<and> Q x"
  show "(\<forall>x. P x) \<and> (\<forall>x. Q x)"
  proof
    show "\<forall>x. P x"
    proof
      fix x
      from pq have "P x \<and> Q x" ..
      then show "P x" ..
    qed
  next
    show "\<forall>x. Q x"
    proof
      fix x
      from pq have "P x \<and> Q x" ..
      then show "Q x" ..
    qed
  qed
qed

lemma "((\<exists> x. P x) \<or> (\<exists> x. Q x)) = (\<exists> x. (P x \<or> Q x))"
proof
  assume "(\<exists>x. P x) \<or> (\<exists>x. Q x)"
  then show "\<exists>x. P x \<or> Q x"
  proof
    assume "\<exists>x. P x"
    then obtain y where "P y" ..
    then have "P y \<or> Q y" ..
    then show ?thesis ..
  next
    assume "\<exists>x. Q x"
    then obtain y where "Q y" ..
    then have "P y \<or> Q y" ..
    then show ?thesis ..
  qed
next
  assume "\<exists>x. P x \<or> Q x"
  then obtain y where "P y \<or> Q y" ..
  then show "(\<exists> x. P x) \<or> (\<exists> x. Q x)"
  proof
    assume "P y"
    then have "\<exists>x. P x" ..
    then show ?thesis ..
  next
    assume "Q y"
    then have "\<exists>x. Q x" ..
    then show ?thesis ..
  qed
qed


text {*
  The following lemma also requires @{text "classical:"}~@{thm
  classical[no_vars]} (or an equivalent theorem) in order to be
  proved.  You need to invoke this explicitly with \textbf{proof}
  @{text "rule classical"} or similar.
*}


lemma "(\<not> (\<forall> x. P x)) = (\<exists> x. \<not> P x)"
proof
  assume "\<not> (\<forall>x. P x)"
  show "\<exists>x. \<not> P x"
  proof (rule classical)
    assume "\<not> (\<exists>x. \<not> P x)"
    have "\<forall>x. P x" proof
      fix x
      show "P x"
      proof (rule classical)
	assume "\<not> P x"
	then have "\<exists>x. \<not> P x" ..
	with `\<not> (\<exists>x. \<not> P x)` show ?thesis ..
      qed
    qed
    with `\<not> (\<forall>x. P x)` show ?thesis ..
  qed
next
  assume "\<exists>x. \<not> P x"
  then obtain x where "\<not> P x" by rule
  show "\<not> (\<forall>x. P x)" proof
    assume "\<forall>x. P x"
    then have "P x" by rule
    from `\<not> P x` `P x` show "False" by rule
  qed
qed

text {*
  \textit{Hint:} it may be useful to study the natural deduction
  proofs of these lemmas before attempting to provide Isar proofs.
*}

(*<*)
section {* Rich Grandfather *}

text {*
  Recall the ``Rich Grandfather'' riddle (Exercises~2).

  {\it  If every poor man has a rich father,\\
   then there is a rich man who has a rich grandfather.}

  $\rhd$ Give an Isar proof of the theorem.  You may use automated tactics, but
  the general proof structure should resemble your informal pen-and-paper proof
  of the theorem.
*}

theorem
  "\<forall>x. \<not> rich x \<longrightarrow> rich (father x) \<Longrightarrow>
  \<exists>x. rich (father (father x)) \<and> rich x"
proof -
  assume a: "\<forall>x. \<not> rich x \<longrightarrow> rich (father x)"
  txt {* (1) *} 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
  txt {* (2) *} 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
(*>*)