theory week02B_demo_s imports Main begin \ \ ------------------------------------\ \ \ {* Quantifier reasoning *} \ \ \ {* A successful proof: *} \ lemma "\a. \b. a = b" apply (rule allI) thm exI apply (rule_tac x="a" in exI) apply (rule refl) done \ \ {* An unsuccessful proof: *} \ lemma "\y. \x. x = y" apply(rule exI) apply(rule allI) thm refl apply(rule refl) oops \ \ {* Intro and elim reasoning: *} \ lemma "\b. \a. P a b \ \a. \b. P a b" (* the safe rules first: *) apply (rule allI) apply (erule exE) thm exI (* now the unsafe ones: *) apply (erule_tac x="a" in allE) apply (rule_tac x="b" in exI) apply assumption done \ \ {* What happens if an unsafe rule is tried too early: *} \ lemma "\y. \x. P x y \ \x. \y. P x y" apply(rule allI) thm exI apply(rule exI) apply(erule exE) apply(erule_tac x="x" in allE) oops \ \ {* Instantiation in more detail: *} \ \ \ {* Instantiating allE: *} \ lemma "\x. P x \ P 37" thm allE apply (erule_tac x = "37" in allE) apply assumption done \ \ {* Instantiating exI: *} \ lemma "\n. P (f n) \ \m. P m" apply(erule exE) thm exI apply(rule_tac x = "f n" in exI) apply assumption done \ \ {* Instantiation removes ambiguity: *} \ lemma "\ A \ B; C \ D \ \ D" apply(erule_tac P = "C" and Q="D" in conjE) (* without instantiation, the wrong one is chosen (first) *) apply assumption done \ \ {* Instantiation with "where" and "of" *} \ thm conjI thm conjI [of "A" "B"] thm conjI [where Q = "f x"] \ \ ---------------------------------------------- \ \ \ {* Renaming parameters: *} \ lemma "\x y z. P x y z" apply(rename_tac a b) oops lemma "\x. P x \ \x. \x. P x" apply(rule allI) apply(rule allI) apply(rename_tac y) apply(erule_tac x=y in allE) apply assumption done \ \ {* Forward reasoning: drule/frule/OF/THEN*} \ lemma "A \ B \ \ \ A" thm conjunct1 apply (drule conjunct1) apply (rule notI) apply (erule notE) apply assumption done lemma "\x. P x \ P t \ P t'" thm spec apply (frule_tac x="t" in spec) apply (drule_tac x="t'" in spec) apply (rule conjI) apply assumption apply assumption done thm dvd_add dvd_refl thm dvd_add [OF dvd_refl] thm dvd_add [OF dvd_refl dvd_refl] \ \ --------------------------------------------- \ \ \ {* Epsilon *} \ lemma "(\x. P x) = P (SOME x. P x)" apply (rule iffI) apply (erule exE)thm someI apply (rule_tac x=x in someI) apply assumption apply (rule_tac x="SOME x. P x" in exI) apply assumption done \ \ {* 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 "\x y. P x y \ Q x y \ R x y" apply safe oops lemma "\y. \x. P x y \ \x. \y. P x y" apply blast done lemma "\y. \x. P x y \ \x. \y. P x y" apply fast done \ \ --------------------------------------------- \ \ \ {* Exercises *} \ \ \ "Quantifier scope is important:" \ lemma "(\x. P x \ Q) = ((\x. P x) \ Q)" oops \ \ {* Derive the axiom of choice from the SOME operator (using the rule someI), i.e. using only the rules: allI, allE, exI, exE and someI; with only the proof methods: rule, erule, rule_tac, erule_tac and assumption, prove: *} \ lemma choice: "\x. \y. R x y \ \f. \x. R x (f x)" oops end