theory Exercise05
imports Main
begin

section {* A Riddle: Rich Grandfather *}

text {*
  Recall the ``Rich Grandfather'' riddle (Exercise~3).

  {\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


section {* Equational Reasoning in Isar: Left-Associativity *}

text {*
  To make ordered rewriting for an associative-commutative operator
  @{text "\<cdot>"} confluent, it is necessary to add a derived
  property, \emph{left-associativity}, to the set of rewrite rules:
  $$x \cdot (y \cdot z) = y \cdot (x \cdot z)$$
  (cf.\ Section~9.1.1 of the Isabelle/HOL tutorial).

  $\rhd$ Give an Isar proof of the following theorem, which states that
  left-associativity follows from associativity and commutativity.  Only use
  @{text "by (simp only: assoc)"}, @{text "by (simp only: comm)"}, and
  @{text "."} as terminal proof methods.
*}

lemma left_assoc:
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)

  assumes assoc: "\<And>x y z. (x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
  assumes comm: "\<And>x y. x \<cdot> y = y \<cdot> x"

  shows "x \<cdot> (y \<cdot> z) = y \<cdot> (x \<cdot> z)"

  oops


end