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