18537
|
1 |
|
|
2 |
(* $Id$ *)
|
|
3 |
|
|
4 |
theory "proof" imports base begin
|
|
5 |
|
20451
|
6 |
chapter {* Structured proofs *}
|
18537
|
7 |
|
20474
|
8 |
section {* Variables \label{sec:variables} *}
|
20026
|
9 |
|
20470
|
10 |
text {*
|
|
11 |
Any variable that is not explicitly bound by @{text "\<lambda>"}-abstraction
|
|
12 |
is considered as ``free''. Logically, free variables act like
|
20474
|
13 |
outermost universal quantification at the sequent level: @{text
|
20470
|
14 |
"A\<^isub>1(x), \<dots>, A\<^isub>n(x) \<turnstile> B(x)"} means that the result
|
|
15 |
holds \emph{for all} values of @{text "x"}. Free variables for
|
|
16 |
terms (not types) can be fully internalized into the logic: @{text
|
20474
|
17 |
"\<turnstile> B(x)"} and @{text "\<turnstile> \<And>x. B(x)"} are interchangeable, provided
|
|
18 |
that @{text "x"} does not occur elsewhere in the context.
|
|
19 |
Inspecting @{text "\<turnstile> \<And>x. B(x)"} more closely, we see that inside the
|
20470
|
20 |
quantifier, @{text "x"} is essentially ``arbitrary, but fixed'',
|
|
21 |
while from outside it appears as a place-holder for instantiation
|
20474
|
22 |
(thanks to @{text "\<And>"} elimination).
|
20470
|
23 |
|
20474
|
24 |
The Pure logic represents the idea of variables being either inside
|
|
25 |
or outside the current scope by providing separate syntactic
|
20470
|
26 |
categories for \emph{fixed variables} (e.g.\ @{text "x"}) vs.\
|
|
27 |
\emph{schematic variables} (e.g.\ @{text "?x"}). Incidently, a
|
20474
|
28 |
universal result @{text "\<turnstile> \<And>x. B(x)"} has the HHF normal form @{text
|
20470
|
29 |
"\<turnstile> B(?x)"}, which represents its generality nicely without requiring
|
20474
|
30 |
an explicit quantifier. The same principle works for type
|
|
31 |
variables: @{text "\<turnstile> B(?\<alpha>)"} represents the idea of ``@{text "\<turnstile>
|
20470
|
32 |
\<forall>\<alpha>. B(\<alpha>)"}'' without demanding a truly polymorphic framework.
|
|
33 |
|
|
34 |
\medskip Additional care is required to treat type variables in a
|
|
35 |
way that facilitates type-inference. In principle, term variables
|
|
36 |
depend on type variables, which means that type variables would have
|
|
37 |
to be declared first. For example, a raw type-theoretic framework
|
|
38 |
would demand the context to be constructed in stages as follows:
|
|
39 |
@{text "\<Gamma> = \<alpha>: type, x: \<alpha>, a: A(x\<^isub>\<alpha>)"}.
|
|
40 |
|
|
41 |
We allow a slightly less formalistic mode of operation: term
|
|
42 |
variables @{text "x"} are fixed without specifying a type yet
|
|
43 |
(essentially \emph{all} potential occurrences of some instance
|
20474
|
44 |
@{text "x\<^isub>\<tau>"} are fixed); the first occurrence of @{text "x"}
|
|
45 |
within a specific term assigns its most general type, which is then
|
|
46 |
maintained consistently in the context. The above example becomes
|
|
47 |
@{text "\<Gamma> = x: term, \<alpha>: type, A(x\<^isub>\<alpha>)"}, where type @{text
|
|
48 |
"\<alpha>"} is fixed \emph{after} term @{text "x"}, and the constraint
|
|
49 |
@{text "x :: \<alpha>"} is an implicit consequence of the occurrence of
|
|
50 |
@{text "x\<^isub>\<alpha>"} in the subsequent proposition.
|
20470
|
51 |
|
|
52 |
This twist of dependencies is also accommodated by the reverse
|
|
53 |
operation of exporting results from a context: a type variable
|
|
54 |
@{text "\<alpha>"} is considered fixed as long as it occurs in some fixed
|
|
55 |
term variable of the context. For example, exporting @{text "x:
|
20474
|
56 |
term, \<alpha>: type \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} produces in the first step
|
|
57 |
@{text "x: term \<turnstile> x\<^isub>\<alpha> = x\<^isub>\<alpha>"} for fixed @{text "\<alpha>"},
|
|
58 |
and only in the second step @{text "\<turnstile> ?x\<^isub>?\<^isub>\<alpha> =
|
|
59 |
?x\<^isub>?\<^isub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}.
|
20470
|
60 |
|
|
61 |
\medskip The Isabelle/Isar proof context manages the gory details of
|
|
62 |
term vs.\ type variables, with high-level principles for moving the
|
20474
|
63 |
frontier between fixed and schematic variables.
|
|
64 |
|
|
65 |
The @{text "add_fixes"} operation explictly declares fixed
|
|
66 |
variables; the @{text "declare_term"} operation absorbs a term into
|
|
67 |
a context by fixing new type variables and adding syntactic
|
|
68 |
constraints.
|
20470
|
69 |
|
20474
|
70 |
The @{text "export"} operation is able to perform the main work of
|
|
71 |
generalizing term and type variables as sketched above, assuming
|
|
72 |
that fixing variables and terms have been declared properly.
|
|
73 |
|
|
74 |
There @{text "import"} operation makes a generalized fact a genuine
|
|
75 |
part of the context, by inventing fixed variables for the schematic
|
|
76 |
ones. The effect can be reversed by using @{text "export"} later,
|
|
77 |
potentially with an extended context; the result is equivalent to
|
|
78 |
the original modulo renaming of schematic variables.
|
20470
|
79 |
|
|
80 |
The @{text "focus"} operation provides a variant of @{text "import"}
|
|
81 |
for nested propositions (with explicit quantification): @{text
|
20474
|
82 |
"\<And>x\<^isub>1 \<dots> x\<^isub>n. B(x\<^isub>1, \<dots>, x\<^isub>n)"} is
|
|
83 |
decomposed by inventing fixed variables @{text "x\<^isub>1, \<dots>,
|
|
84 |
x\<^isub>n"} for the body.
|
20470
|
85 |
*}
|
20064
|
86 |
|
20026
|
87 |
text %mlref {*
|
|
88 |
\begin{mldecls}
|
20474
|
89 |
@{index_ML Variable.add_fixes: "
|
|
90 |
string list -> Proof.context -> string list * Proof.context"} \\
|
|
91 |
@{index_ML Variable.invent_fixes: "
|
|
92 |
string list -> Proof.context -> string list * Proof.context"} \\
|
20026
|
93 |
@{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
|
20470
|
94 |
@{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
|
|
95 |
@{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
|
|
96 |
@{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
|
20474
|
97 |
@{index_ML Variable.import: "bool -> thm list -> Proof.context ->
|
|
98 |
((ctyp list * cterm list) * thm list) * Proof.context"} \\
|
20470
|
99 |
@{index_ML Variable.focus: "cterm -> Proof.context -> (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 |
|
|
111 |
\item @{ML Variable.invent_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 |
|
20474
|
136 |
\item @{ML Variable.import}~@{text "open thms ctxt"} invents fixed
|
|
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 |
|
18537
|
148 |
|
20474
|
149 |
section {* Assumptions \label{sec:assumptions} *}
|
20451
|
150 |
|
20458
|
151 |
text {*
|
|
152 |
An \emph{assumption} is a proposition that it is postulated in the
|
|
153 |
current context. Local conclusions may use assumptions as
|
|
154 |
additional facts, but this imposes implicit hypotheses that weaken
|
|
155 |
the overall statement.
|
|
156 |
|
20474
|
157 |
Assumptions are restricted to fixed non-schematic statements, i.e.\
|
|
158 |
all generality needs to be expressed by explicit quantifiers.
|
20458
|
159 |
Nevertheless, the result will be in HHF normal form with outermost
|
|
160 |
quantifiers stripped. For example, by assuming @{text "\<And>x :: \<alpha>. P
|
20474
|
161 |
x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for schematic @{text "?x"}
|
|
162 |
of fixed type @{text "\<alpha>"}. Local derivations accumulate more and
|
|
163 |
more explicit references to hypotheses: @{text "A\<^isub>1, \<dots>,
|
20458
|
164 |
A\<^isub>n \<turnstile> B"} where @{text "A\<^isub>1, \<dots>, A\<^isub>n"} needs to
|
|
165 |
be covered by the assumptions of the current context.
|
|
166 |
|
20459
|
167 |
\medskip The @{text "add_assms"} operation augments the context by
|
|
168 |
local assumptions, which are parameterized by an arbitrary @{text
|
|
169 |
"export"} rule (see below).
|
20458
|
170 |
|
|
171 |
The @{text "export"} operation moves facts from a (larger) inner
|
|
172 |
context into a (smaller) outer context, by discharging the
|
|
173 |
difference of the assumptions as specified by the associated export
|
|
174 |
rules. Note that the discharged portion is determined by the
|
20459
|
175 |
difference contexts, not the facts being exported! There is a
|
|
176 |
separate flag to indicate a goal context, where the result is meant
|
|
177 |
to refine an enclosing sub-goal of a structured proof state (cf.\
|
|
178 |
\secref{sec:isar-proof-state}).
|
20458
|
179 |
|
|
180 |
\medskip The most basic export rule discharges assumptions directly
|
|
181 |
by means of the @{text "\<Longrightarrow>"} introduction rule:
|
|
182 |
\[
|
|
183 |
\infer[(@{text "\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
|
|
184 |
\]
|
|
185 |
|
|
186 |
The variant for goal refinements marks the newly introduced
|
20474
|
187 |
premises, which causes the canonical Isar goal refinement scheme to
|
20458
|
188 |
enforce unification with local premises within the goal:
|
|
189 |
\[
|
|
190 |
\infer[(@{text "#\<Longrightarrow>_intro"})]{@{text "\<Gamma> \\ A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}
|
|
191 |
\]
|
|
192 |
|
20474
|
193 |
\medskip Alternative versions of assumptions may perform arbitrary
|
|
194 |
transformations on export, as long as the corresponding portion of
|
20459
|
195 |
hypotheses is removed from the given facts. For example, a local
|
|
196 |
definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"},
|
|
197 |
with the following export rule to reverse the effect:
|
20458
|
198 |
\[
|
20491
|
199 |
\infer[(@{text "\<equiv>-expand"})]{@{text "\<Gamma> \\ x \<equiv> t \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}
|
20458
|
200 |
\]
|
20474
|
201 |
This works, because the assumption @{text "x \<equiv> t"} was introduced in
|
|
202 |
a context with @{text "x"} being fresh, so @{text "x"} does not
|
|
203 |
occur in @{text "\<Gamma>"} here.
|
20458
|
204 |
*}
|
|
205 |
|
|
206 |
text %mlref {*
|
|
207 |
\begin{mldecls}
|
|
208 |
@{index_ML_type Assumption.export} \\
|
|
209 |
@{index_ML Assumption.assume: "cterm -> thm"} \\
|
|
210 |
@{index_ML Assumption.add_assms:
|
20459
|
211 |
"Assumption.export ->
|
|
212 |
cterm list -> Proof.context -> thm list * Proof.context"} \\
|
|
213 |
@{index_ML Assumption.add_assumes: "
|
|
214 |
cterm list -> Proof.context -> thm list * Proof.context"} \\
|
20458
|
215 |
@{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
|
|
216 |
\end{mldecls}
|
|
217 |
|
|
218 |
\begin{description}
|
|
219 |
|
20459
|
220 |
\item @{ML_type Assumption.export} represents arbitrary export
|
|
221 |
rules, which is any function of type @{ML_type "bool -> cterm list -> thm -> thm"},
|
|
222 |
where the @{ML_type "bool"} indicates goal mode, and the @{ML_type
|
|
223 |
"cterm list"} the collection of assumptions to be discharged
|
|
224 |
simultaneously.
|
20458
|
225 |
|
20459
|
226 |
\item @{ML Assumption.assume}~@{text "A"} turns proposition @{text
|
|
227 |
"A"} into a raw assumption @{text "A \<turnstile> A'"}, where the conclusion
|
|
228 |
@{text "A'"} is in HHF normal form.
|
20458
|
229 |
|
20474
|
230 |
\item @{ML Assumption.add_assms}~@{text "r As"} augments the context
|
|
231 |
by assumptions @{text "As"} with export rule @{text "r"}. The
|
|
232 |
resulting facts are hypothetical theorems as produced by the raw
|
|
233 |
@{ML Assumption.assume}.
|
20459
|
234 |
|
|
235 |
\item @{ML Assumption.add_assumes}~@{text "As"} is a special case of
|
|
236 |
@{ML Assumption.add_assms} where the export rule performs @{text
|
|
237 |
"\<Longrightarrow>_intro"} or @{text "#\<Longrightarrow>_intro"}, depending on goal mode.
|
20458
|
238 |
|
20474
|
239 |
\item @{ML Assumption.export}~@{text "is_goal inner outer thm"}
|
|
240 |
exports result @{text "thm"} from the the @{text "inner"} context
|
20459
|
241 |
back into the @{text "outer"} one; @{text "is_goal = true"} means
|
|
242 |
this is a goal context. The result is in HHF normal form. Note
|
|
243 |
that @{ML "ProofContext.export"} combines @{ML "Variable.export"}
|
|
244 |
and @{ML "Assumption.export"} in the canonical way.
|
20458
|
245 |
|
|
246 |
\end{description}
|
|
247 |
*}
|
20451
|
248 |
|
|
249 |
|
|
250 |
section {* Conclusions *}
|
|
251 |
|
18537
|
252 |
text {*
|
20472
|
253 |
Local results are established by monotonic reasoning from facts
|
20474
|
254 |
within a context. This allows common combinations of theorems,
|
|
255 |
e.g.\ via @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or equational
|
|
256 |
reasoning, see \secref{sec:thms}. Unaccounted context manipulations
|
|
257 |
should be avoided, notably raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc
|
20472
|
258 |
references to free variables or assumptions not present in the proof
|
|
259 |
context.
|
18537
|
260 |
|
20491
|
261 |
\medskip The @{text "SUBPROOF"} combinator allows to structure a
|
|
262 |
tactical proof recursively by decomposing a selected sub-goal:
|
|
263 |
@{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"}
|
|
264 |
after fixing @{text "x"} and assuming @{text "A(x)"}. This means
|
|
265 |
the tactic needs to solve the conclusion, but may use the premise as
|
|
266 |
a local fact, for locally fixed variables.
|
18537
|
267 |
|
20491
|
268 |
The @{text "prove"} operation provides an interface for structured
|
|
269 |
backwards reasoning under program control, with some explicit sanity
|
|
270 |
checks of the result. The goal context can be augmented by
|
|
271 |
additional fixed variables (cf.\ \secref{sec:variables}) and
|
|
272 |
assumptions (cf.\ \secref{sec:assumptions}), which will be available
|
|
273 |
as local facts during the proof and discharged into implications in
|
|
274 |
the result. Type and term variables are generalized as usual,
|
|
275 |
according to the context.
|
18537
|
276 |
|
20491
|
277 |
The @{text "obtain"} operation produces results by eliminating
|
|
278 |
existing facts by means of a given tactic. This acts like a dual
|
|
279 |
conclusion: the proof demonstrates that the context may be augmented
|
|
280 |
by certain fixed variables and assumptions. See also
|
|
281 |
\cite{isabelle-isar-ref} for the user-level @{text "\<OBTAIN>"} and
|
|
282 |
@{text "\<GUESS>"} elements. Final results, which may not refer to
|
|
283 |
the parameters in the conclusion, need to exported explicitly into
|
|
284 |
the original context.
|
18537
|
285 |
*}
|
|
286 |
|
20472
|
287 |
text %mlref {*
|
|
288 |
\begin{mldecls}
|
20491
|
289 |
@{index_ML SUBPROOF:
|
|
290 |
"({context: Proof.context, schematics: ctyp list * cterm list,
|
|
291 |
params: cterm list, asms: cterm list, concl: cterm,
|
|
292 |
prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\
|
20472
|
293 |
@{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
|
|
294 |
({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
|
|
295 |
@{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
|
|
296 |
({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
|
20491
|
297 |
@{index_ML Obtain.result: "(Proof.context -> tactic) ->
|
|
298 |
thm list -> Proof.context -> (cterm list * thm list) * Proof.context"}
|
20472
|
299 |
\end{mldecls}
|
18537
|
300 |
|
20472
|
301 |
\begin{description}
|
18537
|
302 |
|
20491
|
303 |
\item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a
|
|
304 |
particular sub-goal, producing an extended context and a reduced
|
|
305 |
goal, which needs to be solved by the given tactic. All schematic
|
|
306 |
parameters of the goal are imported into the context as fixed ones,
|
|
307 |
which may not be instantiated in the sub-proof.
|
|
308 |
|
20472
|
309 |
\item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
|
20474
|
310 |
"C"} in the context augmented by fixed variables @{text "xs"} and
|
|
311 |
assumptions @{text "As"}, and applies tactic @{text "tac"} to solve
|
|
312 |
it. The latter may depend on the local assumptions being presented
|
|
313 |
as facts. The result is in HHF normal form.
|
18537
|
314 |
|
20472
|
315 |
\item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
|
20491
|
316 |
states several conclusions simultaneously. The goal is encoded by
|
|
317 |
means of Pure conjunction; @{ML Tactic.conjunction_tac} will turn
|
|
318 |
this into a collection of individual subgoals.
|
20472
|
319 |
|
20491
|
320 |
\item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the
|
|
321 |
given facts using a tactic, which results in additional fixed
|
|
322 |
variables and assumptions in the context. Final results need to be
|
|
323 |
exported explicitly.
|
20472
|
324 |
|
|
325 |
\end{description}
|
|
326 |
*}
|
18537
|
327 |
|
|
328 |
end
|