doc-src/IsarImplementation/Thy/document/proof.tex
author wenzelm
Wed, 13 Dec 2006 16:26:45 +0100
changeset 21827 0b1d07f79c1e
parent 20797 c1f0bc7e7d80
child 22568 ed7aa5a350ef
permissions -rw-r--r--
updated;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     1
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     2
\begin{isabellebody}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     3
\def\isabellecontext{proof}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     5
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     7
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     8
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     9
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    10
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    11
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    12
\isatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    13
\isacommand{theory}\isamarkupfalse%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    14
\ {\isachardoublequoteopen}proof{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    15
\endisatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    16
{\isafoldtheory}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    17
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    18
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    19
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    20
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    21
%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
    22
\isamarkupchapter{Structured proofs%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    23
}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    24
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    25
%
20474
wenzelm
parents: 20472
diff changeset
    26
\isamarkupsection{Variables \label{sec:variables}%
20027
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
    27
}
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
    28
\isamarkuptrue%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
    29
%
20063
d8d9ea6a6b55 updated;
wenzelm
parents: 20043
diff changeset
    30
\begin{isamarkuptext}%
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    31
Any variable that is not explicitly bound by \isa{{\isasymlambda}}-abstraction
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    32
  is considered as ``free''.  Logically, free variables act like
20474
wenzelm
parents: 20472
diff changeset
    33
  outermost universal quantification at the sequent level: \isa{A\isactrlisub {\isadigit{1}}{\isacharparenleft}x{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n{\isacharparenleft}x{\isacharparenright}\ {\isasymturnstile}\ B{\isacharparenleft}x{\isacharparenright}} means that the result
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    34
  holds \emph{for all} values of \isa{x}.  Free variables for
20474
wenzelm
parents: 20472
diff changeset
    35
  terms (not types) can be fully internalized into the logic: \isa{{\isasymturnstile}\ B{\isacharparenleft}x{\isacharparenright}} and \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} are interchangeable, provided
wenzelm
parents: 20472
diff changeset
    36
  that \isa{x} does not occur elsewhere in the context.
wenzelm
parents: 20472
diff changeset
    37
  Inspecting \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} more closely, we see that inside the
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    38
  quantifier, \isa{x} is essentially ``arbitrary, but fixed'',
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    39
  while from outside it appears as a place-holder for instantiation
20474
wenzelm
parents: 20472
diff changeset
    40
  (thanks to \isa{{\isasymAnd}} elimination).
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    41
20474
wenzelm
parents: 20472
diff changeset
    42
  The Pure logic represents the idea of variables being either inside
wenzelm
parents: 20472
diff changeset
    43
  or outside the current scope by providing separate syntactic
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    44
  categories for \emph{fixed variables} (e.g.\ \isa{x}) vs.\
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    45
  \emph{schematic variables} (e.g.\ \isa{{\isacharquery}x}).  Incidently, a
20474
wenzelm
parents: 20472
diff changeset
    46
  universal result \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} has the HHF normal form \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}x{\isacharparenright}}, which represents its generality nicely without requiring
wenzelm
parents: 20472
diff changeset
    47
  an explicit quantifier.  The same principle works for type
wenzelm
parents: 20472
diff changeset
    48
  variables: \isa{{\isasymturnstile}\ B{\isacharparenleft}{\isacharquery}{\isasymalpha}{\isacharparenright}} represents the idea of ``\isa{{\isasymturnstile}\ {\isasymforall}{\isasymalpha}{\isachardot}\ B{\isacharparenleft}{\isasymalpha}{\isacharparenright}}'' without demanding a truly polymorphic framework.
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    49
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    50
  \medskip Additional care is required to treat type variables in a
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    51
  way that facilitates type-inference.  In principle, term variables
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    52
  depend on type variables, which means that type variables would have
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    53
  to be declared first.  For example, a raw type-theoretic framework
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    54
  would demand the context to be constructed in stages as follows:
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    55
  \isa{{\isasymGamma}\ {\isacharequal}\ {\isasymalpha}{\isacharcolon}\ type{\isacharcomma}\ x{\isacharcolon}\ {\isasymalpha}{\isacharcomma}\ a{\isacharcolon}\ A{\isacharparenleft}x\isactrlisub {\isasymalpha}{\isacharparenright}}.
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    56
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    57
  We allow a slightly less formalistic mode of operation: term
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    58
  variables \isa{x} are fixed without specifying a type yet
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    59
  (essentially \emph{all} potential occurrences of some instance
20474
wenzelm
parents: 20472
diff changeset
    60
  \isa{x\isactrlisub {\isasymtau}} are fixed); the first occurrence of \isa{x}
wenzelm
parents: 20472
diff changeset
    61
  within a specific term assigns its most general type, which is then
wenzelm
parents: 20472
diff changeset
    62
  maintained consistently in the context.  The above example becomes
wenzelm
parents: 20472
diff changeset
    63
  \isa{{\isasymGamma}\ {\isacharequal}\ x{\isacharcolon}\ term{\isacharcomma}\ {\isasymalpha}{\isacharcolon}\ type{\isacharcomma}\ A{\isacharparenleft}x\isactrlisub {\isasymalpha}{\isacharparenright}}, where type \isa{{\isasymalpha}} is fixed \emph{after} term \isa{x}, and the constraint
wenzelm
parents: 20472
diff changeset
    64
  \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}} is an implicit consequence of the occurrence of
wenzelm
parents: 20472
diff changeset
    65
  \isa{x\isactrlisub {\isasymalpha}} in the subsequent proposition.
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    66
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    67
  This twist of dependencies is also accommodated by the reverse
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    68
  operation of exporting results from a context: a type variable
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    69
  \isa{{\isasymalpha}} is considered fixed as long as it occurs in some fixed
20474
wenzelm
parents: 20472
diff changeset
    70
  term variable of the context.  For example, exporting \isa{x{\isacharcolon}\ term{\isacharcomma}\ {\isasymalpha}{\isacharcolon}\ type\ {\isasymturnstile}\ x\isactrlisub {\isasymalpha}\ {\isacharequal}\ x\isactrlisub {\isasymalpha}} produces in the first step
wenzelm
parents: 20472
diff changeset
    71
  \isa{x{\isacharcolon}\ term\ {\isasymturnstile}\ x\isactrlisub {\isasymalpha}\ {\isacharequal}\ x\isactrlisub {\isasymalpha}} for fixed \isa{{\isasymalpha}},
wenzelm
parents: 20472
diff changeset
    72
  and only in the second step \isa{{\isasymturnstile}\ {\isacharquery}x\isactrlisub {\isacharquery}\isactrlisub {\isasymalpha}\ {\isacharequal}\ {\isacharquery}x\isactrlisub {\isacharquery}\isactrlisub {\isasymalpha}} for schematic \isa{{\isacharquery}x} and \isa{{\isacharquery}{\isasymalpha}}.
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    73
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    74
  \medskip The Isabelle/Isar proof context manages the gory details of
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    75
  term vs.\ type variables, with high-level principles for moving the
20474
wenzelm
parents: 20472
diff changeset
    76
  frontier between fixed and schematic variables.
wenzelm
parents: 20472
diff changeset
    77
wenzelm
parents: 20472
diff changeset
    78
  The \isa{add{\isacharunderscore}fixes} operation explictly declares fixed
wenzelm
parents: 20472
diff changeset
    79
  variables; the \isa{declare{\isacharunderscore}term} operation absorbs a term into
wenzelm
parents: 20472
diff changeset
    80
  a context by fixing new type variables and adding syntactic
wenzelm
parents: 20472
diff changeset
    81
  constraints.
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    82
20474
wenzelm
parents: 20472
diff changeset
    83
  The \isa{export} operation is able to perform the main work of
wenzelm
parents: 20472
diff changeset
    84
  generalizing term and type variables as sketched above, assuming
wenzelm
parents: 20472
diff changeset
    85
  that fixing variables and terms have been declared properly.
wenzelm
parents: 20472
diff changeset
    86
wenzelm
parents: 20472
diff changeset
    87
  There \isa{import} operation makes a generalized fact a genuine
wenzelm
parents: 20472
diff changeset
    88
  part of the context, by inventing fixed variables for the schematic
wenzelm
parents: 20472
diff changeset
    89
  ones.  The effect can be reversed by using \isa{export} later,
wenzelm
parents: 20472
diff changeset
    90
  potentially with an extended context; the result is equivalent to
wenzelm
parents: 20472
diff changeset
    91
  the original modulo renaming of schematic variables.
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    92
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
    93
  The \isa{focus} operation provides a variant of \isa{import}
20474
wenzelm
parents: 20472
diff changeset
    94
  for nested propositions (with explicit quantification): \isa{{\isasymAnd}x\isactrlisub {\isadigit{1}}\ {\isasymdots}\ x\isactrlisub n{\isachardot}\ B{\isacharparenleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n{\isacharparenright}} is
wenzelm
parents: 20472
diff changeset
    95
  decomposed by inventing fixed variables \isa{x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n} for the body.%
20063
d8d9ea6a6b55 updated;
wenzelm
parents: 20043
diff changeset
    96
\end{isamarkuptext}%
d8d9ea6a6b55 updated;
wenzelm
parents: 20043
diff changeset
    97
\isamarkuptrue%
d8d9ea6a6b55 updated;
wenzelm
parents: 20043
diff changeset
    98
%
20027
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
    99
\isadelimmlref
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   100
%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   101
\endisadelimmlref
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   102
%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   103
\isatagmlref
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   104
%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   105
\begin{isamarkuptext}%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   106
\begin{mldecls}
20474
wenzelm
parents: 20472
diff changeset
   107
  \indexml{Variable.add-fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
wenzelm
parents: 20472
diff changeset
   108
\verb|  string list -> Proof.context -> string list * Proof.context| \\
20797
c1f0bc7e7d80 renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents: 20547
diff changeset
   109
  \indexml{Variable.variant-fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
20474
wenzelm
parents: 20472
diff changeset
   110
\verb|  string list -> Proof.context -> string list * Proof.context| \\
20027
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   111
  \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   112
  \indexml{Variable.declare-constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   113
  \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   114
  \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
20474
wenzelm
parents: 20472
diff changeset
   115
  \indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
wenzelm
parents: 20472
diff changeset
   116
\verb|  ((ctyp list * cterm list) * thm list) * Proof.context| \\
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   117
  \indexml{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
20027
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   118
  \end{mldecls}
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   119
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   120
  \begin{description}
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   121
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   122
  \item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   123
  variables \isa{xs}, returning the resulting internal names.  By
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   124
  default, the internal representation coincides with the external
20474
wenzelm
parents: 20472
diff changeset
   125
  one, which also means that the given variables must not be fixed
wenzelm
parents: 20472
diff changeset
   126
  already.  There is a different policy within a local proof body: the
wenzelm
parents: 20472
diff changeset
   127
  given names are just hints for newly invented Skolem variables.
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   128
20797
c1f0bc7e7d80 renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents: 20547
diff changeset
   129
  \item \verb|Variable.variant_fixes| is similar to \verb|Variable.add_fixes|, but always produces fresh variants of the given
20474
wenzelm
parents: 20472
diff changeset
   130
  names.
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   131
20063
d8d9ea6a6b55 updated;
wenzelm
parents: 20043
diff changeset
   132
  \item \verb|Variable.declare_term|~\isa{t\ ctxt} declares term
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   133
  \isa{t} to belong to the context.  This automatically fixes new
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   134
  type variables, but not term variables.  Syntactic constraints for
20474
wenzelm
parents: 20472
diff changeset
   135
  type and term variables are declared uniformly, though.
20063
d8d9ea6a6b55 updated;
wenzelm
parents: 20043
diff changeset
   136
20474
wenzelm
parents: 20472
diff changeset
   137
  \item \verb|Variable.declare_constraints|~\isa{t\ ctxt} declares
wenzelm
parents: 20472
diff changeset
   138
  syntactic constraints from term \isa{t}, without making it part
wenzelm
parents: 20472
diff changeset
   139
  of the context yet.
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   140
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   141
  \item \verb|Variable.export|~\isa{inner\ outer\ thms} generalizes
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   142
  fixed type and term variables in \isa{thms} according to the
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   143
  difference of the \isa{inner} and \isa{outer} context,
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   144
  following the principles sketched above.
20063
d8d9ea6a6b55 updated;
wenzelm
parents: 20043
diff changeset
   145
20471
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   146
  \item \verb|Variable.polymorphic|~\isa{ctxt\ ts} generalizes type
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   147
  variables in \isa{ts} as far as possible, even those occurring
ffafbd4103c0 updated;
wenzelm
parents: 20460
diff changeset
   148
  in fixed term variables.  The default policy of type-inference is to
20474
wenzelm
parents: 20472
diff changeset
   149
  fix newly introduced type variables, which is essentially reversed
wenzelm
parents: 20472
diff changeset
   150
  with \verb|Variable.polymorphic|: here the given terms are detached
wenzelm
parents: 20472
diff changeset
   151
  from the context as far as possible.
20027
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   152
20474
wenzelm
parents: 20472
diff changeset
   153
  \item \verb|Variable.import|~\isa{open\ thms\ ctxt} invents fixed
wenzelm
parents: 20472
diff changeset
   154
  type and term variables for the schematic ones occurring in \isa{thms}.  The \isa{open} flag indicates whether the fixed names
wenzelm
parents: 20472
diff changeset
   155
  should be accessible to the user, otherwise newly introduced names
wenzelm
parents: 20472
diff changeset
   156
  are marked as ``internal'' (\secref{sec:names}).
20027
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   157
20474
wenzelm
parents: 20472
diff changeset
   158
  \item \verb|Variable.focus|~\isa{B} decomposes the outermost \isa{{\isasymAnd}} prefix of proposition \isa{B}.
20027
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   159
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   160
  \end{description}%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   161
\end{isamarkuptext}%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   162
\isamarkuptrue%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   163
%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   164
\endisatagmlref
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   165
{\isafoldmlref}%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   166
%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   167
\isadelimmlref
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   168
%
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   169
\endisadelimmlref
413d4224269b updated;
wenzelm
parents: 18537
diff changeset
   170
%
20474
wenzelm
parents: 20472
diff changeset
   171
\isamarkupsection{Assumptions \label{sec:assumptions}%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   172
}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   173
\isamarkuptrue%
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   174
%
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   175
\begin{isamarkuptext}%
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   176
An \emph{assumption} is a proposition that it is postulated in the
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   177
  current context.  Local conclusions may use assumptions as
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   178
  additional facts, but this imposes implicit hypotheses that weaken
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   179
  the overall statement.
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   180
20474
wenzelm
parents: 20472
diff changeset
   181
  Assumptions are restricted to fixed non-schematic statements, i.e.\
wenzelm
parents: 20472
diff changeset
   182
  all generality needs to be expressed by explicit quantifiers.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   183
  Nevertheless, the result will be in HHF normal form with outermost
20474
wenzelm
parents: 20472
diff changeset
   184
  quantifiers stripped.  For example, by assuming \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ P\ x} we get \isa{{\isasymAnd}x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isachardot}\ P\ x\ {\isasymturnstile}\ P\ {\isacharquery}x} for schematic \isa{{\isacharquery}x}
wenzelm
parents: 20472
diff changeset
   185
  of fixed type \isa{{\isasymalpha}}.  Local derivations accumulate more and
wenzelm
parents: 20472
diff changeset
   186
  more explicit references to hypotheses: \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} where \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n} needs to
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   187
  be covered by the assumptions of the current context.
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   188
20459
wenzelm
parents: 20458
diff changeset
   189
  \medskip The \isa{add{\isacharunderscore}assms} operation augments the context by
wenzelm
parents: 20458
diff changeset
   190
  local assumptions, which are parameterized by an arbitrary \isa{export} rule (see below).
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   191
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   192
  The \isa{export} operation moves facts from a (larger) inner
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   193
  context into a (smaller) outer context, by discharging the
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   194
  difference of the assumptions as specified by the associated export
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   195
  rules.  Note that the discharged portion is determined by the
20459
wenzelm
parents: 20458
diff changeset
   196
  difference contexts, not the facts being exported!  There is a
wenzelm
parents: 20458
diff changeset
   197
  separate flag to indicate a goal context, where the result is meant
wenzelm
parents: 20458
diff changeset
   198
  to refine an enclosing sub-goal of a structured proof state (cf.\
wenzelm
parents: 20458
diff changeset
   199
  \secref{sec:isar-proof-state}).
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   200
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   201
  \medskip The most basic export rule discharges assumptions directly
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   202
  by means of the \isa{{\isasymLongrightarrow}} introduction rule:
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   203
  \[
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   204
  \infer[(\isa{{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   205
  \]
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   206
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   207
  The variant for goal refinements marks the newly introduced
20474
wenzelm
parents: 20472
diff changeset
   208
  premises, which causes the canonical Isar goal refinement scheme to
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   209
  enforce unification with local premises within the goal:
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   210
  \[
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   211
  \infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   212
  \]
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   213
20474
wenzelm
parents: 20472
diff changeset
   214
  \medskip Alternative versions of assumptions may perform arbitrary
wenzelm
parents: 20472
diff changeset
   215
  transformations on export, as long as the corresponding portion of
20459
wenzelm
parents: 20458
diff changeset
   216
  hypotheses is removed from the given facts.  For example, a local
wenzelm
parents: 20458
diff changeset
   217
  definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t},
wenzelm
parents: 20458
diff changeset
   218
  with the following export rule to reverse the effect:
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   219
  \[
20491
wenzelm
parents: 20474
diff changeset
   220
  \infer[(\isa{{\isasymequiv}{\isacharminus}expand})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   221
  \]
20474
wenzelm
parents: 20472
diff changeset
   222
  This works, because the assumption \isa{x\ {\isasymequiv}\ t} was introduced in
wenzelm
parents: 20472
diff changeset
   223
  a context with \isa{x} being fresh, so \isa{x} does not
wenzelm
parents: 20472
diff changeset
   224
  occur in \isa{{\isasymGamma}} here.%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   225
\end{isamarkuptext}%
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   226
\isamarkuptrue%
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   227
%
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   228
\isadelimmlref
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   229
%
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   230
\endisadelimmlref
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   231
%
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   232
\isatagmlref
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   233
%
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   234
\begin{isamarkuptext}%
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   235
\begin{mldecls}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   236
  \indexmltype{Assumption.export}\verb|type Assumption.export| \\
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   237
  \indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
20459
wenzelm
parents: 20458
diff changeset
   238
  \indexml{Assumption.add-assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
wenzelm
parents: 20458
diff changeset
   239
\verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
wenzelm
parents: 20458
diff changeset
   240
  \indexml{Assumption.add-assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
wenzelm
parents: 20458
diff changeset
   241
\verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   242
  \indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   243
  \end{mldecls}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   244
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   245
  \begin{description}
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   246
20459
wenzelm
parents: 20458
diff changeset
   247
  \item \verb|Assumption.export| represents arbitrary export
wenzelm
parents: 20458
diff changeset
   248
  rules, which is any function of type \verb|bool -> cterm list -> thm -> thm|,
wenzelm
parents: 20458
diff changeset
   249
  where the \verb|bool| indicates goal mode, and the \verb|cterm list| the collection of assumptions to be discharged
wenzelm
parents: 20458
diff changeset
   250
  simultaneously.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   251
20459
wenzelm
parents: 20458
diff changeset
   252
  \item \verb|Assumption.assume|~\isa{A} turns proposition \isa{A} into a raw assumption \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the conclusion
wenzelm
parents: 20458
diff changeset
   253
  \isa{A{\isacharprime}} is in HHF normal form.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   254
20474
wenzelm
parents: 20472
diff changeset
   255
  \item \verb|Assumption.add_assms|~\isa{r\ As} augments the context
wenzelm
parents: 20472
diff changeset
   256
  by assumptions \isa{As} with export rule \isa{r}.  The
wenzelm
parents: 20472
diff changeset
   257
  resulting facts are hypothetical theorems as produced by the raw
wenzelm
parents: 20472
diff changeset
   258
  \verb|Assumption.assume|.
20459
wenzelm
parents: 20458
diff changeset
   259
wenzelm
parents: 20458
diff changeset
   260
  \item \verb|Assumption.add_assumes|~\isa{As} is a special case of
wenzelm
parents: 20458
diff changeset
   261
  \verb|Assumption.add_assms| where the export rule performs \isa{{\isasymLongrightarrow}{\isacharunderscore}intro} or \isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro}, depending on goal mode.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   262
20474
wenzelm
parents: 20472
diff changeset
   263
  \item \verb|Assumption.export|~\isa{is{\isacharunderscore}goal\ inner\ outer\ thm}
wenzelm
parents: 20472
diff changeset
   264
  exports result \isa{thm} from the the \isa{inner} context
20459
wenzelm
parents: 20458
diff changeset
   265
  back into the \isa{outer} one; \isa{is{\isacharunderscore}goal\ {\isacharequal}\ true} means
wenzelm
parents: 20458
diff changeset
   266
  this is a goal context.  The result is in HHF normal form.  Note
wenzelm
parents: 20458
diff changeset
   267
  that \verb|ProofContext.export| combines \verb|Variable.export|
wenzelm
parents: 20458
diff changeset
   268
  and \verb|Assumption.export| in the canonical way.
20458
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   269
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   270
  \end{description}%
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   271
\end{isamarkuptext}%
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   272
\isamarkuptrue%
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   273
%
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   274
\endisatagmlref
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   275
{\isafoldmlref}%
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   276
%
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   277
\isadelimmlref
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   278
%
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   279
\endisadelimmlref
ab1d60e1ee31 explain assumptions;
wenzelm
parents: 20452
diff changeset
   280
%
20520
wenzelm
parents: 20491
diff changeset
   281
\isamarkupsection{Results%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   282
}
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   283
\isamarkuptrue%
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   284
%
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   285
\begin{isamarkuptext}%
20472
wenzelm
parents: 20471
diff changeset
   286
Local results are established by monotonic reasoning from facts
20474
wenzelm
parents: 20472
diff changeset
   287
  within a context.  This allows common combinations of theorems,
wenzelm
parents: 20472
diff changeset
   288
  e.g.\ via \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} elimination, resolution rules, or equational
wenzelm
parents: 20472
diff changeset
   289
  reasoning, see \secref{sec:thms}.  Unaccounted context manipulations
wenzelm
parents: 20472
diff changeset
   290
  should be avoided, notably raw \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} introduction or ad-hoc
20472
wenzelm
parents: 20471
diff changeset
   291
  references to free variables or assumptions not present in the proof
wenzelm
parents: 20471
diff changeset
   292
  context.
wenzelm
parents: 20471
diff changeset
   293
20491
wenzelm
parents: 20474
diff changeset
   294
  \medskip The \isa{SUBPROOF} combinator allows to structure a
wenzelm
parents: 20474
diff changeset
   295
  tactical proof recursively by decomposing a selected sub-goal:
wenzelm
parents: 20474
diff changeset
   296
  \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ A{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ B{\isacharparenleft}x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}} is turned into \isa{B{\isacharparenleft}x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymdots}}
wenzelm
parents: 20474
diff changeset
   297
  after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}.  This means
wenzelm
parents: 20474
diff changeset
   298
  the tactic needs to solve the conclusion, but may use the premise as
wenzelm
parents: 20474
diff changeset
   299
  a local fact, for locally fixed variables.
20472
wenzelm
parents: 20471
diff changeset
   300
20491
wenzelm
parents: 20474
diff changeset
   301
  The \isa{prove} operation provides an interface for structured
wenzelm
parents: 20474
diff changeset
   302
  backwards reasoning under program control, with some explicit sanity
wenzelm
parents: 20474
diff changeset
   303
  checks of the result.  The goal context can be augmented by
wenzelm
parents: 20474
diff changeset
   304
  additional fixed variables (cf.\ \secref{sec:variables}) and
wenzelm
parents: 20474
diff changeset
   305
  assumptions (cf.\ \secref{sec:assumptions}), which will be available
wenzelm
parents: 20474
diff changeset
   306
  as local facts during the proof and discharged into implications in
wenzelm
parents: 20474
diff changeset
   307
  the result.  Type and term variables are generalized as usual,
wenzelm
parents: 20474
diff changeset
   308
  according to the context.
20472
wenzelm
parents: 20471
diff changeset
   309
20491
wenzelm
parents: 20474
diff changeset
   310
  The \isa{obtain} operation produces results by eliminating
wenzelm
parents: 20474
diff changeset
   311
  existing facts by means of a given tactic.  This acts like a dual
wenzelm
parents: 20474
diff changeset
   312
  conclusion: the proof demonstrates that the context may be augmented
wenzelm
parents: 20474
diff changeset
   313
  by certain fixed variables and assumptions.  See also
wenzelm
parents: 20474
diff changeset
   314
  \cite{isabelle-isar-ref} for the user-level \isa{{\isasymOBTAIN}} and
wenzelm
parents: 20474
diff changeset
   315
  \isa{{\isasymGUESS}} elements.  Final results, which may not refer to
wenzelm
parents: 20474
diff changeset
   316
  the parameters in the conclusion, need to exported explicitly into
wenzelm
parents: 20474
diff changeset
   317
  the original context.%
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   318
\end{isamarkuptext}%
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   319
\isamarkuptrue%
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20221
diff changeset
   320
%
20472
wenzelm
parents: 20471
diff changeset
   321
\isadelimmlref
wenzelm
parents: 20471
diff changeset
   322
%
wenzelm
parents: 20471
diff changeset
   323
\endisadelimmlref
wenzelm
parents: 20471
diff changeset
   324
%
wenzelm
parents: 20471
diff changeset
   325
\isatagmlref
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   326
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   327
\begin{isamarkuptext}%
20472
wenzelm
parents: 20471
diff changeset
   328
\begin{mldecls}
20491
wenzelm
parents: 20474
diff changeset
   329
  \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
wenzelm
parents: 20474
diff changeset
   330
\verb|    params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
wenzelm
parents: 20474
diff changeset
   331
\verb|    prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
20547
wenzelm
parents: 20542
diff changeset
   332
  \end{mldecls}
wenzelm
parents: 20542
diff changeset
   333
  \begin{mldecls}
20472
wenzelm
parents: 20471
diff changeset
   334
  \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
wenzelm
parents: 20471
diff changeset
   335
\verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
wenzelm
parents: 20471
diff changeset
   336
  \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
wenzelm
parents: 20471
diff changeset
   337
\verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
20547
wenzelm
parents: 20542
diff changeset
   338
  \end{mldecls}
wenzelm
parents: 20542
diff changeset
   339
  \begin{mldecls}
20491
wenzelm
parents: 20474
diff changeset
   340
  \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
20542
a54ca4e90874 more on theorems;
wenzelm
parents: 20520
diff changeset
   341
\verb|  thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
20472
wenzelm
parents: 20471
diff changeset
   342
  \end{mldecls}
wenzelm
parents: 20471
diff changeset
   343
wenzelm
parents: 20471
diff changeset
   344
  \begin{description}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   345
20491
wenzelm
parents: 20474
diff changeset
   346
  \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a
wenzelm
parents: 20474
diff changeset
   347
  particular sub-goal, producing an extended context and a reduced
wenzelm
parents: 20474
diff changeset
   348
  goal, which needs to be solved by the given tactic.  All schematic
wenzelm
parents: 20474
diff changeset
   349
  parameters of the goal are imported into the context as fixed ones,
wenzelm
parents: 20474
diff changeset
   350
  which may not be instantiated in the sub-proof.
wenzelm
parents: 20474
diff changeset
   351
20474
wenzelm
parents: 20472
diff changeset
   352
  \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context augmented by fixed variables \isa{xs} and
wenzelm
parents: 20472
diff changeset
   353
  assumptions \isa{As}, and applies tactic \isa{tac} to solve
wenzelm
parents: 20472
diff changeset
   354
  it.  The latter may depend on the local assumptions being presented
wenzelm
parents: 20472
diff changeset
   355
  as facts.  The result is in HHF normal form.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   356
20472
wenzelm
parents: 20471
diff changeset
   357
  \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
20491
wenzelm
parents: 20474
diff changeset
   358
  states several conclusions simultaneously.  The goal is encoded by
21827
0b1d07f79c1e updated;
wenzelm
parents: 20797
diff changeset
   359
  means of Pure conjunction; \verb|Goal.conjunction_tac| will turn this
0b1d07f79c1e updated;
wenzelm
parents: 20797
diff changeset
   360
  into a collection of individual subgoals.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   361
20491
wenzelm
parents: 20474
diff changeset
   362
  \item \verb|Obtain.result|~\isa{tac\ thms\ ctxt} eliminates the
wenzelm
parents: 20474
diff changeset
   363
  given facts using a tactic, which results in additional fixed
wenzelm
parents: 20474
diff changeset
   364
  variables and assumptions in the context.  Final results need to be
wenzelm
parents: 20474
diff changeset
   365
  exported explicitly.
20472
wenzelm
parents: 20471
diff changeset
   366
wenzelm
parents: 20471
diff changeset
   367
  \end{description}%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   368
\end{isamarkuptext}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   369
\isamarkuptrue%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   370
%
20472
wenzelm
parents: 20471
diff changeset
   371
\endisatagmlref
wenzelm
parents: 20471
diff changeset
   372
{\isafoldmlref}%
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   373
%
20472
wenzelm
parents: 20471
diff changeset
   374
\isadelimmlref
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   375
%
20472
wenzelm
parents: 20471
diff changeset
   376
\endisadelimmlref
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   377
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   378
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   379
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   380
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   381
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   382
\isatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   383
\isacommand{end}\isamarkupfalse%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   384
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   385
\endisatagtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   386
{\isafoldtheory}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   387
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   388
\isadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   389
%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   390
\endisadelimtheory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   391
\isanewline
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   392
\end{isabellebody}%
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   393
%%% Local Variables:
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   394
%%% mode: latex
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   395
%%% TeX-master: "root"
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   396
%%% End: