# HG changeset patch # User wenzelm # Date 1352754592 -3600 # Node ID 24ef81a22ee9e98fc0ea4166775be480611925d7 # Parent 3a3c54342e58e2948b58e4ef905c01ee49a1b0b3 updated basic equality rules; diff -r 3a3c54342e58 -r 24ef81a22ee9 src/Doc/IsarImplementation/Eq.thy --- 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 "\"} for equality of arbitrary + terms, which includes equivalence of propositions of the logical + framework. The conceptual axiomatization of the constant @{text "\ + :: \ \ \ \ 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 \ u"} to one + stating @{text "u \ 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 "\\"}-conversion) and lifting of @{text + "\/\"} 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 "\"} and + @{text "\"} conversions. Note that @{text "\"} conversion is + implicit due to the representation of terms with de-Bruijn indices + (\secref{sec:terms}). *} section {* Conversions \label{sec:conv} *} diff -r 3a3c54342e58 -r 24ef81a22ee9 src/Doc/Ref/document/thm.tex --- 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.