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
"\x. \ rich x \ rich (father x) \
\x. rich (father (father x)) \ rich x" oops
section {* Equational Reasoning in Isar: Left-Associativity *}
text {*
To make ordered rewriting for an associative-commutative operator
@{text "\"} 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 \ 'a \ 'a" (infixl "\" 70)
assumes assoc: "\x y z. (x \ y) \ z = x \ (y \ z)"
assumes comm: "\x y. x \ y = y \ x"
shows "x \ (y \ z) = y \ (x \ z)"
oops
end