theory Demo3 = Main: section{* Predicate logic *} subsection{* Quantifier reasoning *} text{* A successful proof: *} lemma "\x. \y. x = y" apply(rule allI) apply(rule exI) thm refl apply(rule refl) done text{* An unsuccessful proof: *} lemma "\y. \x. x = y" apply(rule exI) apply(rule allI) (* Does not work: apply(rule refl) *) oops text{* Intro and elim resoning: *} lemma "\y. \x. P x y \ \x. \y. P x y" (* the safe rules first: *) apply(rule allI) apply(erule exE) (* now the unsafe ones: *) apply(rule_tac x=y in exI) apply(erule_tac x=x in allE) apply(assumption) done text{* What happens if an unsafe rule is tried too early: *} lemma "\y. \x. P x y \ \x. \y. P x y" apply(rule allI) apply(rule exI) apply(erule exE) apply(erule allE) (* Fails now: apply(assumption) *) oops subsubsection{* Forward reasoning *} lemma "A \ B \ \ \ A" thm conjunct1 apply(drule conjunct1) apply blast done subsubsection{* Automation *} lemma "\x y. P x y \ Q x y \ R x y" apply(intro allI conjI) oops lemma "\x y. P x y \ Q x y \ R x y" apply(clarify) oops lemma "\y. \x. P x y \ \x. \y. P x y" apply blast done end