theory Propositional imports Pure begin typedecl bool judgment Trueprop :: "bool \ prop" ("_" 5) axiomatization False :: bool ("\") where FalseE: "\ \ A" axiomatization implication :: "bool \ bool \ bool" (infixr "\" 25) where impI: "(A \ B) \ A \ B" and mp: "A \ B \ A \ B" axiomatization where TND: "(A \ B) \ ((A \ \) \ B) \ B" lemma impE: assumes "A \ B" and "A" obtains "B" proof from \A \ B\ and \A\ show "B" by (rule mp) qed definition True :: "bool" ("\") where "\ \ \ \ \" lemma TrueI: "\" unfolding True_def by (rule impI) definition negation :: "bool \ bool" ("\ _" [40] 40) where "\ A \ A \ \" lemma notI: "(A \ \) \ \ A" unfolding negation_def by (rule impI) lemma notE: assumes "\ A" and "A" obtains "B" proof from \\ A\ have "A \ \" unfolding negation_def . from this \A\ have "\" by (rule mp) then show "B" by (rule FalseE) qed definition disjunction :: "bool \ bool \ bool" (infixl "\" 30) where "A \ B \ \ A \ B" lemma "A \ \ A" unfolding disjunction_def by (rule impI) lemma disjI1: assumes "A" shows "A \ B" unfolding disjunction_def proof (rule impI) assume "\ A" from this \A\ have "\" by (rule notE) then show "B" by (rule FalseE) qed lemma disjI2: assumes "B" shows "A \ B" unfolding disjunction_def proof (rule impI) from \B\ show "B" . qed lemma disjE: assumes "A \ B" obtains "A" | "B" proof (rule TND [where A=A]) assume "A" then show ?thesis by (rule that) next assume "A \ \" then have "\ A" by (rule notI) with \A \ B\ have "B" unfolding disjunction_def by (rule mp) then show ?thesis by (rule that) qed definition conjunction :: "bool \ bool \ bool" (infixl "\" 35) where "A \ B \ \ (\ A \ \ B)" lemma conjI: assumes "A" and "B" shows "A \ B" unfolding conjunction_def proof (rule notI) assume "\ A \ \ B" then show "\" proof (rule disjE) assume "\ A" from this \A\ show "\" by (rule notE) next assume "\ B" from this \B\ show "\" by (rule notE) qed qed lemma conjD1: assumes "A \ B" shows "A" proof (rule TND [where A=A]) assume "A" then show "A" . next from \A \ B\ have "\ (\ A \ \ B)" unfolding conjunction_def . moreover assume "A \ \" then have "\ A" by (rule notI) then have "\ A \ \ B" by (rule disjI1) ultimately show "A" by (rule notE) qed lemma conjD2: assumes "A \ B" shows "B" proof (rule TND [where A=B]) assume "B" then show "B" . next from \A \ B\ have "\ (\ A \ \ B)" unfolding conjunction_def . moreover assume "B \ \" then have "\ B" by (rule notI) then have "\ A \ \ B" by (rule disjI2) ultimately show "B" by (rule notE) qed end