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