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