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" (* TODO*) 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" (* TODO*) sorry 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*) 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 Peirce: "((A \ B) \ A) \ A" thm classical 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