
diff -r ab23493e1f0f -r 31f8d9eaceff doc-src/IsarImplementation/Thy/document/Proof.tex
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex	Fri Feb 05 11:51:52 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex	Fri Feb 05 14:39:02 2010 +0100
@@ -42,9 +42,10 @@
   or outside the current scope by providing separate syntactic
   categories for \emph{fixed variables} (e.g.\ \isa{x}) vs.\
   \emph{schematic variables} (e.g.\ \isa{{\isacharquery}x}).  Incidently, a
-  universal result \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} has the HHF normal form \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}x{\isacharparenright}}, which represents its generality nicely without requiring
-  an explicit quantifier.  The same principle works for type
-  variables: \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}{\isasymalpha}{\isacharparenright}} represents the idea of ``\isa{{\isasymturnstile}\ {\isasymforall}{\isasymalpha}{\isachardot}\ B{\isacharparenleft}{\isasymalpha}{\isacharparenright}}'' without demanding a truly polymorphic framework.
+  universal result \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} has the HHF normal form \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}x{\isacharparenright}}, which represents its generality without requiring an
+  explicit quantifier.  The same principle works for type variables:
+  \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}{\isasymalpha}{\isacharparenright}} represents the idea of ``\isa{{\isasymturnstile}\ {\isasymforall}{\isasymalpha}{\isachardot}\ B{\isacharparenleft}{\isasymalpha}{\isacharparenright}}''
+  without demanding a truly polymorphic framework.
 
   \medskip Additional care is required to treat type variables in a
   way that facilitates type-inference.  In principle, term variables
@@ -113,7 +114,8 @@
   \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
   \indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
 \verb|  (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context| \\
-  \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context| \\
+  \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context ->|\isasep\isanewline%
+\verb|  ((string * cterm) list * cterm) * Proof.context| \\
   \end{mldecls}
 
   \begin{description}
@@ -167,6 +169,160 @@
 %
 \endisadelimmlref
 %
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example (in theory \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}) shows
+  how to work with fixed term and type parameters work with
+  type-inference.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+\isacommand{typedecl}\isamarkupfalse%
+\ foo\ \ %
+\isamarkupcmt{some basic type for testing purposes%
+}
+\isanewline
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}static\ compile{\isacharminus}time\ context\ {\isacharminus}{\isacharminus}\ for\ testing\ only{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ %
+\isaantiq
+context%
+\endisaantiq
+{\isacharsemicolon}\isanewline
+\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}locally\ fixed\ parameters\ {\isacharminus}{\isacharminus}\ no\ type\ assignment\ yet{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isacharcomma}\ y{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}y{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}t{\isadigit{1}}{\isacharcolon}\ most\ general\ fixed\ type{\isacharsemicolon}\ t{\isadigit{1}}{\isacharprime}{\isacharcolon}\ most\ general\ arbitrary\ type{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ t{\isadigit{1}}\ {\isacharequal}\ Syntax{\isachardot}read{\isacharunderscore}term\ ctxt{\isadigit{1}}\ {\isachardoublequote}x{\isachardoublequote}{\isacharsemicolon}\isanewline
+\ \ val\ t{\isadigit{1}}{\isacharprime}\ {\isacharequal}\ singleton\ {\isacharparenleft}Variable{\isachardot}polymorphic\ ctxt{\isadigit{1}}{\isacharparenright}\ t{\isadigit{1}}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}term\ u\ enforces\ specific\ type\ assignment{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ u\ {\isacharequal}\ Syntax{\isachardot}read{\isacharunderscore}term\ ctxt{\isadigit{1}}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcolon}{\isacharcolon}foo{\isacharparenright}\ {\isasymequiv}\ y{\isachardoublequote}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}official\ declaration\ of\ u\ {\isacharminus}{\isacharminus}\ propagates\ constraints\ etc{\isachardot}{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ ctxt{\isadigit{2}}\ {\isacharequal}\ ctxt{\isadigit{1}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}declare{\isacharunderscore}term\ u{\isacharsemicolon}\isanewline
+\ \ val\ t{\isadigit{2}}\ {\isacharequal}\ Syntax{\isachardot}read{\isacharunderscore}term\ ctxt{\isadigit{2}}\ {\isachardoublequote}x{\isachardoublequote}{\isacharsemicolon}\ \ {\isacharparenleft}{\isacharasterisk}x{\isacharcolon}{\isacharcolon}foo\ is\ enforced{\isacharasterisk}{\isacharparenright}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+In the above example, the starting context had been derived
+  from the toplevel theory, which means that fixed variables are
+  internalized literally: \verb|x| is mapped again to
+  \verb|x|, and attempting to fix it again in the subsequent
+  context is an error.  Alternatively, fixed parameters can be renamed
+  explicitly as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ %
+\isaantiq
+context%
+\endisaantiq
+{\isacharsemicolon}\isanewline
+\ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{1}}{\isacharcomma}\ x{\isadigit{2}}{\isacharcomma}\ x{\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}variant{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}x{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\noindent Subsequent ML code can now work with the invented
+  names of \verb|x1|, \verb|x2|, \verb|x3|, without
+  depending on the details on the system policy for introducing these
+  variants.  Recall that within a proof body the system always invents
+  fresh ``skolem constants'', e.g.\ as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}PROP\ XXX{\isachardoublequoteclose}\isanewline
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+%
+\isadelimML
+\ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ \ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ %
+\isaantiq
+context%
+\endisaantiq
+{\isacharsemicolon}\isanewline
+\isanewline
+\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{1}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{1}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}x{\isadigit{3}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{3}}{\isacharparenright}\ {\isacharequal}\ ctxt{\isadigit{2}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}add{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}x{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ \ \ val\ {\isacharparenleft}{\isacharbrackleft}y{\isadigit{1}}{\isacharcomma}\ y{\isadigit{2}}{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{4}}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ ctxt{\isadigit{3}}\ {\isacharbar}{\isachargreater}\ Variable{\isachardot}variant{\isacharunderscore}fixes\ {\isacharbrackleft}{\isachardoublequote}y{\isachardoublequote}{\isacharcomma}\ {\isachardoublequote}y{\isachardoublequote}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ {\isacharverbatimclose}\isanewline
+\ \ \isacommand{oops}\isamarkupfalse%
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\noindent In this situation \verb|Variable.add_fixes| and \verb|Variable.variant_fixes| are very similar, but identical name
+  proposals given in a row are only accepted by the second version.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Assumptions \label{sec:assumptions}%
 }
 \isamarkuptrue%
@@ -192,21 +348,21 @@
   context into a (smaller) outer context, by discharging the
   difference of the assumptions as specified by the associated export
   rules.  Note that the discharged portion is determined by the
-  difference contexts, not the facts being exported!  There is a
+  difference of contexts, not the facts being exported!  There is a
   separate flag to indicate a goal context, where the result is meant
   to refine an enclosing sub-goal of a structured proof state.
 
   \medskip The most basic export rule discharges assumptions directly
   by means of the \isa{{\isasymLongrightarrow}} introduction rule:
   \[
-  \infer[(\isa{{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
+  \infer[(\isa{{\isasymLongrightarrow}{\isasymdash}intro})]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
   \]
 
   The variant for goal refinements marks the newly introduced
   premises, which causes the canonical Isar goal refinement scheme to
   enforce unification with local premises within the goal:
   \[
-  \infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
+  \infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isasymdash}intro})]{\isa{{\isasymGamma}\ {\isacharminus}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
   \]
 
   \medskip Alternative versions of assumptions may perform arbitrary
@@ -215,7 +371,7 @@
   definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t},
   with the following export rule to reverse the effect:
   \[
-  \infer[(\isa{{\isasymequiv}{\isacharminus}expand})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
+  \infer[(\isa{{\isasymequiv}{\isasymdash}expand})]{\isa{{\isasymGamma}\ {\isacharminus}\ {\isacharparenleft}x\ {\isasymequiv}\ t{\isacharparenright}\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
   \]
   This works, because the assumption \isa{x\ {\isasymequiv}\ t} was introduced in
   a context with \isa{x} being fresh, so \isa{x} does not
@@ -247,8 +403,8 @@
   where the \verb|bool| indicates goal mode, and the \verb|cterm list| the collection of assumptions to be discharged
   simultaneously.
 
-  \item \verb|Assumption.assume|~\isa{A} turns proposition \isa{A} into a raw assumption \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the conclusion
-  \isa{A{\isacharprime}} is in HHF normal form.
+  \item \verb|Assumption.assume|~\isa{A} turns proposition \isa{A} into a primitive assumption \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the
+  conclusion \isa{A{\isacharprime}} is in HHF normal form.
 
   \item \verb|Assumption.add_assms|~\isa{r\ As} augments the context
   by assumptions \isa{As} with export rule \isa{r}.  The
@@ -256,7 +412,8 @@
   \verb|Assumption.assume|.
 
   \item \verb|Assumption.add_assumes|~\isa{As} is a special case of
-  \verb|Assumption.add_assms| where the export rule performs \isa{{\isasymLongrightarrow}{\isacharunderscore}intro} or \isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro}, depending on goal mode.
+  \verb|Assumption.add_assms| where the export rule performs \isa{{\isasymLongrightarrow}{\isasymdash}intro} or \isa{{\isacharhash}{\isasymLongrightarrow}{\isasymdash}intro}, depending on goal
+  mode.
 
   \item \verb|Assumption.export|~\isa{is{\isacharunderscore}goal\ inner\ outer\ thm}
   exports result \isa{thm} from the the \isa{inner} context
@@ -276,7 +433,68 @@
 %
 \endisadelimmlref
 %
-\isamarkupsection{Results \label{sec:results}%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example demonstrates how rules can be
+  derived by building up a context of assumptions first, and exporting
+  some local fact afterwards.  We refer to \hyperlink{theory.Pure}{\mbox{\isa{Pure}}} equality
+  here for testing purposes.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}static\ compile{\isacharminus}time\ context\ {\isacharminus}{\isacharminus}\ for\ testing\ only{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ ctxt{\isadigit{0}}\ {\isacharequal}\ %
+\isaantiq
+context%
+\endisaantiq
+{\isacharsemicolon}\isanewline
+\isanewline
+\ \ val\ {\isacharparenleft}{\isacharbrackleft}eq{\isacharbrackright}{\isacharcomma}\ ctxt{\isadigit{1}}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ ctxt{\isadigit{0}}\ {\isacharbar}{\isachargreater}\ Assumption{\isachardot}add{\isacharunderscore}assumes\ {\isacharbrackleft}%
+\isaantiq
+cprop\ {\isachardoublequote}x\ {\isasymequiv}\ y{\isachardoublequote}%
+\endisaantiq
+{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ val\ eq{\isacharprime}\ {\isacharequal}\ Thm{\isachardot}symmetric\ eq{\isacharsemicolon}\isanewline
+\isanewline
+\ \ {\isacharparenleft}{\isacharasterisk}back\ to\ original\ context\ {\isacharminus}{\isacharminus}\ discharges\ assumption{\isacharasterisk}{\isacharparenright}\isanewline
+\ \ val\ r\ {\isacharequal}\ Assumption{\isachardot}export\ false\ ctxt{\isadigit{1}}\ ctxt{\isadigit{0}}\ eq{\isacharprime}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+\noindent Note that the variables of the resulting rule are
+  not generalized.  This would have required to fix them properly in
+  the context beforehand, and export wrt.\ variables afterwards (cf.\
+  \verb|Variable.export| or the combined \verb|ProofContext.export|).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Structured goals and results \label{sec:struct-goals}%
 }
 \isamarkuptrue%
 %
@@ -296,6 +514,9 @@
   the tactic needs to solve the conclusion, but may use the premise as
   a local fact, for locally fixed variables.
 
+  The family of \isa{FOCUS} combinators is similar to \isa{SUBPROOF}, but allows to retain schematic variables and pending
+  subgoals in the resulting goal state.
+
   The \isa{prove} operation provides an interface for structured
   backwards reasoning under program control, with some explicit sanity
   checks of the result.  The goal context can be augmented by
@@ -308,7 +529,8 @@
   The \isa{obtain} operation produces results by eliminating
   existing facts by means of a given tactic.  This acts like a dual
   conclusion: the proof demonstrates that the context may be augmented
-  by certain fixed variables and assumptions.  See also
+  by parameters and assumptions, without affecting any conclusions
+  that do not mention these parameters.  See also
   \cite{isabelle-isar-ref} for the user-level \isa{{\isasymOBTAIN}} and
   \isa{{\isasymGUESS}} elements.  Final results, which may not refer to
   the parameters in the conclusion, need to exported explicitly into
@@ -325,7 +547,11 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexdef{}{ML}{SUBPROOF}\verb|SUBPROOF: (Subgoal.focus -> tactic) -> Proof.context -> int -> tactic| \\
+  \indexdef{}{ML}{Subgoal.FOCUS}\verb|Subgoal.FOCUS: (Subgoal.focus -> tactic) -> Proof.context -> int -> tactic| \\
+  \indexdef{}{ML}{Subgoal.FOCUS\_PREMS}\verb|Subgoal.FOCUS_PREMS: (Subgoal.focus -> tactic) -> Proof.context -> int -> tactic| \\
+  \indexdef{}{ML}{Subgoal.FOCUS\_PARAMS}\verb|Subgoal.FOCUS_PARAMS: (Subgoal.focus -> tactic) -> Proof.context -> int -> tactic| \\
   \end{mldecls}
+
   \begin{mldecls}
   \indexdef{}{ML}{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
 \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
@@ -345,6 +571,11 @@
   schematic parameters of the goal are imported into the context as
   fixed ones, which may not be instantiated in the sub-proof.
 
+  \item \verb|Subgoal.FOCUS|, \verb|Subgoal.FOCUS_PREMS|, and \verb|Subgoal.FOCUS_PARAMS| are similar to \verb|SUBPROOF|, but are
+  slightly more flexible: only the specified parts of the subgoal are
+  imported into the context, and the body tactic may introduce new
+  subgoals and schematic variables.
+
   \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and
   assumptions \isa{As}, and applies tactic \isa{tac} to solve
   it.  The latter may depend on the local assumptions being presented




