src/Doc/Implementation/Proof.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 59567 3ff1dd7ac7f0
child 59902 6afbe5a99139
permissions -rw-r--r--
tuned signature;
     1 theory Proof
     2 imports Base
     3 begin
     4 
     5 chapter \<open>Structured proofs\<close>
     6 
     7 section \<open>Variables \label{sec:variables}\<close>
     8 
     9 text \<open>
    10   Any variable that is not explicitly bound by @{text "\<lambda>"}-abstraction
    11   is considered as ``free''.  Logically, free variables act like
    12   outermost universal quantification at the sequent level: @{text
    13   "A\<^sub>1(x), \<dots>, A\<^sub>n(x) \<turnstile> B(x)"} means that the result
    14   holds \emph{for all} values of @{text "x"}.  Free variables for
    15   terms (not types) can be fully internalized into the logic: @{text
    16   "\<turnstile> B(x)"} and @{text "\<turnstile> \<And>x. B(x)"} are interchangeable, provided
    17   that @{text "x"} does not occur elsewhere in the context.
    18   Inspecting @{text "\<turnstile> \<And>x. B(x)"} more closely, we see that inside the
    19   quantifier, @{text "x"} is essentially ``arbitrary, but fixed'',
    20   while from outside it appears as a place-holder for instantiation
    21   (thanks to @{text "\<And>"} elimination).
    22 
    23   The Pure logic represents the idea of variables being either inside
    24   or outside the current scope by providing separate syntactic
    25   categories for \emph{fixed variables} (e.g.\ @{text "x"}) vs.\
    26   \emph{schematic variables} (e.g.\ @{text "?x"}).  Incidently, a
    27   universal result @{text "\<turnstile> \<And>x. B(x)"} has the HHF normal form @{text
    28   "\<turnstile> B(?x)"}, which represents its generality without requiring an
    29   explicit quantifier.  The same principle works for type variables:
    30   @{text "\<turnstile> B(?\<alpha>)"} represents the idea of ``@{text "\<turnstile> \<forall>\<alpha>. B(\<alpha>)"}''
    31   without demanding a truly polymorphic framework.
    32 
    33   \medskip Additional care is required to treat type variables in a
    34   way that facilitates type-inference.  In principle, term variables
    35   depend on type variables, which means that type variables would have
    36   to be declared first.  For example, a raw type-theoretic framework
    37   would demand the context to be constructed in stages as follows:
    38   @{text "\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^sub>\<alpha>)"}.
    39 
    40   We allow a slightly less formalistic mode of operation: term
    41   variables @{text "x"} are fixed without specifying a type yet
    42   (essentially \emph{all} potential occurrences of some instance
    43   @{text "x\<^sub>\<tau>"} are fixed); the first occurrence of @{text "x"}
    44   within a specific term assigns its most general type, which is then
    45   maintained consistently in the context.  The above example becomes
    46   @{text "\<Gamma> = x: term, \<alpha>: type, A(x\<^sub>\<alpha>)"}, where type @{text
    47   "\<alpha>"} is fixed \emph{after} term @{text "x"}, and the constraint
    48   @{text "x :: \<alpha>"} is an implicit consequence of the occurrence of
    49   @{text "x\<^sub>\<alpha>"} in the subsequent proposition.
    50 
    51   This twist of dependencies is also accommodated by the reverse
    52   operation of exporting results from a context: a type variable
    53   @{text "\<alpha>"} is considered fixed as long as it occurs in some fixed
    54   term variable of the context.  For example, exporting @{text "x:
    55   term, \<alpha>: type \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>"} produces in the first step @{text "x: term
    56   \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>"} for fixed @{text "\<alpha>"}, and only in the second step
    57   @{text "\<turnstile> ?x\<^sub>?\<^sub>\<alpha> \<equiv> ?x\<^sub>?\<^sub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}.
    58   The following Isar source text illustrates this scenario.
    59 \<close>
    60 
    61 notepad
    62 begin
    63   {
    64     fix x  -- \<open>all potential occurrences of some @{text "x::\<tau>"} are fixed\<close>
    65     {
    66       have "x::'a \<equiv> x"  -- \<open>implicit type assignment by concrete occurrence\<close>
    67         by (rule reflexive)
    68     }
    69     thm this  -- \<open>result still with fixed type @{text "'a"}\<close>
    70   }
    71   thm this  -- \<open>fully general result for arbitrary @{text "?x::?'a"}\<close>
    72 end
    73 
    74 text \<open>The Isabelle/Isar proof context manages the details of term
    75   vs.\ type variables, with high-level principles for moving the
    76   frontier between fixed and schematic variables.
    77 
    78   The @{text "add_fixes"} operation explicitly declares fixed
    79   variables; the @{text "declare_term"} operation absorbs a term into
    80   a context by fixing new type variables and adding syntactic
    81   constraints.
    82 
    83   The @{text "export"} operation is able to perform the main work of
    84   generalizing term and type variables as sketched above, assuming
    85   that fixing variables and terms have been declared properly.
    86 
    87   There @{text "import"} operation makes a generalized fact a genuine
    88   part of the context, by inventing fixed variables for the schematic
    89   ones.  The effect can be reversed by using @{text "export"} later,
    90   potentially with an extended context; the result is equivalent to
    91   the original modulo renaming of schematic variables.
    92 
    93   The @{text "focus"} operation provides a variant of @{text "import"}
    94   for nested propositions (with explicit quantification): @{text
    95   "\<And>x\<^sub>1 \<dots> x\<^sub>n. B(x\<^sub>1, \<dots>, x\<^sub>n)"} is
    96   decomposed by inventing fixed variables @{text "x\<^sub>1, \<dots>,
    97   x\<^sub>n"} for the body.
    98 \<close>
    99 
   100 text %mlref \<open>
   101   \begin{mldecls}
   102   @{index_ML Variable.add_fixes: "
   103   string list -> Proof.context -> string list * Proof.context"} \\
   104   @{index_ML Variable.variant_fixes: "
   105   string list -> Proof.context -> string list * Proof.context"} \\
   106   @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
   107   @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
   108   @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
   109   @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
   110   @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
   111   (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\
   112   @{index_ML Variable.focus: "term -> Proof.context ->
   113   ((string * (string * typ)) list * term) * Proof.context"} \\
   114   \end{mldecls}
   115 
   116   \begin{description}
   117 
   118   \item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term
   119   variables @{text "xs"}, returning the resulting internal names.  By
   120   default, the internal representation coincides with the external
   121   one, which also means that the given variables must not be fixed
   122   already.  There is a different policy within a local proof body: the
   123   given names are just hints for newly invented Skolem variables.
   124 
   125   \item @{ML Variable.variant_fixes} is similar to @{ML
   126   Variable.add_fixes}, but always produces fresh variants of the given
   127   names.
   128 
   129   \item @{ML Variable.declare_term}~@{text "t ctxt"} declares term
   130   @{text "t"} to belong to the context.  This automatically fixes new
   131   type variables, but not term variables.  Syntactic constraints for
   132   type and term variables are declared uniformly, though.
   133 
   134   \item @{ML Variable.declare_constraints}~@{text "t ctxt"} declares
   135   syntactic constraints from term @{text "t"}, without making it part
   136   of the context yet.
   137 
   138   \item @{ML Variable.export}~@{text "inner outer thms"} generalizes
   139   fixed type and term variables in @{text "thms"} according to the
   140   difference of the @{text "inner"} and @{text "outer"} context,
   141   following the principles sketched above.
   142 
   143   \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
   144   variables in @{text "ts"} as far as possible, even those occurring
   145   in fixed term variables.  The default policy of type-inference is to
   146   fix newly introduced type variables, which is essentially reversed
   147   with @{ML Variable.polymorphic}: here the given terms are detached
   148   from the context as far as possible.
   149 
   150   \item @{ML Variable.import}~@{text "open thms ctxt"} invents fixed
   151   type and term variables for the schematic ones occurring in @{text
   152   "thms"}.  The @{text "open"} flag indicates whether the fixed names
   153   should be accessible to the user, otherwise newly introduced names
   154   are marked as ``internal'' (\secref{sec:names}).
   155 
   156   \item @{ML Variable.focus}~@{text B} decomposes the outermost @{text
   157   "\<And>"} prefix of proposition @{text "B"}.
   158 
   159   \end{description}
   160 \<close>
   161 
   162 text %mlex \<open>The following example shows how to work with fixed term
   163   and type parameters and with type-inference.\<close>
   164 
   165 ML \<open>
   166   (*static compile-time context -- for testing only*)
   167   val ctxt0 = @{context};
   168 
   169   (*locally fixed parameters -- no type assignment yet*)
   170   val ([x, y], ctxt1) = ctxt0 |> Variable.add_fixes ["x", "y"];
   171 
   172   (*t1: most general fixed type; t1': most general arbitrary type*)
   173   val t1 = Syntax.read_term ctxt1 "x";
   174   val t1' = singleton (Variable.polymorphic ctxt1) t1;
   175 
   176   (*term u enforces specific type assignment*)
   177   val u = Syntax.read_term ctxt1 "(x::nat) \<equiv> y";
   178 
   179   (*official declaration of u -- propagates constraints etc.*)
   180   val ctxt2 = ctxt1 |> Variable.declare_term u;
   181   val t2 = Syntax.read_term ctxt2 "x";  (*x::nat is enforced*)
   182 \<close>
   183 
   184 text \<open>In the above example, the starting context is derived from the
   185   toplevel theory, which means that fixed variables are internalized
   186   literally: @{text "x"} is mapped again to @{text "x"}, and
   187   attempting to fix it again in the subsequent context is an error.
   188   Alternatively, fixed parameters can be renamed explicitly as
   189   follows:\<close>
   190 
   191 ML \<open>
   192   val ctxt0 = @{context};
   193   val ([x1, x2, x3], ctxt1) =
   194     ctxt0 |> Variable.variant_fixes ["x", "x", "x"];
   195 \<close>
   196 
   197 text \<open>The following ML code can now work with the invented names of
   198   @{text x1}, @{text x2}, @{text x3}, without depending on
   199   the details on the system policy for introducing these variants.
   200   Recall that within a proof body the system always invents fresh
   201   ``Skolem constants'', e.g.\ as follows:\<close>
   202 
   203 notepad
   204 begin
   205   ML_prf %"ML"
   206    \<open>val ctxt0 = @{context};
   207 
   208     val ([x1], ctxt1) = ctxt0 |> Variable.add_fixes ["x"];
   209     val ([x2], ctxt2) = ctxt1 |> Variable.add_fixes ["x"];
   210     val ([x3], ctxt3) = ctxt2 |> Variable.add_fixes ["x"];
   211 
   212     val ([y1, y2], ctxt4) =
   213       ctxt3 |> Variable.variant_fixes ["y", "y"];\<close>
   214 end
   215 
   216 text \<open>In this situation @{ML Variable.add_fixes} and @{ML
   217   Variable.variant_fixes} are very similar, but identical name
   218   proposals given in a row are only accepted by the second version.
   219 \<close>
   220 
   221 
   222 section \<open>Assumptions \label{sec:assumptions}\<close>
   223 
   224 text \<open>
   225   An \emph{assumption} is a proposition that it is postulated in the
   226   current context.  Local conclusions may use assumptions as
   227   additional facts, but this imposes implicit hypotheses that weaken
   228   the overall statement.
   229 
   230   Assumptions are restricted to fixed non-schematic statements, i.e.\
   231   all generality needs to be expressed by explicit quantifiers.
   232   Nevertheless, the result will be in HHF normal form with outermost
   233   quantifiers stripped.  For example, by assuming @{text "\<And>x :: \<alpha>. P
   234   x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for schematic @{text "?x"}
   235   of fixed type @{text "\<alpha>"}.  Local derivations accumulate more and
   236   more explicit references to hypotheses: @{text "A\<^sub>1, \<dots>,
   237   A\<^sub>n \<turnstile> B"} where @{text "A\<^sub>1, \<dots>, A\<^sub>n"} needs to
   238   be covered by the assumptions of the current context.
   239 
   240   \medskip The @{text "add_assms"} operation augments the context by
   241   local assumptions, which are parameterized by an arbitrary @{text
   242   "export"} rule (see below).
   243 
   244   The @{text "export"} operation moves facts from a (larger) inner
   245   context into a (smaller) outer context, by discharging the
   246   difference of the assumptions as specified by the associated export
   247   rules.  Note that the discharged portion is determined by the
   248   difference of contexts, not the facts being exported!  There is a
   249   separate flag to indicate a goal context, where the result is meant
   250   to refine an enclosing sub-goal of a structured proof state.
   251 
   252   \medskip The most basic export rule discharges assumptions directly
   253   by means of the @{text "\<Longrightarrow>"} introduction rule:
   254   \[
   255   \infer[(@{text "\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
   256   \]
   257 
   258   The variant for goal refinements marks the newly introduced
   259   premises, which causes the canonical Isar goal refinement scheme to
   260   enforce unification with local premises within the goal:
   261   \[
   262   \infer[(@{text "#\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
   263   \]
   264 
   265   \medskip Alternative versions of assumptions may perform arbitrary
   266   transformations on export, as long as the corresponding portion of
   267   hypotheses is removed from the given facts.  For example, a local
   268   definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"},
   269   with the following export rule to reverse the effect:
   270   \[
   271   \infer[(@{text "\<equiv>\<hyphen>expand"})]{@{text "\<Gamma> - (x \<equiv> t) \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
   272   \]
   273   This works, because the assumption @{text "x \<equiv> t"} was introduced in
   274   a context with @{text "x"} being fresh, so @{text "x"} does not
   275   occur in @{text "\<Gamma>"} here.
   276 \<close>
   277 
   278 text %mlref \<open>
   279   \begin{mldecls}
   280   @{index_ML_type Assumption.export} \\
   281   @{index_ML Assumption.assume: "Proof.context -> cterm -> thm"} \\
   282   @{index_ML Assumption.add_assms:
   283     "Assumption.export ->
   284   cterm list -> Proof.context -> thm list * Proof.context"} \\
   285   @{index_ML Assumption.add_assumes: "
   286   cterm list -> Proof.context -> thm list * Proof.context"} \\
   287   @{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
   288   \end{mldecls}
   289 
   290   \begin{description}
   291 
   292   \item Type @{ML_type Assumption.export} represents arbitrary export
   293   rules, which is any function of type @{ML_type "bool -> cterm list
   294   -> thm -> thm"}, where the @{ML_type "bool"} indicates goal mode,
   295   and the @{ML_type "cterm list"} the collection of assumptions to be
   296   discharged simultaneously.
   297 
   298   \item @{ML Assumption.assume}~@{text "ctxt A"} turns proposition @{text
   299   "A"} into a primitive assumption @{text "A \<turnstile> A'"}, where the
   300   conclusion @{text "A'"} is in HHF normal form.
   301 
   302   \item @{ML Assumption.add_assms}~@{text "r As"} augments the context
   303   by assumptions @{text "As"} with export rule @{text "r"}.  The
   304   resulting facts are hypothetical theorems as produced by the raw
   305   @{ML Assumption.assume}.
   306 
   307   \item @{ML Assumption.add_assumes}~@{text "As"} is a special case of
   308   @{ML Assumption.add_assms} where the export rule performs @{text
   309   "\<Longrightarrow>\<hyphen>intro"} or @{text "#\<Longrightarrow>\<hyphen>intro"}, depending on goal
   310   mode.
   311 
   312   \item @{ML Assumption.export}~@{text "is_goal inner outer thm"}
   313   exports result @{text "thm"} from the the @{text "inner"} context
   314   back into the @{text "outer"} one; @{text "is_goal = true"} means
   315   this is a goal context.  The result is in HHF normal form.  Note
   316   that @{ML "Proof_Context.export"} combines @{ML "Variable.export"}
   317   and @{ML "Assumption.export"} in the canonical way.
   318 
   319   \end{description}
   320 \<close>
   321 
   322 text %mlex \<open>The following example demonstrates how rules can be
   323   derived by building up a context of assumptions first, and exporting
   324   some local fact afterwards.  We refer to @{theory Pure} equality
   325   here for testing purposes.
   326 \<close>
   327 
   328 ML \<open>
   329   (*static compile-time context -- for testing only*)
   330   val ctxt0 = @{context};
   331 
   332   val ([eq], ctxt1) =
   333     ctxt0 |> Assumption.add_assumes [@{cprop "x \<equiv> y"}];
   334   val eq' = Thm.symmetric eq;
   335 
   336   (*back to original context -- discharges assumption*)
   337   val r = Assumption.export false ctxt1 ctxt0 eq';
   338 \<close>
   339 
   340 text \<open>Note that the variables of the resulting rule are not
   341   generalized.  This would have required to fix them properly in the
   342   context beforehand, and export wrt.\ variables afterwards (cf.\ @{ML
   343   Variable.export} or the combined @{ML "Proof_Context.export"}).\<close>
   344 
   345 
   346 section \<open>Structured goals and results \label{sec:struct-goals}\<close>
   347 
   348 text \<open>
   349   Local results are established by monotonic reasoning from facts
   350   within a context.  This allows common combinations of theorems,
   351   e.g.\ via @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or equational
   352   reasoning, see \secref{sec:thms}.  Unaccounted context manipulations
   353   should be avoided, notably raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc
   354   references to free variables or assumptions not present in the proof
   355   context.
   356 
   357   \medskip The @{text "SUBPROOF"} combinator allows to structure a
   358   tactical proof recursively by decomposing a selected sub-goal:
   359   @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"}
   360   after fixing @{text "x"} and assuming @{text "A(x)"}.  This means
   361   the tactic needs to solve the conclusion, but may use the premise as
   362   a local fact, for locally fixed variables.
   363 
   364   The family of @{text "FOCUS"} combinators is similar to @{text
   365   "SUBPROOF"}, but allows to retain schematic variables and pending
   366   subgoals in the resulting goal state.
   367 
   368   The @{text "prove"} operation provides an interface for structured
   369   backwards reasoning under program control, with some explicit sanity
   370   checks of the result.  The goal context can be augmented by
   371   additional fixed variables (cf.\ \secref{sec:variables}) and
   372   assumptions (cf.\ \secref{sec:assumptions}), which will be available
   373   as local facts during the proof and discharged into implications in
   374   the result.  Type and term variables are generalized as usual,
   375   according to the context.
   376 
   377   The @{text "obtain"} operation produces results by eliminating
   378   existing facts by means of a given tactic.  This acts like a dual
   379   conclusion: the proof demonstrates that the context may be augmented
   380   by parameters and assumptions, without affecting any conclusions
   381   that do not mention these parameters.  See also
   382   @{cite "isabelle-isar-ref"} for the user-level @{command obtain} and
   383   @{command guess} elements.  Final results, which may not refer to
   384   the parameters in the conclusion, need to exported explicitly into
   385   the original context.\<close>
   386 
   387 text %mlref \<open>
   388   \begin{mldecls}
   389   @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) ->
   390   Proof.context -> int -> tactic"} \\
   391   @{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) ->
   392   Proof.context -> int -> tactic"} \\
   393   @{index_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) ->
   394   Proof.context -> int -> tactic"} \\
   395   @{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) ->
   396   Proof.context -> int -> tactic"} \\
   397   @{index_ML Subgoal.focus: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
   398   @{index_ML Subgoal.focus_prems: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
   399   @{index_ML Subgoal.focus_params: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
   400   \end{mldecls}
   401 
   402   \begin{mldecls}
   403   @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
   404   ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
   405   @{index_ML Goal.prove_common: "Proof.context -> int option ->
   406   string list -> term list -> term list ->
   407   ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
   408   \end{mldecls}
   409   \begin{mldecls}
   410   @{index_ML Obtain.result: "(Proof.context -> tactic) -> thm list ->
   411   Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\
   412   \end{mldecls}
   413 
   414   \begin{description}
   415 
   416   \item @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure
   417   of the specified sub-goal, producing an extended context and a
   418   reduced goal, which needs to be solved by the given tactic.  All
   419   schematic parameters of the goal are imported into the context as
   420   fixed ones, which may not be instantiated in the sub-proof.
   421 
   422   \item @{ML Subgoal.FOCUS}, @{ML Subgoal.FOCUS_PREMS}, and @{ML
   423   Subgoal.FOCUS_PARAMS} are similar to @{ML SUBPROOF}, but are
   424   slightly more flexible: only the specified parts of the subgoal are
   425   imported into the context, and the body tactic may introduce new
   426   subgoals and schematic variables.
   427 
   428   \item @{ML Subgoal.focus}, @{ML Subgoal.focus_prems}, @{ML
   429   Subgoal.focus_params} extract the focus information from a goal
   430   state in the same way as the corresponding tacticals above.  This is
   431   occasionally useful to experiment without writing actual tactics
   432   yet.
   433 
   434   \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
   435   "C"} in the context augmented by fixed variables @{text "xs"} and
   436   assumptions @{text "As"}, and applies tactic @{text "tac"} to solve
   437   it.  The latter may depend on the local assumptions being presented
   438   as facts.  The result is in HHF normal form.
   439 
   440   \item @{ML Goal.prove_common}~@{text "ctxt fork_pri"} is the common form
   441   to state and prove a simultaneous goal statement, where @{ML Goal.prove}
   442   is a convenient shorthand that is most frequently used in applications.
   443 
   444   The given list of simultaneous conclusions is encoded in the goal state by
   445   means of Pure conjunction: @{ML Goal.conjunction_tac} will turn this into
   446   a collection of individual subgoals, but note that the original multi-goal
   447   state is usually required for advanced induction.
   448 
   449   It is possible to provide an optional priority for a forked proof,
   450   typically @{ML "SOME ~1"}, while @{ML NONE} means the proof is immediate
   451   (sequential) as for @{ML Goal.prove}. Note that a forked proof does not
   452   exhibit any failures in the usual way via exceptions in ML, but
   453   accumulates error situations under the execution id of the running
   454   transaction. Thus the system is able to expose error messages ultimately
   455   to the end-user, even though the subsequent ML code misses them.
   456 
   457   \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the
   458   given facts using a tactic, which results in additional fixed
   459   variables and assumptions in the context.  Final results need to be
   460   exported explicitly.
   461 
   462   \end{description}
   463 \<close>
   464 
   465 text %mlex \<open>The following minimal example illustrates how to access
   466   the focus information of a structured goal state.\<close>
   467 
   468 notepad
   469 begin
   470   fix A B C :: "'a \<Rightarrow> bool"
   471 
   472   have "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
   473     ML_val
   474      \<open>val {goal, context = goal_ctxt, ...} = @{Isar.goal};
   475       val (focus as {params, asms, concl, ...}, goal') =
   476         Subgoal.focus goal_ctxt 1 goal;
   477       val [A, B] = #prems focus;
   478       val [(_, x)] = #params focus;\<close>
   479     sorry
   480 end
   481 
   482 text \<open>\medskip The next example demonstrates forward-elimination in
   483   a local context, using @{ML Obtain.result}.\<close>
   484 
   485 notepad
   486 begin
   487   assume ex: "\<exists>x. B x"
   488 
   489   ML_prf %"ML"
   490    \<open>val ctxt0 = @{context};
   491     val (([(_, x)], [B]), ctxt1) = ctxt0
   492       |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}];\<close>
   493   ML_prf %"ML"
   494    \<open>singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl};\<close>
   495   ML_prf %"ML"
   496    \<open>Proof_Context.export ctxt1 ctxt0 [Thm.reflexive x]
   497       handle ERROR msg => (warning msg; []);\<close>
   498 end
   499 
   500 end