theory week02A_demo imports Main begin section\Propositional logic\ subsection\Basic rules\ text\\\ thm conjI thm conjunct2 thm conjE text\\\ thm disjI1 thm disjI2 thm disjE text\\\ thm impI impE subsection\Examples\ text\a simple backward step:\ lemma "A \ B" thm conjI apply(rule conjI) oops text\a simple backward proof:\ lemma "B \ A \ A \ B" (*TODO*) sorry lemma "(A \ B) \ (B \ A)" (*TODO*) sorry lemma "\ B \ C; A \ B \ \ A \ C" sorry thm notI notE lemma "\A \ \B \ \(A \ B)" (*TODO*) sorry text \Case distinctions\ lemma "P \ \P" apply (case_tac "P") oops thm FalseE lemma "(\P \ False) \ P" oops text\Explicit backtracking:\ lemma "\ P \ Q; A \ B \ \ A" apply(erule conjE) back apply(assumption) done text \UGLY! EVIL! AVOID!\ text\Implicit backtracking: chaining with ,\ lemma "\ P \ Q; A \ B \ \ A" apply (erule conjE, assumption) done text\OR: use rule_tac or erule_tac to instantiate the schematic variables of the rule\ lemma "\ P \ Q; A \ B \ \ A" apply (erule_tac P=A and Q=B in conjE) apply assumption done text \more rules\ text\\\ thm conjunct1 conjunct2 text\\\ thm disjCI lemma our_own_disjCI: "(\Q \ P) \ P \ Q" (*TODO (with case_tac) *) sorry text\\\ thm mp text\= (iff)\ thm iffI iffE iffD1 iffD2 text\Equality\ thm refl sym trans text\\\ thm notI notE text\Contradictions\ thm FalseE ccontr classical excluded_middle \ \more rules\ text \defer and prefer\ lemma "(A \ A) = (A \ A)" apply (rule iffI) prefer 2 defer sorry text\classical propositional logic:\ lemma Pierce: "((A \ B) \ A) \ A" apply (rule impI) apply (rule classical) apply (erule impE) apply (rule impI) apply (erule notE) apply assumption apply assumption done text \Exercises\ lemma "A \ B \ A \ B" oops lemma "A \ (B \ C) \ (\ A \ \ B) \ C" oops lemma"((A \ B) \ (B \ A)) = (A = B)" oops lemma "(A \ (B \ C)) \ (A \ C)" oops end