theory week03A_demo imports Main begin -- ------------------------------------ text {* Quantifier reasoning *} text{* A successful proof: *} lemma "\a. \b. a = b" (*TODO*) sorry text{* An unsuccessful proof: *} lemma "\y. \x. x = y" apply(rule exI) apply(rule allI) thm refl apply(rule refl) oops text{* 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) *) sorry text {* Instantiation in more detail: *} text{* Instantiating allE: *} lemma "\x. P x \ P 37" thm allE (*TODO*) sorry text{* Instantiating exI: *} lemma "\n. P (f n) \ \m. P m" thm exI (*TODO*) sorry text{* 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 text {* Instantiation with "where" and "of" *} thm conjI thm conjI [of "A" "B"] thm conjI [where Q = "f x"] -- ---------------------------------------------- text{* 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 text {* 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 (*TODO*) sorry thm dvd_add dvd_refl thm dvd_add [OF dvd_refl] thm dvd_add [OF dvd_refl dvd_refl] -- --------------------------------------------- text {* Epsilon *} lemma "(\x. P x) = P (SOME x. P x)" (*TODO*) sorry text {* 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 -- --------------------------------------------- text {* Exercises *} -- "Quantifier scope is important:" lemma "(\x. P x \ Q) = ((\x. P x) \ Q)" oops text {* 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