# Theory Hilbert_Classical

theory Hilbert_Classical
imports Main

section

theory Hilbert_Classical
imports Main
begin

text

subsection

theorem tertium_non_datur:
proof -
let ?P =
let ?Q =

have a:
proof (rule someI)
have  ..
then show  ..
qed
have b:
proof (rule someI)
have True ..
then show  ..
qed

from a show ?thesis
proof
assume
then have A ..
then show ?thesis ..
next
assume
from b show ?thesis
proof
assume
then have A ..
then show ?thesis ..
next
assume
have neq:
proof
assume
then have  by (rule arg_cong)
also note
finally have  .
qed
have
proof
assume A
have
proof (rule ext)
show  for x
proof
assume
then show
proof
assume
with  have  ..
then show ?thesis ..
next
assume
then have x ..
then show ?thesis ..
qed
next
assume
then show
proof
assume
then have  ..
then show ?thesis ..
next
assume x
with  have  ..
then show ?thesis ..
qed
qed
qed
with neq show False by contradiction
qed
then show ?thesis ..
qed
qed
qed

subsection

theorem tertium_non_datur1:
proof -
let ?P =
let ?Q =

have a:
proof (rule someI)
show  using refl ..
qed
have b:
proof (rule someI)
show  using refl ..
qed

from a show ?thesis
proof
assume
then have A ..
then show ?thesis ..
next
assume P:
from b show ?thesis
proof
assume
then have A ..
then show ?thesis ..
next
assume Q:
have neq:
proof
assume
then have  by (rule arg_cong)
also note P
also note Q
finally show False by (rule False_neq_True)
qed
have
proof
assume A
have
proof (rule ext)
show  for x
proof
assume
then show
proof
assume
from this and  have  ..
then show ?thesis ..
next
assume
then have  ..
then show ?thesis ..
qed
next
assume
then show
proof
assume
then have  ..
then show ?thesis ..
next
assume
from this and  have  ..
then show ?thesis ..
qed
qed
qed
with neq show False by contradiction
qed
then show ?thesis ..
qed
qed
qed

subsection

theorem tertium_non_datur2:
apply (subgoal_tac
)
prefer 2
apply (rule conjI)
apply (rule someI)
apply (rule disjI1)
apply (rule refl)
apply (rule someI)
apply (rule disjI2)
apply (rule refl)
apply (erule conjE)
apply (erule disjE)
apply (erule disjE)
apply (erule conjE)
apply (erule disjI1)
prefer 2
apply (erule conjE)
apply (erule disjI1)
apply (subgoal_tac
)
prefer 2
apply (rule notI)
apply (drule_tac f =  in arg_cong)
apply (drule trans, assumption)
apply (drule sym)
apply (drule trans, assumption)
apply (erule False_neq_True)
apply (rule disjI2)
apply (rule notI)
apply (erule notE)
apply (rule ext)
apply (rule iffI)
apply (erule disjE)
apply (rule disjI1)
apply (erule conjI)
apply assumption
apply (erule conjE)
apply (erule disjI2)
apply (erule disjE)
apply (erule conjE)
apply (erule disjI1)
apply (rule disjI2)
apply (erule conjI)
apply assumption
done

subsection

prf tertium_non_datur
prf tertium_non_datur1
prf tertium_non_datur2

end