theory week02B_demo imports Main begin \ \ ------------------------------------ \ \ \ {* Quantifier reasoning *} \ \ \ {* A successful proof: *} \ lemma "\a. \b. a = b" (* TODO *) oops \ \An unsuccessful proof:\ \ \ {* 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" (* TODO *) (* the safe rules first! *) (* (check what happens if you use unsafe rule too early) *) oops \ \ {* Instantiation in more detail: *} \ \ \ {* Instantiating allE: *} \ lemma "\x. P x \ P 37" thm allE (*TODO*) oops \ \ {* Instantiating exI: *} \ lemma "\n. P (f n) \ \m. P m" thm exI (*TODO*) oops \ \ {* 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) thm notI apply (rule notI) thm notE apply (erule notE) apply assumption done lemma "\x. P x \ P t \ P t'" thm spec (*TODO*) oops 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)" (*TODO*) sorry apply (rule iffI) apply (erule exE) 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