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 "\<lambda>"}-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), \<dots>, A\<^isub>n(x) \<turnstile> 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
  "\<turnstile> B(x)"} and @{text "\<turnstile> \<And>x. B(x)"} are interchangeable, provided
wenzelm@20474
    17
  that @{text "x"} does not occur elsewhere in the context.
wenzelm@20474
    18
  Inspecting @{text "\<turnstile> \<And>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 "\<And>"} 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 "\<turnstile> \<And>x. B(x)"} has the HHF normal form @{text
wenzelm@34930
    28
  "\<turnstile> 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 "\<turnstile> B(?\<alpha>)"} represents the idea of ``@{text "\<turnstile> \<forall>\<alpha>. B(\<alpha>)"}''
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 "\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^isub>\<alpha>)"}.
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>\<tau>"} 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 "\<Gamma> = x: term, \<alpha>: type, A(x\<^isub>\<alpha>)"}, where type @{text
wenzelm@20474
    47
  "\<alpha>"} is fixed \emph{after} term @{text "x"}, and the constraint
wenzelm@20474
    48
  @{text "x :: \<alpha>"} is an implicit consequence of the occurrence of
wenzelm@20474
    49
  @{text "x\<^isub>\<alpha>"} 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 "\<alpha>"} 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, \<alpha>: type \<turnstile> x\<^isub>\<alpha> \<equiv> x\<^isub>\<alpha>"} produces in the first step @{text "x: term
wenzelm@39841
    56
  \<turnstile> x\<^isub>\<alpha> \<equiv> x\<^isub>\<alpha>"} for fixed @{text "\<alpha>"}, and only in the second step
wenzelm@39841
    57
  @{text "\<turnstile> ?x\<^isub>?\<^isub>\<alpha> \<equiv> ?x\<^isub>?\<^isub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}.
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::\<tau>"} are fixed *}
wenzelm@39841
    65
    {
wenzelm@39841
    66
      have "x::'a \<equiv> 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
  "\<And>x\<^isub>1 \<dots> x\<^isub>n. B(x\<^isub>1, \<dots>, x\<^isub>n)"} is
wenzelm@20474
    96
  decomposed by inventing fixed variables @{text "x\<^isub>1, \<dots>,
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
  "\<And>"} 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) \<equiv> 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 "\<And>x :: \<alpha>. P
wenzelm@20474
   235
  x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for schematic @{text "?x"}
wenzelm@20474
   236
  of fixed type @{text "\<alpha>"}.  Local derivations accumulate more and
wenzelm@20474
   237
  more explicit references to hypotheses: @{text "A\<^isub>1, \<dots>,
wenzelm@20458
   238
  A\<^isub>n \<turnstile> B"} where @{text "A\<^isub>1, \<dots>, 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 "\<Longrightarrow>"} introduction rule:
wenzelm@20458
   255
  \[
wenzelm@42666
   256
  \infer[(@{text "\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> 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 "#\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> 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 \<equiv> t"},
wenzelm@20459
   270
  with the following export rule to reverse the effect:
wenzelm@20458
   271
  \[
wenzelm@42666
   272
  \infer[(@{text "\<equiv>\<hyphen>expand"})]{@{text "\<Gamma> - (x \<equiv> t) \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
wenzelm@20458
   273
  \]
wenzelm@20474
   274
  This works, because the assumption @{text "x \<equiv> 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 "\<Gamma>"} 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 \<turnstile> 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
  "\<Longrightarrow>\<hyphen>intro"} or @{text "#\<Longrightarrow>\<hyphen>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 \<equiv> 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 "\<And>/\<Longrightarrow>"} 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 "\<And>/\<Longrightarrow>"} 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 "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"}
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 \<Rightarrow> bool"
wenzelm@39853
   459
wenzelm@39853
   460
  have "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> 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: "\<exists>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