theory week02A_demo_s 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" apply (rule impI) thm impI apply (erule conjE) thm conjI apply (rule conjI) apply assumption apply assumption done lemma "A \ B \ B \ A" apply (rule impI) apply (erule disjE) apply (rule disjI2) apply assumption apply (rule disjI1) apply assumption done lemma "\ B \ C; A \ B \ \ A \ C" apply (rule impI) apply (erule impE) apply (erule impE) apply assumption apply assumption apply assumption done thm notI notE lemma "\A \ \B \ \(A \ B)" apply (rule notI) apply (erule disjE) apply (erule conjE) apply (erule notE) apply assumption apply (erule conjE) apply (erule notE) apply assumption done text \Case distinctions\ lemma "P \ \P" apply (case_tac "P") oops thm FalseE lemma "(\P \ False) \ P" apply (rule impI) apply (case_tac P) apply assumption apply (erule impE) apply assumption apply (erule FalseE) done 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" apply (case_tac Q) apply (rule disjI2) apply assumption apply (erule impE) apply assumption apply (rule disjI1) apply assumption done 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 oops 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