3 \def\isabellecontext{proof}%
13 \isacommand{theory}\isamarkupfalse%
14 \ {\isachardoublequoteopen}proof{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
22 \isamarkupchapter{Structured proofs%
26 \isamarkupsection{Variables \label{sec:variables}%
30 \begin{isamarkuptext}%
31 Any variable that is not explicitly bound by \isa{{\isasymlambda}}-abstraction
32 is considered as ``free''. Logically, free variables act like
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
34 holds \emph{for all} values of \isa{x}. Free variables for
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
36 that \isa{x} does not occur elsewhere in the context.
37 Inspecting \isa{{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ B{\isacharparenleft}x{\isacharparenright}} more closely, we see that inside the
38 quantifier, \isa{x} is essentially ``arbitrary, but fixed'',
39 while from outside it appears as a place-holder for instantiation
40 (thanks to \isa{{\isasymAnd}} elimination).
42 The Pure logic represents the idea of variables being either inside
43 or outside the current scope by providing separate syntactic
44 categories for \emph{fixed variables} (e.g.\ \isa{x}) vs.\
45 \emph{schematic variables} (e.g.\ \isa{{\isacharquery}x}). Incidently, a
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
47 an explicit quantifier. The same principle works for type
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.
50 \medskip Additional care is required to treat type variables in a
51 way that facilitates type-inference. In principle, term variables
52 depend on type variables, which means that type variables would have
53 to be declared first. For example, a raw type-theoretic framework
54 would demand the context to be constructed in stages as follows:
55 \isa{{\isasymGamma}\ {\isacharequal}\ {\isasymalpha}{\isacharcolon}\ type{\isacharcomma}\ x{\isacharcolon}\ {\isasymalpha}{\isacharcomma}\ a{\isacharcolon}\ A{\isacharparenleft}x\isactrlisub {\isasymalpha}{\isacharparenright}}.
57 We allow a slightly less formalistic mode of operation: term
58 variables \isa{x} are fixed without specifying a type yet
59 (essentially \emph{all} potential occurrences of some instance
60 \isa{x\isactrlisub {\isasymtau}} are fixed); the first occurrence of \isa{x}
61 within a specific term assigns its most general type, which is then
62 maintained consistently in the context. The above example becomes
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
64 \isa{x\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}} is an implicit consequence of the occurrence of
65 \isa{x\isactrlisub {\isasymalpha}} in the subsequent proposition.
67 This twist of dependencies is also accommodated by the reverse
68 operation of exporting results from a context: a type variable
69 \isa{{\isasymalpha}} is considered fixed as long as it occurs in some fixed
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
71 \isa{x{\isacharcolon}\ term\ {\isasymturnstile}\ x\isactrlisub {\isasymalpha}\ {\isacharequal}\ x\isactrlisub {\isasymalpha}} for fixed \isa{{\isasymalpha}},
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}}.
74 \medskip The Isabelle/Isar proof context manages the gory details of
75 term vs.\ type variables, with high-level principles for moving the
76 frontier between fixed and schematic variables.
78 The \isa{add{\isacharunderscore}fixes} operation explictly declares fixed
79 variables; the \isa{declare{\isacharunderscore}term} operation absorbs a term into
80 a context by fixing new type variables and adding syntactic
83 The \isa{export} operation is able to perform the main work of
84 generalizing term and type variables as sketched above, assuming
85 that fixing variables and terms have been declared properly.
87 There \isa{import} operation makes a generalized fact a genuine
88 part of the context, by inventing fixed variables for the schematic
89 ones. The effect can be reversed by using \isa{export} later,
90 potentially with an extended context; the result is equivalent to
91 the original modulo renaming of schematic variables.
93 The \isa{focus} operation provides a variant of \isa{import}
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
95 decomposed by inventing fixed variables \isa{x\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlisub n} for the body.%
105 \begin{isamarkuptext}%
107 \indexml{Variable.add\_fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
108 \verb| string list -> Proof.context -> string list * Proof.context| \\
109 \indexml{Variable.variant\_fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
110 \verb| string list -> Proof.context -> string list * Proof.context| \\
111 \indexml{Variable.declare\_term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
112 \indexml{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
113 \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
114 \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
115 \indexml{Variable.import\_thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
116 \verb| ((ctyp list * cterm list) * thm list) * Proof.context| \\
117 \indexml{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
122 \item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term
123 variables \isa{xs}, returning the resulting internal names. By
124 default, the internal representation coincides with the external
125 one, which also means that the given variables must not be fixed
126 already. There is a different policy within a local proof body: the
127 given names are just hints for newly invented Skolem variables.
129 \item \verb|Variable.variant_fixes| is similar to \verb|Variable.add_fixes|, but always produces fresh variants of the given
132 \item \verb|Variable.declare_term|~\isa{t\ ctxt} declares term
133 \isa{t} to belong to the context. This automatically fixes new
134 type variables, but not term variables. Syntactic constraints for
135 type and term variables are declared uniformly, though.
137 \item \verb|Variable.declare_constraints|~\isa{t\ ctxt} declares
138 syntactic constraints from term \isa{t}, without making it part
141 \item \verb|Variable.export|~\isa{inner\ outer\ thms} generalizes
142 fixed type and term variables in \isa{thms} according to the
143 difference of the \isa{inner} and \isa{outer} context,
144 following the principles sketched above.
146 \item \verb|Variable.polymorphic|~\isa{ctxt\ ts} generalizes type
147 variables in \isa{ts} as far as possible, even those occurring
148 in fixed term variables. The default policy of type-inference is to
149 fix newly introduced type variables, which is essentially reversed
150 with \verb|Variable.polymorphic|: here the given terms are detached
151 from the context as far as possible.
153 \item \verb|Variable.import_thms|~\isa{open\ thms\ ctxt} invents fixed
154 type and term variables for the schematic ones occurring in \isa{thms}. The \isa{open} flag indicates whether the fixed names
155 should be accessible to the user, otherwise newly introduced names
156 are marked as ``internal'' (\secref{sec:names}).
158 \item \verb|Variable.focus|~\isa{B} decomposes the outermost \isa{{\isasymAnd}} prefix of proposition \isa{B}.
171 \isamarkupsection{Assumptions \label{sec:assumptions}%
175 \begin{isamarkuptext}%
176 An \emph{assumption} is a proposition that it is postulated in the
177 current context. Local conclusions may use assumptions as
178 additional facts, but this imposes implicit hypotheses that weaken
179 the overall statement.
181 Assumptions are restricted to fixed non-schematic statements, i.e.\
182 all generality needs to be expressed by explicit quantifiers.
183 Nevertheless, the result will be in HHF normal form with outermost
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}
185 of fixed type \isa{{\isasymalpha}}. Local derivations accumulate more and
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
187 be covered by the assumptions of the current context.
189 \medskip The \isa{add{\isacharunderscore}assms} operation augments the context by
190 local assumptions, which are parameterized by an arbitrary \isa{export} rule (see below).
192 The \isa{export} operation moves facts from a (larger) inner
193 context into a (smaller) outer context, by discharging the
194 difference of the assumptions as specified by the associated export
195 rules. Note that the discharged portion is determined by the
196 difference contexts, not the facts being exported! There is a
197 separate flag to indicate a goal context, where the result is meant
198 to refine an enclosing sub-goal of a structured proof state (cf.\
199 \secref{sec:isar-proof-state}).
201 \medskip The most basic export rule discharges assumptions directly
202 by means of the \isa{{\isasymLongrightarrow}} introduction rule:
204 \infer[(\isa{{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
207 The variant for goal refinements marks the newly introduced
208 premises, which causes the canonical Isar goal refinement scheme to
209 enforce unification with local premises within the goal:
211 \infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
214 \medskip Alternative versions of assumptions may perform arbitrary
215 transformations on export, as long as the corresponding portion of
216 hypotheses is removed from the given facts. For example, a local
217 definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t},
218 with the following export rule to reverse the effect:
220 \infer[(\isa{{\isasymequiv}{\isacharminus}expand})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
222 This works, because the assumption \isa{x\ {\isasymequiv}\ t} was introduced in
223 a context with \isa{x} being fresh, so \isa{x} does not
224 occur in \isa{{\isasymGamma}} here.%
234 \begin{isamarkuptext}%
236 \indexmltype{Assumption.export}\verb|type Assumption.export| \\
237 \indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
238 \indexml{Assumption.add\_assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
239 \verb| cterm list -> Proof.context -> thm list * Proof.context| \\
240 \indexml{Assumption.add\_assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
241 \verb| cterm list -> Proof.context -> thm list * Proof.context| \\
242 \indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
247 \item \verb|Assumption.export| represents arbitrary export
248 rules, which is any function of type \verb|bool -> cterm list -> thm -> thm|,
249 where the \verb|bool| indicates goal mode, and the \verb|cterm list| the collection of assumptions to be discharged
252 \item \verb|Assumption.assume|~\isa{A} turns proposition \isa{A} into a raw assumption \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the conclusion
253 \isa{A{\isacharprime}} is in HHF normal form.
255 \item \verb|Assumption.add_assms|~\isa{r\ As} augments the context
256 by assumptions \isa{As} with export rule \isa{r}. The
257 resulting facts are hypothetical theorems as produced by the raw
258 \verb|Assumption.assume|.
260 \item \verb|Assumption.add_assumes|~\isa{As} is a special case of
261 \verb|Assumption.add_assms| where the export rule performs \isa{{\isasymLongrightarrow}{\isacharunderscore}intro} or \isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro}, depending on goal mode.
263 \item \verb|Assumption.export|~\isa{is{\isacharunderscore}goal\ inner\ outer\ thm}
264 exports result \isa{thm} from the the \isa{inner} context
265 back into the \isa{outer} one; \isa{is{\isacharunderscore}goal\ {\isacharequal}\ true} means
266 this is a goal context. The result is in HHF normal form. Note
267 that \verb|ProofContext.export| combines \verb|Variable.export|
268 and \verb|Assumption.export| in the canonical way.
281 \isamarkupsection{Results%
285 \begin{isamarkuptext}%
286 Local results are established by monotonic reasoning from facts
287 within a context. This allows common combinations of theorems,
288 e.g.\ via \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} elimination, resolution rules, or equational
289 reasoning, see \secref{sec:thms}. Unaccounted context manipulations
290 should be avoided, notably raw \isa{{\isasymAnd}{\isacharslash}{\isasymLongrightarrow}} introduction or ad-hoc
291 references to free variables or assumptions not present in the proof
294 \medskip The \isa{SUBPROOF} combinator allows to structure a
295 tactical proof recursively by decomposing a selected sub-goal:
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}}
297 after fixing \isa{x} and assuming \isa{A{\isacharparenleft}x{\isacharparenright}}. This means
298 the tactic needs to solve the conclusion, but may use the premise as
299 a local fact, for locally fixed variables.
301 The \isa{prove} operation provides an interface for structured
302 backwards reasoning under program control, with some explicit sanity
303 checks of the result. The goal context can be augmented by
304 additional fixed variables (cf.\ \secref{sec:variables}) and
305 assumptions (cf.\ \secref{sec:assumptions}), which will be available
306 as local facts during the proof and discharged into implications in
307 the result. Type and term variables are generalized as usual,
308 according to the context.
310 The \isa{obtain} operation produces results by eliminating
311 existing facts by means of a given tactic. This acts like a dual
312 conclusion: the proof demonstrates that the context may be augmented
313 by certain fixed variables and assumptions. See also
314 \cite{isabelle-isar-ref} for the user-level \isa{{\isasymOBTAIN}} and
315 \isa{{\isasymGUESS}} elements. Final results, which may not refer to
316 the parameters in the conclusion, need to exported explicitly into
317 the original context.%
327 \begin{isamarkuptext}%
329 \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
330 \verb| params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
331 \verb| prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
334 \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
335 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
336 \indexml{Goal.prove\_multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
337 \verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
340 \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
341 \verb| thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
346 \item \verb|SUBPROOF|~\isa{tac} decomposes the structure of a
347 particular sub-goal, producing an extended context and a reduced
348 goal, which needs to be solved by the given tactic. All schematic
349 parameters of the goal are imported into the context as fixed ones,
350 which may not be instantiated in the sub-proof.
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
353 assumptions \isa{As}, and applies tactic \isa{tac} to solve
354 it. The latter may depend on the local assumptions being presented
355 as facts. The result is in HHF normal form.
357 \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
358 states several conclusions simultaneously. The goal is encoded by
359 means of Pure conjunction; \verb|Goal.conjunction_tac| will turn this
360 into a collection of individual subgoals.
362 \item \verb|Obtain.result|~\isa{tac\ thms\ ctxt} eliminates the
363 given facts using a tactic, which results in additional fixed
364 variables and assumptions in the context. Final results need to be
383 \isacommand{end}\isamarkupfalse%
395 %%% TeX-master: "root"