doc-src/Exercises/0304/a3/generated/a3.tex
author obua
Sun, 09 May 2004 23:04:36 +0200
changeset 14722 8e739a6eaf11
parent 14500 2015348ceecb
permissions -rw-r--r--
replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14500
streckem
parents:
diff changeset
     1
%
streckem
parents:
diff changeset
     2
\begin{isabellebody}%
streckem
parents:
diff changeset
     3
\def\isabellecontext{a{\isadigit{3}}}%
streckem
parents:
diff changeset
     4
\isamarkupfalse%
streckem
parents:
diff changeset
     5
%
streckem
parents:
diff changeset
     6
\isamarkupsubsection{Natural deduction -- Propositional Logic \label{psv0304a3}%
streckem
parents:
diff changeset
     7
}
streckem
parents:
diff changeset
     8
\isamarkuptrue%
streckem
parents:
diff changeset
     9
%
streckem
parents:
diff changeset
    10
\begin{isamarkuptext}%
streckem
parents:
diff changeset
    11
In this exercise, we will prove some lemmas of propositional
streckem
parents:
diff changeset
    12
logic with the aid of a calculus of natural deduction.
streckem
parents:
diff changeset
    13
streckem
parents:
diff changeset
    14
For the proofs, you may only use
streckem
parents:
diff changeset
    15
streckem
parents:
diff changeset
    16
\begin{itemize}
streckem
parents:
diff changeset
    17
\item the following lemmas: \\
streckem
parents:
diff changeset
    18
\isa{notI{\isacharcolon}}~\isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ False{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymnot}\ A},\\
streckem
parents:
diff changeset
    19
\isa{notE{\isacharcolon}}~\isa{{\isasymlbrakk}{\isasymnot}\ A{\isacharsemicolon}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ B},\\
streckem
parents:
diff changeset
    20
\isa{conjI{\isacharcolon}}~\isa{{\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ A\ {\isasymand}\ B},\\ 
streckem
parents:
diff changeset
    21
\isa{conjE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymand}\ B{\isacharsemicolon}\ {\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C},\\
streckem
parents:
diff changeset
    22
\isa{disjI{\isadigit{1}}{\isacharcolon}}~\isa{A\ {\isasymLongrightarrow}\ A\ {\isasymor}\ B},\\
streckem
parents:
diff changeset
    23
\isa{disjI{\isadigit{2}}{\isacharcolon}}~\isa{A\ {\isasymLongrightarrow}\ B\ {\isasymor}\ A},\\
streckem
parents:
diff changeset
    24
\isa{disjE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymor}\ B{\isacharsemicolon}\ A\ {\isasymLongrightarrow}\ C{\isacharsemicolon}\ B\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C},\\
streckem
parents:
diff changeset
    25
\isa{impI{\isacharcolon}}~\isa{{\isacharparenleft}A\ {\isasymLongrightarrow}\ B{\isacharparenright}\ {\isasymLongrightarrow}\ A\ {\isasymlongrightarrow}\ B},\\
streckem
parents:
diff changeset
    26
\isa{impE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymlongrightarrow}\ B{\isacharsemicolon}\ A{\isacharsemicolon}\ B\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C},\\
streckem
parents:
diff changeset
    27
\isa{mp{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymlongrightarrow}\ B{\isacharsemicolon}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ B}\\
streckem
parents:
diff changeset
    28
\isa{iffI{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isasymLongrightarrow}\ B{\isacharsemicolon}\ B\ {\isasymLongrightarrow}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ A\ {\isacharequal}\ B}, \\
streckem
parents:
diff changeset
    29
\isa{iffE{\isacharcolon}}~\isa{{\isasymlbrakk}A\ {\isacharequal}\ B{\isacharsemicolon}\ {\isasymlbrakk}A\ {\isasymlongrightarrow}\ B{\isacharsemicolon}\ B\ {\isasymlongrightarrow}\ A{\isasymrbrakk}\ {\isasymLongrightarrow}\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ C}\\
streckem
parents:
diff changeset
    30
\isa{classical{\isacharcolon}}~\isa{{\isacharparenleft}{\isasymnot}\ A\ {\isasymLongrightarrow}\ A{\isacharparenright}\ {\isasymLongrightarrow}\ A}
streckem
parents:
diff changeset
    31
streckem
parents:
diff changeset
    32
\item the proof methods \isa{rule}, \isa{erule} and \isa{assumption}
streckem
parents:
diff changeset
    33
\end{itemize}%
streckem
parents:
diff changeset
    34
\end{isamarkuptext}%
streckem
parents:
diff changeset
    35
\isamarkuptrue%
streckem
parents:
diff changeset
    36
\isacommand{lemma}\ I{\isacharcolon}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    37
\isanewline
streckem
parents:
diff changeset
    38
\isamarkupfalse%
streckem
parents:
diff changeset
    39
\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    40
\isanewline
streckem
parents:
diff changeset
    41
\isamarkupfalse%
streckem
parents:
diff changeset
    42
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    43
\isanewline
streckem
parents:
diff changeset
    44
\isamarkupfalse%
streckem
parents:
diff changeset
    45
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}A\ {\isasymor}\ B{\isacharparenright}\ {\isasymor}\ C{\isacharparenright}\ {\isasymlongrightarrow}\ A\ {\isasymor}\ {\isacharparenleft}B\ {\isasymor}\ C{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    46
\isanewline
streckem
parents:
diff changeset
    47
\isamarkupfalse%
streckem
parents:
diff changeset
    48
\isacommand{lemma}\ K{\isacharcolon}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    49
\isanewline
streckem
parents:
diff changeset
    50
\isamarkupfalse%
streckem
parents:
diff changeset
    51
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymor}\ A{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}A\ {\isasymand}\ A{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    52
\isanewline
streckem
parents:
diff changeset
    53
\isamarkupfalse%
streckem
parents:
diff changeset
    54
\isacommand{lemma}\ S{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B\ {\isasymlongrightarrow}\ C{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ A\ {\isasymlongrightarrow}\ C{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    55
\isanewline
streckem
parents:
diff changeset
    56
\isamarkupfalse%
streckem
parents:
diff changeset
    57
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}B\ {\isasymlongrightarrow}\ C{\isacharparenright}\ {\isasymlongrightarrow}\ A\ {\isasymlongrightarrow}\ C{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    58
\isanewline
streckem
parents:
diff changeset
    59
\isamarkupfalse%
streckem
parents:
diff changeset
    60
\isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ {\isasymnot}\ A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    61
\isanewline
streckem
parents:
diff changeset
    62
\isamarkupfalse%
streckem
parents:
diff changeset
    63
\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ {\isasymnot}\ {\isasymnot}\ A{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    64
\isanewline
streckem
parents:
diff changeset
    65
\isamarkupfalse%
streckem
parents:
diff changeset
    66
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymnot}\ A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymnot}\ B\ {\isasymlongrightarrow}\ A{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    67
\isanewline
streckem
parents:
diff changeset
    68
\isamarkupfalse%
streckem
parents:
diff changeset
    69
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ A{\isacharparenright}\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    70
\isanewline
streckem
parents:
diff changeset
    71
\isamarkupfalse%
streckem
parents:
diff changeset
    72
\isacommand{lemma}\ {\isachardoublequote}A\ {\isasymor}\ {\isasymnot}\ A{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    73
\isanewline
streckem
parents:
diff changeset
    74
\isamarkupfalse%
streckem
parents:
diff changeset
    75
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isacharparenright}\ {\isacharequal} {\isacharparenleft}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
streckem
parents:
diff changeset
    76
\isamarkupfalse%
streckem
parents:
diff changeset
    77
\isanewline
streckem
parents:
diff changeset
    78
\isamarkupfalse%
streckem
parents:
diff changeset
    79
\end{isabellebody}%
streckem
parents:
diff changeset
    80
%%% Local Variables:
streckem
parents:
diff changeset
    81
%%% mode: latex
streckem
parents:
diff changeset
    82
%%% TeX-master: "root"
streckem
parents:
diff changeset
    83
%%% End: