author | wenzelm |
Tue, 03 Apr 2007 19:24:13 +0200 | |
changeset 22568 | ed7aa5a350ef |
parent 21827 | 0b1d07f79c1e |
child 28541 | 9b259710d9d3 |
permissions | -rw-r--r-- |
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"} \\ |
|
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20547
diff
changeset
|
91 |
@{index_ML Variable.variant_fixes: " |
20474 | 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"} \\ |
|
22568
ed7aa5a350ef
renamed Variable.import to import_thms (avoid clash with Alice keywords);
wenzelm
parents:
21827
diff
changeset
|
97 |
@{index_ML Variable.import_thms: "bool -> thm list -> Proof.context -> |
20474 | 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 |
|
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 |
|
22568
ed7aa5a350ef
renamed Variable.import to import_thms (avoid clash with Alice keywords);
wenzelm
parents:
21827
diff
changeset
|
136 |
\item @{ML Variable.import_thms}~@{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 |
||
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 |
||
20520 | 250 |
section {* Results *} |
20451 | 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"} \\ |
|
20547 | 293 |
\end{mldecls} |
294 |
\begin{mldecls} |
|
20472 | 295 |
@{index_ML Goal.prove: "Proof.context -> string list -> term list -> term -> |
296 |
({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\ |
|
297 |
@{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list -> |
|
298 |
({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\ |
|
20547 | 299 |
\end{mldecls} |
300 |
\begin{mldecls} |
|
20491 | 301 |
@{index_ML Obtain.result: "(Proof.context -> tactic) -> |
20542 | 302 |
thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\ |
20472 | 303 |
\end{mldecls} |
18537 | 304 |
|
20472 | 305 |
\begin{description} |
18537 | 306 |
|
20491 | 307 |
\item @{ML SUBPROOF}~@{text "tac"} decomposes the structure of a |
308 |
particular sub-goal, producing an extended context and a reduced |
|
309 |
goal, which needs to be solved by the given tactic. All schematic |
|
310 |
parameters of the goal are imported into the context as fixed ones, |
|
311 |
which may not be instantiated in the sub-proof. |
|
312 |
||
20472 | 313 |
\item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text |
20474 | 314 |
"C"} in the context augmented by fixed variables @{text "xs"} and |
315 |
assumptions @{text "As"}, and applies tactic @{text "tac"} to solve |
|
316 |
it. The latter may depend on the local assumptions being presented |
|
317 |
as facts. The result is in HHF normal form. |
|
18537 | 318 |
|
20472 | 319 |
\item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but |
20491 | 320 |
states several conclusions simultaneously. The goal is encoded by |
21827 | 321 |
means of Pure conjunction; @{ML Goal.conjunction_tac} will turn this |
322 |
into a collection of individual subgoals. |
|
20472 | 323 |
|
20491 | 324 |
\item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the |
325 |
given facts using a tactic, which results in additional fixed |
|
326 |
variables and assumptions in the context. Final results need to be |
|
327 |
exported explicitly. |
|
20472 | 328 |
|
329 |
\end{description} |
|
330 |
*} |
|
18537 | 331 |
|
332 |
end |