(*<*)
theory Exercise
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"
  show "A \<and> A" sorry
next
  assume "A \<and> A"
  show "A \<or> A" sorry
qed


lemma "(A \<or> B) \<or> C \<longrightarrow> A \<or> (B \<or> C)"
oops


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))"
oops

lemma "((\<exists> x. P x) \<or> (\<exists> x. Q x)) = (\<exists> x. (P x \<or> Q x))"
oops

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)"
oops

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"
oops

(*<*)
end
(*>*)