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