theory week03A_demo_s imports Main begin -- ------------------------------------ text {* Quantifier reasoning *} text{* A successful proof: *} lemma "\a. \b. a = b" apply (rule allI) thm exI apply (rule_tac x="a" in exI) apply (rule refl) done 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" (* 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 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) thm exI apply(rule exI) apply(erule exE) apply(erule_tac x="x" in allE) oops text {* Instantiation in more detail: *} text{* Instantiating allE: *} lemma "\x. P x \ P 37" thm allE apply (erule_tac x = "37" in allE) apply assumption done text{* 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 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 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] -- --------------------------------------------- text {* 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 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