diff -r 4e6626725e21 -r 48cafea0684b doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Thu Jan 03 17:01:59 2002 +0100 +++ b/doc-src/IsarRef/generic.tex Thu Jan 03 17:48:02 2002 +0100 @@ -1,7 +1,7 @@ \chapter{Generic Tools and Packages}\label{ch:gen-tools} -\section{Theory commands} +\section{Theory specification commands} \subsection{Axiomatic type classes}\label{sec:axclass} @@ -57,10 +57,62 @@ FIXME +\indexouternonterm{contextelem} -\section{Proof commands} + +\section{Derived proof schemes} + +\subsection{Generalized elimination}\label{sec:obtain} + +\indexisarcmd{obtain} +\begin{matharray}{rcl} + \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ +\end{matharray} + +Generalized elimination means that additional elements with certain properties +may introduced in the current context, by virtue of a locally proven +``soundness statement''. Technically speaking, the $\OBTAINNAME$ language +element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see +\S\ref{sec:proof-context}), together with a soundness proof of its additional +claim. According to the nature of existential reasoning, assumptions get +eliminated from any result exported from the context later, provided that the +corresponding parameters do \emph{not} occur in the conclusion. + +\begin{rail} + 'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and') + ; +\end{rail} -\subsection{Calculational Reasoning}\label{sec:calculation} +$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$ +shall refer to (optional) facts indicated for forward chaining. +\begin{matharray}{l} + \langle facts~\vec b\rangle \\ + \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex] + \quad \BG \\ + \qquad \FIX{thesis} \\ + \qquad \ASSUME{that~[simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\ + \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\ + \quad \EN \\ + \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\ +\end{matharray} + +Typically, the soundness proof is relatively straight-forward, often just by +canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or +$\BY{blast}$ (see \S\ref{sec:classical-auto}). Accordingly, the ``$that$'' +reduction above is declared as simplification and introduction rule. + +\medskip + +In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be +meta-logical existential quantifiers and conjunctions. This concept has a +broad range of useful applications, ranging from plain elimination (or even +introduction) of object-level existentials and conjunctions, to elimination +over results of symbolic evaluation of recursive definitions, for example. +Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$, +where the result is treated as an assumption. + + +\subsection{Calculational reasoning}\label{sec:calculation} \indexisarcmd{also}\indexisarcmd{finally} \indexisarcmd{moreover}\indexisarcmd{ultimately} @@ -150,55 +202,7 @@ \end{descr} -\subsection{Generalized elimination}\label{sec:obtain} - -\indexisarcmd{obtain} -\begin{matharray}{rcl} - \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ -\end{matharray} - -Generalized elimination means that additional elements with certain properties -may introduced in the current context, by virtue of a locally proven -``soundness statement''. Technically speaking, the $\OBTAINNAME$ language -element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see also see -\S\ref{sec:proof-context}), together with a soundness proof of its additional -claim. According to the nature of existential reasoning, assumptions get -eliminated from any result exported from the context later, provided that the -corresponding parameters do \emph{not} occur in the conclusion. - -\begin{rail} - 'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and') - ; -\end{rail} - -$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$ -shall refer to (optional) facts indicated for forward chaining. -\begin{matharray}{l} - \langle facts~\vec b\rangle \\ - \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex] - \quad \BG \\ - \qquad \FIX{thesis} \\ - \qquad \ASSUME{that~[simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\ - \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\ - \quad \EN \\ - \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\ -\end{matharray} - -Typically, the soundness proof is relatively straight-forward, often just by -canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or -$\BY{blast}$ (see \S\ref{sec:classical-auto}). Accordingly, the ``$that$'' -reduction above is declared as simplification and introduction rule. - -\medskip - -In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be -meta-logical existential quantifiers and conjunctions. This concept has a -broad range of useful applications, ranging from plain elimination (or even -introduction) of object-level existentials and conjunctions, to elimination -over results of symbolic evaluation of recursive definitions, for example. -Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$, -where the result is treated as an assumption. - +\section{Specific proof tools} \subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att} @@ -308,7 +312,7 @@ \end{descr} -\subsection{Tactic emulations}\label{sec:tactics} +\subsection{Further tactic emulations}\label{sec:tactics} The following improper proof methods emulate traditional tactics. These admit direct access to the goal state, which is normally considered harmful! In @@ -432,11 +436,13 @@ \end{descr} -\section{The Simplifier}\label{sec:simplifier} +\subsection{The Simplifier}\label{sec:simplifier} + +\subsubsection{Basic equational reasoning} -\subsection{Simplification methods}\label{sec:simp} +FIXME -\subsubsection{FIXME} +\subsubsection{Simplification methods}\label{sec:simp} \indexisarmeth{simp}\indexisarmeth{simp-all} \begin{matharray}{rcl} @@ -509,7 +515,7 @@ method available for single-step case splitting, see \S\ref{sec:basic-eq}. -\subsection{Declaring rules} +\subsubsection{Declaring rules} \indexisarcmd{print-simpset} \indexisaratt{simp}\indexisaratt{split}\indexisaratt{cong} @@ -535,7 +541,9 @@ \end{descr} -\subsection{Forward simplification} +\subsubsection{Forward simplification} + +FIXME thmargs \indexisaratt{simplified} \begin{matharray}{rcl} @@ -563,7 +571,9 @@ \end{descr} -\section{Basic equational reasoning}\label{sec:basic-eq} +\subsubsection{Basic equational reasoning}\label{sec:basic-eq} + +FIXME move? \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric} \begin{matharray}{rcl} @@ -601,9 +611,9 @@ \end{descr} -\section{The Classical Reasoner}\label{sec:classical} +\subsection{The Classical Reasoner}\label{sec:classical} -\subsection{Basic methods}\label{sec:classical-basic} +\subsubsection{Basic methods}\label{sec:classical-basic} \indexisarmeth{rule}\indexisarmeth{intro} \indexisarmeth{elim}\indexisarmeth{default}\indexisarmeth{contradiction} @@ -642,7 +652,7 @@ \end{descr} -\subsection{Automated methods}\label{sec:classical-auto} +\subsubsection{Automated methods}\label{sec:classical-auto} \indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow} \indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify} @@ -686,7 +696,7 @@ \S\ref{sec:simp}). -\subsection{Combined automated methods}\label{sec:clasimp} +\subsubsection{Combined automated methods}\label{sec:clasimp} \indexisarmeth{auto}\indexisarmeth{force}\indexisarmeth{clarsimp} \indexisarmeth{fastsimp}\indexisarmeth{slowsimp}\indexisarmeth{bestsimp} @@ -728,7 +738,7 @@ \end{descr} -\subsection{Declaring rules}\label{sec:classical-mod} +\subsubsection{Declaring rules}\label{sec:classical-mod} \indexisarcmd{print-claset} \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest} @@ -780,9 +790,9 @@ \end{descr} -\section{Proof by cases and induction}\label{sec:cases-induct} +\subsection{Proof by cases and induction}\label{sec:cases-induct} -\subsection{Rule contexts}\label{sec:rule-cases} +\subsubsection{Rule contexts}\label{sec:rule-cases} \indexisarcmd{case}\indexisarcmd{print-cases} \indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes} @@ -871,7 +881,7 @@ \end{descr} -\subsection{Proof methods}\label{sec:cases-induct-meth} +\subsubsection{Proof methods}\label{sec:cases-induct-meth} \indexisarmeth{cases}\indexisarmeth{induct} \begin{matharray}{rcl} @@ -1013,7 +1023,7 @@ ``$type: name$'' to the method argument. -\subsection{Declaring rules}\label{sec:cases-induct-att} +\subsubsection{Declaring rules}\label{sec:cases-induct-att} \indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct} \begin{matharray}{rcl} @@ -1044,83 +1054,6 @@ automatically (if none had been given already): $consumes~0$ is specified for ``type'' rules and $consumes~1$ for ``set'' rules. - -\section{Object-logic setup}\label{sec:object-logic} - -The very starting point for any Isabelle object-logic is a ``truth judgment'' -that links object-level statements to the meta-logic (with its minimal -language of $prop$ that covers universal quantification $\Forall$ and -implication $\Imp$). Common object-logics are sufficiently expressive to -\emph{internalize} rule statements over $\Forall$ and $\Imp$ within their own -language. This is useful in certain situations where a rule needs to be -viewed as an atomic statement from the meta-level perspective (e.g.\ $\All x x -\in A \Imp P(x)$ versus $\forall x \in A. P(x)$). - -From the following language elements, only the $atomize$ method and -$rule_format$ attribute are occasionally required by end-users, the rest is -mainly for those who need to setup their own object-logic. In the latter case -existing formulations of Isabelle/FOL or Isabelle/HOL may be taken as -realistic examples. - -Further generic tools may refer to the information provided by object-logic -declarations internally (such as locales \S\ref{sec:locale}, or the Classical -Reasoner \S\ref{sec:classical}). - -\indexisarcmd{judgment} -\indexisarmeth{atomize}\indexisaratt{atomize} -\indexisaratt{rule-format}\indexisaratt{rulify} - -\begin{matharray}{rcl} - \isarcmd{judgment} & : & \isartrans{theory}{theory} \\ - atomize & : & \isarmeth \\ - atomize & : & \isaratt \\ - rule_format & : & \isaratt \\ - rulify & : & \isaratt \\ -\end{matharray} - -\railalias{ruleformat}{rule\_format} -\railterm{ruleformat} - -\begin{rail} - 'judgment' constdecl - ; - ruleformat ('(' noasm ')')? - ; -\end{rail} - -\begin{descr} - -\item [$\isarkeyword{judgment}~c::\sigma~~syn$] declares constant $c$ as the - truth judgment of the current object-logic. Its type $\sigma$ should - specify a coercion of the category of object-level propositions to $prop$ of - the Pure meta-logic; the mixfix annotation $syn$ would typically just link - the object language (internally of syntactic category $logic$) with that of - $prop$. Only one $\isarkeyword{judgment}$ declaration may be given in any - theory development. - -\item [$atomize$] (as a method) rewrites any non-atomic premises of a - sub-goal, using the meta-level equations that have been declared via - $atomize$ (as an attribute) beforehand. As a result, heavily nested goals - become amenable to fundamental operations such as resolution (cf.\ the - $rule$ method) and proof-by-assumption (cf.\ $assumption$). - - A typical collection of $atomize$ rules for a particular object-logic would - provide an internalization for each of the connectives of $\Forall$, $\Imp$, - $\equiv$; meta-level conjunction expressed as $\All{\PROP\,C} (A \Imp B \Imp - \PROP\,C) \Imp PROP\,C$ should be covered as well. - -\item [$rule_format$] rewrites a theorem by the equalities declared as - $rulify$ rules in the current object-logic. By default, the result is fully - normalized, including assumptions and conclusions at any depth. The - $no_asm$ option restricts the transformation to the conclusion of a rule. - - In common object logics (HOL, FOL, ZF), the effect of $rule_format$ is to - replace (bounded) universal quantification ($\forall$) and implication - ($\imp$) by the corresponding rule statements over $\Forall$ and $\Imp$. - -\end{descr} - - %%% Local Variables: %%% mode: latex %%% TeX-master: "isar-ref"