# HG changeset patch # User wenzelm # Date 1010076482 -3600 # Node ID 48cafea0684b4a34227d6758fe01fa2ab409b295 # Parent 4e6626725e21f74acffc909126b78975e0e71166 next round of updates; diff -r 4e6626725e21 -r 48cafea0684b doc-src/IsarRef/Makefile --- a/doc-src/IsarRef/Makefile Thu Jan 03 17:01:59 2002 +0100 +++ b/doc-src/IsarRef/Makefile Thu Jan 03 17:48:02 2002 +0100 @@ -14,7 +14,7 @@ NAME = isar-ref FILES = isar-ref.tex intro.tex basics.tex syntax.tex pure.tex \ - generic.tex hol.tex zf.tex refcard.tex conversion.tex \ + generic.tex logics.tex refcard.tex conversion.tex \ ../isar.sty ../rail.sty ../railsetup.sty ../proof.sty \ ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib diff -r 4e6626725e21 -r 48cafea0684b doc-src/IsarRef/conversion.tex --- a/doc-src/IsarRef/conversion.tex Thu Jan 03 17:01:59 2002 +0100 +++ b/doc-src/IsarRef/conversion.tex Thu Jan 03 17:48:02 2002 +0100 @@ -508,7 +508,7 @@ declare the theorem otherwise later (e.g.\ as $[simp~del]$). -\section{Converting to actual Isar proof texts} +\section{Writing actual Isar proof texts} Porting legacy ML proof scripts into Isar tactic emulation scripts (see \S\ref{sec:port-scripts}) is mainly a technical issue, since the basic 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" diff -r 4e6626725e21 -r 48cafea0684b doc-src/IsarRef/hol.tex --- a/doc-src/IsarRef/hol.tex Thu Jan 03 17:01:59 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,356 +0,0 @@ - -\chapter{Isabelle/HOL specific elements}\label{ch:hol-tools} - -\section{Miscellaneous attributes} - -\indexisarattof{HOL}{split-format} -\begin{matharray}{rcl} - split_format^* & : & \isaratt \\ -\end{matharray} - -\railalias{splitformat}{split\_format} -\railterm{splitformat} -\railterm{complete} - -\begin{rail} - splitformat (((name * ) + 'and') | ('(' complete ')')) - ; -\end{rail} - -\begin{descr} - -\item [$split_format~\vec p@1 \dots \vec p@n$] puts tuple objects into - canonical form as specified by the arguments given; $\vec p@i$ refers to - occurrences in premise $i$ of the rule. The $split_format~(complete)$ form - causes \emph{all} arguments in function applications to be represented - canonically according to their tuple type structure. - - Note that these operations tend to invent funny names for new local - parameters to be introduced. - -\end{descr} - - -\section{Primitive types}\label{sec:typedef} - -\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef} -\begin{matharray}{rcl} - \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ - \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\ -\end{matharray} - -\begin{rail} - 'typedecl' typespec infix? comment? - ; - 'typedef' parname? typespec infix? \\ '=' term comment? - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original - $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but - also declares type arity $t :: (term, \dots, term) term$, making $t$ an - actual HOL type constructor. -\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating - non-emptiness of the set $A$. After finishing the proof, the theory will be - augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL} - for more information. Note that user-level theories usually do not directly - refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced - packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and - $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}). -\end{descr} - - -\section{Records}\label{sec:hol-record} - -FIXME proof tools (simp, cases/induct; no split!?); - -\indexisarcmdof{HOL}{record} -\begin{matharray}{rcl} - \isarcmd{record} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\begin{rail} - 'record' typespec '=' (type '+')? (field +) - ; - - field: name '::' type comment? - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$] - defines extensible record type $(\vec\alpha)t$, derived from the optional - parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$. - See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on - simply-typed extensible records. -\end{descr} - - -\section{Datatypes}\label{sec:hol-datatype} - -\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype} -\begin{matharray}{rcl} - \isarcmd{datatype} & : & \isartrans{theory}{theory} \\ - \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\railalias{repdatatype}{rep\_datatype} -\railterm{repdatatype} - -\begin{rail} - 'datatype' (dtspec + 'and') - ; - repdatatype (name * ) dtrules - ; - - dtspec: parname? typespec infix? '=' (cons + '|') - ; - cons: name (type * ) mixfix? comment? - ; - dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs -\end{rail} - -\begin{descr} -\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL. -\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive - ones, generating the standard infrastructure of derived concepts (primitive - recursion etc.). -\end{descr} - -The induction and exhaustion theorems generated provide case names according -to the constructors involved, while parameters are named after the types (see -also \S\ref{sec:cases-induct}). - -See \cite{isabelle-HOL} for more details on datatypes. Note that the theory -syntax above has been slightly simplified over the old version, usually -requiring more quotes and less parentheses. Apart from proper proof methods -for case-analysis and induction, there are also emulations of ML tactics -\texttt{case_tac} and \texttt{induct_tac} available, see -\S\ref{sec:induct_tac}. - - -\section{Recursive functions}\label{sec:recursion} - -\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc} -\begin{matharray}{rcl} - \isarcmd{primrec} & : & \isartrans{theory}{theory} \\ - \isarcmd{recdef} & : & \isartrans{theory}{theory} \\ - \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\ -%FIXME -% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\railalias{recdefsimp}{recdef\_simp} -\railterm{recdefsimp} - -\railalias{recdefcong}{recdef\_cong} -\railterm{recdefcong} - -\railalias{recdefwf}{recdef\_wf} -\railterm{recdefwf} - -\railalias{recdeftc}{recdef\_tc} -\railterm{recdeftc} - -\begin{rail} - 'primrec' parname? (equation + ) - ; - 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints? - ; - recdeftc thmdecl? tc comment? - ; - - equation: thmdecl? eqn - ; - eqn: prop comment? - ; - hints: '(' 'hints' (recdefmod * ) ')' - ; - recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod - ; - tc: nameref ('(' nat ')')? - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{primrec}$] defines primitive recursive functions over - datatypes, see also \cite{isabelle-HOL}. -\item [$\isarkeyword{recdef}$] defines general well-founded recursive - functions (using the TFL package), see also \cite{isabelle-HOL}. The - $(permissive)$ option tells TFL to recover from failed proof attempts, - returning unfinished results. The $recdef_simp$, $recdef_cong$, and - $recdef_wf$ hints refer to auxiliary rules to be used in the internal - automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\ - \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier - (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ - \S\ref{sec:classical}). -\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover - termination condition number $i$ (default $1$) as generated by a - $\isarkeyword{recdef}$ definition of constant $c$. - - Note that in most cases, $\isarkeyword{recdef}$ is able to finish its - internal proofs without manual intervention. -\end{descr} - -Both kinds of recursive definitions accommodate reasoning by induction (cf.\ -\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of -the function definition) refers to a specific induction rule, with parameters -named according to the user-specified equations. Case names of -$\isarkeyword{primrec}$ are that of the datatypes involved, while those of -$\isarkeyword{recdef}$ are numbered (starting from $1$). - -The equations provided by these packages may be referred later as theorem list -$f\mathord.simps$, where $f$ is the (collective) name of the functions -defined. Individual equations may be named explicitly as well; note that for -$\isarkeyword{recdef}$ each specification given by the user may result in -several theorems. - -\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using -the following attributes. - -\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf} -\begin{matharray}{rcl} - recdef_simp & : & \isaratt \\ - recdef_cong & : & \isaratt \\ - recdef_wf & : & \isaratt \\ -\end{matharray} - -\railalias{recdefsimp}{recdef\_simp} -\railterm{recdefsimp} - -\railalias{recdefcong}{recdef\_cong} -\railterm{recdefcong} - -\railalias{recdefwf}{recdef\_wf} -\railterm{recdefwf} - -\begin{rail} - (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') - ; -\end{rail} - - -\section{(Co)Inductive sets}\label{sec:hol-inductive} - -\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono} -\begin{matharray}{rcl} - \isarcmd{inductive} & : & \isartrans{theory}{theory} \\ - \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ - mono & : & \isaratt \\ -\end{matharray} - -\railalias{condefs}{con\_defs} -\railterm{condefs} - -\begin{rail} - ('inductive' | 'coinductive') sets intros monos? - ; - 'mono' (() | 'add' | 'del') - ; - - sets: (term comment? +) - ; - intros: 'intros' (thmdecl? prop comment? +) - ; - monos: 'monos' thmrefs comment? - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define - (co)inductive sets from the given introduction rules. -\item [$mono$] declares monotonicity rules. These rule are involved in the - automated monotonicity proof of $\isarkeyword{inductive}$. -\end{descr} - -See \cite{isabelle-HOL} for further information on inductive definitions in -HOL. - - -\section{Arithmetic} - -\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split} -\begin{matharray}{rcl} - arith & : & \isarmeth \\ - arith_split & : & \isaratt \\ -\end{matharray} - -\begin{rail} - 'arith' '!'? - ; -\end{rail} - -The $arith$ method decides linear arithmetic problems (on types $nat$, $int$, -$real$). Any current facts are inserted into the goal before running the -procedure. The ``!''~argument causes the full context of assumptions to be -included. The $arith_split$ attribute declares case split rules to be -expanded before the arithmetic procedure is invoked. - -Note that a simpler (but faster) version of arithmetic reasoning is already -performed by the Simplifier. - - -\section{Cases and induction: emulating tactic scripts}\label{sec:induct_tac} - -The following important tactical tools of Isabelle/HOL have been ported to -Isar. These should be never used in proper proof texts! - -\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac} -\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases} -\begin{matharray}{rcl} - case_tac^* & : & \isarmeth \\ - induct_tac^* & : & \isarmeth \\ - ind_cases^* & : & \isarmeth \\ - \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\railalias{casetac}{case\_tac} -\railterm{casetac} - -\railalias{inducttac}{induct\_tac} -\railterm{inducttac} - -\railalias{indcases}{ind\_cases} -\railterm{indcases} - -\railalias{inductivecases}{inductive\_cases} -\railterm{inductivecases} - -\begin{rail} - casetac goalspec? term rule? - ; - inducttac goalspec? (insts * 'and') rule? - ; - indcases (prop +) - ; - inductivecases thmdecl? (prop +) comment? - ; - - rule: ('rule' ':' thmref) - ; -\end{rail} - -\begin{descr} -\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes - only (unless an alternative rule is given explicitly). Furthermore, - $case_tac$ does a classical case split on booleans; $induct_tac$ allows only - variables to be given as instantiation. These tactic emulations feature - both goal addressing and dynamic instantiation. Note that named rule cases - are \emph{not} provided as would be by the proper $induct$ and $cases$ proof - methods (see \S\ref{sec:cases-induct}). - -\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface - to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted - forward manner. - - While $ind_cases$ is a proof method to apply the result immediately as - elimination rules, $\isarkeyword{inductive_cases}$ provides case split - theorems at the theory level for later use, -\end{descr} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "isar-ref" -%%% End: diff -r 4e6626725e21 -r 48cafea0684b doc-src/IsarRef/intro.tex --- a/doc-src/IsarRef/intro.tex Thu Jan 03 17:01:59 2002 +0100 +++ b/doc-src/IsarRef/intro.tex Thu Jan 03 17:48:02 2002 +0100 @@ -265,6 +265,8 @@ \subsection{How to write Isar proofs anyway?}\label{sec:isar-howto} +%FIXME tune + This is one of the key questions, of course. Isar offers a rather different approach to formal proof documents than plain old tactic scripts. Experienced users of existing interactive theorem proving systems may have to learn diff -r 4e6626725e21 -r 48cafea0684b doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Thu Jan 03 17:01:59 2002 +0100 +++ b/doc-src/IsarRef/isar-ref.tex Thu Jan 03 17:48:02 2002 +0100 @@ -89,8 +89,7 @@ \include{syntax} \include{pure} \include{generic} -\include{hol} -\include{zf} +\include{logics} \appendix \include{refcard} diff -r 4e6626725e21 -r 48cafea0684b doc-src/IsarRef/logics.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/logics.tex Thu Jan 03 17:48:02 2002 +0100 @@ -0,0 +1,500 @@ + +\chapter{Object-logic specific elements}\label{ch:logics} + +\section{General logic setup}\label{sec:object-logic} + +\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} + +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 +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. + +Generic tools may refer to the information provided by object-logic +declarations internally (e.g.\ locales \S\ref{sec:locale}, or the Classical +Reasoner \S\ref{sec:classical}). + +\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 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$, + and $\equiv$. Meta-level conjunction expressed in the manner of minimal + higher-order logic as $\All{\PROP\,C} (A \Imp B \Imp \PROP\,C) \Imp PROP\,C$ + should be covered as well (this is particularly important for locales, see + \S\ref{sec:locale}). + +\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} + + +\section{HOL} + +\subsection{Primitive types}\label{sec:typedef} + +\indexisarcmdof{HOL}{typedecl}\indexisarcmdof{HOL}{typedef} +\begin{matharray}{rcl} + \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ + \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\ +\end{matharray} + +\begin{rail} + 'typedecl' typespec infix? comment? + ; + 'typedef' parname? typespec infix? \\ '=' term comment? + ; +\end{rail} + +\begin{descr} +\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original + $\isarkeyword{typedecl}$ of Isabelle/Pure (see \S\ref{sec:types-pure}), but + also declares type arity $t :: (term, \dots, term) term$, making $t$ an + actual HOL type constructor. +\item [$\isarkeyword{typedef}~(\vec\alpha)t = A$] sets up a goal stating + non-emptiness of the set $A$. After finishing the proof, the theory will be + augmented by a Gordon/HOL-style type definition. See \cite{isabelle-HOL} + for more information. Note that user-level theories usually do not directly + refer to the HOL $\isarkeyword{typedef}$ primitive, but use more advanced + packages such as $\isarkeyword{record}$ (see \S\ref{sec:hol-record}) and + $\isarkeyword{datatype}$ (see \S\ref{sec:hol-datatype}). +\end{descr} + + +\subsection{Low-level tuples} + +\indexisarattof{HOL}{split-format} +\begin{matharray}{rcl} + split_format^* & : & \isaratt \\ +\end{matharray} + +\railalias{splitformat}{split\_format} +\railterm{splitformat} +\railterm{complete} + +\begin{rail} + splitformat (((name * ) + 'and') | ('(' complete ')')) + ; +\end{rail} + +\begin{descr} + +\item [$split_format~\vec p@1 \dots \vec p@n$] puts expressions of low-level + tuple types into canonical form as specified by the arguments given; $\vec + p@i$ refers to occurrences in premise $i$ of the rule. The + $split_format~(complete)$ form causes \emph{all} arguments in function + applications to be represented canonically according to their tuple type + structure. + + Note that these operations tend to invent funny names for new local + parameters to be introduced. + +\end{descr} + + +\subsection{Records}\label{sec:hol-record} + +FIXME proof tools (simp, cases/induct; no split!?); + +FIXME mixfix syntax; + +\indexisarcmdof{HOL}{record} +\begin{matharray}{rcl} + \isarcmd{record} & : & \isartrans{theory}{theory} \\ +\end{matharray} + +\begin{rail} + 'record' typespec '=' (type '+')? (constdecl +) + ; +\end{rail} + +\begin{descr} +\item [$\isarkeyword{record}~(\vec\alpha)t = \tau + \vec c :: \vec\sigma$] + defines extensible record type $(\vec\alpha)t$, derived from the optional + parent record $\tau$ by adding new field components $\vec c :: \vec\sigma$. + See \cite{isabelle-HOL,NaraschewskiW-TPHOLs98} for more information on + simply-typed extensible records. +\end{descr} + + +\subsection{Datatypes}\label{sec:hol-datatype} + +\indexisarcmdof{HOL}{datatype}\indexisarcmdof{HOL}{rep-datatype} +\begin{matharray}{rcl} + \isarcmd{datatype} & : & \isartrans{theory}{theory} \\ + \isarcmd{rep_datatype} & : & \isartrans{theory}{theory} \\ +\end{matharray} + +\railalias{repdatatype}{rep\_datatype} +\railterm{repdatatype} + +\begin{rail} + 'datatype' (dtspec + 'and') + ; + repdatatype (name * ) dtrules + ; + + dtspec: parname? typespec infix? '=' (cons + '|') + ; + cons: name (type * ) mixfix? comment? + ; + dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs +\end{rail} + +\begin{descr} +\item [$\isarkeyword{datatype}$] defines inductive datatypes in HOL. +\item [$\isarkeyword{rep_datatype}$] represents existing types as inductive + ones, generating the standard infrastructure of derived concepts (primitive + recursion etc.). +\end{descr} + +The induction and exhaustion theorems generated provide case names according +to the constructors involved, while parameters are named after the types (see +also \S\ref{sec:cases-induct}). + +See \cite{isabelle-HOL} for more details on datatypes. Note that the theory +syntax above has been slightly simplified over the old version, usually +requiring more quotes and less parentheses. Apart from proper proof methods +for case-analysis and induction, there are also emulations of ML tactics +\texttt{case_tac} and \texttt{induct_tac} available, see +\S\ref{sec:induct_tac}. + + +\subsection{Recursive functions}\label{sec:recursion} + +\indexisarcmdof{HOL}{primrec}\indexisarcmdof{HOL}{recdef}\indexisarcmdof{HOL}{recdef-tc} +\begin{matharray}{rcl} + \isarcmd{primrec} & : & \isartrans{theory}{theory} \\ + \isarcmd{recdef} & : & \isartrans{theory}{theory} \\ + \isarcmd{recdef_tc}^* & : & \isartrans{theory}{proof(prove)} \\ +%FIXME +% \isarcmd{defer_recdef} & : & \isartrans{theory}{theory} \\ +\end{matharray} + +\railalias{recdefsimp}{recdef\_simp} +\railterm{recdefsimp} + +\railalias{recdefcong}{recdef\_cong} +\railterm{recdefcong} + +\railalias{recdefwf}{recdef\_wf} +\railterm{recdefwf} + +\railalias{recdeftc}{recdef\_tc} +\railterm{recdeftc} + +\begin{rail} + 'primrec' parname? (equation + ) + ; + 'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints? + ; + recdeftc thmdecl? tc comment? + ; + + equation: thmdecl? eqn + ; + eqn: prop comment? + ; + hints: '(' 'hints' (recdefmod * ) ')' + ; + recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod + ; + tc: nameref ('(' nat ')')? + ; +\end{rail} + +\begin{descr} +\item [$\isarkeyword{primrec}$] defines primitive recursive functions over + datatypes, see also \cite{isabelle-HOL}. +\item [$\isarkeyword{recdef}$] defines general well-founded recursive + functions (using the TFL package), see also \cite{isabelle-HOL}. The + $(permissive)$ option tells TFL to recover from failed proof attempts, + returning unfinished results. The $recdef_simp$, $recdef_cong$, and + $recdef_wf$ hints refer to auxiliary rules to be used in the internal + automated proof process of TFL. Additional $clasimpmod$ declarations (cf.\ + \S\ref{sec:clasimp}) may be given to tune the context of the Simplifier + (cf.\ \S\ref{sec:simplifier}) and Classical reasoner (cf.\ + \S\ref{sec:classical}). +\item [$\isarkeyword{recdef_tc}~c~(i)$] recommences the proof for leftover + termination condition number $i$ (default $1$) as generated by a + $\isarkeyword{recdef}$ definition of constant $c$. + + Note that in most cases, $\isarkeyword{recdef}$ is able to finish its + internal proofs without manual intervention. +\end{descr} + +Both kinds of recursive definitions accommodate reasoning by induction (cf.\ +\S\ref{sec:cases-induct}): rule $c\mathord{.}induct$ (where $c$ is the name of +the function definition) refers to a specific induction rule, with parameters +named according to the user-specified equations. Case names of +$\isarkeyword{primrec}$ are that of the datatypes involved, while those of +$\isarkeyword{recdef}$ are numbered (starting from $1$). + +The equations provided by these packages may be referred later as theorem list +$f\mathord.simps$, where $f$ is the (collective) name of the functions +defined. Individual equations may be named explicitly as well; note that for +$\isarkeyword{recdef}$ each specification given by the user may result in +several theorems. + +\medskip Hints for $\isarkeyword{recdef}$ may be also declared globally, using +the following attributes. + +\indexisarattof{HOL}{recdef-simp}\indexisarattof{HOL}{recdef-cong}\indexisarattof{HOL}{recdef-wf} +\begin{matharray}{rcl} + recdef_simp & : & \isaratt \\ + recdef_cong & : & \isaratt \\ + recdef_wf & : & \isaratt \\ +\end{matharray} + +\railalias{recdefsimp}{recdef\_simp} +\railterm{recdefsimp} + +\railalias{recdefcong}{recdef\_cong} +\railterm{recdefcong} + +\railalias{recdefwf}{recdef\_wf} +\railterm{recdefwf} + +\begin{rail} + (recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') + ; +\end{rail} + + +\subsection{(Co)Inductive sets}\label{sec:hol-inductive} + +\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono} +\begin{matharray}{rcl} + \isarcmd{inductive} & : & \isartrans{theory}{theory} \\ + \isarcmd{coinductive} & : & \isartrans{theory}{theory} \\ + mono & : & \isaratt \\ +\end{matharray} + +\railalias{condefs}{con\_defs} +\railterm{condefs} + +\begin{rail} + ('inductive' | 'coinductive') sets intros monos? + ; + 'mono' (() | 'add' | 'del') + ; + + sets: (term comment? +) + ; + intros: 'intros' (thmdecl? prop comment? +) + ; + monos: 'monos' thmrefs comment? + ; +\end{rail} + +\begin{descr} +\item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define + (co)inductive sets from the given introduction rules. +\item [$mono$] declares monotonicity rules. These rule are involved in the + automated monotonicity proof of $\isarkeyword{inductive}$. +\end{descr} + +See \cite{isabelle-HOL} for further information on inductive definitions in +HOL. + + +\subsection{Arithmetic proof support} + +\indexisarmethof{HOL}{arith}\indexisarattof{HOL}{arith-split} +\begin{matharray}{rcl} + arith & : & \isarmeth \\ + arith_split & : & \isaratt \\ +\end{matharray} + +\begin{rail} + 'arith' '!'? + ; +\end{rail} + +The $arith$ method decides linear arithmetic problems (on types $nat$, $int$, +$real$). Any current facts are inserted into the goal before running the +procedure. The ``!''~argument causes the full context of assumptions to be +included. The $arith_split$ attribute declares case split rules to be +expanded before the arithmetic procedure is invoked. + +Note that a simpler (but faster) version of arithmetic reasoning is already +performed by the Simplifier. + + +\subsection{Cases and induction: emulating tactic scripts}\label{sec:induct_tac} + +The following important tactical tools of Isabelle/HOL have been ported to +Isar. These should be never used in proper proof texts! + +\indexisarmethof{HOL}{case-tac}\indexisarmethof{HOL}{induct-tac} +\indexisarmethof{HOL}{ind-cases}\indexisarcmdof{HOL}{inductive-cases} +\begin{matharray}{rcl} + case_tac^* & : & \isarmeth \\ + induct_tac^* & : & \isarmeth \\ + ind_cases^* & : & \isarmeth \\ + \isarcmd{inductive_cases} & : & \isartrans{theory}{theory} \\ +\end{matharray} + +\railalias{casetac}{case\_tac} +\railterm{casetac} + +\railalias{inducttac}{induct\_tac} +\railterm{inducttac} + +\railalias{indcases}{ind\_cases} +\railterm{indcases} + +\railalias{inductivecases}{inductive\_cases} +\railterm{inductivecases} + +\begin{rail} + casetac goalspec? term rule? + ; + inducttac goalspec? (insts * 'and') rule? + ; + indcases (prop +) + ; + inductivecases thmdecl? (prop +) comment? + ; + + rule: ('rule' ':' thmref) + ; +\end{rail} + +\begin{descr} +\item [$case_tac$ and $induct_tac$] admit to reason about inductive datatypes + only (unless an alternative rule is given explicitly). Furthermore, + $case_tac$ does a classical case split on booleans; $induct_tac$ allows only + variables to be given as instantiation. These tactic emulations feature + both goal addressing and dynamic instantiation. Note that named rule cases + are \emph{not} provided as would be by the proper $induct$ and $cases$ proof + methods (see \S\ref{sec:cases-induct}). + +\item [$ind_cases$ and $\isarkeyword{inductive_cases}$] provide an interface + to the \texttt{mk_cases} operation. Rules are simplified in an unrestricted + forward manner. + + While $ind_cases$ is a proof method to apply the result immediately as + elimination rules, $\isarkeyword{inductive_cases}$ provides case split + theorems at the theory level for later use, +\end{descr} + + +\section{HOLCF} + +\subsection{Mixfix syntax for continuous operations} + +\indexisarcmdof{HOLCF}{consts}\indexisarcmdof{HOLCF}{constdefs} + +\begin{matharray}{rcl} + \isarcmd{consts} & : & \isartrans{theory}{theory} \\ + \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\ +\end{matharray} + +HOLCF provides a separate type for continuous functions $\alpha \rightarrow +\beta$, with an explicit application operator $f \cdot x$. Isabelle mixfix +syntax normally refers directly to the pure meta-level function type $\alpha +\To \beta$, with application $f\,x$. + +The HOLCF variants of $\CONSTS$ and $\CONSTDEFS$ have the same outer syntax as +the pure versions (cf.\ \S\ref{sec:consts}). Internally, declarations +involving continuous function types are treated specifically, transforming the +syntax template accordingly and generating syntax translation rules for the +abstract and concrete representation of application. + +The behavior for plain meta-level function types is unchanged. Mixed +continuous and meta-level application is \emph{not} supported. + +\subsection{Recursive domains} + +\indexisarcmdof{HOLCF}{domain} +\begin{matharray}{rcl} + \isarcmd{domain} & : & \isartrans{theory}{theory} \\ +\end{matharray} + +\begin{rail} + 'domain' parname? (dmspec + 'and') + ; + + dmspec: typespec '=' (cons + '|') + ; + cons: name (type * ) mixfix? comment? + ; + dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs +\end{rail} + +Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\ +\S\ref{sec:hol-datatype}). Mutual recursive is supported, but no nesting nor +arbitrary branching. Domain constructors may be strict (default) or lazy, the +latter admits to introduce infinitary objects in the typical LCF manner (lazy +lists etc.). + +See also \cite{MuellerNvOS99} for further information HOLCF domains in +general. + + +\section{ZF} + +\subsection{Type checking} + +FIXME + +\subsection{Inductive sets and datatypes} + +FIXME + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "isar-ref" +%%% End: diff -r 4e6626725e21 -r 48cafea0684b doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Thu Jan 03 17:01:59 2002 +0100 +++ b/doc-src/IsarRef/pure.tex Thu Jan 03 17:48:02 2002 +0100 @@ -5,8 +5,8 @@ commands, together with fundamental proof methods and attributes. Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic tools and packages (such as the Simplifier) that are either part of Pure -Isabelle or pre-installed by most object logics. Chapter~\ref{ch:hol-tools} -refers to actual object-logic specific elements of Isabelle/HOL. +Isabelle or pre-installed by most object logics. Chapter~\ref{ch:logics} +refers to object-logic specific elements (mainly for HOL and ZF). \medskip @@ -16,15 +16,14 @@ are subsequently marked by ``$^*$'', are often helpful when developing proof documents, while their use is discouraged for the final outcome. Typical examples are diagnostic commands that print terms or theorems according to the -current context; other commands even emulate old-style tactical theorem -proving. +current context; other commands emulate old-style tactical theorem proving. -\section{Theory specification commands} +\section{Theory commands} \subsection{Defining theories}\label{sec:begin-thy} -\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context} +\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{context}\indexisarcmd{end} \begin{matharray}{rcl} \isarcmd{header} & : & \isarkeep{toplevel} \\ \isarcmd{theory} & : & \isartrans{toplevel}{theory} \\ @@ -38,14 +37,14 @@ proof as well. In contrast, ``old-style'' Isabelle theories support batch processing only, with the proof scripts collected in separate ML files. -The first actual command of any theory has to be $\THEORY$, starting a new -theory based on the merge of existing ones. Just preceding $\THEORY$, there -may be an optional $\isarkeyword{header}$ declaration, which is relevant to -document preparation only; it acts very much like a special pre-theory markup -command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The theory -context may be also changed by $\CONTEXT$ without creating a new theory. In -both cases, $\END$ concludes the theory development; it has to be the very -last command of any theory file. +The first ``real'' command of any theory has to be $\THEORY$, which starts a +new theory based on the merge of existing ones. Just preceding $\THEORY$, +there may be an optional $\isarkeyword{header}$ declaration, which is relevant +to document preparation only; it acts very much like a special pre-theory +markup command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}). The +$\END$ commands concludes a theory development; it has to be the very last +command of any theory file to loaded in batch-mode. The theory context may be +also changed interactively by $\CONTEXT$ without creating a new theory. \begin{rail} 'header' text @@ -54,8 +53,6 @@ ; 'context' name ; - 'end' - ;; filespecs: 'files' ((name | parname) +); \end{rail} @@ -67,28 +64,42 @@ produce chapter or section headings. See also \S\ref{sec:markup-thy} and \S\ref{sec:markup-prf} for further markup commands. -\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] commences a new theory $A$ - based on existing ones $B@1 + \cdots + B@n$. Isabelle's theory loader - system ensures that any of the base theories are properly loaded (and fully - up-to-date when $\THEORY$ is executed interactively). The optional - $\isarkeyword{files}$ specification declares additional dependencies on ML - files. Unless put in parentheses, any file will be loaded immediately via - $\isarcmd{use}$ (see also \S\ref{sec:ML}). The optional ML file - \texttt{$A$.ML} that may be associated with any theory should \emph{not} be - included in $\isarkeyword{files}$, though. +\item [$\THEORY~A = B@1 + \cdots + B@n\colon$] starts a new theory $A$ based + on the merge of existing theories $B@1, \dots, B@n$. + + Due to inclusion of several ancestors, the overall theory structure emerging + in an Isabelle session forms a directed acyclic graph (DAG). Isabelle's + theory loader ensures that the sources contributing to the development graph + are always up-to-date. Changed files are automatically reloaded when + processing theory headers interactively; batch-mode explicitly distinguishes + \verb,update_thy, from \verb,use_thy,, see also \cite{isabelle-ref}. + + The optional $\isarkeyword{files}$ specification declares additional + dependencies on ML files. Files will be loaded immediately, unless the name + is put in parentheses, which merely documents the dependency to be resolved + later in the text (typically via explicit $\isarcmd{use}$ in the body text, + see \S\ref{sec:ML}). In reminiscence of the old-style theory system of + Isabelle, \texttt{$A$.thy} may be also accompanied by an additional file + \texttt{$A$.ML} consisting of ML code that is executed in the context of the + \emph{finished} theory $A$. That file should not be included in the + $\isarkeyword{files}$ dependency declaration, though. \item [$\CONTEXT~B$] enters an existing theory context, basically in read-only mode, so only a limited set of commands may be performed without destroying the theory. Just as for $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date. + This command is occasionally useful for quick interactive experiments; + normally one should always commence a new context via $\THEORY$. + \item [$\END$] concludes the current theory definition or context switch. -Note that this command cannot be undone, but the whole theory definition has -to be retracted. + Note that this command cannot be undone, but the whole theory definition has + to be retracted. + \end{descr} -\subsection{Theory markup commands}\label{sec:markup-thy} +\subsection{Markup commands}\label{sec:markup-thy} \indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection} \indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw} @@ -144,9 +155,9 @@ \subsection{Type classes and sorts}\label{sec:classes} \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort} -\begin{matharray}{rcl} +\begin{matharray}{rcll} \isarcmd{classes} & : & \isartrans{theory}{theory} \\ - \isarcmd{classrel} & : & \isartrans{theory}{theory} \\ + \isarcmd{classrel} & : & \isartrans{theory}{theory} & (axiomatic!) \\ \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\ \end{matharray} @@ -169,18 +180,18 @@ proven class relations. \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for any type variables given without sort constraints. Usually, the default - sort would be only changed when defining new object-logics. + sort would be only changed when defining a new object-logic. \end{descr} \subsection{Primitive types and type abbreviations}\label{sec:types-pure} \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities} -\begin{matharray}{rcl} +\begin{matharray}{rcll} \isarcmd{types} & : & \isartrans{theory}{theory} \\ \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\ - \isarcmd{arities} & : & \isartrans{theory}{theory} \\ + \isarcmd{arities} & : & \isartrans{theory}{theory} & (axiomatic!) \\ \end{matharray} \begin{rail} @@ -247,10 +258,9 @@ Unless this option is given, a warning message would be issued for any definitional equation with a more special type than that of the corresponding constant declaration. - -\item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and - definitions of constants, using the canonical name $c_def$ for the - definitional axiom. + +\item [$\CONSTDEFS~c::\sigma~eqn$] combines declarations and definitions of + constants, using the canonical name $c_def$ for the definitional axiom. \end{descr} @@ -300,8 +310,8 @@ \subsection{Axioms and theorems}\label{sec:axms-thms} \indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems} -\begin{matharray}{rcl} - \isarcmd{axioms} & : & \isartrans{theory}{theory} \\ +\begin{matharray}{rcll} + \isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\ \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\ \isarcmd{theorems} & : & \isartrans{theory}{theory} \\ \end{matharray} @@ -366,9 +376,7 @@ name space (which may be $class$, $type$, or $const$). Hidden objects remain valid within the logic, but are inaccessible from user input. In output, the special qualifier ``$\mathord?\mathord?$'' is prefixed to the - full internal name. - - Unqualified (global) names may not be hidden deliberately. + full internal name. Unqualified (global) names may not be hidden. \end{descr} @@ -550,9 +558,15 @@ goal claimed next. \end{descr} -%FIXME diagram? +The proof mode indicator may be read as a verb telling the writer what kind of +operation may be performed next. The corresponding typings of proof commands +restricts the shape of well-formed proof texts to particular command +sequences. So dynamic arrangements of commands eventually turn out as static +texts. Appendix~\ref{ap:refcard} gives a simplified grammar of the overall +(extensible) language emerging that way. -\subsection{Proof markup commands}\label{sec:markup-prf} + +\subsection{Markup commands}\label{sec:markup-prf} \indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect} \indexisarcmd{txt}\indexisarcmd{txt-raw} @@ -576,7 +590,7 @@ \end{rail} -\subsection{Proof context}\label{sec:proof-context} +\subsection{Context elements}\label{sec:proof-context} \indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def} \begin{matharray}{rcl} @@ -699,7 +713,7 @@ Forward chaining with an empty list of theorems is the same as not chaining. Thus $\FROM{nothing}$ has no effect apart from entering $prove(chain)$ mode, -since $nothing$\indexisarthm{nothing} is bound to the empty list of facts. +since $nothing$\indexisarthm{nothing} is bound to the empty list of theorems. \subsection{Goal statements} @@ -716,11 +730,11 @@ \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ \end{matharray} -From a theory context, proof mode is entered from theory mode by initial goal -commands $\LEMMANAME$, $\THEOREMNAME$, and $\COROLLARYNAME$. Within a proof, -new claims may be introduced locally as well; four variants are available, -indicating whether the result is meant to solve some pending goal or whether -forward chaining is indicated. +From a theory context, proof mode is entered by an initial goal command such +as $\LEMMANAME$, $\THEOREMNAME$, $\COROLLARYNAME$. Within a proof, new claims +may be introduced locally as well; four variants are available here to +indicate whether forward chaining of facts should be performed initially (via +$\THEN$), and whether the emerging result is meant to solve some pending goal. Goals may consist of multiple statements, resulting in a list of facts eventually. A pending multi-goal is internally represented as a meta-level @@ -731,16 +745,21 @@ the $induct$ method covered in \S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.} -%FIXME define locale, context - \begin{rail} - ('lemma' | 'theorem' | 'corollary') locale context goal + ('lemma' | 'theorem' | 'corollary') goalprefix goal ; ('have' | 'show' | 'hence' | 'thus') goal ; goal: (props comment? + 'and') ; + + goalprefix: thmdecl? locale? context? + ; + locale: '(' 'in' name ')' + ; + context: '(' (contextelem +) ')' + ; \end{rail} \begin{descr} @@ -749,8 +768,8 @@ theory context, and optionally into the specified locale, cf.\ \S\ref{sec:locale}. An additional \railnonterm{context} specification may build an initial proof context for the subsequent claim; this may include - local definitions and syntax as well, see \S\ref{sec:locale} for more - information. + local definitions and syntax as well, see the definition of $contextelem$ in + \S\ref{sec:locale}. \item [$\THEOREM{a}{\vec\phi}$ and $\COROLLARY{a}{\vec\phi}$] are essentially the same as $\LEMMA{a}{\vec\phi}$, but the facts are internally marked as @@ -832,18 +851,19 @@ remaining goals. No facts are passed to $m@2$. \end{enumerate} -The only other proper way to affect pending goals is by $\SHOWNAME$, which -involves an explicit statement of what is to be solved. +The only other proper way to affect pending goals in a proof body is by +$\SHOWNAME$, which involves an explicit statement of what is to be solved +eventually. Thus we avoid the fundamental problem of unstructured tactic +scripts that consist of numerous consecutive goal transformations, with +invisible effects. \medskip -Also note that initial proof methods should either solve the goal completely, -or constitute some well-understood reduction to new sub-goals. Arbitrary -automatic proof tools that are prone leave a large number of badly structured -sub-goals are no help in continuing the proof document in any intelligible -way. - -\medskip +As a general rule of thumb for good proof style, initial proof methods should +either solve the goal completely, or constitute some well-understood reduction +to new sub-goals. Arbitrary automatic proof tools that are prone leave a +large number of badly structured sub-goals are no help in continuing the proof +document in any intelligible way. Unless given explicitly by the user, the default initial method is ``$rule$'', which applies a single standard elimination or introduction rule according to @@ -903,11 +923,12 @@ The following proof methods and attributes refer to basic logical operations of Isar. Further methods and attributes are provided by several generic and object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and -\ref{ch:hol-tools}). +\ref{ch:logics}). \indexisarmeth{assumption}\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{$-$} -\indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}\indexisaratt{rule} \indexisaratt{OF}\indexisaratt{of} +\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim} +\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule} \begin{matharray}{rcl} assumption & : & \isarmeth \\ this & : & \isarmeth \\ @@ -921,6 +942,8 @@ rule & : & \isaratt \\ \end{matharray} +%FIXME intro!, intro, intro? + \begin{rail} 'rule' thmrefs? ; @@ -990,8 +1013,8 @@ patterns occur on the left-hand side, while the $\ISNAME$ patterns are in postfix position. -Polymorphism of term bindings is handled in Hindley-Milner style, as in ML. -Type variables referring to local assumptions or open goal statements are +Polymorphism of term bindings is handled in Hindley-Milner style, similar to +ML. Type variables referring to local assumptions or open goal statements are \emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur in \emph{arbitrary} instances later. Even though actual polymorphism should be rarely used in practice, this mechanism is essential to achieve proper diff -r 4e6626725e21 -r 48cafea0684b doc-src/IsarRef/zf.tex --- a/doc-src/IsarRef/zf.tex Thu Jan 03 17:01:59 2002 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ - -\chapter{Isabelle/ZF specific elements}\label{ch:zf-tools} - -\section{Type checking} - -FIXME - - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "isar-ref" -%%% End: