1.1 --- a/src/Doc/IsarImplementation/Eq.thy Mon Nov 12 21:17:58 2012 +0100
1.2 +++ b/src/Doc/IsarImplementation/Eq.thy Mon Nov 12 22:09:52 2012 +0100
1.3 @@ -31,7 +31,43 @@
1.4
1.5 section {* Basic equality rules \label{sec:eq-rules} *}
1.6
1.7 -text {* FIXME *}
1.8 +text {* Isabelle/Pure uses @{text "\<equiv>"} for equality of arbitrary
1.9 + terms, which includes equivalence of propositions of the logical
1.10 + framework. The conceptual axiomatization of the constant @{text "\<equiv>
1.11 + :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> prop"} is given in \figref{fig:pure-equality}. The
1.12 + inference kernel presents slightly different equality rules, which
1.13 + may be understood as derived rules from this minimal axiomatization.
1.14 + The Pure theory also provides some theorems that express the same
1.15 + reasoning schemes as theorems that can be composed like object-level
1.16 + rules as explained in \secref{sec:obj-rules}.
1.17 +
1.18 + For example, @{ML Thm.symmetric} as Pure inference is an ML function
1.19 + that maps a theorem @{text "th"} stating @{text "t \<equiv> u"} to one
1.20 + stating @{text "u \<equiv> t"}. In contrast, @{thm [source]
1.21 + Pure.symmetric} as Pure theorem expresses the same reasoning in
1.22 + declarative form. If used like @{text "th [THEN Pure.symmetric]"}
1.23 + in Isar source notation, it achieves a similar effect as the ML
1.24 + inference function, although the rule attribute @{attribute THEN} or
1.25 + ML operator @{ML "op RS"} involve the full machinery of higher-order
1.26 + unification (modulo @{text "\<beta>\<eta>"}-conversion) and lifting of @{text
1.27 + "\<And>/\<Longrightarrow>"} contexts. *}
1.28 +
1.29 +text %mlref {*
1.30 + \begin{mldecls}
1.31 + @{index_ML Thm.reflexive: "cterm -> thm"} \\
1.32 + @{index_ML Thm.symmetric: "thm -> thm"} \\
1.33 + @{index_ML Thm.transitive: "thm -> thm -> thm"} \\
1.34 + @{index_ML Thm.abstract_rule: "string -> cterm -> thm -> thm"} \\
1.35 + @{index_ML Thm.combination: "thm -> thm -> thm"} \\[0.5ex]
1.36 + @{index_ML Thm.equal_intr: "thm -> thm -> thm"} \\
1.37 + @{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
1.38 + \end{mldecls}
1.39 +
1.40 + See also @{"file" "~~/src/Pure/thm.ML" } for further description of
1.41 + these inference rules, and a few more for primitive @{text "\<beta>"} and
1.42 + @{text "\<eta>"} conversions. Note that @{text "\<alpha>"} conversion is
1.43 + implicit due to the representation of terms with de-Bruijn indices
1.44 + (\secref{sec:terms}). *}
1.45
1.46
1.47 section {* Conversions \label{sec:conv} *}
2.1 --- a/src/Doc/Ref/document/thm.tex Mon Nov 12 21:17:58 2012 +0100
2.2 +++ b/src/Doc/Ref/document/thm.tex Mon Nov 12 22:09:52 2012 +0100
2.3 @@ -1,7 +1,7 @@
2.4
2.5 \chapter{Theorems and Forward Proof}
2.6
2.7 -\subsection{*Sort hypotheses} \label{sec:sort-hyps}
2.8 +\section{*Sort hypotheses} \label{sec:sort-hyps}
2.9
2.10 \begin{ttbox}
2.11 strip_shyps : thm -> thm
2.12 @@ -46,80 +46,6 @@
2.13 \end{ttdescription}
2.14
2.15
2.16 -\section{*Primitive meta-level inference rules}
2.17 -
2.18 -\subsection{Logical equivalence rules}
2.19 -
2.20 -\begin{ttbox}
2.21 -equal_intr : thm -> thm -> thm
2.22 -equal_elim : thm -> thm -> thm
2.23 -\end{ttbox}
2.24 -\begin{ttdescription}
2.25 -\item[\ttindexbold{equal_intr} $thm@1$ $thm@2$]
2.26 -applies $({\equiv}I)$ to $thm@1$ and~$thm@2$. It maps the premises~$\psi$
2.27 -and~$\phi$ to the conclusion~$\phi\equiv\psi$; the assumptions are those of
2.28 -the first premise with~$\phi$ removed, plus those of
2.29 -the second premise with~$\psi$ removed.
2.30 -
2.31 -\item[\ttindexbold{equal_elim} $thm@1$ $thm@2$]
2.32 -applies $({\equiv}E)$ to $thm@1$ and~$thm@2$. It maps the premises
2.33 -$\phi\equiv\psi$ and $\phi$ to the conclusion~$\psi$.
2.34 -\end{ttdescription}
2.35 -
2.36 -
2.37 -\subsection{Equality rules}
2.38 -
2.39 -\begin{ttbox}
2.40 -reflexive : cterm -> thm
2.41 -symmetric : thm -> thm
2.42 -transitive : thm -> thm -> thm
2.43 -\end{ttbox}
2.44 -\begin{ttdescription}
2.45 -\item[\ttindexbold{reflexive} $ct$]
2.46 -makes the theorem \(ct\equiv ct\).
2.47 -
2.48 -\item[\ttindexbold{symmetric} $thm$]
2.49 -maps the premise $a\equiv b$ to the conclusion $b\equiv a$.
2.50 -
2.51 -\item[\ttindexbold{transitive} $thm@1$ $thm@2$]
2.52 -maps the premises $a\equiv b$ and $b\equiv c$ to the conclusion~${a\equiv c}$.
2.53 -\end{ttdescription}
2.54 -
2.55 -
2.56 -\subsection{The $\lambda$-conversion rules}
2.57 -
2.58 -\begin{ttbox}
2.59 -beta_conversion : cterm -> thm
2.60 -extensional : thm -> thm
2.61 -abstract_rule : string -> cterm -> thm -> thm
2.62 -combination : thm -> thm -> thm
2.63 -\end{ttbox}
2.64 -There is no rule for $\alpha$-conversion because Isabelle regards
2.65 -$\alpha$-convertible theorems as equal.
2.66 -\begin{ttdescription}
2.67 -\item[\ttindexbold{beta_conversion} $ct$]
2.68 -makes the theorem $((\lambda x.a)(b)) \equiv a[b/x]$, where $ct$ is the
2.69 -term $(\lambda x.a)(b)$.
2.70 -
2.71 -\item[\ttindexbold{extensional} $thm$]
2.72 -maps the premise $f(x) \equiv g(x)$ to the conclusion $f\equiv g$.
2.73 -Parameter~$x$ is taken from the premise. It may be an unknown or a free
2.74 -variable (provided it does not occur in the assumptions); it must not occur
2.75 -in $f$ or~$g$.
2.76 -
2.77 -\item[\ttindexbold{abstract_rule} $v$ $x$ $thm$]
2.78 -maps the premise $a\equiv b$ to the conclusion $(\lambda x.a) \equiv
2.79 -(\lambda x.b)$, abstracting over all occurrences (if any!) of~$x$.
2.80 -Parameter~$x$ is supplied as a cterm. It may be an unknown or a free
2.81 -variable (provided it does not occur in the assumptions). In the
2.82 -conclusion, the bound variable is named~$v$.
2.83 -
2.84 -\item[\ttindexbold{combination} $thm@1$ $thm@2$]
2.85 -maps the premises $f\equiv g$ and $a\equiv b$ to the conclusion~$f(a)\equiv
2.86 -g(b)$.
2.87 -\end{ttdescription}
2.88 -
2.89 -
2.90 \section{Proof terms}\label{sec:proofObjects}
2.91 \index{proof terms|(} Isabelle can record the full meta-level proof of each
2.92 theorem. The proof term contains all logical inferences in detail.