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