author  wenzelm 
Wed, 13 Dec 2006 16:26:45 +0100  
changeset 21827  0b1d07f79c1e 
parent 20797  c1f0bc7e7d80 
child 22568  ed7aa5a350ef 
permissions  rwrr 
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 placeholder 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 typeinference. 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 typetheoretic 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 highlevel 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"} \\ 

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 

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 typeinference 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 nonschematic 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 subgoal of a structured proof state (cf.\ 

178 
\secref{sec:isarproofstate}). 

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 adhoc 

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 subgoal: 

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{isabelleisarref} for the userlevel @{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 subgoal, 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 subproof. 

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 