doc-src/Logics/LK.tex
 changeset 111 1b3cddf41b2d parent 104 d8205bb279a7 child 264 ca6eb7e6e94f
--- a/doc-src/Logics/LK.tex	Thu Nov 11 12:44:43 1993 +0100
+++ b/doc-src/Logics/LK.tex	Thu Nov 11 13:18:49 1993 +0100
@@ -40,7 +40,7 @@
This technique lets Isabelle formalize sequent calculus rules,
where the comma is the associative operator:
$\infer[\conj\hbox{-left}] - {\Gamma,P\conj Q,\Delta \turn \Theta} + {\Gamma,P\conj Q,\Delta \turn \Theta} {\Gamma,P,Q,\Delta \turn \Theta}$
Multiple unifiers occur whenever this is resolved against a goal containing
more than one conjunction on the left.  Explicit formalization of sequents
@@ -56,25 +56,25 @@
\begin{figure}
\begin{center}
\begin{tabular}{rrr}
-  \it name    	&\it meta-type 		& \it description	\\
-  \idx{Trueprop}& $o\To prop$		& coercion to $prop$	\\
-  \idx{Seqof}   & $[o,sobj]\To sobj$  	& singleton sequence	\\
-  \idx{Not}	& $o\To o$		& negation ($\neg$) 	\\
-  \idx{True}	& $o$			& tautology ($\top$) 	\\
-  \idx{False}	& $o$			& absurdity ($\bot$)
+  \it name      &\it meta-type          & \it description       \\
+  \idx{Trueprop}& $o\To prop$           & coercion to $prop$    \\
+  \idx{Seqof}   & $[o,sobj]\To sobj$    & singleton sequence    \\
+  \idx{Not}     & $o\To o$              & negation ($\neg$)     \\
+  \idx{True}    & $o$                   & tautology ($\top$)    \\
+  \idx{False}   & $o$                   & absurdity ($\bot$)
\end{tabular}
\end{center}
\subcaption{Constants}

\begin{center}
\begin{tabular}{llrrr}
-  \it symbol &\it name	   &\it meta-type & \it precedence & \it description \\
+  \it symbol &\it name     &\it meta-type & \it precedence & \it description \\
\idx{ALL}  & \idx{All}  & $(\alpha\To o)\To o$ & 10 &
-	universal quantifier ($\forall$) \\
+        universal quantifier ($\forall$) \\
\idx{EX}   & \idx{Ex}   & $(\alpha\To o)\To o$ & 10 &
-	existential quantifier ($\exists$) \\
+        existential quantifier ($\exists$) \\
\idx{THE} & \idx{The}  & $(\alpha\To o)\To \alpha$ & 10 &
-	definite description ($\iota$)
+        definite description ($\iota$)
\end{tabular}
\end{center}
\subcaption{Binders}
@@ -98,7 +98,7 @@

\begin{center}
\begin{tabular}{rrr}
-  \it external		& \it internal	& \it description \\
+  \it external          & \it internal  & \it description \\
\tt $\Gamma$ |- $\Delta$  &  \tt Trueprop($\Gamma$, $\Delta$) &
sequent $\Gamma\turn \Delta$
\end{tabular}
@@ -121,15 +121,15 @@
& | & formula
\$2ex] formula & = & \hbox{expression of type~o} \\ - & | & term " = " term \\ - & | & "\ttilde\ " formula \\ - & | & formula " \& " formula \\ - & | & formula " | " formula \\ - & | & formula " --> " formula \\ - & | & formula " <-> " formula \\ - & | & "ALL~" id~id^* " . " formula \\ - & | & "EX~~" id~id^* " . " formula \\ - & | & "THE~" id~ " . " formula + & | & term " = " term \\ + & | & "\ttilde\ " formula \\ + & | & formula " \& " formula \\ + & | & formula " | " formula \\ + & | & formula " --> " formula \\ + & | & formula " <-> " formula \\ + & | & "ALL~" id~id^* " . " formula \\ + & | & "EX~~" id~id^* " . " formula \\ + & | & "THE~" id~ " . " formula \end{array}$
\caption{Grammar of {\tt LK}} \label{lk-grammar}
@@ -166,8 +166,13 @@
\idx{notL}    $H,$G |- $E, P ==>$H, ~P, $G |-$E

\idx{FalseL}  $H, False,$G |- $E +\end{ttbox} \subcaption{Propositional rules} +\caption{Rules of {\tt LK}} \label{lk-rules} +\end{figure} +\begin{figure} +\begin{ttbox} \idx{allR} (!!x.$H|- $E, P(x),$F) ==> $H|-$E, ALL x.P(x), $F \idx{allL}$H, P(x), $G, ALL x.P(x) |-$E ==> $H, ALL x.P(x),$G|- $E @@ -176,10 +181,10 @@ \idx{The} [|$H |- $E, P(a),$F;  !!x.$H, P(x) |-$E, x=a, $F |] ==>$H |- $E, P(THE x.P(x)),$F
+\end{ttbox}
\subcaption{Quantifier rules}
-\end{ttbox}

-\caption{Rules of {\tt LK}}  \label{lk-rules}
+\caption{Rules of {\tt LK} (continued)}  \label{lk-rules2}
\end{figure}

@@ -223,13 +228,13 @@
as a formula.

The theory has the \ML\ identifier \ttindexbold{LK.thy}.
-Figure~\ref{lk-rules} presents the rules.  The connective $\bimp$ is
-defined using $\conj$ and $\imp$.  The axiom for basic sequents is
-expressed in a form that provides automatic thinning: redundant formulae
-are simply ignored.  The other rules are expressed in the form most
-suitable for backward proof --- they do not require exchange or contraction
-rules.  The contraction rules are actually derivable (via cut) in this
-formulation.
+Figures~\ref{lk-rules} and~\ref{lk-rules2} present the rules.  The
+connective $\bimp$ is defined using $\conj$ and $\imp$.  The axiom for
+basic sequents is expressed in a form that provides automatic thinning:
+redundant formulae are simply ignored.  The other rules are expressed in
+the form most suitable for backward proof --- they do not require exchange
+or contraction rules.  The contraction rules are actually derivable (via
+cut) in this formulation.

Figure~\ref{lk-derived} presents derived rules, including rules for
$\bimp$.  The weakened quantifier rules discard each quantification after a