diff -r ab63d9842332 -r 43a97a2155d0 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Wed Jan 02 21:52:54 2002 +0100 +++ b/doc-src/IsarRef/generic.tex Wed Jan 02 21:53:50 2002 +0100 @@ -1,7 +1,9 @@ \chapter{Generic Tools and Packages}\label{ch:gen-tools} -\section{Axiomatic Type Classes}\label{sec:axclass} +\section{Theory commands} + +\subsection{Axiomatic type classes}\label{sec:axclass} %FIXME % - qualified names @@ -51,7 +53,14 @@ \end{descr} -\section{Calculational proof}\label{sec:calculation} +\subsection{Locales and local contexts}\label{sec:locale} + +FIXME + + +\section{Proof commands} + +\subsection{Calculational Reasoning}\label{sec:calculation} \indexisarcmd{also}\indexisarcmd{finally} \indexisarcmd{moreover}\indexisarcmd{ultimately} @@ -141,110 +150,24 @@ \end{descr} -\section{Named local contexts (cases)}\label{sec:cases} - -\indexisarcmd{case}\indexisarcmd{print-cases} -\indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes} -\begin{matharray}{rcl} - \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{print_cases}^* & : & \isarkeep{proof} \\ - case_names & : & \isaratt \\ - params & : & \isaratt \\ - consumes & : & \isaratt \\ -\end{matharray} - -Basically, Isar proof contexts are built up explicitly using commands like -$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical -verification tasks this can become hard to manage, though. In particular, a -large number of local contexts may emerge from case analysis or induction over -inductive sets and types. - -\medskip - -The $\CASENAME$ command provides a shorthand to refer to certain parts of -logical context symbolically. Proof methods may provide an environment of -named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of -$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. - -It is important to note that $\CASENAME$ does \emph{not} provide any means to -peek at the current goal state, which is treated as strictly non-observable in -Isar! Instead, the cases considered here usually emerge in a canonical way -from certain pieces of specification that appear in the theory somewhere else -(e.g.\ in an inductive definition, or recursive function). See also -\S\ref{sec:induct-method} for more details of how this works in HOL. - -\medskip - -Named cases may be exhibited in the current proof context only if both the -proof method and the rules involved support this. Case names and parameters -of basic rules may be declared by hand as well, by using appropriate -attributes. Thus variant versions of rules that have been derived manually -may be used in advanced case analysis later. - -\railalias{casenames}{case\_names} -\railterm{casenames} - -\begin{rail} - 'case' nameref attributes? - ; - casenames (name + ) - ; - 'params' ((name * ) + 'and') - ; - 'consumes' nat? - ; -\end{rail} -%FIXME bug in rail - -\begin{descr} -\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$, - as provided by an appropriate proof method (such as $cases$ and $induct$ in - Isabelle/HOL, see \S\ref{sec:induct-method}). The command $\CASE{c}$ - abbreviates $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. -\item [$\isarkeyword{print_cases}$] prints all local contexts of the current - state, using Isar proof language notation. This is a diagnostic command; - $undo$ does not apply. -\item [$case_names~\vec c$] declares names for the local contexts of premises - of some theorem; $\vec c$ refers to the \emph{suffix} of the list of - premises. -\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of - premises $1, \dots, n$ of some theorem. An empty list of names may be given - to skip positions, leaving the present parameters unchanged. - - Note that the default usage of case rules does \emph{not} directly expose - parameters to the proof context (see also \S\ref{sec:induct-method-proper}). -\item [$consumes~n$] declares the number of ``major premises'' of a rule, - i.e.\ the number of facts to be consumed when it is applied by an - appropriate proof method (cf.\ \S\ref{sec:induct-method}). The default - value of $consumes$ is $n = 1$, which is appropriate for the usual kind of - cases and induction rules for inductive sets (cf.\ \S\ref{sec:inductive}). - Rules without any $consumes$ declaration given are treated as if - $consumes~0$ had been specified. - - Note that explicit $consumes$ declarations are only rarely needed; this is - already taken care of automatically by the higher-level $cases$ and $induct$ - declarations, see also \S\ref{sec:induct-att}. -\end{descr} - - -\section{Generalized existence}\label{sec:obtain} +\subsection{Generalized elimination}\label{sec:obtain} \indexisarcmd{obtain} \begin{matharray}{rcl} \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ \end{matharray} -Generalized existence means that additional elements with certain properties -may introduced in the current context. Technically, 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. +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' (assm comment? + 'and') + 'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and') ; \end{rail} @@ -277,7 +200,7 @@ where the result is treated as an assumption. -\section{Miscellaneous methods and attributes}\label{sec:misc-methods} +\subsection{Miscellaneous methods and attributes}\label{sec:misc-meth-att} \indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert} \indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} @@ -385,7 +308,7 @@ \end{descr} -\section{Tactic emulations}\label{sec:tactics} +\subsection{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 @@ -513,6 +436,8 @@ \subsection{Simplification methods}\label{sec:simp} +\subsubsection{FIXME} + \indexisarmeth{simp}\indexisarmeth{simp-all} \begin{matharray}{rcl} simp & : & \isarmeth \\ @@ -631,7 +556,7 @@ additional rules). By default the result is fully simplified, including assumptions and conclusion. The options $no_asm$ etc.\ restrict the Simplifier in the same way as the for the $simp$ method (see - \S\ref{sec:simp}). + \S\ref{sec:simp}). FIXME args The $simplified$ operation should be used only very rarely, usually for experimentation only. @@ -672,6 +597,7 @@ Note that the $simp$ method already involves repeated application of split rules as declared in the current context (see \S\ref{sec:simp}). \item [$symmetric$] applies the symmetry rule of meta or object equality. + FIXME sym decl \end{descr} @@ -850,13 +776,102 @@ The ``?'' version of $iff$ declares ``extra'' Classical Reasoner rules only, and omits the Simplifier declaration. Thus the declaration does not have any effect on automated proof tools, but only on simple methods such as - $rule$ (see \S\ref{sec:misc-methods}). + $rule$ (see \S\ref{sec:misc-meth-att}). \end{descr} -\section{Proof by cases and induction}\label{sec:induct-method} +\section{Proof by cases and induction}\label{sec:cases-induct} + +\subsection{Rule contexts}\label{sec:rule-cases} + +\indexisarcmd{case}\indexisarcmd{print-cases} +\indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes} +\begin{matharray}{rcl} + \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\ + \isarcmd{print_cases}^* & : & \isarkeep{proof} \\ + case_names & : & \isaratt \\ + params & : & \isaratt \\ + consumes & : & \isaratt \\ +\end{matharray} + +Basically, Isar proof contexts are built up explicitly using commands like +$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}). In typical +verification tasks this can become hard to manage, though. In particular, a +large number of local contexts may emerge from case analysis or induction over +inductive sets and types. + +\medskip + +The $\CASENAME$ command provides a shorthand to refer to certain parts of +logical context symbolically. Proof methods may provide an environment of +named ``cases'' of the form $c\colon \vec x, \vec \phi$. Then the effect of +$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. + +FIXME + +It is important to note that $\CASENAME$ does \emph{not} provide any means to +peek at the current goal state, which is treated as strictly non-observable in +Isar! Instead, the cases considered here usually emerge in a canonical way +from certain pieces of specification that appear in the theory somewhere else +(e.g.\ in an inductive definition, or recursive function). + +FIXME + +\medskip + +Named cases may be exhibited in the current proof context only if both the +proof method and the rules involved support this. Case names and parameters +of basic rules may be declared by hand as well, by using appropriate +attributes. Thus variant versions of rules that have been derived manually +may be used in advanced case analysis later. -\subsection{Proof methods}\label{sec:induct-method-proper} +\railalias{casenames}{case\_names} +\railterm{casenames} + +\begin{rail} + 'case' nameref attributes? + ; + casenames (name + ) + ; + 'params' ((name * ) + 'and') + ; + 'consumes' nat? + ; +\end{rail} +%FIXME bug in rail + +\begin{descr} +\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \phi$, + as provided by an appropriate proof method (such as $cases$ and $induct$, + see \S\ref{sec:cases-induct-meth}). The command $\CASE{c}$ abbreviates + $\FIX{\vec x}~\ASSUME{c}{\vec\phi}$. +\item [$\isarkeyword{print_cases}$] prints all local contexts of the current + state, using Isar proof language notation. This is a diagnostic command; + $undo$ does not apply. +\item [$case_names~\vec c$] declares names for the local contexts of premises + of some theorem; $\vec c$ refers to the \emph{suffix} of the list of + premises. +\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of + premises $1, \dots, n$ of some theorem. An empty list of names may be given + to skip positions, leaving the present parameters unchanged. + + Note that the default usage of case rules does \emph{not} directly expose + parameters to the proof context (see also \S\ref{sec:cases-induct-meth}). +\item [$consumes~n$] declares the number of ``major premises'' of a rule, + i.e.\ the number of facts to be consumed when it is applied by an + appropriate proof method (cf.\ \S\ref{sec:cases-induct-meth}). The default + value of $consumes$ is $n = 1$, which is appropriate for the usual kind of + cases and induction rules for inductive sets (cf.\ + \S\ref{sec:hol-inductive}). Rules without any $consumes$ declaration given + are treated as if $consumes~0$ had been specified. + + Note that explicit $consumes$ declarations are only rarely needed; this is + already taken care of automatically by the higher-level $cases$ and $induct$ + declarations, see also \S\ref{sec:cases-induct-att}. +\end{descr} + + +\subsection{Proof methods}\label{sec:cases-induct-meth} \indexisarmeth{cases}\indexisarmeth{induct} \begin{matharray}{rcl} @@ -869,12 +884,13 @@ corresponding rules may be specified and instantiated in a casual manner. Furthermore, these methods provide named local contexts that may be invoked via the $\CASENAME$ proof command within the subsequent proof text (cf.\ -\S\ref{sec:cases}). This accommodates compact proof texts even when reasoning -about large specifications. +\S\ref{sec:rule-cases}). This accommodates compact proof texts even when +reasoning about large specifications. Note that the full spectrum of this generic functionality is currently only supported by Isabelle/HOL, when used in conjunction with advanced definitional -packages (see especially \S\ref{sec:datatype} and \S\ref{sec:inductive}). +packages (see especially \S\ref{sec:hol-datatype} and +\S\ref{sec:hol-inductive}). \begin{rail} 'cases' spec @@ -920,7 +936,7 @@ \S\ref{sec:pure-meth-att}). This feature is rarely needed in practice; a typical application would be to specify additional arguments for rules stemming from parameterized inductive definitions (see also - \S\ref{sec:inductive}). + \S\ref{sec:hol-inductive}). The $open$ option causes the parameters of the new local contexts to be exposed to the current proof context. Thus local variables stemming from @@ -949,7 +965,7 @@ way as for $cases$, see above. \end{descr} -Above methods produce named local contexts (cf.\ \S\ref{sec:cases}), as +Above methods produce named local contexts (cf.\ \S\ref{sec:rule-cases}), as determined by the instantiated rule \emph{before} it has been applied to the internal proof state.\footnote{As a general principle, Isar proof text may never refer to parts of proof states directly.} Thus proper use of symbolic @@ -961,8 +977,8 @@ term variable $\Var{case}$\indexisarvar{case} --- for each case where it is fully specified. -The $\isarkeyword{print_cases}$ command (\S\ref{sec:cases}) prints all named -cases present in the current proof state. +The $\isarkeyword{print_cases}$ command (\S\ref{sec:rule-cases}) prints all +named cases present in the current proof state. \medskip @@ -984,12 +1000,11 @@ \medskip Facts presented to either method are consumed according to the number of -``major premises'' of the rule involved (see also \S\ref{sec:induct-att} and -\S\ref{sec:cases}), which is usually $0$ for plain cases and induction rules -of datatypes etc.\ and $1$ for rules of inductive sets and the like. The -remaining facts are inserted into the goal verbatim before the actual $cases$ -or $induct$ rule is applied (thus facts may be even passed through an -induction). +``major premises'' of the rule involved (see also \S\ref{sec:cases-induct}), +which is usually $0$ for plain cases and induction rules of datatypes etc.\ +and $1$ for rules of inductive sets and the like. The remaining facts are +inserted into the goal verbatim before the actual $cases$ or $induct$ rule is +applied (thus facts may be even passed through an induction). Note that whenever facts are present, the default rule selection scheme would provide a ``set'' rule only, with the first fact consumed and the rest @@ -998,7 +1013,7 @@ ``$type: name$'' to the method argument. -\subsection{Declaring rules}\label{sec:induct-att} +\subsection{Declaring rules}\label{sec:cases-induct-att} \indexisarcmd{print-induct-rules}\indexisaratt{cases}\indexisaratt{induct} \begin{matharray}{rcl} @@ -1022,14 +1037,90 @@ declared by advanced definitional packages. For special applications, these may be replaced manually by variant versions. -Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:cases}) to +Refer to the $case_names$ and $ps$ attributes (see \S\ref{sec:rule-cases}) to adjust names of cases and parameters of a rule. -The $consumes$ declaration (cf.\ \S\ref{sec:cases}) is taken care of +The $consumes$ declaration (cf.\ \S\ref{sec:rule-cases}) is taken care of 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"