# HG changeset patch # User wenzelm # Date 1209738965 -7200 # Node ID cc127cc0951bf69f37adc3a32968c4da9f221c29 # Parent 0e2a29a1065c971359264602670d3659a8fd4370 converted pure.tex to Thy/pure.thy; diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/IsaMakefile --- a/doc-src/IsarRef/IsaMakefile Fri May 02 16:32:51 2008 +0200 +++ b/doc-src/IsarRef/IsaMakefile Fri May 02 16:36:05 2008 +0200 @@ -22,7 +22,7 @@ Thy: $(LOG)/HOL-Thy.gz $(LOG)/HOL-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/intro.thy \ - Thy/syntax.thy + Thy/pure.thy Thy/syntax.thy @$(USEDIR) HOL Thy diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/Makefile --- a/doc-src/IsarRef/Makefile Fri May 02 16:32:51 2008 +0200 +++ b/doc-src/IsarRef/Makefile Fri May 02 16:36:05 2008 +0200 @@ -13,8 +13,8 @@ NAME = isar-ref -FILES = isar-ref.tex Thy/document/intro.tex basics.tex Thy/document/syntax.tex pure.tex \ - generic.tex logics.tex refcard.tex conversion.tex \ +FILES = isar-ref.tex Thy/document/intro.tex basics.tex Thy/document/syntax.tex \ + Thy/document/pure.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 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/Thy/ROOT.ML --- a/doc-src/IsarRef/Thy/ROOT.ML Fri May 02 16:32:51 2008 +0200 +++ b/doc-src/IsarRef/Thy/ROOT.ML Fri May 02 16:36:05 2008 +0200 @@ -4,3 +4,4 @@ use "../../antiquote_setup.ML"; use_thy "intro"; use_thy "syntax"; +use_thy "pure"; diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/Thy/document/intro.tex --- a/doc-src/IsarRef/Thy/document/intro.tex Fri May 02 16:32:51 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/intro.tex Fri May 02 16:36:05 2008 +0200 @@ -4,6 +4,7 @@ % \isadelimtheory \isanewline +\isanewline % \endisadelimtheory % diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/Thy/document/pure.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/document/pure.tex Fri May 02 16:36:05 2008 +0200 @@ -0,0 +1,1806 @@ +% +\begin{isabellebody}% +\def\isabellecontext{pure}% +% +\isadelimtheory +\isanewline +\isanewline +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ pure\isanewline +\isakeyword{imports}\ CPure\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupchapter{Basic language elements \label{ch:pure-syntax}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Subsequently, we introduce the main part of Pure theory and proof + commands, together with fundamental proof methods and attributes. + \Chref{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 in most object logics. + \Chref{ch:logics} refers to object-logic specific elements (mainly + for HOL and ZF). + + \medskip Isar commands may be either \emph{proper} document + constructors, or \emph{improper commands}. Some proof methods and + attributes introduced later are classified as improper as well. + Improper Isar language elements, which are subsequently marked by + ``\isa{\isactrlsup {\isacharasterisk}}'', are often helpful when developing proof + documents, while their use is discouraged for the final + human-readable outcome. Typical examples are diagnostic commands + that print terms or theorems according to the current context; other + commands emulate old-style tactical theorem proving.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Theory commands% +} +\isamarkuptrue% +% +\isamarkupsubsection{Defining theories \label{sec:begin-thy}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{header}\isa{\isacommand{header}} & : & \isarkeep{toplevel} \\ + \indexdef{}{command}{theory}\isa{\isacommand{theory}} & : & \isartrans{toplevel}{theory} \\ + \indexdef{}{command}{end}\isa{\isacommand{end}} & : & \isartrans{theory}{toplevel} \\ + \end{matharray} + + Isabelle/Isar theories are defined via theory, which contain both + specifications and proofs; occasionally definitional mechanisms also + require some explicit proof. + + The first ``real'' command of any theory has to be \isa{\isacommand{theory}}, which starts a new theory based on the merge of existing + ones. Just preceding the \isa{\isacommand{theory}} keyword, there may be + an optional \isa{\isacommand{header}} declaration, which is relevant to + document preparation only; it acts very much like a special + pre-theory markup command (cf.\ \secref{sec:markup-thy} and + \secref{sec:markup-thy}). The \isa{\isacommand{end}} command concludes a + theory development; it has to be the very last command of any theory + file loaded in batch-mode. + + \begin{rail} + 'header' text + ; + 'theory' name 'imports' (name +) uses? 'begin' + ; + + uses: 'uses' ((name | parname) +); + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{header}}~\isa{text}] provides plain text + markup just preceding the formal beginning of a theory. In actual + document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section + headings. See also \secref{sec:markup-thy} and + \secref{sec:markup-prf} for further markup commands. + + \item [\isa{\isacommand{theory}}~\isa{A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}}] starts a new theory \isa{A} based on the + merge of existing theories \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub 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. + + The optional \indexdef{}{keyword}{uses}\isa{\isakeyword{uses}} specification declares additional + dependencies on extra files (usually ML sources). Files will be + loaded immediately (as ML), unless the name is put in parentheses, + which merely documents the dependency to be resolved later in the + text (typically via explicit \indexref{}{command}{use}\isa{\isacommand{use}} in the body text, + see \secref{sec:ML}). + + \item [\isa{\isacommand{end}}] concludes the current theory definition or + context switch. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Markup commands \label{sec:markup-thy}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{chapter}\isa{\isacommand{chapter}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{}{command}{section}\isa{\isacommand{section}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{}{command}{subsection}\isa{\isacommand{subsection}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{}{command}{subsubsection}\isa{\isacommand{subsubsection}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{}{command}{text}\isa{\isacommand{text}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{}{command}{text-raw}\isa{\isacommand{text{\isacharunderscore}raw}} & : & \isarkeep{local{\dsh}theory} \\ + \end{matharray} + + Apart from formal comments (see \secref{sec:comments}), markup + commands provide a structured way to insert text into the document + generated from a theory (see \cite{isabelle-sys} for more + information on Isabelle's document preparation tools). + + \begin{rail} + ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text + ; + 'text\_raw' text + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{chapter}}, \isa{\isacommand{section}}, \isa{\isacommand{subsection}}, and \isa{\isacommand{subsubsection}}] mark chapter and + section headings. + + \item [\isa{\isacommand{text}}] specifies paragraphs of plain text. + + \item [\isa{\isacommand{text{\isacharunderscore}raw}}] inserts {\LaTeX} source into the + output, without additional markup. Thus the full range of document + manipulations becomes available. + + \end{descr} + + The \isa{text} argument of these markup commands (except for + \isa{\isacommand{text{\isacharunderscore}raw}}) may contain references to formal entities + (``antiquotations'', see also \secref{sec:antiq}). These are + interpreted in the present theory context, or the named \isa{target}. + + Any of these markup elements corresponds to a {\LaTeX} command with + the name prefixed by \verb|\isamarkup|. For the sectioning + commands this is a plain macro with a single argument, e.g.\ + \verb|\isamarkupchapter{|\isa{{\isasymdots}}\verb|}| for + \isa{\isacommand{chapter}}. The \isa{\isacommand{text}} markup results in a + {\LaTeX} environment \verb|\begin{isamarkuptext}|~\isa{{\isasymdots}}~\verb|\end{isamarkuptext}|, while \isa{\isacommand{text{\isacharunderscore}raw}} + causes the text to be inserted directly into the {\LaTeX} source. + + \medskip Additional markup commands are available for proofs (see + \secref{sec:markup-prf}). Also note that the \indexref{}{command}{header}\isa{\isacommand{header}} declaration (see \secref{sec:begin-thy}) admits to insert + section markup just preceding the actual theory definition.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Type classes and sorts \label{sec:classes}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcll} + \indexdef{}{command}{classes}\isa{\isacommand{classes}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{classrel}\isa{\isacommand{classrel}} & : & \isartrans{theory}{theory} & (axiomatic!) \\ + \indexdef{}{command}{defaultsort}\isa{\isacommand{defaultsort}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{class-deps}\isa{\isacommand{class{\isacharunderscore}deps}} & : & \isarkeep{theory~|~proof} \\ + \end{matharray} + + \begin{rail} + 'classes' (classdecl +) + ; + 'classrel' (nameref ('<' | subseteq) nameref + 'and') + ; + 'defaultsort' sort + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{classes}}~\isa{c\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n}] + declares class \isa{c} to be a subclass of existing classes \isa{c\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ c\isactrlsub n}. Cyclic class structures are not permitted. + + \item [\isa{\isacommand{classrel}}~\isa{c\isactrlsub {\isadigit{1}}\ {\isasymsubseteq}\ c\isactrlsub {\isadigit{2}}}] states + subclass relations between existing classes \isa{c\isactrlsub {\isadigit{1}}} and + \isa{c\isactrlsub {\isadigit{2}}}. This is done axiomatically! The \indexref{}{command}{instance}\isa{\isacommand{instance}} command (see \secref{sec:axclass}) provides a way to + introduce proven class relations. + + \item [\isa{\isacommand{defaultsort}}~\isa{s}] makes sort \isa{s} the + new default sort for any type variables given without sort + constraints. Usually, the default sort would be only changed when + defining a new object-logic. + + \item [\isa{\isacommand{class{\isacharunderscore}deps}}] visualizes the subclass relation, + using Isabelle's graph browser tool (see also \cite{isabelle-sys}). + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Primitive types and type abbreviations \label{sec:types-pure}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcll} + \indexdef{}{command}{types}\isa{\isacommand{types}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{typedecl}\isa{\isacommand{typedecl}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{nonterminals}\isa{\isacommand{nonterminals}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{arities}\isa{\isacommand{arities}} & : & \isartrans{theory}{theory} & (axiomatic!) \\ + \end{matharray} + + \begin{rail} + 'types' (typespec '=' type infix? +) + ; + 'typedecl' typespec infix? + ; + 'nonterminals' (name +) + ; + 'arities' (nameref '::' arity +) + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{types}}~\isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t\ {\isacharequal}\ {\isasymtau}}] + introduces \emph{type synonym} \isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t} + for existing type \isa{{\isasymtau}}. Unlike actual type definitions, as + are available in Isabelle/HOL for example, type synonyms are just + purely syntactic abbreviations without any logical significance. + Internally, type synonyms are fully expanded. + + \item [\isa{\isacommand{typedecl}}~\isa{{\isacharparenleft}{\isasymalpha}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlsub n{\isacharparenright}\ t}] + declares a new type constructor \isa{t}, intended as an actual + logical type (of the object-logic, if available). + + \item [\isa{\isacommand{nonterminals}}~\isa{c}] declares type + constructors \isa{c} (without arguments) to act as purely + syntactic types, i.e.\ nonterminal symbols of Isabelle's inner + syntax of terms or types. + + \item [\isa{\isacommand{arities}}~\isa{t\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}s\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ s\isactrlsub n{\isacharparenright}\ s}] augments Isabelle's order-sorted signature of types by new type + constructor arities. This is done axiomatically! The \indexref{}{command}{instance}\isa{\isacommand{instance}} command (see \S\ref{sec:axclass}) provides a way to + introduce proven type arities. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Primitive constants and definitions \label{sec:consts}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Definitions essentially express abbreviations within the logic. The + simplest form of a definition is \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}\ {\isasymequiv}\ t}, where \isa{c} is a newly declared constant. Isabelle also allows derived forms + where the arguments of \isa{c} appear on the left, abbreviating a + prefix of \isa{{\isasymlambda}}-abstractions, e.g.\ \isa{c\ {\isasymequiv}\ {\isasymlambda}x\ y{\isachardot}\ t} may be + written more conveniently as \isa{c\ x\ y\ {\isasymequiv}\ t}. Moreover, + definitions may be weakened by adding arbitrary pre-conditions: + \isa{A\ {\isasymLongrightarrow}\ c\ x\ y\ {\isasymequiv}\ t}. + + \medskip The built-in well-formedness conditions for definitional + specifications are: + + \begin{itemize} + + \item Arguments (on the left-hand side) must be distinct variables. + + \item All variables on the right-hand side must also appear on the + left-hand side. + + \item All type variables on the right-hand side must also appear on + the left-hand side; this prohibits \isa{{\isadigit{0}}\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymequiv}\ length\ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ list{\isacharparenright}} for example. + + \item The definition must not be recursive. Most object-logics + provide definitional principles that can be used to express + recursion safely. + + \end{itemize} + + Overloading means that a constant being declared as \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ decl} may be defined separately on type instances \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n{\isacharparenright}\ t\ decl} for each type constructor \isa{t}. The right-hand side may mention overloaded constants + recursively at type instances corresponding to the immediate + argument types \isa{{\isasymbeta}\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymbeta}\isactrlsub n}. Incomplete + specification patterns impose global constraints on all occurrences, + e.g.\ \isa{d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymalpha}} on the left-hand side means that all + corresponding occurrences on some right-hand side need to be an + instance of this, general \isa{d\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}} will be disallowed. + + \begin{matharray}{rcl} + \indexdef{}{command}{consts}\isa{\isacommand{consts}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{defs}\isa{\isacommand{defs}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{constdefs}\isa{\isacommand{constdefs}} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'consts' ((name '::' type mixfix?) +) + ; + 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +) + ; + \end{rail} + + \begin{rail} + 'constdefs' structs? (constdecl? constdef +) + ; + + structs: '(' 'structure' (vars + 'and') ')' + ; + constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where' + ; + constdef: thmdecl? prop + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{consts}}~\isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}}] declares constant + \isa{c} to have any instance of type scheme \isa{{\isasymsigma}}. The + optional mixfix annotations may attach concrete syntax to the + constants declared. + + \item [\isa{\isacommand{defs}}~\isa{name{\isacharcolon}\ eqn}] introduces \isa{eqn} + as a definitional axiom for some existing constant. + + The \isa{{\isacharparenleft}unchecked{\isacharparenright}} option disables global dependency checks + for this definition, which is occasionally useful for exotic + overloading. It is at the discretion of the user to avoid malformed + theory specifications! + + The \isa{{\isacharparenleft}overloaded{\isacharparenright}} option declares definitions to be + potentially overloaded. 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 [\isa{\isacommand{constdefs}}] provides a streamlined combination of + constants declarations and definitions: type-inference takes care of + the most general typing of the given specification (the optional + type constraint may refer to type-inference dummies ``\verb|_|'' as usual). The resulting type declaration needs to agree with + that of the specification; overloading is \emph{not} supported here! + + The constant name may be omitted altogether, if neither type nor + syntax declarations are given. The canonical name of the + definitional axiom for constant \isa{c} will be \isa{c{\isacharunderscore}def}, + unless specified otherwise. Also note that the given list of + specifications is processed in a strictly sequential manner, with + type-checking being performed independently. + + An optional initial context of \isa{{\isacharparenleft}structure{\isacharparenright}} declarations + admits use of indexed syntax, using the special symbol \verb|\| (printed as ``\isa{{\isasymindex}}''). The latter concept is + particularly useful with locales (see also \S\ref{sec:locale}). + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Syntax and translations \label{sec:syn-trans}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{syntax}\isa{\isacommand{syntax}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{no-syntax}\isa{\isacommand{no{\isacharunderscore}syntax}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{translations}\isa{\isacommand{translations}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{no-translations}\isa{\isacommand{no{\isacharunderscore}translations}} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \railalias{rightleftharpoons}{\isasymrightleftharpoons} + \railterm{rightleftharpoons} + + \railalias{rightharpoonup}{\isasymrightharpoonup} + \railterm{rightharpoonup} + + \railalias{leftharpoondown}{\isasymleftharpoondown} + \railterm{leftharpoondown} + + \begin{rail} + ('syntax' | 'no\_syntax') mode? (constdecl +) + ; + ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) + ; + + mode: ('(' ( name | 'output' | name 'output' ) ')') + ; + transpat: ('(' nameref ')')? string + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{syntax}}~\isa{{\isacharparenleft}mode{\isacharparenright}\ decls}] is similar to + \isa{\isacommand{consts}}~\isa{decls}, except that the actual logical + signature extension is omitted. Thus the context free grammar of + Isabelle's inner syntax may be augmented in arbitrary ways, + independently of the logic. The \isa{mode} argument refers to the + print mode that the grammar rules belong; unless the \indexref{}{keyword}{output}\isa{\isakeyword{output}} indicator is given, all productions are added both to the + input and output grammar. + + \item [\isa{\isacommand{no{\isacharunderscore}syntax}}~\isa{{\isacharparenleft}mode{\isacharparenright}\ decls}] removes + grammar declarations (and translations) resulting from \isa{decls}, which are interpreted in the same manner as for \isa{\isacommand{syntax}} above. + + \item [\isa{\isacommand{translations}}~\isa{rules}] specifies syntactic + translation rules (i.e.\ macros): parse~/ print rules (\isa{{\isasymrightleftharpoons}}), + parse rules (\isa{{\isasymrightharpoonup}}), or print rules (\isa{{\isasymleftharpoondown}}). + Translation patterns may be prefixed by the syntactic category to be + used for parsing; the default is \isa{logic}. + + \item [\isa{\isacommand{no{\isacharunderscore}translations}}~\isa{rules}] removes syntactic + translation rules, which are interpreted in the same manner as for + \isa{\isacommand{translations}} above. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Axioms and theorems \label{sec:axms-thms}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcll} + \indexdef{}{command}{axioms}\isa{\isacommand{axioms}} & : & \isartrans{theory}{theory} & (axiomatic!) \\ + \indexdef{}{command}{lemmas}\isa{\isacommand{lemmas}} & : & \isarkeep{local{\dsh}theory} \\ + \indexdef{}{command}{theorems}\isa{\isacommand{theorems}} & : & isarkeep{local{\dsh}theory} \\ + \end{matharray} + + \begin{rail} + 'axioms' (axmdecl prop +) + ; + ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and') + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{axioms}}~\isa{a{\isacharcolon}\ {\isasymphi}}] introduces arbitrary + statements as axioms of the meta-logic. In fact, axioms are + ``axiomatic theorems'', and may be referred later just as any other + theorem. + + Axioms are usually only introduced when declaring new logical + systems. Everyday work is typically done the hard way, with proper + definitions and proven theorems. + + \item [\isa{\isacommand{lemmas}}~\isa{a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}] + retrieves and stores existing facts in the theory context, or the + specified target context (see also \secref{sec:target}). Typical + applications would also involve attributes, to declare Simplifier + rules, for example. + + \item [\isa{\isacommand{theorems}}] is essentially the same as \isa{\isacommand{lemmas}}, but marks the result as a different kind of facts. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Name spaces% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{global}\isa{\isacommand{global}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{local}\isa{\isacommand{local}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{hide}\isa{\isacommand{hide}} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'hide' ('(open)')? name (nameref + ) + ; + \end{rail} + + Isabelle organizes any kind of name declarations (of types, + constants, theorems etc.) by separate hierarchically structured name + spaces. Normally the user does not have to control the behavior of + name spaces by hand, yet the following commands provide some way to + do so. + + \begin{descr} + + \item [\isa{\isacommand{global}} and \isa{\isacommand{local}}] change the + current name declaration mode. Initially, theories start in + \isa{\isacommand{local}} mode, causing all names to be automatically + qualified by the theory name. Changing this to \isa{\isacommand{global}} + causes all names to be declared without the theory prefix, until + \isa{\isacommand{local}} is declared again. + + Note that global names are prone to get hidden accidently later, + when qualified names of the same base name are introduced. + + \item [\isa{\isacommand{hide}}~\isa{space\ names}] fully removes + declarations from a given name space (which may be \isa{class}, + \isa{type}, \isa{const}, or \isa{fact}); with the \isa{{\isacharparenleft}open{\isacharparenright}} option, only the base name is hidden. Global + (unqualified) names may never be hidden. + + Note that hiding name space accesses has no impact on logical + declarations -- they remain valid internally. Entities that are no + longer accessible to the user are printed with the special qualifier + ``\isa{{\isacharquery}{\isacharquery}}'' prefixed to the full internal name. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Incorporating ML code \label{sec:ML}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{use}\isa{\isacommand{use}} & : & \isarkeep{theory~|~local{\dsh}theory} \\ + \indexdef{}{command}{ML}\isa{\isacommand{ML}} & : & \isarkeep{theory~|~local{\dsh}theory} \\ + \indexdef{}{command}{ML-val}\isa{\isacommand{ML{\isacharunderscore}val}} & : & \isartrans{\cdot}{\cdot} \\ + \indexdef{}{command}{ML-command}\isa{\isacommand{ML{\isacharunderscore}command}} & : & \isartrans{\cdot}{\cdot} \\ + \indexdef{}{command}{setup}\isa{\isacommand{setup}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{method-setup}\isa{\isacommand{method{\isacharunderscore}setup}} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'use' name + ; + ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text + ; + 'method\_setup' name '=' text text + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{use}}~\isa{file}] reads and executes ML + commands from \isa{file}. The current theory context is passed + down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands. The file name is checked with + the \indexref{}{keyword}{uses}\isa{\isakeyword{uses}} dependency declaration given in the theory + header (see also \secref{sec:begin-thy}). + + \item [\isa{\isacommand{ML}}~\isa{text}] is similar to \isa{\isacommand{use}}, but executes ML commands directly from the given \isa{text}. + + \item [\isa{\isacommand{ML{\isacharunderscore}val}} and \isa{\isacommand{ML{\isacharunderscore}command}}] are + diagnostic versions of \isa{\isacommand{ML}}, which means that the context + may not be updated. \isa{\isacommand{ML{\isacharunderscore}val}} echos the bindings produced + at the ML toplevel, but \isa{\isacommand{ML{\isacharunderscore}command}} is silent. + + \item [\isa{\isacommand{setup}}~\isa{text}] changes the current theory + context by applying \isa{text}, which refers to an ML expression + of type \verb|theory -> theory|. This enables to initialize + any object-logic specific tools and packages written in ML, for + example. + + \item [\isa{\isacommand{method{\isacharunderscore}setup}}~\isa{name\ {\isacharequal}\ text\ description}] + defines a proof method in the current theory. The given \isa{text} has to be an ML expression of type \verb|Args.src ->|\isasep\isanewline% +\verb| Proof.context -> Proof.method|. Parsing concrete method syntax + from \verb|Args.src| input can be quite tedious in general. The + following simple examples are for methods without any explicit + arguments, or a list of theorems, respectively. + +%FIXME proper antiquotations +{\footnotesize +\begin{verbatim} + Method.no_args (Method.METHOD (fn facts => foobar_tac)) + Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) + Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) + Method.thms_ctxt_args (fn thms => fn ctxt => + Method.METHOD (fn facts => foobar_tac)) +\end{verbatim} +} + + Note that mere tactic emulations may ignore the \isa{facts} + parameter above. Proper proof methods would do something + appropriate with the list of current facts, though. Single-rule + methods usually do strict forward-chaining (e.g.\ by using \verb|Drule.multi_resolves|), while automatic ones just insert the facts + using \verb|Method.insert_tac| before applying the main tactic. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Syntax translation functions% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{parse-ast-translation}\isa{\isacommand{parse{\isacharunderscore}ast{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{parse-translation}\isa{\isacommand{parse{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{print-translation}\isa{\isacommand{print{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{typed-print-translation}\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{print-ast-translation}\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\ + \indexdef{}{command}{token-translation}\isa{\isacommand{token{\isacharunderscore}translation}} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | + 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text + ; + + 'token\_translation' text + ; + \end{rail} + + Syntax translation functions written in ML admit almost arbitrary + manipulations of Isabelle's inner syntax. Any of the above commands + have a single \railqtok{text} argument that refers to an ML + expression of appropriate type, which are as follows by default: + +%FIXME proper antiquotations +\begin{ttbox} +val parse_ast_translation : (string * (ast list -> ast)) list +val parse_translation : (string * (term list -> term)) list +val print_translation : (string * (term list -> term)) list +val typed_print_translation : + (string * (bool -> typ -> term list -> term)) list +val print_ast_translation : (string * (ast list -> ast)) list +val token_translation : + (string * string * (string -> string * real)) list +\end{ttbox} + + If the \isa{{\isacharparenleft}advanced{\isacharparenright}} option is given, the corresponding + translation functions may depend on the current theory or proof + context. This allows to implement advanced syntax mechanisms, as + translations functions may refer to specific theory declarations or + auxiliary proof data. + + See also \cite[\S8]{isabelle-ref} for more information on the + general concept of syntax transformations in Isabelle. + +%FIXME proper antiquotations +\begin{ttbox} +val parse_ast_translation: + (string * (Context.generic -> ast list -> ast)) list +val parse_translation: + (string * (Context.generic -> term list -> term)) list +val print_translation: + (string * (Context.generic -> term list -> term)) list +val typed_print_translation: + (string * (Context.generic -> bool -> typ -> term list -> term)) list +val print_ast_translation: + (string * (Context.generic -> ast list -> ast)) list +\end{ttbox}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Oracles% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{oracle}\isa{\isacommand{oracle}} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some type + \verb|T| given by the user. This acts like an infinitary + specification of axioms -- there is no internal check of the + correctness of the results! The inference kernel records oracle + invocations within the internal derivation object of theorems, and + the pretty printer attaches ``\isa{{\isacharbrackleft}{\isacharbang}{\isacharbrackright}}'' to indicate results + that are not fully checked by Isabelle inferences. + + \begin{rail} + 'oracle' name '(' type ')' '=' text + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{oracle}}~\isa{name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text}] turns the + given ML expression \isa{text} of type \verb|{theory|\isasep\isanewline% +\verb| ->|~\isa{type}~\verb|-> term| into an ML function + \verb|name| of type \verb|{theory ->|~\isa{type}~\verb|-> thm|. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Proof commands% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Proof commands perform transitions of Isar/VM machine + configurations, which are block-structured, consisting of a stack of + nodes with three main components: logical proof context, current + facts, and open goals. Isar/VM transitions are \emph{typed} + according to the following three different modes of operation: + + \begin{descr} + + \item [\isa{proof{\isacharparenleft}prove{\isacharparenright}}] means that a new goal has just been + stated that is now to be \emph{proven}; the next command may refine + it by some proof method, and enter a sub-proof to establish the + actual result. + + \item [\isa{proof{\isacharparenleft}state{\isacharparenright}}] is like a nested theory mode: the + context may be augmented by \emph{stating} additional assumptions, + intermediate results etc. + + \item [\isa{proof{\isacharparenleft}chain{\isacharparenright}}] is intermediate between \isa{proof{\isacharparenleft}state{\isacharparenright}} and \isa{proof{\isacharparenleft}prove{\isacharparenright}}: existing facts (i.e.\ + the contents of the special ``\indexref{}{fact}{this}\isa{this}'' register) have been + just picked up in order to be used when refining the goal claimed + next. + + \end{descr} + + 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 of a certain structure. + \Appref{ap:refcard} gives a simplified grammar of the overall + (extensible) language emerging that way.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Markup commands \label{sec:markup-prf}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{sect}\isa{\isacommand{sect}} & : & \isartrans{proof}{proof} \\ + \indexdef{}{command}{subsect}\isa{\isacommand{subsect}} & : & \isartrans{proof}{proof} \\ + \indexdef{}{command}{subsubsect}\isa{\isacommand{subsubsect}} & : & \isartrans{proof}{proof} \\ + \indexdef{}{command}{txt}\isa{\isacommand{txt}} & : & \isartrans{proof}{proof} \\ + \indexdef{}{command}{txt-raw}\isa{\isacommand{txt{\isacharunderscore}raw}} & : & \isartrans{proof}{proof} \\ + \end{matharray} + + These markup commands for proof mode closely correspond to the ones + of theory mode (see \S\ref{sec:markup-thy}). + + \begin{rail} + ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text + ; + \end{rail}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Context elements \label{sec:proof-context}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{fix}\isa{\isacommand{fix}} & : & \isartrans{proof(state)}{proof(state)} \\ + \indexdef{}{command}{assume}\isa{\isacommand{assume}} & : & \isartrans{proof(state)}{proof(state)} \\ + \indexdef{}{command}{presume}\isa{\isacommand{presume}} & : & \isartrans{proof(state)}{proof(state)} \\ + \indexdef{}{command}{def}\isa{\isacommand{def}} & : & \isartrans{proof(state)}{proof(state)} \\ + \end{matharray} + + The logical proof context consists of fixed variables and + assumptions. The former closely correspond to Skolem constants, or + meta-level universal quantification as provided by the Isabelle/Pure + logical framework. Introducing some \emph{arbitrary, but fixed} + variable via ``\isa{\isacommand{fix}}~\isa{x} results in a local value + that may be used in the subsequent proof as any other variable or + constant. Furthermore, any result \isa{{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} exported from + the context will be universally closed wrt.\ \isa{x} at the + outermost level: \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} (this is expressed in normal + form using Isabelle's meta-variables). + + Similarly, introducing some assumption \isa{{\isasymchi}} has two effects. + On the one hand, a local theorem is created that may be used as a + fact in subsequent proof steps. On the other hand, any result + \isa{{\isasymchi}\ {\isasymturnstile}\ {\isasymphi}} exported from the context becomes conditional wrt.\ + the assumption: \isa{{\isasymturnstile}\ {\isasymchi}\ {\isasymLongrightarrow}\ {\isasymphi}}. Thus, solving an enclosing goal + using such a result would basically introduce a new subgoal stemming + from the assumption. How this situation is handled depends on the + version of assumption command used: while \isa{\isacommand{assume}} + insists on solving the subgoal by unification with some premise of + the goal, \isa{\isacommand{presume}} leaves the subgoal unchanged in order + to be proved later by the user. + + Local definitions, introduced by ``\isa{\isacommand{def}}~\isa{x\ {\isasymequiv}\ t}'', are achieved by combining ``\isa{\isacommand{fix}}~\isa{x}'' with + another version of assumption that causes any hypothetical equation + \isa{x\ {\isasymequiv}\ t} to be eliminated by the reflexivity rule. Thus, + exporting some result \isa{x\ {\isasymequiv}\ t\ {\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} yields \isa{{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}t{\isacharbrackright}}. + + \railalias{equiv}{\isasymequiv} + \railterm{equiv} + + \begin{rail} + 'fix' (vars + 'and') + ; + ('assume' | 'presume') (props + 'and') + ; + 'def' (def + 'and') + ; + def: thmdecl? \\ name ('==' | equiv) term termpat? + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{fix}}~\isa{x}] introduces a local variable + \isa{x} that is \emph{arbitrary, but fixed.} + + \item [\isa{\isacommand{assume}}~\isa{a{\isacharcolon}\ {\isasymphi}} and \isa{\isacommand{presume}}~\isa{a{\isacharcolon}\ {\isasymphi}}] introduce a local fact \isa{{\isasymphi}\ {\isasymturnstile}\ {\isasymphi}} by + assumption. Subsequent results applied to an enclosing goal (e.g.\ + by \indexref{}{command}{show}\isa{\isacommand{show}}) are handled as follows: \isa{\isacommand{assume}} expects to be able to unify with existing premises in the + goal, while \isa{\isacommand{presume}} leaves \isa{{\isasymphi}} as new subgoals. + + Several lists of assumptions may be given (separated by + \indexref{}{keyword}{and}\isa{\isakeyword{and}}; the resulting list of current facts consists + of all of these concatenated. + + \item [\isa{\isacommand{def}}~\isa{x\ {\isasymequiv}\ t}] introduces a local + (non-polymorphic) definition. In results exported from the context, + \isa{x} is replaced by \isa{t}. Basically, ``\isa{\isacommand{def}}~\isa{x\ {\isasymequiv}\ t}'' abbreviates ``\isa{\isacommand{fix}}~\isa{x}~\isa{\isacommand{assume}}~\isa{x\ {\isasymequiv}\ t}'', with the resulting + hypothetical equation solved by reflexivity. + + The default name for the definitional equation is \isa{x{\isacharunderscore}def}. + Several simultaneous definitions may be given at the same time. + + \end{descr} + + The special name \indexref{}{fact}{prems}\isa{prems} refers to all assumptions of the + current context as a list of theorems. This feature should be used + with great care! It is better avoided in final proof texts.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Facts and forward chaining% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{note}\isa{\isacommand{note}} & : & \isartrans{proof(state)}{proof(state)} \\ + \indexdef{}{command}{then}\isa{\isacommand{then}} & : & \isartrans{proof(state)}{proof(chain)} \\ + \indexdef{}{command}{from}\isa{\isacommand{from}} & : & \isartrans{proof(state)}{proof(chain)} \\ + \indexdef{}{command}{with}\isa{\isacommand{with}} & : & \isartrans{proof(state)}{proof(chain)} \\ + \indexdef{}{command}{using}\isa{\isacommand{using}} & : & \isartrans{proof(prove)}{proof(prove)} \\ + \indexdef{}{command}{unfolding}\isa{\isacommand{unfolding}} & : & \isartrans{proof(prove)}{proof(prove)} \\ + \end{matharray} + + New facts are established either by assumption or proof of local + statements. Any fact will usually be involved in further proofs, + either as explicit arguments of proof methods, or when forward + chaining towards the next goal via \isa{\isacommand{then}} (and variants); + \isa{\isacommand{from}} and \isa{\isacommand{with}} are composite forms + involving \isa{\isacommand{note}}. The \isa{\isacommand{using}} elements + augments the collection of used facts \emph{after} a goal has been + stated. Note that the special theorem name \indexref{}{fact}{this}\isa{this} refers + to the most recently established facts, but only \emph{before} + issuing a follow-up claim. + + \begin{rail} + 'note' (thmdef? thmrefs + 'and') + ; + ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and') + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{note}}~\isa{a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}] + recalls existing facts \isa{b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub n}, binding + the result as \isa{a}. Note that attributes may be involved as + well, both on the left and right hand sides. + + \item [\isa{\isacommand{then}}] indicates forward chaining by the current + facts in order to establish the goal to be claimed next. The + initial proof method invoked to refine that will be offered the + facts to do ``anything appropriate'' (see also + \secref{sec:proof-steps}). For example, method \indexref{}{method}{rule}\isa{rule} + (see \secref{sec:pure-meth-att}) would typically do an elimination + rather than an introduction. Automatic methods usually insert the + facts into the goal state before operation. This provides a simple + scheme to control relevance of facts in automated proof search. + + \item [\isa{\isacommand{from}}~\isa{b}] abbreviates ``\isa{\isacommand{note}}~\isa{b}~\isa{\isacommand{then}}''; thus \isa{\isacommand{then}} is + equivalent to ``\isa{\isacommand{from}}~\isa{this}''. + + \item [\isa{\isacommand{with}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}] + abbreviates ``\isa{\isacommand{from}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n\ {\isasymAND}\ this}''; thus the forward chaining is from earlier facts together + with the current ones. + + \item [\isa{\isacommand{using}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}] augments + the facts being currently indicated for use by a subsequent + refinement step (such as \indexref{}{command}{apply}\isa{\isacommand{apply}} or \indexref{}{command}{proof}\isa{\isacommand{proof}}). + + \item [\isa{\isacommand{unfolding}}~\isa{b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n}] is + structurally similar to \isa{\isacommand{using}}, but unfolds definitional + equations \isa{b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ b\isactrlsub n} throughout the goal state + and facts. + + \end{descr} + + Forward chaining with an empty list of theorems is the same as not + chaining at all. Thus ``\isa{\isacommand{from}}~\isa{nothing}'' has no + effect apart from entering \isa{prove{\isacharparenleft}chain{\isacharparenright}} mode, since + \indexref{}{fact}{nothing}\isa{nothing} is bound to the empty list of theorems. + + Basic proof methods (such as \indexref{}{method}{rule}\isa{rule}) expect multiple + facts to be given in their proper order, corresponding to a prefix + of the premises of the rule involved. Note that positions may be + easily skipped using something like \isa{\isacommand{from}}~\isa{{\isacharunderscore}\ {\isasymAND}\ a\ {\isasymAND}\ b}, for example. This involves the trivial rule + \isa{PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}}, which is bound in Isabelle/Pure as + ``\indexref{}{fact}{-}\isa{{\isacharunderscore}}'' (underscore). + + Automated methods (such as \isa{simp} or \isa{auto}) just + insert any given facts before their usual operation. Depending on + the kind of procedure involved, the order of facts is less + significant here.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Goal statements \label{sec:goals}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \isarcmd{lemma} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ + \isarcmd{theorem} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ + \isarcmd{corollary} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ + \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ + \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ + \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ + \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ + \isarcmd{print_statement}^* & : & \isarkeep{theory~|~proof} \\ + \end{matharray} + + From a theory context, proof mode is entered by an initial goal + command such as \isa{\isacommand{lemma}}, \isa{\isacommand{theorem}}, or + \isa{\isacommand{corollary}}. 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 \indexref{}{command}{then}\isa{\isacommand{then}}), and whether the final 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 conjunction (printed as \isa{{\isacharampersand}{\isacharampersand}}), which is usually + split into the corresponding number of sub-goals prior to an initial + method application, via \indexref{}{command}{proof}\isa{\isacommand{proof}} + (\secref{sec:proof-steps}) or \indexref{}{command}{apply}\isa{\isacommand{apply}} + (\secref{sec:tactic-commands}). The \indexref{}{method}{induct}\isa{induct} method + covered in \secref{sec:cases-induct} acts on multiple claims + simultaneously. + + Claims at the theory level may be either in short or long form. A + short goal merely consists of several simultaneous propositions + (often just one). A long goal includes an explicit context + specification for the subsequent conclusion, involving local + parameters and assumptions. Here the role of each part of the + statement is explicitly marked by separate keywords (see also + \secref{sec:locale}); the local assumptions being introduced here + are available as \indexref{}{fact}{assms}\isa{assms} in the proof. Moreover, there + are two kinds of conclusions: \indexdef{}{element}{shows}\isa{shows} states several + simultaneous propositions (essentially a big conjunction), while + \indexdef{}{element}{obtains}\isa{obtains} claims several simultaneous simultaneous + contexts of (essentially a big disjunction of eliminated parameters + and assumptions, cf.\ \secref{sec:obtain}). + + \begin{rail} + ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal) + ; + ('have' | 'show' | 'hence' | 'thus') goal + ; + 'print\_statement' modes? thmrefs + ; + + goal: (props + 'and') + ; + longgoal: thmdecl? (contextelem *) conclusion + ; + conclusion: 'shows' goal | 'obtains' (parname? case + '|') + ; + case: (vars + 'and') 'where' (props + 'and') + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{lemma}}~\isa{a{\isacharcolon}\ {\isasymphi}}] enters proof mode with + \isa{{\isasymphi}} as main goal, eventually resulting in some fact \isa{{\isasymturnstile}\ {\isasymphi}} to be put back into the target context. An additional + \railnonterm{context} specification may build up an initial proof + context for the subsequent claim; this includes local definitions + and syntax as well, see the definition of \isa{contextelem} in + \secref{sec:locale}. + + \item [\isa{\isacommand{theorem}}~\isa{a{\isacharcolon}\ {\isasymphi}} and \isa{\isacommand{corollary}}~\isa{a{\isacharcolon}\ {\isasymphi}}] are essentially the same as \isa{\isacommand{lemma}}~\isa{a{\isacharcolon}\ {\isasymphi}}, but the facts are internally marked as + being of a different kind. This discrimination acts like a formal + comment. + + \item [\isa{\isacommand{have}}~\isa{a{\isacharcolon}\ {\isasymphi}}] claims a local goal, + eventually resulting in a fact within the current logical context. + This operation is completely independent of any pending sub-goals of + an enclosing goal statements, so \isa{\isacommand{have}} may be freely + used for experimental exploration of potential results within a + proof body. + + \item [\isa{\isacommand{show}}~\isa{a{\isacharcolon}\ {\isasymphi}}] is like \isa{\isacommand{have}}~\isa{a{\isacharcolon}\ {\isasymphi}} plus a second stage to refine some pending + sub-goal for each one of the finished result, after having been + exported into the corresponding context (at the head of the + sub-proof of this \isa{\isacommand{show}} command). + + To accommodate interactive debugging, resulting rules are printed + before being applied internally. Even more, interactive execution + of \isa{\isacommand{show}} predicts potential failure and displays the + resulting error as a warning beforehand. Watch out for the + following message: + + %FIXME proper antiquitation + \begin{ttbox} + Problem! Local statement will fail to solve any pending goal + \end{ttbox} + + \item [\isa{\isacommand{hence}}] abbreviates ``\isa{\isacommand{then}}~\isa{\isacommand{have}}'', i.e.\ claims a local goal to be proven by forward + chaining the current facts. Note that \isa{\isacommand{hence}} is also + equivalent to ``\isa{\isacommand{from}}~\isa{this}~\isa{\isacommand{have}}''. + + \item [\isa{\isacommand{thus}}] abbreviates ``\isa{\isacommand{then}}~\isa{\isacommand{show}}''. Note that \isa{\isacommand{thus}} is also equivalent to + ``\isa{\isacommand{from}}~\isa{this}~\isa{\isacommand{show}}''. + + \item [\isa{\isacommand{print{\isacharunderscore}statement}}~\isa{a}] prints facts from the + current theory or proof context in long statement form, according to + the syntax for \isa{\isacommand{lemma}} given above. + + \end{descr} + + Any goal statement causes some term abbreviations (such as + \indexref{}{variable}{?thesis}\isa{{\isacharquery}thesis}) to be bound automatically, see also + \secref{sec:term-abbrev}. Furthermore, the local context of a + (non-atomic) goal is provided via the \indexref{}{case}{rule-context}\isa{rule{\isacharunderscore}context} case. + + The optional case names of \indexref{}{element}{obtains}\isa{obtains} have a twofold + meaning: (1) during the of this claim they refer to the the local + context introductions, (2) the resulting rule is annotated + accordingly to support symbolic case splits when used with the + \indexref{}{method}{cases}\isa{cases} method (cf. \secref{sec:cases-induct}). + + \medskip + + \begin{warn} + Isabelle/Isar suffers theory-level goal statements to contain + \emph{unbound schematic variables}, although this does not conform + to the aim of human-readable proof documents! The main problem + with schematic goals is that the actual outcome is usually hard to + predict, depending on the behavior of the proof methods applied + during the course of reasoning. Note that most semi-automated + methods heavily depend on several kinds of implicit rule + declarations within the current theory context. As this would + also result in non-compositional checking of sub-proofs, + \emph{local goals} are not allowed to be schematic at all. + Nevertheless, schematic goals do have their use in Prolog-style + interactive synthesis of proven results, usually by stepwise + refinement via emulation of traditional Isabelle tactic scripts + (see also \secref{sec:tactic-commands}). In any case, users + should know what they are doing. + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Initial and terminal proof steps \label{sec:proof-steps}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{proof}\isa{\isacommand{proof}} & : & \isartrans{proof(prove)}{proof(state)} \\ + \indexdef{}{command}{qed}\isa{\isacommand{qed}} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\ + \indexdef{}{command}{by}\isa{\isacommand{by}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ + \indexdef{}{command}{..}\isa{\isacommand{{\isachardot}{\isachardot}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ + \indexdef{}{command}{.}\isa{\isacommand{{\isachardot}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ + \indexdef{}{command}{sorry}\isa{\isacommand{sorry}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ + \end{matharray} + + Arbitrary goal refinement via tactics is considered harmful. + Structured proof composition in Isar admits proof methods to be + invoked in two places only. + + \begin{enumerate} + + \item An \emph{initial} refinement step \indexref{}{command}{proof}\isa{\isacommand{proof}}~\isa{m\isactrlsub {\isadigit{1}}} reduces a newly stated goal to a number + of sub-goals that are to be solved later. Facts are passed to + \isa{m\isactrlsub {\isadigit{1}}} for forward chaining, if so indicated by \isa{proof{\isacharparenleft}chain{\isacharparenright}} mode. + + \item A \emph{terminal} conclusion step \indexref{}{command}{qed}\isa{\isacommand{qed}}~\isa{m\isactrlsub {\isadigit{2}}} is intended to solve remaining goals. No facts are + passed to \isa{m\isactrlsub {\isadigit{2}}}. + + \end{enumerate} + + The only other (proper) way to affect pending goals in a proof body + is by \indexref{}{command}{show}\isa{\isacommand{show}}, 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 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 + an intelligible manner. + + Unless given explicitly by the user, the default initial method is + ``\indexref{}{method}{rule}\isa{rule}'', which applies a single standard elimination + or introduction rule according to the topmost symbol involved. + There is no separate default terminal method. Any remaining goals + are always solved by assumption in the very last step. + + \begin{rail} + 'proof' method? + ; + 'qed' method? + ; + 'by' method method? + ; + ('.' | '..' | 'sorry') + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{proof}}~\isa{m\isactrlsub {\isadigit{1}}}] refines the goal by + proof method \isa{m\isactrlsub {\isadigit{1}}}; facts for forward chaining are + passed if so indicated by \isa{proof{\isacharparenleft}chain{\isacharparenright}} mode. + + \item [\isa{\isacommand{qed}}~\isa{m\isactrlsub {\isadigit{2}}}] refines any remaining + goals by proof method \isa{m\isactrlsub {\isadigit{2}}} and concludes the + sub-proof by assumption. If the goal had been \isa{show} (or + \isa{thus}), some pending sub-goal is solved as well by the rule + resulting from the result \emph{exported} into the enclosing goal + context. Thus \isa{qed} may fail for two reasons: either \isa{m\isactrlsub {\isadigit{2}}} fails, or the resulting rule does not fit to any + pending goal\footnote{This includes any additional ``strong'' + assumptions as introduced by \isa{assume}.} of the enclosing + context. Debugging such a situation might involve temporarily + changing \isa{\isacommand{show}} into \isa{\isacommand{have}}, or weakening the + local context by replacing occurrences of \isa{\isacommand{assume}} by + \isa{\isacommand{presume}}. + + \item [\isa{\isacommand{by}}~\isa{m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}}] is a + \emph{terminal proof}\index{proof!terminal}; it abbreviates + \isa{\isacommand{proof}}~\isa{m\isactrlsub {\isadigit{1}}}~\isa{qed}~\isa{m\isactrlsub {\isadigit{2}}}, but with backtracking across both methods. Debugging + an unsuccessful \isa{\isacommand{by}}~\isa{m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}} + command can be done by expanding its definition; in many cases + \isa{\isacommand{proof}}~\isa{m\isactrlsub {\isadigit{1}}} (or even \isa{apply}~\isa{m\isactrlsub {\isadigit{1}}}) is already sufficient to see the + problem. + + \item [``\isa{\isacommand{{\isachardot}{\isachardot}}}''] is a \emph{default + proof}\index{proof!default}; it abbreviates \isa{\isacommand{by}}~\isa{rule}. + + \item [``\isa{\isacommand{{\isachardot}}}''] is a \emph{trivial + proof}\index{proof!trivial}; it abbreviates \isa{\isacommand{by}}~\isa{this}. + + \item [\isa{\isacommand{sorry}}] is a \emph{fake proof}\index{proof!fake} + pretending to solve the pending claim without further ado. This + only works in interactive development, or if the \verb|quick_and_dirty| flag is enabled (in ML). Facts emerging from fake + proofs are not the real thing. Internally, each theorem container + is tainted by an oracle invocation, which is indicated as ``\isa{{\isacharbrackleft}{\isacharbang}{\isacharbrackright}}'' in the printed result. + + The most important application of \isa{\isacommand{sorry}} is to support + experimentation and top-down proof development. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Fundamental methods and attributes \label{sec:pure-meth-att}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +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 + \chref{ch:gen-tools} and \chref{ch:logics}). + + \begin{matharray}{rcl} + \indexdef{}{method}{-}\isa{{\isacharminus}} & : & \isarmeth \\ + \indexdef{}{method}{fact}\isa{fact} & : & \isarmeth \\ + \indexdef{}{method}{assumption}\isa{assumption} & : & \isarmeth \\ + \indexdef{}{method}{this}\isa{this} & : & \isarmeth \\ + \indexdef{}{method}{rule}\isa{rule} & : & \isarmeth \\ + \indexdef{}{method}{iprover}\isa{iprover} & : & \isarmeth \\[0.5ex] + \indexdef{}{attribute}{intro}\isa{intro} & : & \isaratt \\ + \indexdef{}{attribute}{elim}\isa{elim} & : & \isaratt \\ + \indexdef{}{attribute}{dest}\isa{dest} & : & \isaratt \\ + \indexdef{}{attribute}{rule}\isa{rule} & : & \isaratt \\[0.5ex] + \indexdef{}{attribute}{OF}\isa{OF} & : & \isaratt \\ + \indexdef{}{attribute}{of}\isa{of} & : & \isaratt \\ + \indexdef{}{attribute}{where}\isa{where} & : & \isaratt \\ + \end{matharray} + + \begin{rail} + 'fact' thmrefs? + ; + 'rule' thmrefs? + ; + 'iprover' ('!' ?) (rulemod *) + ; + rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs + ; + ('intro' | 'elim' | 'dest') ('!' | () | '?') nat? + ; + 'rule' 'del' + ; + 'OF' thmrefs + ; + 'of' insts ('concl' ':' insts)? + ; + 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and') + ; + \end{rail} + + \begin{descr} + + \item [``\isa{{\isacharminus}}''] does nothing but insert the forward + chaining facts as premises into the goal. Note that command + \indexref{}{command}{proof}\isa{\isacommand{proof}} without any method actually performs a single + reduction step using the \indexref{}{method}{rule}\isa{rule} method; thus a plain + \emph{do-nothing} proof step would be ``\isa{\isacommand{proof}}~\isa{{\isacharminus}}'' rather than \isa{\isacommand{proof}} alone. + + \item [\isa{fact}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] composes + some fact from \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n} (or implicitly from + the current proof context) modulo unification of schematic type and + term variables. The rule structure is not taken into account, i.e.\ + meta-level implication is considered atomic. This is the same + principle underlying literal facts (cf.\ \secref{sec:syn-att}): + ``\isa{\isacommand{have}}~\isa{{\isasymphi}}~\isa{\isacommand{by}}~\isa{fact}'' is + equivalent to ``\isa{\isacommand{note}}~\verb|`|\isa{{\isasymphi}}\verb|`|'' provided that \isa{{\isasymturnstile}\ {\isasymphi}} is an instance of some known + \isa{{\isasymturnstile}\ {\isasymphi}} in the proof context. + + \item [\isa{assumption}] solves some goal by a single assumption + step. All given facts are guaranteed to participate in the + refinement; this means there may be only 0 or 1 in the first place. + Recall that \isa{\isacommand{qed}} (\secref{sec:proof-steps}) already + concludes any remaining sub-goals by assumption, so structured + proofs usually need not quote the \isa{assumption} method at + all. + + \item [\isa{this}] applies all of the current facts directly as + rules. Recall that ``\isa{\isacommand{{\isachardot}}}'' (dot) abbreviates ``\isa{\isacommand{by}}~\isa{this}''. + + \item [\isa{rule}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] applies some + rule given as argument in backward manner; facts are used to reduce + the rule before applying it to the goal. Thus \isa{rule} + without facts is plain introduction, while with facts it becomes + elimination. + + When no arguments are given, the \isa{rule} method tries to pick + appropriate rules automatically, as declared in the current context + using the \isa{intro}, \isa{elim}, \isa{dest} + attributes (see below). This is the default behavior of \isa{\isacommand{proof}} and ``\isa{\isacommand{{\isachardot}{\isachardot}}}'' (double-dot) steps (see + \secref{sec:proof-steps}). + + \item [\isa{iprover}] performs intuitionistic proof search, + depending on specifically declared rules from the context, or given + as explicit arguments. Chained facts are inserted into the goal + before commencing proof search; ``\isa{iprover}\isa{{\isacharbang}}'' + means to include the current \isa{prems} as well. + + Rules need to be classified as \isa{intro}, \isa{elim}, or \isa{dest}; here the ``\isa{{\isacharbang}} indicator refers + to ``safe'' rules, which may be applied aggressively (without + considering back-tracking later). Rules declared with ``\isa{{\isacharquery}}'' are ignored in proof search (the single-step \isa{rule} + method still observes these). An explicit weight annotation may be + given as well; otherwise the number of rule premises will be taken + into account here. + + \item [\isa{intro}, \isa{elim}, and \isa{dest}] + declare introduction, elimination, and destruct rules, to be used + with the \isa{rule} and \isa{iprover} methods. Note that + the latter will ignore rules declared with ``\isa{{\isacharquery}}'', while + ``\isa{{\isacharbang}}'' are used most aggressively. + + The classical reasoner (see \secref{sec:classical}) introduces its + own variants of these attributes; use qualified names to access the + present versions of Isabelle/Pure, i.e.\ \isa{Pure{\isachardot}intro}. + + \item [\isa{rule}~\isa{del}] undeclares introduction, + elimination, or destruct rules. + + \item [\isa{OF}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] applies some + theorem to all of the given rules \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n} + (in parallel). This corresponds to the \verb|op MRS| operation in + ML, but note the reversed order. Positions may be effectively + skipped by including ``\verb|_|'' (underscore) as argument. + + \item [\isa{of}~\isa{t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n}] performs + positional instantiation of term variables. The terms \isa{t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n} are substituted for any schematic + variables occurring in a theorem from left to right; ``\verb|_|'' (underscore) indicates to skip a position. Arguments following + a ``\isa{\isakeyword{concl}}\isa{{\isacharcolon}}'' specification refer to positions + of the conclusion of a rule. + + \item [\isa{where}~\isa{x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymAND}\ x\isactrlsub n\ {\isacharequal}\ t\isactrlsub n}] performs named instantiation of + schematic type and term variables occurring in a theorem. Schematic + variables have to be specified on the left-hand side (e.g.\ \isa{{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{3}}}). The question mark may be omitted if the variable name is + a plain identifier without index. As type instantiations are + inferred from term instantiations, explicit type instantiations are + seldom necessary. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Term abbreviations \label{sec:term-abbrev}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{let}\isa{\isacommand{let}} & : & \isartrans{proof(state)}{proof(state)} \\ + \indexdef{}{keyword}{is}\isa{\isakeyword{is}} & : & syntax \\ + \end{matharray} + + Abbreviations may be either bound by explicit \isa{\isacommand{let}}\isa{p\ {\isasymequiv}\ t} statements, or by annotating assumptions or goal statements + with a list of patterns ``\isa{{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n}''. + In both cases, higher-order matching is invoked to bind + extra-logical term variables, which may be either named schematic + variables of the form \isa{{\isacharquery}x}, or nameless dummies ``\isa{{\isacharunderscore}}'' (underscore). Note that in the \isa{\isacommand{let}} form the + patterns occur on the left-hand side, while the \isa{\isakeyword{is}} + patterns are in postfix position. + + 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 \isa{\isacommand{let}} may occur in \emph{arbitrary} + instances later. Even though actual polymorphism should be rarely + used in practice, this mechanism is essential to achieve proper + incremental type-inference, as the user proceeds to build up the + Isar proof text from left to right. + + \medskip Term abbreviations are quite different from local + definitions as introduced via \isa{\isacommand{def}} (see + \secref{sec:proof-context}). The latter are visible within the + logic as actual equations, while abbreviations disappear during the + input process just after type checking. Also note that \isa{\isacommand{def}} does not support polymorphism. + + \begin{rail} + 'let' ((term + 'and') '=' term + 'and') + ; + \end{rail} + + The syntax of \isa{\isakeyword{is}} patterns follows \railnonterm{termpat} + or \railnonterm{proppat} (see \secref{sec:term-decls}). + + \begin{descr} + + \item [\isa{\isacommand{let}}~\isa{p\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}p\isactrlsub n\ {\isacharequal}\ t\isactrlsub n}] binds any text variables in patterns + \isa{p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n} by simultaneous higher-order + matching against terms \isa{t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n}. + + \item [\isa{{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}}] resembles \isa{\isacommand{let}}, but matches \isa{p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n} against the + preceding statement. Also note that \isa{\isakeyword{is}} is not a + separate command, but part of others (such as \isa{\isacommand{assume}}, + \isa{\isacommand{have}} etc.). + + \end{descr} + + Some \emph{implicit} term abbreviations\index{term abbreviations} + for goals and facts are available as well. For any open goal, + \indexref{}{variable}{thesis}\isa{thesis} refers to its object-level statement, + abstracted over any meta-level parameters (if present). Likewise, + \indexref{}{variable}{this}\isa{this} is bound for fact statements resulting from + assumptions or finished goals. In case \isa{this} refers to + an object-logic statement that is an application \isa{f\ t}, then + \isa{t} is bound to the special text variable ``\isa{{\isasymdots}}'' + (three dots). The canonical application of this convenience are + calculational proofs (see \secref{sec:calculation}).% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Block structure% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{next}\isa{\isacommand{next}} & : & \isartrans{proof(state)}{proof(state)} \\ + \indexdef{}{command}{\{}\isa{\isacommand{{\isacharbraceleft}}} & : & \isartrans{proof(state)}{proof(state)} \\ + \indexdef{}{command}{\}}\isa{\isacommand{{\isacharbraceright}}} & : & \isartrans{proof(state)}{proof(state)} \\ + \end{matharray} + + While Isar is inherently block-structured, opening and closing + blocks is mostly handled rather casually, with little explicit + user-intervention. Any local goal statement automatically opens + \emph{two} internal blocks, which are closed again when concluding + the sub-proof (by \isa{\isacommand{qed}} etc.). Sections of different + context within a sub-proof may be switched via \isa{\isacommand{next}}, + which is just a single block-close followed by block-open again. + The effect of \isa{\isacommand{next}} is to reset the local proof context; + there is no goal focus involved here! + + For slightly more advanced applications, there are explicit block + parentheses as well. These typically achieve a stronger forward + style of reasoning. + + \begin{descr} + + \item [\isa{\isacommand{next}}] switches to a fresh block within a + sub-proof, resetting the local context to the initial one. + + \item [\isa{\isacommand{{\isacharbraceleft}}} and \isa{\isacommand{{\isacharbraceright}}}] explicitly open and close + blocks. Any current facts pass through ``\isa{\isacommand{{\isacharbraceleft}}}'' + unchanged, while ``\isa{\isacommand{{\isacharbraceright}}}'' causes any result to be + \emph{exported} into the enclosing context. Thus fixed variables + are generalized, assumptions discharged, and local definitions + unfolded (cf.\ \secref{sec:proof-context}). There is no difference + of \isa{\isacommand{assume}} and \isa{\isacommand{presume}} in this mode of + forward reasoning --- in contrast to plain backward reasoning with + the result exported at \isa{\isacommand{show}} time. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Emulating tactic scripts \label{sec:tactic-commands}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The Isar provides separate commands to accommodate tactic-style + proof scripts within the same system. While being outside the + orthodox Isar proof language, these might come in handy for + interactive exploration and debugging, or even actual tactical proof + within new-style theories (to benefit from document preparation, for + example). See also \secref{sec:tactics} for actual tactics, that + have been encapsulated as proof methods. Proper proof methods may + be used in scripts, too. + + \begin{matharray}{rcl} + \indexdef{}{command}{apply}\isa{\isacommand{apply}}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ + \indexdef{}{command}{apply-end}\isa{\isacommand{apply{\isacharunderscore}end}}^* & : & \isartrans{proof(state)}{proof(state)} \\ + \indexdef{}{command}{done}\isa{\isacommand{done}}^* & : & \isartrans{proof(prove)}{proof(state)} \\ + \indexdef{}{command}{defer}\isa{\isacommand{defer}}^* & : & \isartrans{proof}{proof} \\ + \indexdef{}{command}{prefer}\isa{\isacommand{prefer}}^* & : & \isartrans{proof}{proof} \\ + \indexdef{}{command}{back}\isa{\isacommand{back}}^* & : & \isartrans{proof}{proof} \\ + \end{matharray} + + \begin{rail} + ( 'apply' | 'apply\_end' ) method + ; + 'defer' nat? + ; + 'prefer' nat + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{apply}}~\isa{m}] applies proof method \isa{m} + in initial position, but unlike \isa{\isacommand{proof}} it retains + ``\isa{proof{\isacharparenleft}prove{\isacharparenright}}'' mode. Thus consecutive method + applications may be given just as in tactic scripts. + + Facts are passed to \isa{m} as indicated by the goal's + forward-chain mode, and are \emph{consumed} afterwards. Thus any + further \isa{\isacommand{apply}} command would always work in a purely + backward manner. + + \item [\isa{\isacommand{apply{\isacharunderscore}end}}~\isa{m}] applies proof method + \isa{m} as if in terminal position. Basically, this simulates a + multi-step tactic script for \isa{\isacommand{qed}}, but may be given + anywhere within the proof body. + + No facts are passed to \isa{m} here. Furthermore, the static + context is that of the enclosing goal (as for actual \isa{\isacommand{qed}}). Thus the proof method may not refer to any assumptions + introduced in the current body, for example. + + \item [\isa{\isacommand{done}}] completes a proof script, provided that + the current goal state is solved completely. Note that actual + structured proof commands (e.g.\ ``\isa{\isacommand{{\isachardot}}}'' or \isa{\isacommand{sorry}}) may be used to conclude proof scripts as well. + + \item [\isa{\isacommand{defer}}~\isa{n} and \isa{\isacommand{prefer}}~\isa{n}] shuffle the list of pending goals: \isa{\isacommand{defer}} puts off + sub-goal \isa{n} to the end of the list (\isa{n\ {\isacharequal}\ {\isadigit{1}}} by + default), while \isa{\isacommand{prefer}} brings sub-goal \isa{n} to the + front. + + \item [\isa{\isacommand{back}}] does back-tracking over the result + sequence of the latest proof command. Basically, any proof command + may return multiple results. + + \end{descr} + + Any proper Isar proof method may be used with tactic script commands + such as \isa{\isacommand{apply}}. A few additional emulations of actual + tactics are provided as well; these would be never used in actual + structured proofs, of course.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Meta-linguistic features% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{oops}\isa{\isacommand{oops}} & : & \isartrans{proof}{theory} \\ + \end{matharray} + + The \isa{\isacommand{oops}} command discontinues the current proof + attempt, while considering the partial proof text as properly + processed. This is conceptually quite different from ``faking'' + actual proofs via \indexref{}{command}{sorry}\isa{\isacommand{sorry}} (see + \secref{sec:proof-steps}): \isa{\isacommand{oops}} does not observe the + proof structure at all, but goes back right to the theory level. + Furthermore, \isa{\isacommand{oops}} does not produce any result theorem + --- there is no intended claim to be able to complete the proof + anyhow. + + A typical application of \isa{\isacommand{oops}} is to explain Isar proofs + \emph{within} the system itself, in conjunction with the document + preparation tools of Isabelle described in \cite{isabelle-sys}. + Thus partial or even wrong proof attempts can be discussed in a + logically sound manner. Note that the Isabelle {\LaTeX} macros can + be easily adapted to print something like ``\isa{{\isasymdots}}'' instead of + the keyword ``\isa{\isacommand{oops}}''. + + \medskip The \isa{\isacommand{oops}} command is undo-able, unlike + \indexref{}{command}{kill}\isa{\isacommand{kill}} (see \secref{sec:history}). The effect is to + get back to the theory just before the opening of the proof.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Other commands% +} +\isamarkuptrue% +% +\isamarkupsubsection{Diagnostics% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \isarcmd{pr}^* & : & \isarkeep{\cdot} \\ + \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{prf}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{full_prf}^* & : & \isarkeep{theory~|~proof} \\ + \end{matharray} + + These diagnostic commands assist interactive development. Note that + \isa{\isacommand{undo}} does not apply here, the theory or proof + configuration is not changed. + + \begin{rail} + 'pr' modes? nat? (',' nat)? + ; + 'thm' modes? thmrefs + ; + 'term' modes? term + ; + 'prop' modes? prop + ; + 'typ' modes? type + ; + 'prf' modes? thmrefs? + ; + 'full\_prf' modes? thmrefs? + ; + + modes: '(' (name + ) ')' + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{pr}}~\isa{goals{\isacharcomma}\ prems}] prints the current + proof state (if present), including the proof context, current facts + and goals. The optional limit arguments affect the number of goals + and premises to be displayed, which is initially 10 for both. + Omitting limit values leaves the current setting unchanged. + + \item [\isa{\isacommand{thm}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] retrieves + theorems from the current theory or proof context. Note that any + attributes included in the theorem specifications are applied to a + temporary context derived from the current theory or proof; the + result is discarded, i.e.\ attributes involved in \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n} do not have any permanent effect. + + \item [\isa{\isacommand{term}}~\isa{t} and \isa{\isacommand{prop}}~\isa{{\isasymphi}}] + read, type-check and print terms or propositions according to the + current theory or proof context; the inferred type of \isa{t} is + output as well. Note that these commands are also useful in + inspecting the current environment of term abbreviations. + + \item [\isa{\isacommand{typ}}~\isa{{\isasymtau}}] reads and prints types of the + meta-logic according to the current theory or proof context. + + \item [\isa{\isacommand{prf}}] displays the (compact) proof term of the + current proof state (if present), or of the given theorems. Note + that this requires proof terms to be switched on for the current + object logic (see the ``Proof terms'' section of the Isabelle + reference manual for information on how to do this). + + \item [\isa{\isacommand{full{\isacharunderscore}prf}}] is like \isa{\isacommand{prf}}, but displays + the full proof term, i.e.\ also displays information omitted in the + compact proof term, which is denoted by ``\verb|_|'' + placeholders there. + + \end{descr} + + All of the diagnostic commands above admit a list of \isa{modes} + to be specified, which is appended to the current print mode (see + also \cite{isabelle-ref}). Thus the output behavior may be modified + according particular print mode features. For example, \isa{\isacommand{pr}}~\isa{{\isacharparenleft}latex\ xsymbols\ symbols{\isacharparenright}} would print the current + proof state with mathematical symbols and special characters + represented in {\LaTeX} source, according to the Isabelle style + \cite{isabelle-sys}. + + Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more + systematic way to include formal items into the printed text + document.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Inspecting the context% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{print-commands}\isa{\isacommand{print{\isacharunderscore}commands}}^* & : & \isarkeep{\cdot} \\ + \indexdef{}{command}{print-theory}\isa{\isacommand{print{\isacharunderscore}theory}}^* & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{print-syntax}\isa{\isacommand{print{\isacharunderscore}syntax}}^* & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{print-methods}\isa{\isacommand{print{\isacharunderscore}methods}}^* & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{print-attributes}\isa{\isacommand{print{\isacharunderscore}attributes}}^* & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{print-theorems}\isa{\isacommand{print{\isacharunderscore}theorems}}^* & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{find-theorems}\isa{\isacommand{find{\isacharunderscore}theorems}}^* & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{thms-deps}\isa{\isacommand{thms{\isacharunderscore}deps}}^* & : & \isarkeep{theory~|~proof} \\ + \indexdef{}{command}{print-facts}\isa{\isacommand{print{\isacharunderscore}facts}}^* & : & \isarkeep{proof} \\ + \indexdef{}{command}{print-binds}\isa{\isacommand{print{\isacharunderscore}binds}}^* & : & \isarkeep{proof} \\ + \end{matharray} + + \begin{rail} + 'print\_theory' ( '!'?) + ; + + 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *) + ; + criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | + 'simp' ':' term | term) + ; + 'thm\_deps' thmrefs + ; + \end{rail} + + These commands print certain parts of the theory and proof context. + Note that there are some further ones available, such as for the set + of rules declared for simplifications. + + \begin{descr} + + \item [\isa{\isacommand{print{\isacharunderscore}commands}}] prints Isabelle's outer theory + syntax, including keywords and command. + + \item [\isa{\isacommand{print{\isacharunderscore}theory}}] prints the main logical content of + the theory context; the ``\isa{{\isacharbang}}'' option indicates extra + verbosity. + + \item [\isa{\isacommand{print{\isacharunderscore}syntax}}] prints the inner syntax of types + and terms, depending on the current context. The output can be very + verbose, including grammar tables and syntax translation rules. See + \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's + inner syntax. + + \item [\isa{\isacommand{print{\isacharunderscore}methods}}] prints all proof methods + available in the current theory context. + + \item [\isa{\isacommand{print{\isacharunderscore}attributes}}] prints all attributes + available in the current theory context. + + \item [\isa{\isacommand{print{\isacharunderscore}theorems}}] prints theorems resulting from + the last command. + + \item [\isa{\isacommand{find{\isacharunderscore}theorems}}~\isa{criteria}] retrieves facts + from the theory or proof context matching all of given search + criteria. The criterion \isa{name{\isacharcolon}\ p} selects all theorems + whose fully qualified name matches pattern \isa{p}, which may + contain ``\isa{{\isacharasterisk}}'' wildcards. The criteria \isa{intro}, + \isa{elim}, and \isa{dest} select theorems that match the + current goal as introduction, elimination or destruction rules, + respectively. The criterion \isa{simp{\isacharcolon}\ t} selects all rewrite + rules whose left-hand side matches the given term. The criterion + term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy + ``\verb|_|'', schematic variables, and type constraints. + + Criteria can be preceded by ``\isa{{\isacharminus}}'' to select theorems that + do \emph{not} match. Note that giving the empty list of criteria + yields \emph{all} currently known facts. An optional limit for the + number of printed facts may be given; the default is 40. By + default, duplicates are removed from the search result. Use + \isa{\isakeyword{with{\isacharunderscore}dups}} to display duplicates. + + \item [\isa{\isacommand{thm{\isacharunderscore}deps}}~\isa{a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n}] + visualizes dependencies of facts, using Isabelle's graph browser + tool (see also \cite{isabelle-sys}). + + \item [\isa{\isacommand{print{\isacharunderscore}facts}}] prints all local facts of the + current context, both named and unnamed ones. + + \item [\isa{\isacommand{print{\isacharunderscore}binds}}] prints all term abbreviations + present in the context. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{History commands \label{sec:history}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{undo}\isa{\isacommand{undo}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + \indexdef{}{command}{redo}\isa{\isacommand{redo}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + \indexdef{}{command}{kill}\isa{\isacommand{kill}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + \end{matharray} + + The Isabelle/Isar top-level maintains a two-stage history, for + theory and proof state transformation. Basically, any command can + be undone using \isa{\isacommand{undo}}, excluding mere diagnostic + elements. Its effect may be revoked via \isa{\isacommand{redo}}, unless + the corresponding \isa{\isacommand{undo}} step has crossed the beginning + of a proof or theory. The \isa{\isacommand{kill}} command aborts the + current history node altogether, discontinuing a proof or even the + whole theory. This operation is \emph{not} undo-able. + + \begin{warn} + History commands should never be used with user interfaces such as + Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes + care of stepping forth and back itself. Interfering by manual + \isa{\isacommand{undo}}, \isa{\isacommand{redo}}, or even \isa{\isacommand{kill}} + commands would quickly result in utter confusion. + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{System operations% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +\begin{matharray}{rcl} + \indexdef{}{command}{cd}\isa{\isacommand{cd}}^* & : & \isarkeep{\cdot} \\ + \indexdef{}{command}{pwd}\isa{\isacommand{pwd}}^* & : & \isarkeep{\cdot} \\ + \indexdef{}{command}{use-thy}\isa{\isacommand{use{\isacharunderscore}thy}}^* & : & \isarkeep{\cdot} \\ + \indexdef{}{command}{display-drafts}\isa{\isacommand{display{\isacharunderscore}drafts}}^* & : & \isarkeep{\cdot} \\ + \indexdef{}{command}{print-drafts}\isa{\isacommand{print{\isacharunderscore}drafts}}^* & : & \isarkeep{\cdot} \\ + \end{matharray} + + \begin{rail} + ('cd' | 'use\_thy' | 'update\_thy') name + ; + ('display\_drafts' | 'print\_drafts') (name +) + ; + \end{rail} + + \begin{descr} + + \item [\isa{\isacommand{cd}}~\isa{path}] changes the current directory + of the Isabelle process. + + \item [\isa{\isacommand{pwd}}] prints the current working directory. + + \item [\isa{\isacommand{use{\isacharunderscore}thy}}~\isa{A}] preload theory \isa{A}. + These system commands are scarcely used when working interactively, + since loading of theories is done automatically as required. + + \item [\isa{\isacommand{display{\isacharunderscore}drafts}}~\isa{paths} and \isa{\isacommand{print{\isacharunderscore}drafts}}~\isa{paths}] perform simple output of a given list + of raw source files. Only those symbols that do not require + additional {\LaTeX} packages are displayed properly, everything else + is left verbatim. + + \end{descr}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\isanewline +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/Thy/document/session.tex --- a/doc-src/IsarRef/Thy/document/session.tex Fri May 02 16:32:51 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/session.tex Fri May 02 16:36:05 2008 +0200 @@ -2,6 +2,8 @@ \input{syntax.tex} +\input{pure.tex} + %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/Thy/document/syntax.tex --- a/doc-src/IsarRef/Thy/document/syntax.tex Fri May 02 16:32:51 2008 +0200 +++ b/doc-src/IsarRef/Thy/document/syntax.tex Fri May 02 16:36:05 2008 +0200 @@ -4,6 +4,7 @@ % \isadelimtheory \isanewline +\isanewline % \endisadelimtheory % diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/Thy/intro.thy --- a/doc-src/IsarRef/Thy/intro.thy Fri May 02 16:32:51 2008 +0200 +++ b/doc-src/IsarRef/Thy/intro.thy Fri May 02 16:36:05 2008 +0200 @@ -1,3 +1,4 @@ +(* $Id$ *) theory intro imports CPure diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/Thy/pure.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/IsarRef/Thy/pure.thy Fri May 02 16:36:05 2008 +0200 @@ -0,0 +1,1792 @@ +(* $Id$ *) + +theory pure +imports CPure +begin + +chapter {* Basic language elements \label{ch:pure-syntax} *} + +text {* + Subsequently, we introduce the main part of Pure theory and proof + commands, together with fundamental proof methods and attributes. + \Chref{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 in most object logics. + \Chref{ch:logics} refers to object-logic specific elements (mainly + for HOL and ZF). + + \medskip Isar commands may be either \emph{proper} document + constructors, or \emph{improper commands}. Some proof methods and + attributes introduced later are classified as improper as well. + Improper Isar language elements, which are subsequently marked by + ``@{text "\<^sup>*"}'', are often helpful when developing proof + documents, while their use is discouraged for the final + human-readable outcome. Typical examples are diagnostic commands + that print terms or theorems according to the current context; other + commands emulate old-style tactical theorem proving. +*} + + +section {* Theory commands *} + +subsection {* Defining theories \label{sec:begin-thy} *} + +text {* + \begin{matharray}{rcl} + @{command_def "header"} & : & \isarkeep{toplevel} \\ + @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\ + @{command_def "end"} & : & \isartrans{theory}{toplevel} \\ + \end{matharray} + + Isabelle/Isar theories are defined via theory, which contain both + specifications and proofs; occasionally definitional mechanisms also + require some explicit proof. + + The first ``real'' command of any theory has to be @{command + "theory"}, which starts a new theory based on the merge of existing + ones. Just preceding the @{command "theory"} keyword, there may be + an optional @{command "header"} declaration, which is relevant to + document preparation only; it acts very much like a special + pre-theory markup command (cf.\ \secref{sec:markup-thy} and + \secref{sec:markup-thy}). The @{command "end"} command concludes a + theory development; it has to be the very last command of any theory + file loaded in batch-mode. + + \begin{rail} + 'header' text + ; + 'theory' name 'imports' (name +) uses? 'begin' + ; + + uses: 'uses' ((name | parname) +); + \end{rail} + + \begin{descr} + + \item [@{command "header"}~@{text "text"}] provides plain text + markup just preceding the formal beginning of a theory. In actual + document preparation the corresponding {\LaTeX} macro @{verbatim + "\\isamarkupheader"} may be redefined to produce chapter or section + headings. See also \secref{sec:markup-thy} and + \secref{sec:markup-prf} for further markup commands. + + \item [@{command "theory"}~@{text "A \ B\<^sub>1 \ + B\<^sub>n \"}] starts a new theory @{text A} based on the + merge of existing theories @{text "B\<^sub>1 \ B\<^sub>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. + + The optional @{keyword_def "uses"} specification declares additional + dependencies on extra files (usually ML sources). Files will be + loaded immediately (as ML), unless the name is put in parentheses, + which merely documents the dependency to be resolved later in the + text (typically via explicit @{command_ref "use"} in the body text, + see \secref{sec:ML}). + + \item [@{command "end"}] concludes the current theory definition or + context switch. + + \end{descr} +*} + + +subsection {* Markup commands \label{sec:markup-thy} *} + +text {* + \begin{matharray}{rcl} + @{command_def "chapter"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def "section"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def "subsection"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def "subsubsection"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def "text"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def "text_raw"} & : & \isarkeep{local{\dsh}theory} \\ + \end{matharray} + + Apart from formal comments (see \secref{sec:comments}), markup + commands provide a structured way to insert text into the document + generated from a theory (see \cite{isabelle-sys} for more + information on Isabelle's document preparation tools). + + \begin{rail} + ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text + ; + 'text\_raw' text + ; + \end{rail} + + \begin{descr} + + \item [@{command "chapter"}, @{command "section"}, @{command + "subsection"}, and @{command "subsubsection"}] mark chapter and + section headings. + + \item [@{command "text"}] specifies paragraphs of plain text. + + \item [@{command "text_raw"}] inserts {\LaTeX} source into the + output, without additional markup. Thus the full range of document + manipulations becomes available. + + \end{descr} + + The @{text "text"} argument of these markup commands (except for + @{command "text_raw"}) may contain references to formal entities + (``antiquotations'', see also \secref{sec:antiq}). These are + interpreted in the present theory context, or the named @{text + "target"}. + + Any of these markup elements corresponds to a {\LaTeX} command with + the name prefixed by @{verbatim "\\isamarkup"}. For the sectioning + commands this is a plain macro with a single argument, e.g.\ + @{verbatim "\\isamarkupchapter{"}@{text "\"}@{verbatim "}"} for + @{command "chapter"}. The @{command "text"} markup results in a + {\LaTeX} environment @{verbatim "\\begin{isamarkuptext}"}~@{text + "\"}~@{verbatim "\\end{isamarkuptext}"}, while @{command "text_raw"} + causes the text to be inserted directly into the {\LaTeX} source. + + \medskip Additional markup commands are available for proofs (see + \secref{sec:markup-prf}). Also note that the @{command_ref + "header"} declaration (see \secref{sec:begin-thy}) admits to insert + section markup just preceding the actual theory definition. +*} + + +subsection {* Type classes and sorts \label{sec:classes} *} + +text {* + \begin{matharray}{rcll} + @{command_def "classes"} & : & \isartrans{theory}{theory} \\ + @{command_def "classrel"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ + @{command_def "defaultsort"} & : & \isartrans{theory}{theory} \\ + @{command_def "class_deps"} & : & \isarkeep{theory~|~proof} \\ + \end{matharray} + + \begin{rail} + 'classes' (classdecl +) + ; + 'classrel' (nameref ('<' | subseteq) nameref + 'and') + ; + 'defaultsort' sort + ; + \end{rail} + + \begin{descr} + + \item [@{command "classes"}~@{text "c \ c\<^sub>1, \, c\<^sub>n"}] + declares class @{text c} to be a subclass of existing classes @{text + "c\<^sub>1, \, c\<^sub>n"}. Cyclic class structures are not permitted. + + \item [@{command "classrel"}~@{text "c\<^sub>1 \ c\<^sub>2"}] states + subclass relations between existing classes @{text "c\<^sub>1"} and + @{text "c\<^sub>2"}. This is done axiomatically! The @{command_ref + "instance"} command (see \secref{sec:axclass}) provides a way to + introduce proven class relations. + + \item [@{command "defaultsort"}~@{text s}] makes sort @{text s} the + new default sort for any type variables given without sort + constraints. Usually, the default sort would be only changed when + defining a new object-logic. + + \item [@{command "class_deps"}] visualizes the subclass relation, + using Isabelle's graph browser tool (see also \cite{isabelle-sys}). + + \end{descr} +*} + + +subsection {* Primitive types and type abbreviations \label{sec:types-pure} *} + +text {* + \begin{matharray}{rcll} + @{command_def "types"} & : & \isartrans{theory}{theory} \\ + @{command_def "typedecl"} & : & \isartrans{theory}{theory} \\ + @{command_def "nonterminals"} & : & \isartrans{theory}{theory} \\ + @{command_def "arities"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ + \end{matharray} + + \begin{rail} + 'types' (typespec '=' type infix? +) + ; + 'typedecl' typespec infix? + ; + 'nonterminals' (name +) + ; + 'arities' (nameref '::' arity +) + ; + \end{rail} + + \begin{descr} + + \item [@{command "types"}~@{text "(\\<^sub>1, \, \\<^sub>n) t = \"}] + introduces \emph{type synonym} @{text "(\\<^sub>1, \, \\<^sub>n) t"} + for existing type @{text "\"}. Unlike actual type definitions, as + are available in Isabelle/HOL for example, type synonyms are just + purely syntactic abbreviations without any logical significance. + Internally, type synonyms are fully expanded. + + \item [@{command "typedecl"}~@{text "(\\<^sub>1, \, \\<^sub>n) t"}] + declares a new type constructor @{text t}, intended as an actual + logical type (of the object-logic, if available). + + \item [@{command "nonterminals"}~@{text c}] declares type + constructors @{text c} (without arguments) to act as purely + syntactic types, i.e.\ nonterminal symbols of Isabelle's inner + syntax of terms or types. + + \item [@{command "arities"}~@{text "t :: (s\<^sub>1, \, s\<^sub>n) + s"}] augments Isabelle's order-sorted signature of types by new type + constructor arities. This is done axiomatically! The @{command_ref + "instance"} command (see \S\ref{sec:axclass}) provides a way to + introduce proven type arities. + + \end{descr} +*} + + +subsection {* Primitive constants and definitions \label{sec:consts} *} + +text {* + Definitions essentially express abbreviations within the logic. The + simplest form of a definition is @{text "c :: \ \ t"}, where @{text + c} is a newly declared constant. Isabelle also allows derived forms + where the arguments of @{text c} appear on the left, abbreviating a + prefix of @{text \}-abstractions, e.g.\ @{text "c \ \x y. t"} may be + written more conveniently as @{text "c x y \ t"}. Moreover, + definitions may be weakened by adding arbitrary pre-conditions: + @{text "A \ c x y \ t"}. + + \medskip The built-in well-formedness conditions for definitional + specifications are: + + \begin{itemize} + + \item Arguments (on the left-hand side) must be distinct variables. + + \item All variables on the right-hand side must also appear on the + left-hand side. + + \item All type variables on the right-hand side must also appear on + the left-hand side; this prohibits @{text "0 :: nat \ length ([] :: + \ list)"} for example. + + \item The definition must not be recursive. Most object-logics + provide definitional principles that can be used to express + recursion safely. + + \end{itemize} + + Overloading means that a constant being declared as @{text "c :: \ + decl"} may be defined separately on type instances @{text "c :: + (\\<^sub>1, \, \\<^sub>n) t decl"} for each type constructor @{text + t}. The right-hand side may mention overloaded constants + recursively at type instances corresponding to the immediate + argument types @{text "\\<^sub>1, \, \\<^sub>n"}. Incomplete + specification patterns impose global constraints on all occurrences, + e.g.\ @{text "d :: \ \ \"} on the left-hand side means that all + corresponding occurrences on some right-hand side need to be an + instance of this, general @{text "d :: \ \ \"} will be disallowed. + + \begin{matharray}{rcl} + @{command_def "consts"} & : & \isartrans{theory}{theory} \\ + @{command_def "defs"} & : & \isartrans{theory}{theory} \\ + @{command_def "constdefs"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'consts' ((name '::' type mixfix?) +) + ; + 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +) + ; + \end{rail} + + \begin{rail} + 'constdefs' structs? (constdecl? constdef +) + ; + + structs: '(' 'structure' (vars + 'and') ')' + ; + constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where' + ; + constdef: thmdecl? prop + ; + \end{rail} + + \begin{descr} + + \item [@{command "consts"}~@{text "c :: \"}] declares constant + @{text c} to have any instance of type scheme @{text \}. The + optional mixfix annotations may attach concrete syntax to the + constants declared. + + \item [@{command "defs"}~@{text "name: eqn"}] introduces @{text eqn} + as a definitional axiom for some existing constant. + + The @{text "(unchecked)"} option disables global dependency checks + for this definition, which is occasionally useful for exotic + overloading. It is at the discretion of the user to avoid malformed + theory specifications! + + The @{text "(overloaded)"} option declares definitions to be + potentially overloaded. 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 [@{command "constdefs"}] provides a streamlined combination of + constants declarations and definitions: type-inference takes care of + the most general typing of the given specification (the optional + type constraint may refer to type-inference dummies ``@{verbatim + _}'' as usual). The resulting type declaration needs to agree with + that of the specification; overloading is \emph{not} supported here! + + The constant name may be omitted altogether, if neither type nor + syntax declarations are given. The canonical name of the + definitional axiom for constant @{text c} will be @{text c_def}, + unless specified otherwise. Also note that the given list of + specifications is processed in a strictly sequential manner, with + type-checking being performed independently. + + An optional initial context of @{text "(structure)"} declarations + admits use of indexed syntax, using the special symbol @{verbatim + "\"} (printed as ``@{text "\"}''). The latter concept is + particularly useful with locales (see also \S\ref{sec:locale}). + + \end{descr} +*} + + +subsection {* Syntax and translations \label{sec:syn-trans} *} + +text {* + \begin{matharray}{rcl} + @{command_def "syntax"} & : & \isartrans{theory}{theory} \\ + @{command_def "no_syntax"} & : & \isartrans{theory}{theory} \\ + @{command_def "translations"} & : & \isartrans{theory}{theory} \\ + @{command_def "no_translations"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \railalias{rightleftharpoons}{\isasymrightleftharpoons} + \railterm{rightleftharpoons} + + \railalias{rightharpoonup}{\isasymrightharpoonup} + \railterm{rightharpoonup} + + \railalias{leftharpoondown}{\isasymleftharpoondown} + \railterm{leftharpoondown} + + \begin{rail} + ('syntax' | 'no\_syntax') mode? (constdecl +) + ; + ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) + ; + + mode: ('(' ( name | 'output' | name 'output' ) ')') + ; + transpat: ('(' nameref ')')? string + ; + \end{rail} + + \begin{descr} + + \item [@{command "syntax"}~@{text "(mode) decls"}] is similar to + @{command "consts"}~@{text decls}, except that the actual logical + signature extension is omitted. Thus the context free grammar of + Isabelle's inner syntax may be augmented in arbitrary ways, + independently of the logic. The @{text mode} argument refers to the + print mode that the grammar rules belong; unless the @{keyword_ref + "output"} indicator is given, all productions are added both to the + input and output grammar. + + \item [@{command "no_syntax"}~@{text "(mode) decls"}] removes + grammar declarations (and translations) resulting from @{text + decls}, which are interpreted in the same manner as for @{command + "syntax"} above. + + \item [@{command "translations"}~@{text rules}] specifies syntactic + translation rules (i.e.\ macros): parse~/ print rules (@{text "\"}), + parse rules (@{text "\"}), or print rules (@{text "\"}). + Translation patterns may be prefixed by the syntactic category to be + used for parsing; the default is @{text logic}. + + \item [@{command "no_translations"}~@{text rules}] removes syntactic + translation rules, which are interpreted in the same manner as for + @{command "translations"} above. + + \end{descr} +*} + + +subsection {* Axioms and theorems \label{sec:axms-thms} *} + +text {* + \begin{matharray}{rcll} + @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\ + @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\ + @{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\ + \end{matharray} + + \begin{rail} + 'axioms' (axmdecl prop +) + ; + ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and') + ; + \end{rail} + + \begin{descr} + + \item [@{command "axioms"}~@{text "a: \"}] introduces arbitrary + statements as axioms of the meta-logic. In fact, axioms are + ``axiomatic theorems'', and may be referred later just as any other + theorem. + + Axioms are usually only introduced when declaring new logical + systems. Everyday work is typically done the hard way, with proper + definitions and proven theorems. + + \item [@{command "lemmas"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}] + retrieves and stores existing facts in the theory context, or the + specified target context (see also \secref{sec:target}). Typical + applications would also involve attributes, to declare Simplifier + rules, for example. + + \item [@{command "theorems"}] is essentially the same as @{command + "lemmas"}, but marks the result as a different kind of facts. + + \end{descr} +*} + + +subsection {* Name spaces *} + +text {* + \begin{matharray}{rcl} + @{command_def "global"} & : & \isartrans{theory}{theory} \\ + @{command_def "local"} & : & \isartrans{theory}{theory} \\ + @{command_def "hide"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'hide' ('(open)')? name (nameref + ) + ; + \end{rail} + + Isabelle organizes any kind of name declarations (of types, + constants, theorems etc.) by separate hierarchically structured name + spaces. Normally the user does not have to control the behavior of + name spaces by hand, yet the following commands provide some way to + do so. + + \begin{descr} + + \item [@{command "global"} and @{command "local"}] change the + current name declaration mode. Initially, theories start in + @{command "local"} mode, causing all names to be automatically + qualified by the theory name. Changing this to @{command "global"} + causes all names to be declared without the theory prefix, until + @{command "local"} is declared again. + + Note that global names are prone to get hidden accidently later, + when qualified names of the same base name are introduced. + + \item [@{command "hide"}~@{text "space names"}] fully removes + declarations from a given name space (which may be @{text "class"}, + @{text "type"}, @{text "const"}, or @{text "fact"}); with the @{text + "(open)"} option, only the base name is hidden. Global + (unqualified) names may never be hidden. + + Note that hiding name space accesses has no impact on logical + declarations -- they remain valid internally. Entities that are no + longer accessible to the user are printed with the special qualifier + ``@{text "??"}'' prefixed to the full internal name. + + \end{descr} +*} + + +subsection {* Incorporating ML code \label{sec:ML} *} + +text {* + \begin{matharray}{rcl} + @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\ + @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\ + @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\ + @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\ + @{command_def "setup"} & : & \isartrans{theory}{theory} \\ + @{command_def "method_setup"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + 'use' name + ; + ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text + ; + 'method\_setup' name '=' text text + ; + \end{rail} + + \begin{descr} + + \item [@{command "use"}~@{text "file"}] reads and executes ML + commands from @{text "file"}. The current theory context is passed + down to the ML toplevel and may be modified, using @{ML + "Context.>>"} or derived ML commands. The file name is checked with + the @{keyword_ref "uses"} dependency declaration given in the theory + header (see also \secref{sec:begin-thy}). + + \item [@{command "ML"}~@{text "text"}] is similar to @{command + "use"}, but executes ML commands directly from the given @{text + "text"}. + + \item [@{command "ML_val"} and @{command "ML_command"}] are + diagnostic versions of @{command "ML"}, which means that the context + may not be updated. @{command "ML_val"} echos the bindings produced + at the ML toplevel, but @{command "ML_command"} is silent. + + \item [@{command "setup"}~@{text "text"}] changes the current theory + context by applying @{text "text"}, which refers to an ML expression + of type @{ML_type "theory -> theory"}. This enables to initialize + any object-logic specific tools and packages written in ML, for + example. + + \item [@{command "method_setup"}~@{text "name = text description"}] + defines a proof method in the current theory. The given @{text + "text"} has to be an ML expression of type @{ML_type "Args.src -> + Proof.context -> Proof.method"}. Parsing concrete method syntax + from @{ML_type Args.src} input can be quite tedious in general. The + following simple examples are for methods without any explicit + arguments, or a list of theorems, respectively. + +%FIXME proper antiquotations +{\footnotesize +\begin{verbatim} + Method.no_args (Method.METHOD (fn facts => foobar_tac)) + Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) + Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) + Method.thms_ctxt_args (fn thms => fn ctxt => + Method.METHOD (fn facts => foobar_tac)) +\end{verbatim} +} + + Note that mere tactic emulations may ignore the @{text facts} + parameter above. Proper proof methods would do something + appropriate with the list of current facts, though. Single-rule + methods usually do strict forward-chaining (e.g.\ by using @{ML + Drule.multi_resolves}), while automatic ones just insert the facts + using @{ML Method.insert_tac} before applying the main tactic. + + \end{descr} +*} + + +subsection {* Syntax translation functions *} + +text {* + \begin{matharray}{rcl} + @{command_def "parse_ast_translation"} & : & \isartrans{theory}{theory} \\ + @{command_def "parse_translation"} & : & \isartrans{theory}{theory} \\ + @{command_def "print_translation"} & : & \isartrans{theory}{theory} \\ + @{command_def "typed_print_translation"} & : & \isartrans{theory}{theory} \\ + @{command_def "print_ast_translation"} & : & \isartrans{theory}{theory} \\ + @{command_def "token_translation"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + \begin{rail} + ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' | + 'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text + ; + + 'token\_translation' text + ; + \end{rail} + + Syntax translation functions written in ML admit almost arbitrary + manipulations of Isabelle's inner syntax. Any of the above commands + have a single \railqtok{text} argument that refers to an ML + expression of appropriate type, which are as follows by default: + +%FIXME proper antiquotations +\begin{ttbox} +val parse_ast_translation : (string * (ast list -> ast)) list +val parse_translation : (string * (term list -> term)) list +val print_translation : (string * (term list -> term)) list +val typed_print_translation : + (string * (bool -> typ -> term list -> term)) list +val print_ast_translation : (string * (ast list -> ast)) list +val token_translation : + (string * string * (string -> string * real)) list +\end{ttbox} + + If the @{text "(advanced)"} option is given, the corresponding + translation functions may depend on the current theory or proof + context. This allows to implement advanced syntax mechanisms, as + translations functions may refer to specific theory declarations or + auxiliary proof data. + + See also \cite[\S8]{isabelle-ref} for more information on the + general concept of syntax transformations in Isabelle. + +%FIXME proper antiquotations +\begin{ttbox} +val parse_ast_translation: + (string * (Context.generic -> ast list -> ast)) list +val parse_translation: + (string * (Context.generic -> term list -> term)) list +val print_translation: + (string * (Context.generic -> term list -> term)) list +val typed_print_translation: + (string * (Context.generic -> bool -> typ -> term list -> term)) list +val print_ast_translation: + (string * (Context.generic -> ast list -> ast)) list +\end{ttbox} +*} + + +subsection {* Oracles *} + +text {* + \begin{matharray}{rcl} + @{command_def "oracle"} & : & \isartrans{theory}{theory} \\ + \end{matharray} + + The oracle interface promotes a given ML function @{ML_text + "theory -> T -> term"} to @{ML_text "theory -> T -> thm"}, for some type + @{ML_text T} given by the user. This acts like an infinitary + specification of axioms -- there is no internal check of the + correctness of the results! The inference kernel records oracle + invocations within the internal derivation object of theorems, and + the pretty printer attaches ``@{text "[!]"}'' to indicate results + that are not fully checked by Isabelle inferences. + + \begin{rail} + 'oracle' name '(' type ')' '=' text + ; + \end{rail} + + \begin{descr} + + \item [@{command "oracle"}~@{text "name (type) = text"}] turns the + given ML expression @{text "text"} of type @{ML_text "{theory + ->"}~@{text "type"}~@{ML_text "-> term"} into an ML function + @{ML_text name} of type @{ML_text "{theory ->"}~@{text + "type"}~@{ML_text "-> thm"}. + + \end{descr} +*} + + +section {* Proof commands *} + +text {* + Proof commands perform transitions of Isar/VM machine + configurations, which are block-structured, consisting of a stack of + nodes with three main components: logical proof context, current + facts, and open goals. Isar/VM transitions are \emph{typed} + according to the following three different modes of operation: + + \begin{descr} + + \item [@{text "proof(prove)"}] means that a new goal has just been + stated that is now to be \emph{proven}; the next command may refine + it by some proof method, and enter a sub-proof to establish the + actual result. + + \item [@{text "proof(state)"}] is like a nested theory mode: the + context may be augmented by \emph{stating} additional assumptions, + intermediate results etc. + + \item [@{text "proof(chain)"}] is intermediate between @{text + "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\ + the contents of the special ``@{fact_ref this}'' register) have been + just picked up in order to be used when refining the goal claimed + next. + + \end{descr} + + 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 of a certain structure. + \Appref{ap:refcard} gives a simplified grammar of the overall + (extensible) language emerging that way. +*} + + +subsection {* Markup commands \label{sec:markup-prf} *} + +text {* + \begin{matharray}{rcl} + @{command_def "sect"} & : & \isartrans{proof}{proof} \\ + @{command_def "subsect"} & : & \isartrans{proof}{proof} \\ + @{command_def "subsubsect"} & : & \isartrans{proof}{proof} \\ + @{command_def "txt"} & : & \isartrans{proof}{proof} \\ + @{command_def "txt_raw"} & : & \isartrans{proof}{proof} \\ + \end{matharray} + + These markup commands for proof mode closely correspond to the ones + of theory mode (see \S\ref{sec:markup-thy}). + + \begin{rail} + ('sect' | 'subsect' | 'subsubsect' | 'txt' | 'txt\_raw') text + ; + \end{rail} +*} + + +subsection {* Context elements \label{sec:proof-context} *} + +text {* + \begin{matharray}{rcl} + @{command_def "fix"} & : & \isartrans{proof(state)}{proof(state)} \\ + @{command_def "assume"} & : & \isartrans{proof(state)}{proof(state)} \\ + @{command_def "presume"} & : & \isartrans{proof(state)}{proof(state)} \\ + @{command_def "def"} & : & \isartrans{proof(state)}{proof(state)} \\ + \end{matharray} + + The logical proof context consists of fixed variables and + assumptions. The former closely correspond to Skolem constants, or + meta-level universal quantification as provided by the Isabelle/Pure + logical framework. Introducing some \emph{arbitrary, but fixed} + variable via ``@{command "fix"}~@{text x} results in a local value + that may be used in the subsequent proof as any other variable or + constant. Furthermore, any result @{text "\ \[x]"} exported from + the context will be universally closed wrt.\ @{text x} at the + outermost level: @{text "\ \x. \[x]"} (this is expressed in normal + form using Isabelle's meta-variables). + + Similarly, introducing some assumption @{text \} has two effects. + On the one hand, a local theorem is created that may be used as a + fact in subsequent proof steps. On the other hand, any result + @{text "\ \ \"} exported from the context becomes conditional wrt.\ + the assumption: @{text "\ \ \ \"}. Thus, solving an enclosing goal + using such a result would basically introduce a new subgoal stemming + from the assumption. How this situation is handled depends on the + version of assumption command used: while @{command "assume"} + insists on solving the subgoal by unification with some premise of + the goal, @{command "presume"} leaves the subgoal unchanged in order + to be proved later by the user. + + Local definitions, introduced by ``@{command "def"}~@{text "x \ + t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with + another version of assumption that causes any hypothetical equation + @{text "x \ t"} to be eliminated by the reflexivity rule. Thus, + exporting some result @{text "x \ t \ \[x]"} yields @{text "\ + \[t]"}. + + \railalias{equiv}{\isasymequiv} + \railterm{equiv} + + \begin{rail} + 'fix' (vars + 'and') + ; + ('assume' | 'presume') (props + 'and') + ; + 'def' (def + 'and') + ; + def: thmdecl? \\ name ('==' | equiv) term termpat? + ; + \end{rail} + + \begin{descr} + + \item [@{command "fix"}~@{text x}] introduces a local variable + @{text x} that is \emph{arbitrary, but fixed.} + + \item [@{command "assume"}~@{text "a: \"} and @{command + "presume"}~@{text "a: \"}] introduce a local fact @{text "\ \ \"} by + assumption. Subsequent results applied to an enclosing goal (e.g.\ + by @{command_ref "show"}) are handled as follows: @{command + "assume"} expects to be able to unify with existing premises in the + goal, while @{command "presume"} leaves @{text \} as new subgoals. + + Several lists of assumptions may be given (separated by + @{keyword_ref "and"}; the resulting list of current facts consists + of all of these concatenated. + + \item [@{command "def"}~@{text "x \ t"}] introduces a local + (non-polymorphic) definition. In results exported from the context, + @{text x} is replaced by @{text t}. Basically, ``@{command + "def"}~@{text "x \ t"}'' abbreviates ``@{command "fix"}~@{text + x}~@{command "assume"}~@{text "x \ t"}'', with the resulting + hypothetical equation solved by reflexivity. + + The default name for the definitional equation is @{text x_def}. + Several simultaneous definitions may be given at the same time. + + \end{descr} + + The special name @{fact_ref prems} refers to all assumptions of the + current context as a list of theorems. This feature should be used + with great care! It is better avoided in final proof texts. +*} + + +subsection {* Facts and forward chaining *} + +text {* + \begin{matharray}{rcl} + @{command_def "note"} & : & \isartrans{proof(state)}{proof(state)} \\ + @{command_def "then"} & : & \isartrans{proof(state)}{proof(chain)} \\ + @{command_def "from"} & : & \isartrans{proof(state)}{proof(chain)} \\ + @{command_def "with"} & : & \isartrans{proof(state)}{proof(chain)} \\ + @{command_def "using"} & : & \isartrans{proof(prove)}{proof(prove)} \\ + @{command_def "unfolding"} & : & \isartrans{proof(prove)}{proof(prove)} \\ + \end{matharray} + + New facts are established either by assumption or proof of local + statements. Any fact will usually be involved in further proofs, + either as explicit arguments of proof methods, or when forward + chaining towards the next goal via @{command "then"} (and variants); + @{command "from"} and @{command "with"} are composite forms + involving @{command "note"}. The @{command "using"} elements + augments the collection of used facts \emph{after} a goal has been + stated. Note that the special theorem name @{fact_ref this} refers + to the most recently established facts, but only \emph{before} + issuing a follow-up claim. + + \begin{rail} + 'note' (thmdef? thmrefs + 'and') + ; + ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and') + ; + \end{rail} + + \begin{descr} + + \item [@{command "note"}~@{text "a = b\<^sub>1 \ b\<^sub>n"}] + recalls existing facts @{text "b\<^sub>1, \, b\<^sub>n"}, binding + the result as @{text a}. Note that attributes may be involved as + well, both on the left and right hand sides. + + \item [@{command "then"}] indicates forward chaining by the current + facts in order to establish the goal to be claimed next. The + initial proof method invoked to refine that will be offered the + facts to do ``anything appropriate'' (see also + \secref{sec:proof-steps}). For example, method @{method_ref rule} + (see \secref{sec:pure-meth-att}) would typically do an elimination + rather than an introduction. Automatic methods usually insert the + facts into the goal state before operation. This provides a simple + scheme to control relevance of facts in automated proof search. + + \item [@{command "from"}~@{text b}] abbreviates ``@{command + "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is + equivalent to ``@{command "from"}~@{text this}''. + + \item [@{command "with"}~@{text "b\<^sub>1 \ b\<^sub>n"}] + abbreviates ``@{command "from"}~@{text "b\<^sub>1 \ b\<^sub>n \ + this"}''; thus the forward chaining is from earlier facts together + with the current ones. + + \item [@{command "using"}~@{text "b\<^sub>1 \ b\<^sub>n"}] augments + the facts being currently indicated for use by a subsequent + refinement step (such as @{command_ref "apply"} or @{command_ref + "proof"}). + + \item [@{command "unfolding"}~@{text "b\<^sub>1 \ b\<^sub>n"}] is + structurally similar to @{command "using"}, but unfolds definitional + equations @{text "b\<^sub>1, \ b\<^sub>n"} throughout the goal state + and facts. + + \end{descr} + + Forward chaining with an empty list of theorems is the same as not + chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no + effect apart from entering @{text "prove(chain)"} mode, since + @{fact_ref nothing} is bound to the empty list of theorems. + + Basic proof methods (such as @{method_ref rule}) expect multiple + facts to be given in their proper order, corresponding to a prefix + of the premises of the rule involved. Note that positions may be + easily skipped using something like @{command "from"}~@{text "_ + \ a \ b"}, for example. This involves the trivial rule + @{text "PROP \ \ PROP \"}, which is bound in Isabelle/Pure as + ``@{fact_ref "_"}'' (underscore). + + Automated methods (such as @{method simp} or @{method auto}) just + insert any given facts before their usual operation. Depending on + the kind of procedure involved, the order of facts is less + significant here. +*} + + +subsection {* Goal statements \label{sec:goals} *} + +text {* + \begin{matharray}{rcl} + \isarcmd{lemma} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ + \isarcmd{theorem} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ + \isarcmd{corollary} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ + \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ + \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ + \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ + \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ + \isarcmd{print_statement}^* & : & \isarkeep{theory~|~proof} \\ + \end{matharray} + + From a theory context, proof mode is entered by an initial goal + command such as @{command "lemma"}, @{command "theorem"}, or + @{command "corollary"}. 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 @{command_ref "then"}), and whether the final 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 conjunction (printed as @{text "&&"}), which is usually + split into the corresponding number of sub-goals prior to an initial + method application, via @{command_ref "proof"} + (\secref{sec:proof-steps}) or @{command_ref "apply"} + (\secref{sec:tactic-commands}). The @{method_ref induct} method + covered in \secref{sec:cases-induct} acts on multiple claims + simultaneously. + + Claims at the theory level may be either in short or long form. A + short goal merely consists of several simultaneous propositions + (often just one). A long goal includes an explicit context + specification for the subsequent conclusion, involving local + parameters and assumptions. Here the role of each part of the + statement is explicitly marked by separate keywords (see also + \secref{sec:locale}); the local assumptions being introduced here + are available as @{fact_ref assms} in the proof. Moreover, there + are two kinds of conclusions: @{element_def "shows"} states several + simultaneous propositions (essentially a big conjunction), while + @{element_def "obtains"} claims several simultaneous simultaneous + contexts of (essentially a big disjunction of eliminated parameters + and assumptions, cf.\ \secref{sec:obtain}). + + \begin{rail} + ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal) + ; + ('have' | 'show' | 'hence' | 'thus') goal + ; + 'print\_statement' modes? thmrefs + ; + + goal: (props + 'and') + ; + longgoal: thmdecl? (contextelem *) conclusion + ; + conclusion: 'shows' goal | 'obtains' (parname? case + '|') + ; + case: (vars + 'and') 'where' (props + 'and') + ; + \end{rail} + + \begin{descr} + + \item [@{command "lemma"}~@{text "a: \"}] enters proof mode with + @{text \} as main goal, eventually resulting in some fact @{text "\ + \"} to be put back into the target context. An additional + \railnonterm{context} specification may build up an initial proof + context for the subsequent claim; this includes local definitions + and syntax as well, see the definition of @{syntax contextelem} in + \secref{sec:locale}. + + \item [@{command "theorem"}~@{text "a: \"} and @{command + "corollary"}~@{text "a: \"}] are essentially the same as @{command + "lemma"}~@{text "a: \"}, but the facts are internally marked as + being of a different kind. This discrimination acts like a formal + comment. + + \item [@{command "have"}~@{text "a: \"}] claims a local goal, + eventually resulting in a fact within the current logical context. + This operation is completely independent of any pending sub-goals of + an enclosing goal statements, so @{command "have"} may be freely + used for experimental exploration of potential results within a + proof body. + + \item [@{command "show"}~@{text "a: \"}] is like @{command + "have"}~@{text "a: \"} plus a second stage to refine some pending + sub-goal for each one of the finished result, after having been + exported into the corresponding context (at the head of the + sub-proof of this @{command "show"} command). + + To accommodate interactive debugging, resulting rules are printed + before being applied internally. Even more, interactive execution + of @{command "show"} predicts potential failure and displays the + resulting error as a warning beforehand. Watch out for the + following message: + + %FIXME proper antiquitation + \begin{ttbox} + Problem! Local statement will fail to solve any pending goal + \end{ttbox} + + \item [@{command "hence"}] abbreviates ``@{command "then"}~@{command + "have"}'', i.e.\ claims a local goal to be proven by forward + chaining the current facts. Note that @{command "hence"} is also + equivalent to ``@{command "from"}~@{text this}~@{command "have"}''. + + \item [@{command "thus"}] abbreviates ``@{command "then"}~@{command + "show"}''. Note that @{command "thus"} is also equivalent to + ``@{command "from"}~@{text this}~@{command "show"}''. + + \item [@{command "print_statement"}~@{text a}] prints facts from the + current theory or proof context in long statement form, according to + the syntax for @{command "lemma"} given above. + + \end{descr} + + Any goal statement causes some term abbreviations (such as + @{variable_ref "?thesis"}) to be bound automatically, see also + \secref{sec:term-abbrev}. Furthermore, the local context of a + (non-atomic) goal is provided via the @{case_ref rule_context} case. + + The optional case names of @{element_ref "obtains"} have a twofold + meaning: (1) during the of this claim they refer to the the local + context introductions, (2) the resulting rule is annotated + accordingly to support symbolic case splits when used with the + @{method_ref cases} method (cf. \secref{sec:cases-induct}). + + \medskip + + \begin{warn} + Isabelle/Isar suffers theory-level goal statements to contain + \emph{unbound schematic variables}, although this does not conform + to the aim of human-readable proof documents! The main problem + with schematic goals is that the actual outcome is usually hard to + predict, depending on the behavior of the proof methods applied + during the course of reasoning. Note that most semi-automated + methods heavily depend on several kinds of implicit rule + declarations within the current theory context. As this would + also result in non-compositional checking of sub-proofs, + \emph{local goals} are not allowed to be schematic at all. + Nevertheless, schematic goals do have their use in Prolog-style + interactive synthesis of proven results, usually by stepwise + refinement via emulation of traditional Isabelle tactic scripts + (see also \secref{sec:tactic-commands}). In any case, users + should know what they are doing. + \end{warn} +*} + + +subsection {* Initial and terminal proof steps \label{sec:proof-steps} *} + +text {* + \begin{matharray}{rcl} + @{command_def "proof"} & : & \isartrans{proof(prove)}{proof(state)} \\ + @{command_def "qed"} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\ + @{command_def "by"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ + @{command_def ".."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ + @{command_def "."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ + @{command_def "sorry"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ + \end{matharray} + + Arbitrary goal refinement via tactics is considered harmful. + Structured proof composition in Isar admits proof methods to be + invoked in two places only. + + \begin{enumerate} + + \item An \emph{initial} refinement step @{command_ref + "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number + of sub-goals that are to be solved later. Facts are passed to + @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text + "proof(chain)"} mode. + + \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text + "m\<^sub>2"} is intended to solve remaining goals. No facts are + passed to @{text "m\<^sub>2"}. + + \end{enumerate} + + The only other (proper) way to affect pending goals in a proof body + is by @{command_ref "show"}, 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 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 + an intelligible manner. + + Unless given explicitly by the user, the default initial method is + ``@{method_ref rule}'', which applies a single standard elimination + or introduction rule according to the topmost symbol involved. + There is no separate default terminal method. Any remaining goals + are always solved by assumption in the very last step. + + \begin{rail} + 'proof' method? + ; + 'qed' method? + ; + 'by' method method? + ; + ('.' | '..' | 'sorry') + ; + \end{rail} + + \begin{descr} + + \item [@{command "proof"}~@{text "m\<^sub>1"}] refines the goal by + proof method @{text "m\<^sub>1"}; facts for forward chaining are + passed if so indicated by @{text "proof(chain)"} mode. + + \item [@{command "qed"}~@{text "m\<^sub>2"}] refines any remaining + goals by proof method @{text "m\<^sub>2"} and concludes the + sub-proof by assumption. If the goal had been @{text "show"} (or + @{text "thus"}), some pending sub-goal is solved as well by the rule + resulting from the result \emph{exported} into the enclosing goal + context. Thus @{text "qed"} may fail for two reasons: either @{text + "m\<^sub>2"} fails, or the resulting rule does not fit to any + pending goal\footnote{This includes any additional ``strong'' + assumptions as introduced by @{text "assume"}.} of the enclosing + context. Debugging such a situation might involve temporarily + changing @{command "show"} into @{command "have"}, or weakening the + local context by replacing occurrences of @{command "assume"} by + @{command "presume"}. + + \item [@{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}] is a + \emph{terminal proof}\index{proof!terminal}; it abbreviates + @{command "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text + "m\<^sub>2"}, but with backtracking across both methods. Debugging + an unsuccessful @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} + command can be done by expanding its definition; in many cases + @{command "proof"}~@{text "m\<^sub>1"} (or even @{text + "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the + problem. + + \item [``@{command ".."}''] is a \emph{default + proof}\index{proof!default}; it abbreviates @{command "by"}~@{text + "rule"}. + + \item [``@{command "."}''] is a \emph{trivial + proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text + "this"}. + + \item [@{command "sorry"}] is a \emph{fake proof}\index{proof!fake} + pretending to solve the pending claim without further ado. This + only works in interactive development, or if the @{ML + quick_and_dirty} flag is enabled (in ML). Facts emerging from fake + proofs are not the real thing. Internally, each theorem container + is tainted by an oracle invocation, which is indicated as ``@{text + "[!]"}'' in the printed result. + + The most important application of @{command "sorry"} is to support + experimentation and top-down proof development. + + \end{descr} +*} + + +subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *} + +text {* + 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 + \chref{ch:gen-tools} and \chref{ch:logics}). + + \begin{matharray}{rcl} + @{method_def "-"} & : & \isarmeth \\ + @{method_def "fact"} & : & \isarmeth \\ + @{method_def "assumption"} & : & \isarmeth \\ + @{method_def "this"} & : & \isarmeth \\ + @{method_def "rule"} & : & \isarmeth \\ + @{method_def "iprover"} & : & \isarmeth \\[0.5ex] + @{attribute_def "intro"} & : & \isaratt \\ + @{attribute_def "elim"} & : & \isaratt \\ + @{attribute_def "dest"} & : & \isaratt \\ + @{attribute_def "rule"} & : & \isaratt \\[0.5ex] + @{attribute_def "OF"} & : & \isaratt \\ + @{attribute_def "of"} & : & \isaratt \\ + @{attribute_def "where"} & : & \isaratt \\ + \end{matharray} + + \begin{rail} + 'fact' thmrefs? + ; + 'rule' thmrefs? + ; + 'iprover' ('!' ?) (rulemod *) + ; + rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs + ; + ('intro' | 'elim' | 'dest') ('!' | () | '?') nat? + ; + 'rule' 'del' + ; + 'OF' thmrefs + ; + 'of' insts ('concl' ':' insts)? + ; + 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and') + ; + \end{rail} + + \begin{descr} + + \item [``@{method "-"}''] does nothing but insert the forward + chaining facts as premises into the goal. Note that command + @{command_ref "proof"} without any method actually performs a single + reduction step using the @{method_ref rule} method; thus a plain + \emph{do-nothing} proof step would be ``@{command "proof"}~@{text + "-"}'' rather than @{command "proof"} alone. + + \item [@{method "fact"}~@{text "a\<^sub>1 \ a\<^sub>n"}] composes + some fact from @{text "a\<^sub>1, \, a\<^sub>n"} (or implicitly from + the current proof context) modulo unification of schematic type and + term variables. The rule structure is not taken into account, i.e.\ + meta-level implication is considered atomic. This is the same + principle underlying literal facts (cf.\ \secref{sec:syn-att}): + ``@{command "have"}~@{text "\"}~@{command "by"}~@{text fact}'' is + equivalent to ``@{command "note"}~@{verbatim "`"}@{text \}@{verbatim + "`"}'' provided that @{text "\ \"} is an instance of some known + @{text "\ \"} in the proof context. + + \item [@{method assumption}] solves some goal by a single assumption + step. All given facts are guaranteed to participate in the + refinement; this means there may be only 0 or 1 in the first place. + Recall that @{command "qed"} (\secref{sec:proof-steps}) already + concludes any remaining sub-goals by assumption, so structured + proofs usually need not quote the @{method assumption} method at + all. + + \item [@{method this}] applies all of the current facts directly as + rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command + "by"}~@{text this}''. + + \item [@{method rule}~@{text "a\<^sub>1 \ a\<^sub>n"}] applies some + rule given as argument in backward manner; facts are used to reduce + the rule before applying it to the goal. Thus @{method rule} + without facts is plain introduction, while with facts it becomes + elimination. + + When no arguments are given, the @{method rule} method tries to pick + appropriate rules automatically, as declared in the current context + using the @{attribute intro}, @{attribute elim}, @{attribute dest} + attributes (see below). This is the default behavior of @{command + "proof"} and ``@{command ".."}'' (double-dot) steps (see + \secref{sec:proof-steps}). + + \item [@{method iprover}] performs intuitionistic proof search, + depending on specifically declared rules from the context, or given + as explicit arguments. Chained facts are inserted into the goal + before commencing proof search; ``@{method iprover}@{text "!"}'' + means to include the current @{fact prems} as well. + + Rules need to be classified as @{attribute intro}, @{attribute + elim}, or @{attribute dest}; here the ``@{text "!"} indicator refers + to ``safe'' rules, which may be applied aggressively (without + considering back-tracking later). Rules declared with ``@{text + "?"}'' are ignored in proof search (the single-step @{method rule} + method still observes these). An explicit weight annotation may be + given as well; otherwise the number of rule premises will be taken + into account here. + + \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}] + declare introduction, elimination, and destruct rules, to be used + with the @{method rule} and @{method iprover} methods. Note that + the latter will ignore rules declared with ``@{text "?"}'', while + ``@{text "!"}'' are used most aggressively. + + The classical reasoner (see \secref{sec:classical}) introduces its + own variants of these attributes; use qualified names to access the + present versions of Isabelle/Pure, i.e.\ @{attribute "Pure.intro"}. + + \item [@{attribute rule}~@{text del}] undeclares introduction, + elimination, or destruct rules. + + \item [@{attribute OF}~@{text "a\<^sub>1 \ a\<^sub>n"}] applies some + theorem to all of the given rules @{text "a\<^sub>1, \, a\<^sub>n"} + (in parallel). This corresponds to the @{ML "op MRS"} operation in + ML, but note the reversed order. Positions may be effectively + skipped by including ``@{verbatim _}'' (underscore) as argument. + + \item [@{attribute of}~@{text "t\<^sub>1 \ t\<^sub>n"}] performs + positional instantiation of term variables. The terms @{text + "t\<^sub>1, \, t\<^sub>n"} are substituted for any schematic + variables occurring in a theorem from left to right; ``@{verbatim + _}'' (underscore) indicates to skip a position. Arguments following + a ``@{keyword "concl"}@{text ":"}'' specification refer to positions + of the conclusion of a rule. + + \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \ \ + \ x\<^sub>n = t\<^sub>n"}] performs named instantiation of + schematic type and term variables occurring in a theorem. Schematic + variables have to be specified on the left-hand side (e.g.\ @{text + "?x1.3"}). The question mark may be omitted if the variable name is + a plain identifier without index. As type instantiations are + inferred from term instantiations, explicit type instantiations are + seldom necessary. + + \end{descr} +*} + + +subsection {* Term abbreviations \label{sec:term-abbrev} *} + +text {* + \begin{matharray}{rcl} + @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\ + @{keyword_def "is"} & : & syntax \\ + \end{matharray} + + Abbreviations may be either bound by explicit @{command "let"}@{text + "p \ t"} statements, or by annotating assumptions or goal statements + with a list of patterns ``@{text "\ p\<^sub>1 \ p\<^sub>n"}''. + In both cases, higher-order matching is invoked to bind + extra-logical term variables, which may be either named schematic + variables of the form @{text ?x}, or nameless dummies ``@{variable + _}'' (underscore). Note that in the @{command "let"} form the + patterns occur on the left-hand side, while the @{keyword "is"} + patterns are in postfix position. + + 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 @{command "let"} may occur in \emph{arbitrary} + instances later. Even though actual polymorphism should be rarely + used in practice, this mechanism is essential to achieve proper + incremental type-inference, as the user proceeds to build up the + Isar proof text from left to right. + + \medskip Term abbreviations are quite different from local + definitions as introduced via @{command "def"} (see + \secref{sec:proof-context}). The latter are visible within the + logic as actual equations, while abbreviations disappear during the + input process just after type checking. Also note that @{command + "def"} does not support polymorphism. + + \begin{rail} + 'let' ((term + 'and') '=' term + 'and') + ; + \end{rail} + + The syntax of @{keyword "is"} patterns follows \railnonterm{termpat} + or \railnonterm{proppat} (see \secref{sec:term-decls}). + + \begin{descr} + + \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \ + \p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns + @{text "p\<^sub>1, \, p\<^sub>n"} by simultaneous higher-order + matching against terms @{text "t\<^sub>1, \, t\<^sub>n"}. + + \item [@{text "(\ p\<^sub>1 \ p\<^sub>n)"}] resembles @{command + "let"}, but matches @{text "p\<^sub>1, \, p\<^sub>n"} against the + preceding statement. Also note that @{keyword "is"} is not a + separate command, but part of others (such as @{command "assume"}, + @{command "have"} etc.). + + \end{descr} + + Some \emph{implicit} term abbreviations\index{term abbreviations} + for goals and facts are available as well. For any open goal, + @{variable_ref thesis} refers to its object-level statement, + abstracted over any meta-level parameters (if present). Likewise, + @{variable_ref this} is bound for fact statements resulting from + assumptions or finished goals. In case @{variable this} refers to + an object-logic statement that is an application @{text "f t"}, then + @{text t} is bound to the special text variable ``@{variable "\"}'' + (three dots). The canonical application of this convenience are + calculational proofs (see \secref{sec:calculation}). +*} + + +subsection {* Block structure *} + +text {* + \begin{matharray}{rcl} + @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\ + @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\ + @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\ + \end{matharray} + + While Isar is inherently block-structured, opening and closing + blocks is mostly handled rather casually, with little explicit + user-intervention. Any local goal statement automatically opens + \emph{two} internal blocks, which are closed again when concluding + the sub-proof (by @{command "qed"} etc.). Sections of different + context within a sub-proof may be switched via @{command "next"}, + which is just a single block-close followed by block-open again. + The effect of @{command "next"} is to reset the local proof context; + there is no goal focus involved here! + + For slightly more advanced applications, there are explicit block + parentheses as well. These typically achieve a stronger forward + style of reasoning. + + \begin{descr} + + \item [@{command "next"}] switches to a fresh block within a + sub-proof, resetting the local context to the initial one. + + \item [@{command "{"} and @{command "}"}] explicitly open and close + blocks. Any current facts pass through ``@{command "{"}'' + unchanged, while ``@{command "}"}'' causes any result to be + \emph{exported} into the enclosing context. Thus fixed variables + are generalized, assumptions discharged, and local definitions + unfolded (cf.\ \secref{sec:proof-context}). There is no difference + of @{command "assume"} and @{command "presume"} in this mode of + forward reasoning --- in contrast to plain backward reasoning with + the result exported at @{command "show"} time. + + \end{descr} +*} + + +subsection {* Emulating tactic scripts \label{sec:tactic-commands} *} + +text {* + The Isar provides separate commands to accommodate tactic-style + proof scripts within the same system. While being outside the + orthodox Isar proof language, these might come in handy for + interactive exploration and debugging, or even actual tactical proof + within new-style theories (to benefit from document preparation, for + example). See also \secref{sec:tactics} for actual tactics, that + have been encapsulated as proof methods. Proper proof methods may + be used in scripts, too. + + \begin{matharray}{rcl} + @{command_def "apply"}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ + @{command_def "apply_end"}^* & : & \isartrans{proof(state)}{proof(state)} \\ + @{command_def "done"}^* & : & \isartrans{proof(prove)}{proof(state)} \\ + @{command_def "defer"}^* & : & \isartrans{proof}{proof} \\ + @{command_def "prefer"}^* & : & \isartrans{proof}{proof} \\ + @{command_def "back"}^* & : & \isartrans{proof}{proof} \\ + \end{matharray} + + \begin{rail} + ( 'apply' | 'apply\_end' ) method + ; + 'defer' nat? + ; + 'prefer' nat + ; + \end{rail} + + \begin{descr} + + \item [@{command "apply"}~@{text m}] applies proof method @{text m} + in initial position, but unlike @{command "proof"} it retains + ``@{text "proof(prove)"}'' mode. Thus consecutive method + applications may be given just as in tactic scripts. + + Facts are passed to @{text m} as indicated by the goal's + forward-chain mode, and are \emph{consumed} afterwards. Thus any + further @{command "apply"} command would always work in a purely + backward manner. + + \item [@{command "apply_end"}~@{text "m"}] applies proof method + @{text m} as if in terminal position. Basically, this simulates a + multi-step tactic script for @{command "qed"}, but may be given + anywhere within the proof body. + + No facts are passed to @{method m} here. Furthermore, the static + context is that of the enclosing goal (as for actual @{command + "qed"}). Thus the proof method may not refer to any assumptions + introduced in the current body, for example. + + \item [@{command "done"}] completes a proof script, provided that + the current goal state is solved completely. Note that actual + structured proof commands (e.g.\ ``@{command "."}'' or @{command + "sorry"}) may be used to conclude proof scripts as well. + + \item [@{command "defer"}~@{text n} and @{command "prefer"}~@{text + n}] shuffle the list of pending goals: @{command "defer"} puts off + sub-goal @{text n} to the end of the list (@{text "n = 1"} by + default), while @{command "prefer"} brings sub-goal @{text n} to the + front. + + \item [@{command "back"}] does back-tracking over the result + sequence of the latest proof command. Basically, any proof command + may return multiple results. + + \end{descr} + + Any proper Isar proof method may be used with tactic script commands + such as @{command "apply"}. A few additional emulations of actual + tactics are provided as well; these would be never used in actual + structured proofs, of course. +*} + + +subsection {* Meta-linguistic features *} + +text {* + \begin{matharray}{rcl} + @{command_def "oops"} & : & \isartrans{proof}{theory} \\ + \end{matharray} + + The @{command "oops"} command discontinues the current proof + attempt, while considering the partial proof text as properly + processed. This is conceptually quite different from ``faking'' + actual proofs via @{command_ref "sorry"} (see + \secref{sec:proof-steps}): @{command "oops"} does not observe the + proof structure at all, but goes back right to the theory level. + Furthermore, @{command "oops"} does not produce any result theorem + --- there is no intended claim to be able to complete the proof + anyhow. + + A typical application of @{command "oops"} is to explain Isar proofs + \emph{within} the system itself, in conjunction with the document + preparation tools of Isabelle described in \cite{isabelle-sys}. + Thus partial or even wrong proof attempts can be discussed in a + logically sound manner. Note that the Isabelle {\LaTeX} macros can + be easily adapted to print something like ``@{text "\"}'' instead of + the keyword ``@{command "oops"}''. + + \medskip The @{command "oops"} command is undo-able, unlike + @{command_ref "kill"} (see \secref{sec:history}). The effect is to + get back to the theory just before the opening of the proof. +*} + + +section {* Other commands *} + +subsection {* Diagnostics *} + +text {* + \begin{matharray}{rcl} + \isarcmd{pr}^* & : & \isarkeep{\cdot} \\ + \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{prf}^* & : & \isarkeep{theory~|~proof} \\ + \isarcmd{full_prf}^* & : & \isarkeep{theory~|~proof} \\ + \end{matharray} + + These diagnostic commands assist interactive development. Note that + @{command undo} does not apply here, the theory or proof + configuration is not changed. + + \begin{rail} + 'pr' modes? nat? (',' nat)? + ; + 'thm' modes? thmrefs + ; + 'term' modes? term + ; + 'prop' modes? prop + ; + 'typ' modes? type + ; + 'prf' modes? thmrefs? + ; + 'full\_prf' modes? thmrefs? + ; + + modes: '(' (name + ) ')' + ; + \end{rail} + + \begin{descr} + + \item [@{command "pr"}~@{text "goals, prems"}] prints the current + proof state (if present), including the proof context, current facts + and goals. The optional limit arguments affect the number of goals + and premises to be displayed, which is initially 10 for both. + Omitting limit values leaves the current setting unchanged. + + \item [@{command "thm"}~@{text "a\<^sub>1 \ a\<^sub>n"}] retrieves + theorems from the current theory or proof context. Note that any + attributes included in the theorem specifications are applied to a + temporary context derived from the current theory or proof; the + result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1, + \, a\<^sub>n"} do not have any permanent effect. + + \item [@{command "term"}~@{text t} and @{command "prop"}~@{text \}] + read, type-check and print terms or propositions according to the + current theory or proof context; the inferred type of @{text t} is + output as well. Note that these commands are also useful in + inspecting the current environment of term abbreviations. + + \item [@{command "typ"}~@{text \}] reads and prints types of the + meta-logic according to the current theory or proof context. + + \item [@{command "prf"}] displays the (compact) proof term of the + current proof state (if present), or of the given theorems. Note + that this requires proof terms to be switched on for the current + object logic (see the ``Proof terms'' section of the Isabelle + reference manual for information on how to do this). + + \item [@{command "full_prf"}] is like @{command "prf"}, but displays + the full proof term, i.e.\ also displays information omitted in the + compact proof term, which is denoted by ``@{verbatim _}'' + placeholders there. + + \end{descr} + + All of the diagnostic commands above admit a list of @{text modes} + to be specified, which is appended to the current print mode (see + also \cite{isabelle-ref}). Thus the output behavior may be modified + according particular print mode features. For example, @{command + "pr"}~@{text "(latex xsymbols symbols)"} would print the current + proof state with mathematical symbols and special characters + represented in {\LaTeX} source, according to the Isabelle style + \cite{isabelle-sys}. + + Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more + systematic way to include formal items into the printed text + document. +*} + + +subsection {* Inspecting the context *} + +text {* + \begin{matharray}{rcl} + @{command_def "print_commands"}^* & : & \isarkeep{\cdot} \\ + @{command_def "print_theory"}^* & : & \isarkeep{theory~|~proof} \\ + @{command_def "print_syntax"}^* & : & \isarkeep{theory~|~proof} \\ + @{command_def "print_methods"}^* & : & \isarkeep{theory~|~proof} \\ + @{command_def "print_attributes"}^* & : & \isarkeep{theory~|~proof} \\ + @{command_def "print_theorems"}^* & : & \isarkeep{theory~|~proof} \\ + @{command_def "find_theorems"}^* & : & \isarkeep{theory~|~proof} \\ + @{command_def "thms_deps"}^* & : & \isarkeep{theory~|~proof} \\ + @{command_def "print_facts"}^* & : & \isarkeep{proof} \\ + @{command_def "print_binds"}^* & : & \isarkeep{proof} \\ + \end{matharray} + + \begin{rail} + 'print\_theory' ( '!'?) + ; + + 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *) + ; + criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | + 'simp' ':' term | term) + ; + 'thm\_deps' thmrefs + ; + \end{rail} + + These commands print certain parts of the theory and proof context. + Note that there are some further ones available, such as for the set + of rules declared for simplifications. + + \begin{descr} + + \item [@{command "print_commands"}] prints Isabelle's outer theory + syntax, including keywords and command. + + \item [@{command "print_theory"}] prints the main logical content of + the theory context; the ``@{text "!"}'' option indicates extra + verbosity. + + \item [@{command "print_syntax"}] prints the inner syntax of types + and terms, depending on the current context. The output can be very + verbose, including grammar tables and syntax translation rules. See + \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's + inner syntax. + + \item [@{command "print_methods"}] prints all proof methods + available in the current theory context. + + \item [@{command "print_attributes"}] prints all attributes + available in the current theory context. + + \item [@{command "print_theorems"}] prints theorems resulting from + the last command. + + \item [@{command "find_theorems"}~@{text criteria}] retrieves facts + from the theory or proof context matching all of given search + criteria. The criterion @{text "name: p"} selects all theorems + whose fully qualified name matches pattern @{text p}, which may + contain ``@{text "*"}'' wildcards. The criteria @{text intro}, + @{text elim}, and @{text dest} select theorems that match the + current goal as introduction, elimination or destruction rules, + respectively. The criterion @{text "simp: t"} selects all rewrite + rules whose left-hand side matches the given term. The criterion + term @{text t} selects all theorems that contain the pattern @{text + t} -- as usual, patterns may contain occurrences of the dummy + ``@{verbatim _}'', schematic variables, and type constraints. + + Criteria can be preceded by ``@{text "-"}'' to select theorems that + do \emph{not} match. Note that giving the empty list of criteria + yields \emph{all} currently known facts. An optional limit for the + number of printed facts may be given; the default is 40. By + default, duplicates are removed from the search result. Use + @{keyword "with_dups"} to display duplicates. + + \item [@{command "thm_deps"}~@{text "a\<^sub>1 \ a\<^sub>n"}] + visualizes dependencies of facts, using Isabelle's graph browser + tool (see also \cite{isabelle-sys}). + + \item [@{command "print_facts"}] prints all local facts of the + current context, both named and unnamed ones. + + \item [@{command "print_binds"}] prints all term abbreviations + present in the context. + + \end{descr} +*} + + +subsection {* History commands \label{sec:history} *} + +text {* + \begin{matharray}{rcl} + @{command_def "undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + @{command_def "redo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + @{command_def "kill"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\ + \end{matharray} + + The Isabelle/Isar top-level maintains a two-stage history, for + theory and proof state transformation. Basically, any command can + be undone using @{command "undo"}, excluding mere diagnostic + elements. Its effect may be revoked via @{command "redo"}, unless + the corresponding @{command "undo"} step has crossed the beginning + of a proof or theory. The @{command "kill"} command aborts the + current history node altogether, discontinuing a proof or even the + whole theory. This operation is \emph{not} undo-able. + + \begin{warn} + History commands should never be used with user interfaces such as + Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes + care of stepping forth and back itself. Interfering by manual + @{command "undo"}, @{command "redo"}, or even @{command "kill"} + commands would quickly result in utter confusion. + \end{warn} +*} + + +subsection {* System operations *} + +text {* + \begin{matharray}{rcl} + @{command_def "cd"}^* & : & \isarkeep{\cdot} \\ + @{command_def "pwd"}^* & : & \isarkeep{\cdot} \\ + @{command_def "use_thy"}^* & : & \isarkeep{\cdot} \\ + @{command_def "display_drafts"}^* & : & \isarkeep{\cdot} \\ + @{command_def "print_drafts"}^* & : & \isarkeep{\cdot} \\ + \end{matharray} + + \begin{rail} + ('cd' | 'use\_thy' | 'update\_thy') name + ; + ('display\_drafts' | 'print\_drafts') (name +) + ; + \end{rail} + + \begin{descr} + + \item [@{command "cd"}~@{text path}] changes the current directory + of the Isabelle process. + + \item [@{command "pwd"}] prints the current working directory. + + \item [@{command "use_thy"}~@{text A}] preload theory @{text A}. + These system commands are scarcely used when working interactively, + since loading of theories is done automatically as required. + + \item [@{command "display_drafts"}~@{text paths} and @{command + "print_drafts"}~@{text paths}] perform simple output of a given list + of raw source files. Only those symbols that do not require + additional {\LaTeX} packages are displayed properly, everything else + is left verbatim. + + \end{descr} +*} + +end diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/Thy/syntax.thy --- a/doc-src/IsarRef/Thy/syntax.thy Fri May 02 16:32:51 2008 +0200 +++ b/doc-src/IsarRef/Thy/syntax.thy Fri May 02 16:36:05 2008 +0200 @@ -1,3 +1,4 @@ +(* $Id$ *) theory "syntax" imports CPure diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/isar-ref.tex --- a/doc-src/IsarRef/isar-ref.tex Fri May 02 16:32:51 2008 +0200 +++ b/doc-src/IsarRef/isar-ref.tex Fri May 02 16:36:05 2008 +0200 @@ -71,7 +71,7 @@ \input{Thy/document/intro.tex} \input{basics.tex} \input{Thy/document/syntax.tex} -\input{pure.tex} +\input{Thy/document/pure.tex} \input{generic.tex} \input{logics.tex} diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/pure.tex --- a/doc-src/IsarRef/pure.tex Fri May 02 16:32:51 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1636 +0,0 @@ - -\chapter{Basic language elements}\label{ch:pure-syntax} - -Subsequently, we introduce the main part of Pure theory and proof 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 in most object logics. Chapter~\ref{ch:logics} -refers to object-logic specific elements (mainly for HOL and ZF). - -\medskip - -Isar commands may be either \emph{proper} document constructors, or -\emph{improper commands}. Some proof methods and attributes introduced later -are classified as improper as well. Improper Isar language elements, which -are subsequently marked by ``$^*$'', are often helpful when developing proof -documents, while their use is discouraged for the final human-readable -outcome. Typical examples are diagnostic commands that print terms or -theorems according to the current context; other commands emulate old-style -tactical theorem proving. - - -\section{Theory commands} - -\subsection{Defining theories}\label{sec:begin-thy} - -\indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{end} -\begin{matharray}{rcl} - \isarcmd{header} & : & \isarkeep{toplevel} \\ - \isarcmd{theory} & : & \isartrans{toplevel}{theory} \\ - \isarcmd{end} & : & \isartrans{theory}{toplevel} \\ -\end{matharray} - -Isabelle/Isar ``new-style'' theories are either defined via theory files or -interactively. Both theory-level specifications and proofs are handled -uniformly --- occasionally definitional mechanisms even require some explicit -proof as well. In contrast, ``old-style'' Isabelle theories support batch -processing only, with the proof scripts collected in separate ML files. - -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$ -command concludes a theory development; it has to be the very last -command of any theory file loaded in batch-mode. - -\begin{rail} - 'header' text - ; - 'theory' name 'imports' (name +) uses? 'begin' - ; - - uses: 'uses' ((name | parname) +); -\end{rail} - -\begin{descr} -\item [$\isarkeyword{header}~text$] provides plain text markup just preceding - the formal beginning of a theory. In actual document preparation the - corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to - 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~\isarkeyword{imports}~B@1~\ldots~B@n~\isarkeyword{begin}$] - 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{uses}$ 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{uses}$ dependency declaration, though. - -\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. - -\end{descr} - - -\subsection{Markup commands}\label{sec:markup-thy} - -\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection} -\indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw} -\begin{matharray}{rcl} - \isarcmd{chapter} & : & \isarkeep{local{\dsh}theory} \\ - \isarcmd{section} & : & \isarkeep{local{\dsh}theory} \\ - \isarcmd{subsection} & : & \isarkeep{local{\dsh}theory} \\ - \isarcmd{subsubsection} & : & \isarkeep{local{\dsh}theory} \\ - \isarcmd{text} & : & \isarkeep{local{\dsh}theory} \\ - \isarcmd{text_raw} & : & \isarkeep{local{\dsh}theory} \\ -\end{matharray} - -Apart from formal comments (see \S\ref{sec:comments}), markup commands provide -a structured way to insert text into the document generated from a theory (see -\cite{isabelle-sys} for more information on Isabelle's document preparation -tools). - -\begin{rail} - ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') target? text - ; - 'text\_raw' text - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{chapter}$, $\isarkeyword{section}$, - $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter - and section headings. -\item [$\TEXT$] specifies paragraphs of plain text. -\item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output, - without additional markup. Thus the full range of document manipulations - becomes available. -\end{descr} - -The $text$ argument of these markup commands (except for -$\isarkeyword{text_raw}$) may contain references to formal entities -(``antiquotations'', see also \S\ref{sec:antiq}). These are -interpreted in the present theory context, or the specified $target$. - -Any of these markup elements corresponds to a {\LaTeX} command with the name -prefixed by \verb,\isamarkup,. For the sectioning commands this is a plain -macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for -$\isarkeyword{chapter}$. The $\isarkeyword{text}$ markup results in a -{\LaTeX} environment \verb,\begin{isamarkuptext}, {\dots} - \verb,\end{isamarkuptext},, while $\isarkeyword{text_raw}$ causes the text -to be inserted directly into the {\LaTeX} source. - -\medskip - -Additional markup commands are available for proofs (see -\S\ref{sec:markup-prf}). Also note that the $\isarkeyword{header}$ -declaration (see \S\ref{sec:begin-thy}) admits to insert section markup just -preceding the actual theory definition. - - -\subsection{Type classes and sorts}\label{sec:classes} - -\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort} -\indexisarcmd{class-deps} -\begin{matharray}{rcll} - \isarcmd{classes} & : & \isartrans{theory}{theory} \\ - \isarcmd{classrel} & : & \isartrans{theory}{theory} & (axiomatic!) \\ - \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\ - \isarcmd{class_deps} & : & \isarkeep{theory~|~proof} \\ -\end{matharray} - -\begin{rail} - 'classes' (classdecl +) - ; - 'classrel' (nameref ('<' | subseteq) nameref + 'and') - ; - 'defaultsort' sort - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{classes}~c \subseteq \vec c$] declares class $c$ to be a - subclass of existing classes $\vec c$. Cyclic class structures are ruled - out. -\item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states subclass relations - between existing classes $c@1$ and $c@2$. This is done axiomatically! The - $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce - 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 a new object-logic. -\item [$\isarkeyword{class_deps}$] visualizes the subclass relation, - using Isabelle's graph browser tool (see also \cite{isabelle-sys}). -\end{descr} - - -\subsection{Primitive types and type abbreviations}\label{sec:types-pure} - -\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities} -\begin{matharray}{rcll} - \isarcmd{types} & : & \isartrans{theory}{theory} \\ - \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\ - \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\ - \isarcmd{arities} & : & \isartrans{theory}{theory} & (axiomatic!) \\ -\end{matharray} - -\begin{rail} - 'types' (typespec '=' type infix? +) - ; - 'typedecl' typespec infix? - ; - 'nonterminals' (name +) - ; - 'arities' (nameref '::' arity +) - ; -\end{rail} - -\begin{descr} - -\item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym} - $(\vec\alpha)t$ for existing type $\tau$. Unlike actual type definitions, - as are available in Isabelle/HOL for example, type synonyms are just purely - syntactic abbreviations without any logical significance. Internally, type - synonyms are fully expanded. - -\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor - $t$, intended as an actual logical type. Note that the Isabelle/HOL - object-logic overrides $\isarkeyword{typedecl}$ by its own version - (\S\ref{sec:hol-typedef}). - -\item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors - $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of - Isabelle's inner syntax of terms or types. - -\item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted - signature of types by new type constructor arities. This is done - axiomatically! The $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a - way to introduce proven type arities. - -\end{descr} - - -\subsection{Primitive constants and definitions}\label{sec:consts} - -Definitions essentially express abbreviations within the logic. The -simplest form of a definition is $f :: \sigma \equiv t$, where $f$ is -a newly declared constant. Isabelle also allows derived forms where -the arguments of~$f$ appear on the left, abbreviating a string of -$\lambda$-abstractions, e.g.\ $f \equiv \lambda x\, y. t$ may be -written more conveniently as $f \, x \, y \equiv t$. Moreover, -definitions may be weakened by adding arbitrary pre-conditions: $A -\Imp f \, x\, y \equiv t$. - -\medskip The built-in well-formedness conditions for definitional -specifications are: -\begin{itemize} -\item Arguments (on the left-hand side) must be distinct variables. -\item All variables on the right-hand side must also appear on the - left-hand side. -\item All type variables on the right-hand side must also appear on - the left-hand side; this prohibits $0::nat \equiv length - ([]::\alpha\, list)$ for example. -\item The definition must not be recursive. Most object-logics - provide definitional principles that can be used to express - recursion safely. -\end{itemize} - -Overloading means that a constant being declared as $c :: \alpha\, -decl$ may be defined separately on type instances $c :: -(\vec\beta)\,t\,decl$ for each type constructor $t$. The RHS may -mention overloaded constants recursively at type instances -corresponding to the immediate argument types $\vec\beta$. Incomplete -specification patterns impose global constraints on all occurrences, -e.g. $d :: \alpha \times \alpha$ on the LHS means that all -corresponding occurrences on some RHS need to be an instance of this, -general $d :: \alpha \times \beta$ will be disallowed. - -\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl} -\begin{matharray}{rcl} - \isarcmd{consts} & : & \isartrans{theory}{theory} \\ - \isarcmd{defs} & : & \isartrans{theory}{theory} \\ - \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\begin{rail} - 'consts' ((name '::' type mixfix?) +) - ; - 'defs' ('(' 'unchecked'? 'overloaded'? ')')? \\ (axmdecl prop +) - ; -\end{rail} - -\begin{rail} - 'constdefs' structs? (constdecl? constdef +) - ; - - structs: '(' 'structure' (vars + 'and') ')' - ; - constdecl: ((name '::' type mixfix | name '::' type | name mixfix) 'where'?) | name 'where' - ; - constdef: thmdecl? prop - ; -\end{rail} - -\begin{descr} -\item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type - scheme $\sigma$. The optional mixfix annotations may attach concrete syntax - to the constants declared. - -\item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for - some existing constant. - - The $(unchecked)$ option disables global dependency checks for this - definition, which is occasionally useful for exotic overloading. It - is at the discretion of the user to avoid malformed theory - specifications! - - The $(overloaded)$ option declares definitions to be potentially - overloaded. 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 [$\CONSTDEFS$] provides a streamlined combination of constants - declarations and definitions: type-inference takes care of the most general - typing of the given specification (the optional type constraint may refer to - type-inference dummies ``$_$'' as usual). The resulting type declaration - needs to agree with that of the specification; overloading is \emph{not} - supported here! - - The constant name may be omitted altogether, if neither type nor syntax - declarations are given. The canonical name of the definitional axiom for - constant $c$ will be $c_def$, unless specified otherwise. Also note that - the given list of specifications is processed in a strictly sequential - manner, with type-checking being performed independently. - - An optional initial context of $(structure)$ declarations admits use of - indexed syntax, using the special symbol \verb,\, (printed as - ``\i''). The latter concept is particularly useful with locales (see also - \S\ref{sec:locale}). -\end{descr} - - -\subsection{Syntax and translations}\label{sec:syn-trans} - -\indexisarcmd{syntax}\indexisarcmd{no-syntax} -\indexisarcmd{translations}\indexisarcmd{no-translations} -\begin{matharray}{rcl} - \isarcmd{syntax} & : & \isartrans{theory}{theory} \\ - \isarcmd{no_syntax} & : & \isartrans{theory}{theory} \\ - \isarcmd{translations} & : & \isartrans{theory}{theory} \\ - \isarcmd{no_translations} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\railalias{rightleftharpoons}{\isasymrightleftharpoons} -\railterm{rightleftharpoons} - -\railalias{rightharpoonup}{\isasymrightharpoonup} -\railterm{rightharpoonup} - -\railalias{leftharpoondown}{\isasymleftharpoondown} -\railterm{leftharpoondown} - -\begin{rail} - ('syntax' | 'no\_syntax') mode? (constdecl +) - ; - ('translations' | 'no\_translations') (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +) - ; - - mode: ('(' ( name | 'output' | name 'output' ) ')') - ; - transpat: ('(' nameref ')')? string - ; -\end{rail} - -\begin{descr} - -\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$, - except that the actual logical signature extension is omitted. Thus the - context free grammar of Isabelle's inner syntax may be augmented in - arbitrary ways, independently of the logic. The $mode$ argument refers to - the print mode that the grammar rules belong; unless the - $\isarkeyword{output}$ indicator is given, all productions are added both to - the input and output grammar. - -\item [$\isarkeyword{no_syntax}~(mode)~decls$] removes grammar declarations - (and translations) resulting from $decls$, which are interpreted in the same - manner as for $\isarkeyword{syntax}$ above. - -\item [$\isarkeyword{translations}~rules$] specifies syntactic translation - rules (i.e.\ macros): parse~/ print rules (\isasymrightleftharpoons), parse - rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown). - Translation patterns may be prefixed by the syntactic category to be used - for parsing; the default is $logic$. - -\item [$\isarkeyword{no_translations}~rules$] removes syntactic - translation rules, which are interpreted in the same manner as for - $\isarkeyword{translations}$ above. - -\end{descr} - - -\subsection{Axioms and theorems}\label{sec:axms-thms} - -\indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems} -\begin{matharray}{rcll} - \isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\ - \isarcmd{lemmas} & : & \isarkeep{local{\dsh}theory} \\ - \isarcmd{theorems} & : & isarkeep{local{\dsh}theory} \\ -\end{matharray} - -\begin{rail} - 'axioms' (axmdecl prop +) - ; - ('lemmas' | 'theorems') target? (thmdef? thmrefs + 'and') - ; -\end{rail} - -\begin{descr} - -\item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as - axioms of the meta-logic. In fact, axioms are ``axiomatic theorems'', and - may be referred later just as any other theorem. - - Axioms are usually only introduced when declaring new logical systems. - Everyday work is typically done the hard way, with proper definitions and - proven theorems. - -\item [$\isarkeyword{lemmas}~a = \vec b$] retrieves and stores - existing facts in the theory context, or the specified target - context (see also \S\ref{sec:target}). Typical applications would - also involve attributes, to declare Simplifier rules, for example. - -\item [$\isarkeyword{theorems}$] is essentially the same as - $\isarkeyword{lemmas}$, but marks the result as a different kind of facts. - -\end{descr} - - -\subsection{Name spaces} - -\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide} -\begin{matharray}{rcl} - \isarcmd{global} & : & \isartrans{theory}{theory} \\ - \isarcmd{local} & : & \isartrans{theory}{theory} \\ - \isarcmd{hide} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\begin{rail} - 'hide' ('(open)')? name (nameref + ) - ; -\end{rail} - -Isabelle organizes any kind of name declarations (of types, constants, -theorems etc.) by separate hierarchically structured name spaces. Normally -the user does not have to control the behavior of name spaces by hand, yet the -following commands provide some way to do so. - -\begin{descr} -\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current - name declaration mode. Initially, theories start in $\isarkeyword{local}$ - mode, causing all names to be automatically qualified by the theory name. - Changing this to $\isarkeyword{global}$ causes all names to be declared - without the theory prefix, until $\isarkeyword{local}$ is declared again. - - Note that global names are prone to get hidden accidently later, when - qualified names of the same base name are introduced. - -\item [$\isarkeyword{hide}~space~names$] fully removes declarations - from a given name space (which may be $class$, $type$, $const$, or - $fact$); with the $(open)$ option, only the base name is hidden. - Global (unqualified) names may never be hidden. - - Note that hiding name space accesses has no impact on logical declarations - -- they remain valid internally. Entities that are no longer accessible to - the user are printed with the special qualifier ``$\mathord?\mathord?$'' - prefixed to the full internal name. -\end{descr} - - -\subsection{Incorporating ML code}\label{sec:ML} - -\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-val}\indexisarcmd{ML-command} -\indexisarcmd{setup}\indexisarcmd{method-setup} -\begin{matharray}{rcl} - \isarcmd{use} & : & \isarkeep{theory~|~local{\dsh}theory} \\ - \isarcmd{ML} & : & \isarkeep{theory~|~local{\dsh}theory} \\ - \isarcmd{ML_val} & : & \isartrans{\cdot}{\cdot} \\ - \isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\ - \isarcmd{setup} & : & \isartrans{theory}{theory} \\ - \isarcmd{method_setup} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\begin{rail} - 'use' name - ; - ('ML' | 'ML\_val' | 'ML\_command' | 'setup') text - ; - 'method\_setup' name '=' text text - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{use}~file$] reads and executes ML commands from - $file$. The current theory context is passed down to the ML - toplevel and may be modified, using \verb,Context.>>, or any other - ML commands derived from it. The file name is checked with the - $\isarkeyword{uses}$ dependency declaration given in the theory - header (see also \S\ref{sec:begin-thy}). - -\item [$\isarkeyword{ML}~text$] is similar to $\isarkeyword{use}$, but - executes ML commands from the given $text$. - -\item [$\isarkeyword{ML_val}$ and $\isarkeyword{ML_command}$] are - diagnostic versions of $\isarkeyword{ML}$, which means that the - context may not be updated. $\isarkeyword{ML_val}$ echos the - bindings produced at the ML toplevel, but $\isarkeyword{ML_command}$ - is silent. - -\item [$\isarkeyword{setup}~text$] changes the current theory context - by applying $text$, which refers to an ML expression of type - \texttt{theory~->~theory)}. The $\isarkeyword{setup}$ command is - the canonical way to initialize any object-logic specific tools and - packages written in ML. - -\item [$\isarkeyword{method_setup}~name = text~description$] defines a proof - method in the current theory. The given $text$ has to be an ML expression - of type \texttt{Args.src -> Proof.context -> Proof.method}. Parsing - concrete method syntax from \texttt{Args.src} input can be quite tedious in - general. The following simple examples are for methods without any explicit - arguments, or a list of theorems, respectively. - -{\footnotesize -\begin{verbatim} - Method.no_args (Method.METHOD (fn facts => foobar_tac)) - Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac)) - Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac)) - Method.thms_ctxt_args (fn thms => fn ctxt => - Method.METHOD (fn facts => foobar_tac)) -\end{verbatim} -} - -Note that mere tactic emulations may ignore the \texttt{facts} parameter -above. Proper proof methods would do something appropriate with the list of -current facts, though. Single-rule methods usually do strict forward-chaining -(e.g.\ by using \texttt{Method.multi_resolves}), while automatic ones just -insert the facts using \texttt{Method.insert_tac} before applying the main -tactic. -\end{descr} - - -\subsection{Syntax translation functions} - -\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation} -\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation} -\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation} -\begin{matharray}{rcl} - \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\ - \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\ - \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\ - \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\ - \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\ - \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -\railalias{parseasttranslation}{parse\_ast\_translation} -\railterm{parseasttranslation} - -\railalias{parsetranslation}{parse\_translation} -\railterm{parsetranslation} - -\railalias{printtranslation}{print\_translation} -\railterm{printtranslation} - -\railalias{typedprinttranslation}{typed\_print\_translation} -\railterm{typedprinttranslation} - -\railalias{printasttranslation}{print\_ast\_translation} -\railterm{printasttranslation} - -\railalias{tokentranslation}{token\_translation} -\railterm{tokentranslation} - -\begin{rail} - ( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation | - printasttranslation ) ('(advanced)')? text; - - tokentranslation text -\end{rail} - -Syntax translation functions written in ML admit almost arbitrary -manipulations of Isabelle's inner syntax. Any of the above commands have a -single \railqtok{text} argument that refers to an ML expression of appropriate -type, which are as follows by default: - -\begin{ttbox} -val parse_ast_translation : (string * (ast list -> ast)) list -val parse_translation : (string * (term list -> term)) list -val print_translation : (string * (term list -> term)) list -val typed_print_translation : - (string * (bool -> typ -> term list -> term)) list -val print_ast_translation : (string * (ast list -> ast)) list -val token_translation : - (string * string * (string -> string * real)) list -\end{ttbox} - -In case that the $(advanced)$ option is given, the corresponding -translation functions may depend on the current theory or proof -context. This allows to implement advanced syntax mechanisms, as -translations functions may refer to specific theory declarations or -auxiliary proof data. - -See also \cite[\S8]{isabelle-ref} for more information on the general concept -of syntax transformations in Isabelle. - -\begin{ttbox} -val parse_ast_translation: - (string * (Context.generic -> ast list -> ast)) list -val parse_translation: - (string * (Context.generic -> term list -> term)) list -val print_translation: - (string * (Context.generic -> term list -> term)) list -val typed_print_translation: - (string * (Context.generic -> bool -> typ -> term list -> term)) list -val print_ast_translation: - (string * (Context.generic -> ast list -> ast)) list -\end{ttbox} - - -\subsection{Oracles} - -\indexisarcmd{oracle} -\begin{matharray}{rcl} - \isarcmd{oracle} & : & \isartrans{theory}{theory} \\ -\end{matharray} - -The oracle interface promotes a given ML function \texttt{theory -> T -> term} -to \texttt{theory -> T -> thm}, for some type \texttt{T} given by the user. -This acts like an infinitary specification of axioms -- there is no internal -check of the correctness of the results! The inference kernel records oracle -invocations within the internal derivation object of theorems, and the pretty -printer attaches ``\texttt{[!]}'' to indicate results that are not fully -checked by Isabelle inferences. - -\begin{rail} - 'oracle' name '(' type ')' '=' text - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{oracle}~name~(type)=~text$] turns the given ML expression - $text$ of type \texttt{theory~->~$type$~->~term} into an ML function $name$ - of type \texttt{theory~->~$type$~->~thm}. -\end{descr} - - -\section{Proof commands} - -Proof commands perform transitions of Isar/VM machine configurations, which -are block-structured, consisting of a stack of nodes with three main -components: logical proof context, current facts, and open goals. Isar/VM -transitions are \emph{typed} according to the following three different modes -of operation: -\begin{descr} -\item [$proof(prove)$] means that a new goal has just been stated that is now - to be \emph{proven}; the next command may refine it by some proof method, - and enter a sub-proof to establish the actual result. -\item [$proof(state)$] is like a nested theory mode: the context may be - augmented by \emph{stating} additional assumptions, intermediate results - etc. -\item [$proof(chain)$] is intermediate between $proof(state)$ and - $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$'' - register) have been just picked up in order to be used when refining the - goal claimed next. -\end{descr} - -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 of a certain structure. Appendix~\ref{ap:refcard} gives a simplified -grammar of the overall (extensible) language emerging that way. - - -\subsection{Markup commands}\label{sec:markup-prf} - -\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect} -\indexisarcmd{txt}\indexisarcmd{txt-raw} -\begin{matharray}{rcl} - \isarcmd{sect} & : & \isartrans{proof}{proof} \\ - \isarcmd{subsect} & : & \isartrans{proof}{proof} \\ - \isarcmd{subsubsect} & : & \isartrans{proof}{proof} \\ - \isarcmd{txt} & : & \isartrans{proof}{proof} \\ - \isarcmd{txt_raw} & : & \isartrans{proof}{proof} \\ -\end{matharray} - -These markup commands for proof mode closely correspond to the ones of theory -mode (see \S\ref{sec:markup-thy}). - -\railalias{txtraw}{txt\_raw} -\railterm{txtraw} - -\begin{rail} - ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text - ; -\end{rail} - - -\subsection{Context elements}\label{sec:proof-context} - -\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def} -\begin{matharray}{rcl} - \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\ -\end{matharray} - -The logical proof context consists of fixed variables and assumptions. The -former closely correspond to Skolem constants, or meta-level universal -quantification as provided by the Isabelle/Pure logical framework. -Introducing some \emph{arbitrary, but fixed} variable via ``$\FIX x$'' results -in a local value that may be used in the subsequent proof as any other -variable or constant. Furthermore, any result $\edrv \phi[x]$ exported from -the context will be universally closed wrt.\ $x$ at the outermost level: -$\edrv \All x \phi$ (this is expressed using Isabelle's meta-variables). - -Similarly, introducing some assumption $\chi$ has two effects. On the one -hand, a local theorem is created that may be used as a fact in subsequent -proof steps. On the other hand, any result $\chi \drv \phi$ exported from the -context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$. -Thus, solving an enclosing goal using such a result would basically introduce -a new subgoal stemming from the assumption. How this situation is handled -depends on the actual version of assumption command used: while $\ASSUMENAME$ -insists on solving the subgoal by unification with some premise of the goal, -$\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the -user. - -Local definitions, introduced by ``$\DEF{}{x \equiv t}$'', are achieved by -combining ``$\FIX x$'' with another version of assumption that causes any -hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule. -Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$. - -\railalias{equiv}{\isasymequiv} -\railterm{equiv} - -\begin{rail} - 'fix' (vars + 'and') - ; - ('assume' | 'presume') (props + 'and') - ; - 'def' (def + 'and') - ; - def: thmdecl? \\ name ('==' | equiv) term termpat? - ; -\end{rail} - -\begin{descr} - -\item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables - $\vec x$. - -\item [$\ASSUME{a}{\vec\phi}$ and $\PRESUME{a}{\vec\phi}$] introduce local - theorems $\vec\phi$ by assumption. Subsequent results applied to an - enclosing goal (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ - expects to be able to unify with existing premises in the goal, while - $\PRESUMENAME$ leaves $\vec\phi$ as new subgoals. - - Several lists of assumptions may be given (separated by - $\isarkeyword{and}$); the resulting list of current facts consists of all of - these concatenated. - -\item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition. - In results exported from the context, $x$ is replaced by $t$. Basically, - ``$\DEF{}{x \equiv t}$'' abbreviates ``$\FIX{x}~\ASSUME{}{x \equiv t}$'', - with the resulting hypothetical equation solved by reflexivity. - - The default name for the definitional equation is $x_def$. Several - simultaneous definitions may be given at the same time. - -\end{descr} - -The special name $prems$\indexisarthm{prems} refers to all assumptions of the -current context as a list of theorems. - - -\subsection{Facts and forward chaining} - -\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with} -\indexisarcmd{using}\indexisarcmd{unfolding} -\begin{matharray}{rcl} - \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\ - \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\ - \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\ - \isarcmd{using} & : & \isartrans{proof(prove)}{proof(prove)} \\ - \isarcmd{unfolding} & : & \isartrans{proof(prove)}{proof(prove)} \\ -\end{matharray} - -New facts are established either by assumption or proof of local statements. -Any fact will usually be involved in further proofs, either as explicit -arguments of proof methods, or when forward chaining towards the next goal via -$\THEN$ (and variants); $\FROMNAME$ and $\WITHNAME$ are composite forms -involving $\NOTENAME$. The $\USINGNAME$ elements augments the collection of -used facts \emph{after} a goal has been stated. Note that the special theorem -name $this$\indexisarthm{this} refers to the most recently established facts, -but only \emph{before} issuing a follow-up claim. - -\begin{rail} - 'note' (thmdef? thmrefs + 'and') - ; - ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and') - ; -\end{rail} - -\begin{descr} - -\item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result - as $a$. Note that attributes may be involved as well, both on the left and - right hand sides. - -\item [$\THEN$] indicates forward chaining by the current facts in order to - establish the goal to be claimed next. The initial proof method invoked to - refine that will be offered the facts to do ``anything appropriate'' (see - also \S\ref{sec:proof-steps}). For example, method $rule$ (see - \S\ref{sec:pure-meth-att}) would typically do an elimination rather than an - introduction. Automatic methods usually insert the facts into the goal - state before operation. This provides a simple scheme to control relevance - of facts in automated proof search. - -\item [$\FROM{\vec b}$] abbreviates ``$\NOTE{}{\vec b}~\THEN$''; thus $\THEN$ - is equivalent to ``$\FROM{this}$''. - -\item [$\WITH{\vec b}$] abbreviates ``$\FROM{\vec b~\AND~this}$''; thus the - forward chaining is from earlier facts together with the current ones. - -\item [$\USING{\vec b}$] augments the facts being currently indicated - for use by a subsequent refinement step (such as $\APPLYNAME$ or - $\PROOFNAME$). - -\item [$\UNFOLDING{\vec b}$] is structurally similar to $\USINGNAME$, - but unfolds definitional equations $\vec b$ throughout the goal - state and facts. - -\end{descr} - -Forward chaining with an empty list of theorems is the same as not chaining at -all. Thus ``$\FROM{nothing}$'' has no effect apart from entering -$prove(chain)$ mode, since $nothing$\indexisarthm{nothing} is bound to the -empty list of theorems. - -Basic proof methods (such as $rule$) expect multiple facts to be given in -their proper order, corresponding to a prefix of the premises of the rule -involved. Note that positions may be easily skipped using something like -$\FROM{\Text{\texttt{_}}~a~b}$, for example. This involves the trivial rule -$\PROP\psi \Imp \PROP\psi$, which happens to be bound in Isabelle/Pure as -``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}} - -Automated methods (such as $simp$ or $auto$) just insert any given facts -before their usual operation. Depending on the kind of procedure involved, -the order of facts is less significant here. - - -\subsection{Goal statements}\label{sec:goals} - -\indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary} -\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus} -\indexisarcmd{print-statement} -\begin{matharray}{rcl} - \isarcmd{lemma} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ - \isarcmd{theorem} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ - \isarcmd{corollary} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\ - \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ - \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\ - \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\ - \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\ - \isarcmd{print_statement}^* & : & \isarkeep{theory~|~proof} \\ -\end{matharray} - -From a theory context, proof mode is entered by an initial goal command such -as $\LEMMANAME$, $\THEOREMNAME$, or $\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 final 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 -conjunction (printed as \verb,&&,), which is usually split into the -corresponding number of sub-goals prior to an initial method application, via -$\PROOFNAME$ (\S\ref{sec:proof-steps}) or $\APPLYNAME$ -(\S\ref{sec:tactic-commands}). The $induct$ method covered in -\S\ref{sec:cases-induct} acts on multiple claims simultaneously. - -Claims at the theory level may be either in short or long form. A -short goal merely consists of several simultaneous propositions (often -just one). A long goal includes an explicit context specification for -the subsequent conclusion, involving local parameters and assumptions. -Here the role of each part of the statement is explicitly marked by -separate keywords (see also \S\ref{sec:locale}); the local assumptions -being introduced here are available as $assms$\indexisarthm{assms} in -the proof. \indexisarelem{shows}\indexisarelem{obtains}Moreover, -there are two kinds of conclusions: $\isarkeyword{shows}$ states -several simultaneous propositions (essentially a big conjunction), -while $\isarkeyword{obtains}$ claims several simultaneous simultaneous -contexts of (essentially a big disjunction of eliminated parameters -and assumptions, cf.\ \S\ref{sec:obtain}). - -\begin{rail} - ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal) - ; - ('have' | 'show' | 'hence' | 'thus') goal - ; - 'print\_statement' modes? thmrefs - ; - - goal: (props + 'and') - ; - longgoal: thmdecl? (contextelem *) conclusion - ; - conclusion: 'shows' goal | 'obtains' (parname? case + '|') - ; - case: (vars + 'and') 'where' (props + 'and') - ; -\end{rail} - -\begin{descr} - -\item [$\LEMMA{a}{\vec\phi}$] enters proof mode with $\vec\phi$ as main goal, - eventually resulting in some fact $\turn \vec\phi$ to be put back into the - theory context, or into the specified locale (cf.\ \S\ref{sec:locale}). An - additional \railnonterm{context} specification may build up an initial proof - context for the subsequent claim; this includes 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 - being of a different kind. This discrimination acts like a formal comment. - -\item [$\HAVE{a}{\vec\phi}$] claims a local goal, eventually resulting in a - fact within the current logical context. This operation is completely - independent of any pending sub-goals of an enclosing goal statements, so - $\HAVENAME$ may be freely used for experimental exploration of potential - results within a proof body. - -\item [$\SHOW{a}{\vec\phi}$] is like $\HAVE{a}{\vec\phi}$ plus a second stage - to refine some pending sub-goal for each one of the finished result, after - having been exported into the corresponding context (at the head of the - sub-proof of this $\SHOWNAME$ command). - - To accommodate interactive debugging, resulting rules are printed before - being applied internally. Even more, interactive execution of $\SHOWNAME$ - predicts potential failure and displays the resulting error as a warning - beforehand. Watch out for the following message: - - \begin{ttbox} - Problem! Local statement will fail to solve any pending goal - \end{ttbox} - -\item [$\HENCENAME$] abbreviates ``$\THEN~\HAVENAME$'', i.e.\ claims a local - goal to be proven by forward chaining the current facts. Note that - $\HENCENAME$ is also equivalent to ``$\FROM{this}~\HAVENAME$''. - -\item [$\THUSNAME$] abbreviates ``$\THEN~\SHOWNAME$''. Note that $\THUSNAME$ - is also equivalent to ``$\FROM{this}~\SHOWNAME$''. - -\item [$\isarkeyword{print_statement}~\vec a$] prints theorems from - the current theory or proof context in long statement form, - according to the syntax for $\isarkeyword{lemma}$ given above. - -\end{descr} - -Any goal statement causes some term abbreviations (such as $\Var{thesis}$) to -be bound automatically, see also \S\ref{sec:term-abbrev}. Furthermore, the -local context of a (non-atomic) goal is provided via the -$rule_context$\indexisarcase{rule-context} case. - -The optional case names of $\isarkeyword{obtains}$ have a twofold -meaning: (1) during the of this claim they refer to the the local -context introductions, (2) the resulting rule is annotated accordingly -to support symbolic case splits when used with the $cases$ method (cf. -\S\ref{sec:cases-induct}). - -\medskip - -\begin{warn} - Isabelle/Isar suffers theory-level goal statements to contain \emph{unbound - schematic variables}, although this does not conform to the aim of - human-readable proof documents! The main problem with schematic goals is - that the actual outcome is usually hard to predict, depending on the - behavior of the proof methods applied during the course of reasoning. Note - that most semi-automated methods heavily depend on several kinds of implicit - rule declarations within the current theory context. As this would also - result in non-compositional checking of sub-proofs, \emph{local goals} are - not allowed to be schematic at all. Nevertheless, schematic goals do have - their use in Prolog-style interactive synthesis of proven results, usually - by stepwise refinement via emulation of traditional Isabelle tactic scripts - (see also \S\ref{sec:tactic-commands}). In any case, users should know what - they are doing. -\end{warn} - - -\subsection{Initial and terminal proof steps}\label{sec:proof-steps} - -\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by} -\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry} -\begin{matharray}{rcl} - \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\ - \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\ - \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ - \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ - \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ - \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\ -\end{matharray} - -Arbitrary goal refinement via tactics is considered harmful. Properly, the -Isar framework admits proof methods to be invoked in two places only. -\begin{enumerate} -\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated - goal to a number of sub-goals that are to be solved later. Facts are passed - to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode. - -\item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve - remaining goals. No facts are passed to $m@2$. -\end{enumerate} - -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 - -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 an intelligible manner. - -Unless given explicitly by the user, the default initial method is ``$rule$'', -which applies a single standard elimination or introduction rule according to -the topmost symbol involved. There is no separate default terminal method. -Any remaining goals are always solved by assumption in the very last step. - -\begin{rail} - 'proof' method? - ; - 'qed' method? - ; - 'by' method method? - ; - ('.' | '..' | 'sorry') - ; -\end{rail} - -\begin{descr} - -\item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for - forward chaining are passed if so indicated by $proof(chain)$ mode. - -\item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and - concludes the sub-proof by assumption. If the goal had been $\SHOWNAME$ (or - $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting - from the result \emph{exported} into the enclosing goal context. Thus - $\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting - rule does not fit to any pending goal\footnote{This includes any additional - ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing - context. Debugging such a situation might involve temporarily changing - $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing - occurrences of $\ASSUMENAME$ by $\PRESUMENAME$. - -\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it - abbreviates $\PROOF{m@1}~\QED{m@2}$, but with backtracking across both - methods. Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done - by expanding its definition; in many cases $\PROOF{m@1}$ (or even - $\APPLY{m@1}$) is already sufficient to see the problem. - -\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it - abbreviates $\BY{rule}$. - -\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it - abbreviates $\BY{this}$. - -\item [$\SORRY$] is a \emph{fake proof}\index{proof!fake} pretending to solve - the pending claim without further ado. This only works in interactive - development, or if the \texttt{quick_and_dirty} flag is enabled. Facts - emerging from fake proofs are not the real thing. Internally, each theorem - container is tainted by an oracle invocation, which is indicated as - ``$[!]$'' in the printed result. - - The most important application of $\SORRY$ is to support experimentation and - top-down proof development. -\end{descr} - - -\subsection{Fundamental methods and attributes}\label{sec:pure-meth-att} - -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:logics}). - -\indexisarmeth{$-$}\indexisarmeth{fact}\indexisarmeth{assumption} -\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{iprover} -\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim} -\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule} -\indexisaratt{OF}\indexisaratt{of}\indexisaratt{where} -\begin{matharray}{rcl} - - & : & \isarmeth \\ - fact & : & \isarmeth \\ - assumption & : & \isarmeth \\ - this & : & \isarmeth \\ - rule & : & \isarmeth \\ - iprover & : & \isarmeth \\[0.5ex] - intro & : & \isaratt \\ - elim & : & \isaratt \\ - dest & : & \isaratt \\ - rule & : & \isaratt \\[0.5ex] - OF & : & \isaratt \\ - of & : & \isaratt \\ - where & : & \isaratt \\ -\end{matharray} - -\begin{rail} - 'fact' thmrefs? - ; - 'rule' thmrefs? - ; - 'iprover' ('!' ?) (rulemod *) - ; - rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs - ; - ('intro' | 'elim' | 'dest') ('!' | () | '?') nat? - ; - 'rule' 'del' - ; - 'OF' thmrefs - ; - 'of' insts ('concl' ':' insts)? - ; - 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and') - ; -\end{rail} - -\begin{descr} - -\item [``$-$''] does nothing but insert the forward chaining facts as premises - into the goal. Note that command $\PROOFNAME$ without any method actually - performs a single reduction step using the $rule$ method; thus a plain - \emph{do-nothing} proof step would be ``$\PROOF{-}$'' rather than - $\PROOFNAME$ alone. - -\item [$fact~\vec a$] composes any previous fact from $\vec a$ (or implicitly - from the current proof context) modulo matching of schematic type and term - variables. The rule structure is not taken into account, i.e.\ meta-level - implication is considered atomic. This is the same principle underlying - literal facts (cf.\ \S\ref{sec:syn-att}): ``$\HAVE{}{\phi}~\BY{fact}$'' is - equivalent to ``$\NOTE{}{\backquote\phi\backquote}$'' provided that $\edrv - \phi$ is an instance of some known $\edrv \phi$ in the proof context. - -\item [$assumption$] solves some goal by a single assumption step. All given - facts are guaranteed to participate in the refinement; this means there may - be only $0$ or $1$ in the first place. Recall that $\QEDNAME$ (see - \S\ref{sec:proof-steps}) already concludes any remaining sub-goals by - assumption, so structured proofs usually need not quote the $assumption$ - method at all. - -\item [$this$] applies all of the current facts directly as rules. Recall - that ``$\DOT$'' (dot) abbreviates ``$\BY{this}$''. - -\item [$rule~\vec a$] applies some rule given as argument in backward manner; - facts are used to reduce the rule before applying it to the goal. Thus - $rule$ without facts is plain introduction, while with facts it becomes - elimination. - - When no arguments are given, the $rule$ method tries to pick appropriate - rules automatically, as declared in the current context using the $intro$, - $elim$, $dest$ attributes (see below). This is the default behavior of - $\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see - \S\ref{sec:proof-steps}). - -\item [$iprover$] performs intuitionistic proof search, depending on - specifically declared rules from the context, or given as explicit - arguments. Chained facts are inserted into the goal before commencing proof - search; ``$iprover!$'' means to include the current $prems$ as well. - - Rules need to be classified as $intro$, $elim$, or $dest$; here the ``$!$'' - indicator refers to ``safe'' rules, which may be applied aggressively - (without considering back-tracking later). Rules declared with ``$?$'' are - ignored in proof search (the single-step $rule$ method still observes - these). An explicit weight annotation may be given as well; otherwise the - number of rule premises will be taken into account here. - -\item [$intro$, $elim$, and $dest$] declare introduction, elimination, and - destruct rules, to be used with the $rule$ and $iprover$ methods. Note that - the latter will ignore rules declared with ``$?$'', while ``$!$'' are used - most aggressively. - - The classical reasoner (see \S\ref{sec:classical}) introduces its own - variants of these attributes; use qualified names to access the present - versions of Isabelle/Pure, i.e.\ $Pure{\dtt}intro$ or $CPure{\dtt}intro$. - -\item [$rule~del$] undeclares introduction, elimination, or destruct rules. - -\item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in - parallel). This corresponds to the \texttt{MRS} operator in ML - \cite[\S5]{isabelle-ref}, but note the reversed order. Positions may be - effectively skipped by including ``$\_$'' (underscore) as argument. - -\item [$of~\vec t$] performs positional instantiation of term variables. The - terms $\vec t$ are substituted for any schematic variables occurring in a - theorem from left to right; ``\texttt{_}'' (underscore) indicates to skip a - position. Arguments following a ``$concl\colon$'' specification refer to - positions of the conclusion of a rule. - -\item [$where~\vec x = \vec t$] performs named instantiation of schematic type - and term variables occurring in a theorem. Schematic variables have to be - specified on the left-hand side (e.g.\ $?x1\!.\!3$). The question mark may - be omitted if the variable name is a plain identifier without index. As - type instantiations are inferred from term instantiations, explicit type - instantiations are seldom necessary. - -\end{descr} - - -\subsection{Term abbreviations}\label{sec:term-abbrev} - -\indexisarcmd{let} -\begin{matharray}{rcl} - \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\ - \isarkeyword{is} & : & syntax \\ -\end{matharray} - -Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements, -or by annotating assumptions or goal statements with a list of patterns -``$\ISS{p@1\;\dots}{p@n}$''. In both cases, higher-order matching is invoked -to bind extra-logical term variables, which may be either named schematic -variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}'' -(underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the -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, 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 -incremental type-inference, as the user proceeds to build up the Isar proof -text from left to right. - -\medskip - -Term abbreviations are quite different from local definitions as introduced -via $\DEFNAME$ (see \S\ref{sec:proof-context}). The latter are visible within -the logic as actual equations, while abbreviations disappear during the input -process just after type checking. Also note that $\DEFNAME$ does not support -polymorphism. - -\begin{rail} - 'let' ((term + 'and') '=' term + 'and') - ; -\end{rail} - -The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or -\railnonterm{proppat} (see \S\ref{sec:term-decls}). - -\begin{descr} -\item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$ - by simultaneous higher-order matching against terms $\vec t$. -\item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the - preceding statement. Also note that $\ISNAME$ is not a separate command, - but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.). -\end{descr} - -Some \emph{automatic} term abbreviations\index{term abbreviations} for goals -and facts are available as well. For any open goal, -$\Var{thesis}$\indexisarvar{thesis} refers to its object-level statement, -abstracted over any meta-level parameters (if present). Likewise, -$\Var{this}$\indexisarvar{this} is bound for fact statements resulting from -assumptions or finished goals. In case $\Var{this}$ refers to an object-logic -statement that is an application $f(t)$, then $t$ is bound to the special text -variable ``$\dots$''\indexisarvar{\dots} (three dots). The canonical -application of the latter are calculational proofs (see -\S\ref{sec:calculation}). - - -\subsection{Block structure} - -\indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}} -\begin{matharray}{rcl} - \NEXT & : & \isartrans{proof(state)}{proof(state)} \\ - \BG & : & \isartrans{proof(state)}{proof(state)} \\ - \EN & : & \isartrans{proof(state)}{proof(state)} \\ -\end{matharray} - -While Isar is inherently block-structured, opening and closing blocks is -mostly handled rather casually, with little explicit user-intervention. Any -local goal statement automatically opens \emph{two} blocks, which are closed -again when concluding the sub-proof (by $\QEDNAME$ etc.). Sections of -different context within a sub-proof may be switched via $\NEXT$, which is -just a single block-close followed by block-open again. The effect of $\NEXT$ -is to reset the local proof context; there is no goal focus involved here! - -For slightly more advanced applications, there are explicit block parentheses -as well. These typically achieve a stronger forward style of reasoning. - -\begin{descr} -\item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the - local context to the initial one. -\item [$\BG$ and $\EN$] explicitly open and close blocks. Any current facts - pass through ``$\BG$'' unchanged, while ``$\EN$'' causes any result to be - \emph{exported} into the enclosing context. Thus fixed variables are - generalized, assumptions discharged, and local definitions unfolded (cf.\ - \S\ref{sec:proof-context}). There is no difference of $\ASSUMENAME$ and - $\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain - backward reasoning with the result exported at $\SHOWNAME$ time. -\end{descr} - - -\subsection{Emulating tactic scripts}\label{sec:tactic-commands} - -The Isar provides separate commands to accommodate tactic-style proof scripts -within the same system. While being outside the orthodox Isar proof language, -these might come in handy for interactive exploration and debugging, or even -actual tactical proof within new-style theories (to benefit from document -preparation, for example). See also \S\ref{sec:tactics} for actual tactics, -that have been encapsulated as proof methods. Proper proof methods may be -used in scripts, too. - -\indexisarcmd{apply}\indexisarcmd{apply-end}\indexisarcmd{done} -\indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back} -\begin{matharray}{rcl} - \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\ - \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\ - \isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\ - \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\ - \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\ - \isarcmd{back}^* & : & \isartrans{proof}{proof} \\ -\end{matharray} - -\begin{rail} - ( 'apply' | 'apply\_end' ) method - ; - 'defer' nat? - ; - 'prefer' nat - ; -\end{rail} - -\begin{descr} - -\item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike - $\PROOFNAME$ it retains ``$proof(prove)$'' mode. Thus consecutive method - applications may be given just as in tactic scripts. - - Facts are passed to $m$ as indicated by the goal's forward-chain mode, and - are \emph{consumed} afterwards. Thus any further $\APPLYNAME$ command would - always work in a purely backward manner. - -\item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in - terminal position. Basically, this simulates a multi-step tactic script for - $\QEDNAME$, but may be given anywhere within the proof body. - - No facts are passed to $m$. Furthermore, the static context is that of the - enclosing goal (as for actual $\QEDNAME$). Thus the proof method may not - refer to any assumptions introduced in the current body, for example. - -\item [$\isarkeyword{done}$] completes a proof script, provided that the - current goal state is solved completely. Note that actual structured proof - commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to conclude proof - scripts as well. - -\item [$\isarkeyword{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list - of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$ - by default), while $prefer$ brings goal $n$ to the top. - -\item [$\isarkeyword{back}$] does back-tracking over the result sequence of - the latest proof command. Basically, any proof command may return multiple - results. - -\end{descr} - -Any proper Isar proof method may be used with tactic script commands such as -$\APPLYNAME$. A few additional emulations of actual tactics are provided as -well; these would be never used in actual structured proofs, of course. - - -\subsection{Meta-linguistic features} - -\indexisarcmd{oops} -\begin{matharray}{rcl} - \isarcmd{oops} & : & \isartrans{proof}{theory} \\ -\end{matharray} - -The $\OOPS$ command discontinues the current proof attempt, while considering -the partial proof text as properly processed. This is conceptually quite -different from ``faking'' actual proofs via $\SORRY$ (see -\S\ref{sec:proof-steps}): $\OOPS$ does not observe the proof structure at all, -but goes back right to the theory level. Furthermore, $\OOPS$ does not -produce any result theorem --- there is no intended claim to be able to -complete the proof anyhow. - -A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the -system itself, in conjunction with the document preparation tools of Isabelle -described in \cite{isabelle-sys}. Thus partial or even wrong proof attempts -can be discussed in a logically sound manner. Note that the Isabelle {\LaTeX} -macros can be easily adapted to print something like ``$\dots$'' instead of an -``$\OOPS$'' keyword. - -\medskip The $\OOPS$ command is undo-able, unlike $\isarkeyword{kill}$ (see -\S\ref{sec:history}). The effect is to get back to the theory just before the -opening of the proof. - - -\section{Other commands} - -\subsection{Diagnostics} - -\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term} -\indexisarcmd{prop}\indexisarcmd{typ} -\begin{matharray}{rcl} - \isarcmd{pr}^* & : & \isarkeep{\cdot} \\ - \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{prf}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{full_prf}^* & : & \isarkeep{theory~|~proof} \\ -\end{matharray} - -These diagnostic commands assist interactive development. Note that $undo$ -does not apply here, the theory or proof configuration is not changed. - -\begin{rail} - 'pr' modes? nat? (',' nat)? - ; - 'thm' modes? thmrefs - ; - 'term' modes? term - ; - 'prop' modes? prop - ; - 'typ' modes? type - ; - 'prf' modes? thmrefs? - ; - 'full\_prf' modes? thmrefs? - ; - - modes: '(' (name + ) ')' - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{pr}~goals, prems$] prints the current proof state (if - present), including the proof context, current facts and goals. The - optional limit arguments affect the number of goals and premises to be - displayed, which is initially 10 for both. Omitting limit values leaves the - current setting unchanged. -\item [$\isarkeyword{thm}~\vec a$] retrieves theorems from the current theory - or proof context. Note that any attributes included in the theorem - specifications are applied to a temporary context derived from the current - theory or proof; the result is discarded, i.e.\ attributes involved in $\vec - a$ do not have any permanent effect. -\item [$\isarkeyword{term}~t$ and $\isarkeyword{prop}~\phi$] read, type-check - and print terms or propositions according to the current theory or proof - context; the inferred type of $t$ is output as well. Note that these - commands are also useful in inspecting the current environment of term - abbreviations. -\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic - according to the current theory or proof context. -\item [$\isarkeyword{prf}$] displays the (compact) proof term of the current - proof state (if present), or of the given theorems. Note that this - requires proof terms to be switched on for the current object logic - (see the ``Proof terms'' section of the Isabelle reference manual - for information on how to do this). -\item [$\isarkeyword{full_prf}$] is like $\isarkeyword{prf}$, but displays - the full proof term, i.e.\ also displays information omitted in - the compact proof term, which is denoted by ``$_$'' placeholders there. -\end{descr} - -All of the diagnostic commands above admit a list of $modes$ to be specified, -which is appended to the current print mode (see also \cite{isabelle-ref}). -Thus the output behavior may be modified according particular print mode -features. For example, $\isarkeyword{pr}~(latex~xsymbols~symbols)$ would -print the current proof state with mathematical symbols and special characters -represented in {\LaTeX} source, according to the Isabelle style -\cite{isabelle-sys}. - -Note that antiquotations (cf.\ \S\ref{sec:antiq}) provide a more systematic -way to include formal items into the printed text document. - - -\subsection{Inspecting the context} - -\indexisarcmd{print-facts}\indexisarcmd{print-binds} -\indexisarcmd{print-commands}\indexisarcmd{print-syntax} -\indexisarcmd{print-methods}\indexisarcmd{print-attributes} -\indexisarcmd{find-theorems}\indexisarcmd{thm-deps} -\indexisarcmd{print-theorems}\indexisarcmd{print-theory} -\begin{matharray}{rcl} - \isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\ - \isarcmd{print_theory}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{print_theorems}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{find_theorems}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{thms_deps}^* & : & \isarkeep{theory~|~proof} \\ - \isarcmd{print_facts}^* & : & \isarkeep{proof} \\ - \isarcmd{print_binds}^* & : & \isarkeep{proof} \\ -\end{matharray} - -\begin{rail} - 'print\_theory' ( '!'?) - ; - - 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *) - ; - criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | - 'simp' ':' term | term) - ; - 'thm\_deps' thmrefs - ; -\end{rail} - -These commands print certain parts of the theory and proof context. Note that -there are some further ones available, such as for the set of rules declared -for simplifications. - -\begin{descr} - -\item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax, - including keywords and command. - -\item [$\isarkeyword{print_theory}$] prints the main logical content - of the theory context; the ``$!$'' option indicates extra verbosity. - -\item [$\isarkeyword{print_syntax}$] prints the inner syntax of types and - terms, depending on the current context. The output can be very verbose, - including grammar tables and syntax translation rules. See \cite[\S7, - \S8]{isabelle-ref} for further information on Isabelle's inner syntax. - -\item [$\isarkeyword{print_methods}$] prints all proof methods available in - the current theory context. - -\item [$\isarkeyword{print_attributes}$] prints all attributes available in - the current theory context. - -\item [$\isarkeyword{print_theorems}$] prints theorems available in the - current theory context. - - In interactive mode this actually refers to the theorems left by the last - transaction; this allows to inspect the result of advanced definitional - packages, such as $\isarkeyword{datatype}$. - -\item [$\isarkeyword{find_theorems}~\vec c$] retrieves facts from the theory - or proof context matching all of the search criteria $\vec c$. The - criterion $name: p$ selects all theorems whose fully qualified name matches - pattern $p$, which may contain ``$*$'' wildcards. The criteria $intro$, - $elim$, and $dest$ select theorems that match the current goal as - introduction, elimination or destruction rules, respectively. The criterion - $simp: t$ selects all rewrite rules whose left-hand side matches the given - term. The criterion term $t$ selects all theorems that contain the pattern - $t$ -- as usual, patterns may contain occurrences of the dummy ``$\_$'', - schematic variables, and type constraints. - - Criteria can be preceded by ``$-$'' to select theorems that do \emph{not} - match. Note that giving the empty list of criteria yields \emph{all} - currently known facts. An optional limit for the number of printed facts - may be given; the default is 40. Per default, duplicates are removed from - the search result. Use $\isarkeyword{with_dups}$ to display duplicates. - -\item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts, - using Isabelle's graph browser tool (see also \cite{isabelle-sys}). - -\item [$\isarkeyword{print_facts}$] prints all local facts of the - current context, both named and unnamed ones. - -\item [$\isarkeyword{print_binds}$] prints all term abbreviations present in - the context. - -\end{descr} - - -\subsection{History commands}\label{sec:history} - -\indexisarcmd{undo}\indexisarcmd{redo}\indexisarcmd{kill} -\begin{matharray}{rcl} - \isarcmd{undo}^{{*}{*}} & : & \isarkeep{\cdot} \\ - \isarcmd{redo}^{{*}{*}} & : & \isarkeep{\cdot} \\ - \isarcmd{kill}^{{*}{*}} & : & \isarkeep{\cdot} \\ -\end{matharray} - -The Isabelle/Isar top-level maintains a two-stage history, for theory and -proof state transformation. Basically, any command can be undone using -$\isarkeyword{undo}$, excluding mere diagnostic elements. Its effect may be -revoked via $\isarkeyword{redo}$, unless the corresponding -$\isarkeyword{undo}$ step has crossed the beginning of a proof or theory. The -$\isarkeyword{kill}$ command aborts the current history node altogether, -discontinuing a proof or even the whole theory. This operation is \emph{not} -undo-able. - -\begin{warn} - History commands should never be used with user interfaces such as - Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes care of - stepping forth and back itself. Interfering by manual $\isarkeyword{undo}$, - $\isarkeyword{redo}$, or even $\isarkeyword{kill}$ commands would quickly - result in utter confusion. -\end{warn} - - -\subsection{System operations} - -\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{update-thy} -\indexisarcmd{display-drafts}\indexisarcmd{print-drafts} -\begin{matharray}{rcl} - \isarcmd{cd}^* & : & \isarkeep{\cdot} \\ - \isarcmd{pwd}^* & : & \isarkeep{\cdot} \\ - \isarcmd{use_thy}^* & : & \isarkeep{\cdot} \\ - \isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\ - \isarcmd{display_drafts}^* & : & \isarkeep{\cdot} \\ - \isarcmd{print_drafts}^* & : & \isarkeep{\cdot} \\ -\end{matharray} - -\begin{rail} - ('cd' | 'use\_thy' | 'update\_thy') name - ; - ('display\_drafts' | 'print\_drafts') (name +) - ; -\end{rail} - -\begin{descr} -\item [$\isarkeyword{cd}~path$] changes the current directory of the Isabelle - process. -\item [$\isarkeyword{pwd}~$] prints the current working directory. -\item [$\isarkeyword{use_thy}$ and $\isarkeyword{update_thy}$] preload - some theory given as $name$ argument. These system commands are - scarcely used when working interactively, since loading of theories - is done transparently. -\item [$\isarkeyword{display_drafts}~paths$ and - $\isarkeyword{print_drafts}~paths$] perform simple output of a given list of - raw source files. Only those symbols that do not require additional - {\LaTeX} packages are displayed properly, everything else is left verbatim. -\end{descr} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "isar-ref" -%%% End: diff -r 0e2a29a1065c -r cc127cc0951b doc-src/IsarRef/style.sty --- a/doc-src/IsarRef/style.sty Fri May 02 16:32:51 2008 +0200 +++ b/doc-src/IsarRef/style.sty Fri May 02 16:36:05 2008 +0200 @@ -36,9 +36,7 @@ \newcommand{\isasymGUESS}{\isakeyword{guess}} \newcommand{\isasymOBTAIN}{\isakeyword{obtain}} \newcommand{\isasymTHEORY}{\isakeyword{theory}} -\newcommand{\isasymIMPORTS}{\isakeyword{imports}} \newcommand{\isasymUSES}{\isakeyword{uses}} -\newcommand{\isasymBEGIN}{\isakeyword{begin}} \newcommand{\isasymEND}{\isakeyword{end}} \newcommand{\isasymCONSTS}{\isakeyword{consts}} \newcommand{\isasymDEFS}{\isakeyword{defs}}