--- a/src/Doc/IsarImplementation/Eq.thy Mon Nov 12 21:17:58 2012 +0100
+++ b/src/Doc/IsarImplementation/Eq.thy Mon Nov 12 22:09:52 2012 +0100
@@ -31,7 +31,43 @@
section {* Basic equality rules \label{sec:eq-rules} *}
-text {* FIXME *}
+text {* Isabelle/Pure uses @{text "\<equiv>"} for equality of arbitrary
+ terms, which includes equivalence of propositions of the logical
+ framework. The conceptual axiomatization of the constant @{text "\<equiv>
+ :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} is given in \figref{fig:pure-equality}. The
+ inference kernel presents slightly different equality rules, which
+ may be understood as derived rules from this minimal axiomatization.
+ The Pure theory also provides some theorems that express the same
+ reasoning schemes as theorems that can be composed like object-level
+ rules as explained in \secref{sec:obj-rules}.
+
+ For example, @{ML Thm.symmetric} as Pure inference is an ML function
+ that maps a theorem @{text "th"} stating @{text "t \<equiv> u"} to one
+ stating @{text "u \<equiv> t"}. In contrast, @{thm [source]
+ Pure.symmetric} as Pure theorem expresses the same reasoning in
+ declarative form. If used like @{text "th [THEN Pure.symmetric]"}
+ in Isar source notation, it achieves a similar effect as the ML
+ inference function, although the rule attribute @{attribute THEN} or
+ ML operator @{ML "op RS"} involve the full machinery of higher-order
+ unification (modulo @{text "\<beta>\<eta>"}-conversion) and lifting of @{text
+ "\<And>/\<Longrightarrow>"} contexts. *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML Thm.reflexive: "cterm -> thm"} \\
+ @{index_ML Thm.symmetric: "thm -> thm"} \\
+ @{index_ML Thm.transitive: "thm -> thm -> thm"} \\
+ @{index_ML Thm.abstract_rule: "string -> cterm -> thm -> thm"} \\
+ @{index_ML Thm.combination: "thm -> thm -> thm"} \\[0.5ex]
+ @{index_ML Thm.equal_intr: "thm -> thm -> thm"} \\
+ @{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
+ \end{mldecls}
+
+ See also @{"file" "~~/src/Pure/thm.ML" } for further description of
+ these inference rules, and a few more for primitive @{text "\<beta>"} and
+ @{text "\<eta>"} conversions. Note that @{text "\<alpha>"} conversion is
+ implicit due to the representation of terms with de-Bruijn indices
+ (\secref{sec:terms}). *}
section {* Conversions \label{sec:conv} *}
--- a/src/Doc/Ref/document/thm.tex Mon Nov 12 21:17:58 2012 +0100
+++ b/src/Doc/Ref/document/thm.tex Mon Nov 12 22:09:52 2012 +0100
@@ -1,7 +1,7 @@
\chapter{Theorems and Forward Proof}
-\subsection{*Sort hypotheses} \label{sec:sort-hyps}
+\section{*Sort hypotheses} \label{sec:sort-hyps}
\begin{ttbox}
strip_shyps : thm -> thm
@@ -46,80 +46,6 @@
\end{ttdescription}
-\section{*Primitive meta-level inference rules}
-
-\subsection{Logical equivalence rules}
-
-\begin{ttbox}
-equal_intr : thm -> thm -> thm
-equal_elim : thm -> thm -> thm
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{equal_intr} $thm@1$ $thm@2$]
-applies $({\equiv}I)$ to $thm@1$ and~$thm@2$. It maps the premises~$\psi$
-and~$\phi$ to the conclusion~$\phi\equiv\psi$; the assumptions are those of
-the first premise with~$\phi$ removed, plus those of
-the second premise with~$\psi$ removed.
-
-\item[\ttindexbold{equal_elim} $thm@1$ $thm@2$]
-applies $({\equiv}E)$ to $thm@1$ and~$thm@2$. It maps the premises
-$\phi\equiv\psi$ and $\phi$ to the conclusion~$\psi$.
-\end{ttdescription}
-
-
-\subsection{Equality rules}
-
-\begin{ttbox}
-reflexive : cterm -> thm
-symmetric : thm -> thm
-transitive : thm -> thm -> thm
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{reflexive} $ct$]
-makes the theorem \(ct\equiv ct\).
-
-\item[\ttindexbold{symmetric} $thm$]
-maps the premise $a\equiv b$ to the conclusion $b\equiv a$.
-
-\item[\ttindexbold{transitive} $thm@1$ $thm@2$]
-maps the premises $a\equiv b$ and $b\equiv c$ to the conclusion~${a\equiv c}$.
-\end{ttdescription}
-
-
-\subsection{The $\lambda$-conversion rules}
-
-\begin{ttbox}
-beta_conversion : cterm -> thm
-extensional : thm -> thm
-abstract_rule : string -> cterm -> thm -> thm
-combination : thm -> thm -> thm
-\end{ttbox}
-There is no rule for $\alpha$-conversion because Isabelle regards
-$\alpha$-convertible theorems as equal.
-\begin{ttdescription}
-\item[\ttindexbold{beta_conversion} $ct$]
-makes the theorem $((\lambda x.a)(b)) \equiv a[b/x]$, where $ct$ is the
-term $(\lambda x.a)(b)$.
-
-\item[\ttindexbold{extensional} $thm$]
-maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$.
-Parameter~$x$ is taken from the premise. It may be an unknown or a free
-variable (provided it does not occur in the assumptions); it must not occur
-in $f$ or~$g$.
-
-\item[\ttindexbold{abstract_rule} $v$ $x$ $thm$]
-maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv
-(\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$.
-Parameter~$x$ is supplied as a cterm. It may be an unknown or a free
-variable (provided it does not occur in the assumptions). In the
-conclusion, the bound variable is named~$v$.
-
-\item[\ttindexbold{combination} $thm@1$ $thm@2$]
-maps the premises $f\equiv g$ and $a\equiv b$ to the conclusion~$f(a)\equiv
-g(b)$.
-\end{ttdescription}
-
-
\section{Proof terms}\label{sec:proofObjects}
\index{proof terms|(} Isabelle can record the full meta-level proof of each
theorem. The proof term contains all logical inferences in detail.