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