summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Doc/Implementation/Proof.thy

author | wenzelm |

Wed Mar 25 11:39:52 2015 +0100 (2015-03-25) | |

changeset 59809 | 87641097d0f3 |

parent 59567 | 3ff1dd7ac7f0 |

child 59902 | 6afbe5a99139 |

permissions | -rw-r--r-- |

tuned signature;

1 theory Proof

2 imports Base

3 begin

5 chapter \<open>Structured proofs\<close>

7 section \<open>Variables \label{sec:variables}\<close>

9 text \<open>

10 Any variable that is not explicitly bound by @{text "\<lambda>"}-abstraction

11 is considered as ``free''. Logically, free variables act like

12 outermost universal quantification at the sequent level: @{text

13 "A\<^sub>1(x), \<dots>, A\<^sub>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

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

19 quantifier, @{text "x"} is essentially ``arbitrary, but fixed'',

20 while from outside it appears as a place-holder for instantiation

21 (thanks to @{text "\<And>"} elimination).

23 The Pure logic represents the idea of variables being either inside

24 or outside the current scope by providing separate syntactic

25 categories for \emph{fixed variables} (e.g.\ @{text "x"}) vs.\

26 \emph{schematic variables} (e.g.\ @{text "?x"}). Incidently, a

27 universal result @{text "\<turnstile> \<And>x. B(x)"} has the HHF normal form @{text

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.

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\<^sub>\<alpha>)"}.

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

43 @{text "x\<^sub>\<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\<^sub>\<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\<^sub>\<alpha>"} in the subsequent proposition.

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:

55 term, \<alpha>: type \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>"} produces in the first step @{text "x: term

56 \<turnstile> x\<^sub>\<alpha> \<equiv> x\<^sub>\<alpha>"} for fixed @{text "\<alpha>"}, and only in the second step

57 @{text "\<turnstile> ?x\<^sub>?\<^sub>\<alpha> \<equiv> ?x\<^sub>?\<^sub>\<alpha>"} for schematic @{text "?x"} and @{text "?\<alpha>"}.

58 The following Isar source text illustrates this scenario.

59 \<close>

61 notepad

62 begin

63 {

64 fix x -- \<open>all potential occurrences of some @{text "x::\<tau>"} are fixed\<close>

65 {

66 have "x::'a \<equiv> x" -- \<open>implicit type assignment by concrete occurrence\<close>

67 by (rule reflexive)

68 }

69 thm this -- \<open>result still with fixed type @{text "'a"}\<close>

70 }

71 thm this -- \<open>fully general result for arbitrary @{text "?x::?'a"}\<close>

72 end

74 text \<open>The Isabelle/Isar proof context manages the details of term

75 vs.\ type variables, with high-level principles for moving the

76 frontier between fixed and schematic variables.

78 The @{text "add_fixes"} operation explicitly declares fixed

79 variables; the @{text "declare_term"} operation absorbs a term into

80 a context by fixing new type variables and adding syntactic

81 constraints.

83 The @{text "export"} operation is able to perform the main work of

84 generalizing term and type variables as sketched above, assuming

85 that fixing variables and terms have been declared properly.

87 There @{text "import"} operation makes a generalized fact a genuine

88 part of the context, by inventing fixed variables for the schematic

89 ones. The effect can be reversed by using @{text "export"} later,

90 potentially with an extended context; the result is equivalent to

91 the original modulo renaming of schematic variables.

93 The @{text "focus"} operation provides a variant of @{text "import"}

94 for nested propositions (with explicit quantification): @{text

95 "\<And>x\<^sub>1 \<dots> x\<^sub>n. B(x\<^sub>1, \<dots>, x\<^sub>n)"} is

96 decomposed by inventing fixed variables @{text "x\<^sub>1, \<dots>,

97 x\<^sub>n"} for the body.

98 \<close>

100 text %mlref \<open>

101 \begin{mldecls}

102 @{index_ML Variable.add_fixes: "

103 string list -> Proof.context -> string list * Proof.context"} \\

104 @{index_ML Variable.variant_fixes: "

105 string list -> Proof.context -> string list * Proof.context"} \\

106 @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\

107 @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\

108 @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\

109 @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\

110 @{index_ML Variable.import: "bool -> thm list -> Proof.context ->

111 (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\

112 @{index_ML Variable.focus: "term -> Proof.context ->

113 ((string * (string * typ)) list * term) * Proof.context"} \\

114 \end{mldecls}

116 \begin{description}

118 \item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term

119 variables @{text "xs"}, returning the resulting internal names. By

120 default, the internal representation coincides with the external

121 one, which also means that the given variables must not be fixed

122 already. There is a different policy within a local proof body: the

123 given names are just hints for newly invented Skolem variables.

125 \item @{ML Variable.variant_fixes} is similar to @{ML

126 Variable.add_fixes}, but always produces fresh variants of the given

127 names.

129 \item @{ML Variable.declare_term}~@{text "t ctxt"} declares term

130 @{text "t"} to belong to the context. This automatically fixes new

131 type variables, but not term variables. Syntactic constraints for

132 type and term variables are declared uniformly, though.

134 \item @{ML Variable.declare_constraints}~@{text "t ctxt"} declares

135 syntactic constraints from term @{text "t"}, without making it part

136 of the context yet.

138 \item @{ML Variable.export}~@{text "inner outer thms"} generalizes

139 fixed type and term variables in @{text "thms"} according to the

140 difference of the @{text "inner"} and @{text "outer"} context,

141 following the principles sketched above.

143 \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type

144 variables in @{text "ts"} as far as possible, even those occurring

145 in fixed term variables. The default policy of type-inference is to

146 fix newly introduced type variables, which is essentially reversed

147 with @{ML Variable.polymorphic}: here the given terms are detached

148 from the context as far as possible.

150 \item @{ML Variable.import}~@{text "open thms ctxt"} invents fixed

151 type and term variables for the schematic ones occurring in @{text

152 "thms"}. The @{text "open"} flag indicates whether the fixed names

153 should be accessible to the user, otherwise newly introduced names

154 are marked as ``internal'' (\secref{sec:names}).

156 \item @{ML Variable.focus}~@{text B} decomposes the outermost @{text

157 "\<And>"} prefix of proposition @{text "B"}.

159 \end{description}

160 \<close>

162 text %mlex \<open>The following example shows how to work with fixed term

163 and type parameters and with type-inference.\<close>

165 ML \<open>

166 (*static compile-time context -- for testing only*)

167 val ctxt0 = @{context};

169 (*locally fixed parameters -- no type assignment yet*)

170 val ([x, y], ctxt1) = ctxt0 |> Variable.add_fixes ["x", "y"];

172 (*t1: most general fixed type; t1': most general arbitrary type*)

173 val t1 = Syntax.read_term ctxt1 "x";

174 val t1' = singleton (Variable.polymorphic ctxt1) t1;

176 (*term u enforces specific type assignment*)

177 val u = Syntax.read_term ctxt1 "(x::nat) \<equiv> y";

179 (*official declaration of u -- propagates constraints etc.*)

180 val ctxt2 = ctxt1 |> Variable.declare_term u;

181 val t2 = Syntax.read_term ctxt2 "x"; (*x::nat is enforced*)

182 \<close>

184 text \<open>In the above example, the starting context is derived from the

185 toplevel theory, which means that fixed variables are internalized

186 literally: @{text "x"} is mapped again to @{text "x"}, and

187 attempting to fix it again in the subsequent context is an error.

188 Alternatively, fixed parameters can be renamed explicitly as

189 follows:\<close>

191 ML \<open>

192 val ctxt0 = @{context};

193 val ([x1, x2, x3], ctxt1) =

194 ctxt0 |> Variable.variant_fixes ["x", "x", "x"];

195 \<close>

197 text \<open>The following ML code can now work with the invented names of

198 @{text x1}, @{text x2}, @{text x3}, without depending on

199 the details on the system policy for introducing these variants.

200 Recall that within a proof body the system always invents fresh

201 ``Skolem constants'', e.g.\ as follows:\<close>

203 notepad

204 begin

205 ML_prf %"ML"

206 \<open>val ctxt0 = @{context};

208 val ([x1], ctxt1) = ctxt0 |> Variable.add_fixes ["x"];

209 val ([x2], ctxt2) = ctxt1 |> Variable.add_fixes ["x"];

210 val ([x3], ctxt3) = ctxt2 |> Variable.add_fixes ["x"];

212 val ([y1, y2], ctxt4) =

213 ctxt3 |> Variable.variant_fixes ["y", "y"];\<close>

214 end

216 text \<open>In this situation @{ML Variable.add_fixes} and @{ML

217 Variable.variant_fixes} are very similar, but identical name

218 proposals given in a row are only accepted by the second version.

219 \<close>

222 section \<open>Assumptions \label{sec:assumptions}\<close>

224 text \<open>

225 An \emph{assumption} is a proposition that it is postulated in the

226 current context. Local conclusions may use assumptions as

227 additional facts, but this imposes implicit hypotheses that weaken

228 the overall statement.

230 Assumptions are restricted to fixed non-schematic statements, i.e.\

231 all generality needs to be expressed by explicit quantifiers.

232 Nevertheless, the result will be in HHF normal form with outermost

233 quantifiers stripped. For example, by assuming @{text "\<And>x :: \<alpha>. P

234 x"} we get @{text "\<And>x :: \<alpha>. P x \<turnstile> P ?x"} for schematic @{text "?x"}

235 of fixed type @{text "\<alpha>"}. Local derivations accumulate more and

236 more explicit references to hypotheses: @{text "A\<^sub>1, \<dots>,

237 A\<^sub>n \<turnstile> B"} where @{text "A\<^sub>1, \<dots>, A\<^sub>n"} needs to

238 be covered by the assumptions of the current context.

240 \medskip The @{text "add_assms"} operation augments the context by

241 local assumptions, which are parameterized by an arbitrary @{text

242 "export"} rule (see below).

244 The @{text "export"} operation moves facts from a (larger) inner

245 context into a (smaller) outer context, by discharging the

246 difference of the assumptions as specified by the associated export

247 rules. Note that the discharged portion is determined by the

248 difference of contexts, not the facts being exported! There is a

249 separate flag to indicate a goal context, where the result is meant

250 to refine an enclosing sub-goal of a structured proof state.

252 \medskip The most basic export rule discharges assumptions directly

253 by means of the @{text "\<Longrightarrow>"} introduction rule:

254 \[

255 \infer[(@{text "\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}

256 \]

258 The variant for goal refinements marks the newly introduced

259 premises, which causes the canonical Isar goal refinement scheme to

260 enforce unification with local premises within the goal:

261 \[

262 \infer[(@{text "#\<Longrightarrow>\<hyphen>intro"})]{@{text "\<Gamma> - A \<turnstile> #A \<Longrightarrow> B"}}{@{text "\<Gamma> \<turnstile> B"}}

263 \]

265 \medskip Alternative versions of assumptions may perform arbitrary

266 transformations on export, as long as the corresponding portion of

267 hypotheses is removed from the given facts. For example, a local

268 definition works by fixing @{text "x"} and assuming @{text "x \<equiv> t"},

269 with the following export rule to reverse the effect:

270 \[

271 \infer[(@{text "\<equiv>\<hyphen>expand"})]{@{text "\<Gamma> - (x \<equiv> t) \<turnstile> B t"}}{@{text "\<Gamma> \<turnstile> B x"}}

272 \]

273 This works, because the assumption @{text "x \<equiv> t"} was introduced in

274 a context with @{text "x"} being fresh, so @{text "x"} does not

275 occur in @{text "\<Gamma>"} here.

276 \<close>

278 text %mlref \<open>

279 \begin{mldecls}

280 @{index_ML_type Assumption.export} \\

281 @{index_ML Assumption.assume: "Proof.context -> cterm -> thm"} \\

282 @{index_ML Assumption.add_assms:

283 "Assumption.export ->

284 cterm list -> Proof.context -> thm list * Proof.context"} \\

285 @{index_ML Assumption.add_assumes: "

286 cterm list -> Proof.context -> thm list * Proof.context"} \\

287 @{index_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\

288 \end{mldecls}

290 \begin{description}

292 \item Type @{ML_type Assumption.export} represents arbitrary export

293 rules, which is any function of type @{ML_type "bool -> cterm list

294 -> thm -> thm"}, where the @{ML_type "bool"} indicates goal mode,

295 and the @{ML_type "cterm list"} the collection of assumptions to be

296 discharged simultaneously.

298 \item @{ML Assumption.assume}~@{text "ctxt A"} turns proposition @{text

299 "A"} into a primitive assumption @{text "A \<turnstile> A'"}, where the

300 conclusion @{text "A'"} is in HHF normal form.

302 \item @{ML Assumption.add_assms}~@{text "r As"} augments the context

303 by assumptions @{text "As"} with export rule @{text "r"}. The

304 resulting facts are hypothetical theorems as produced by the raw

305 @{ML Assumption.assume}.

307 \item @{ML Assumption.add_assumes}~@{text "As"} is a special case of

308 @{ML Assumption.add_assms} where the export rule performs @{text

309 "\<Longrightarrow>\<hyphen>intro"} or @{text "#\<Longrightarrow>\<hyphen>intro"}, depending on goal

310 mode.

312 \item @{ML Assumption.export}~@{text "is_goal inner outer thm"}

313 exports result @{text "thm"} from the the @{text "inner"} context

314 back into the @{text "outer"} one; @{text "is_goal = true"} means

315 this is a goal context. The result is in HHF normal form. Note

316 that @{ML "Proof_Context.export"} combines @{ML "Variable.export"}

317 and @{ML "Assumption.export"} in the canonical way.

319 \end{description}

320 \<close>

322 text %mlex \<open>The following example demonstrates how rules can be

323 derived by building up a context of assumptions first, and exporting

324 some local fact afterwards. We refer to @{theory Pure} equality

325 here for testing purposes.

326 \<close>

328 ML \<open>

329 (*static compile-time context -- for testing only*)

330 val ctxt0 = @{context};

332 val ([eq], ctxt1) =

333 ctxt0 |> Assumption.add_assumes [@{cprop "x \<equiv> y"}];

334 val eq' = Thm.symmetric eq;

336 (*back to original context -- discharges assumption*)

337 val r = Assumption.export false ctxt1 ctxt0 eq';

338 \<close>

340 text \<open>Note that the variables of the resulting rule are not

341 generalized. This would have required to fix them properly in the

342 context beforehand, and export wrt.\ variables afterwards (cf.\ @{ML

343 Variable.export} or the combined @{ML "Proof_Context.export"}).\<close>

346 section \<open>Structured goals and results \label{sec:struct-goals}\<close>

348 text \<open>

349 Local results are established by monotonic reasoning from facts

350 within a context. This allows common combinations of theorems,

351 e.g.\ via @{text "\<And>/\<Longrightarrow>"} elimination, resolution rules, or equational

352 reasoning, see \secref{sec:thms}. Unaccounted context manipulations

353 should be avoided, notably raw @{text "\<And>/\<Longrightarrow>"} introduction or ad-hoc

354 references to free variables or assumptions not present in the proof

355 context.

357 \medskip The @{text "SUBPROOF"} combinator allows to structure a

358 tactical proof recursively by decomposing a selected sub-goal:

359 @{text "(\<And>x. A(x) \<Longrightarrow> B(x)) \<Longrightarrow> \<dots>"} is turned into @{text "B(x) \<Longrightarrow> \<dots>"}

360 after fixing @{text "x"} and assuming @{text "A(x)"}. This means

361 the tactic needs to solve the conclusion, but may use the premise as

362 a local fact, for locally fixed variables.

364 The family of @{text "FOCUS"} combinators is similar to @{text

365 "SUBPROOF"}, but allows to retain schematic variables and pending

366 subgoals in the resulting goal state.

368 The @{text "prove"} operation provides an interface for structured

369 backwards reasoning under program control, with some explicit sanity

370 checks of the result. The goal context can be augmented by

371 additional fixed variables (cf.\ \secref{sec:variables}) and

372 assumptions (cf.\ \secref{sec:assumptions}), which will be available

373 as local facts during the proof and discharged into implications in

374 the result. Type and term variables are generalized as usual,

375 according to the context.

377 The @{text "obtain"} operation produces results by eliminating

378 existing facts by means of a given tactic. This acts like a dual

379 conclusion: the proof demonstrates that the context may be augmented

380 by parameters and assumptions, without affecting any conclusions

381 that do not mention these parameters. See also

382 @{cite "isabelle-isar-ref"} for the user-level @{command obtain} and

383 @{command guess} elements. Final results, which may not refer to

384 the parameters in the conclusion, need to exported explicitly into

385 the original context.\<close>

387 text %mlref \<open>

388 \begin{mldecls}

389 @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) ->

390 Proof.context -> int -> tactic"} \\

391 @{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) ->

392 Proof.context -> int -> tactic"} \\

393 @{index_ML Subgoal.FOCUS_PREMS: "(Subgoal.focus -> tactic) ->

394 Proof.context -> int -> tactic"} \\

395 @{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) ->

396 Proof.context -> int -> tactic"} \\

397 @{index_ML Subgoal.focus: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\

398 @{index_ML Subgoal.focus_prems: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\

399 @{index_ML Subgoal.focus_params: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\

400 \end{mldecls}

402 \begin{mldecls}

403 @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->

404 ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\

405 @{index_ML Goal.prove_common: "Proof.context -> int option ->

406 string list -> term list -> term list ->

407 ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\

408 \end{mldecls}

409 \begin{mldecls}

410 @{index_ML Obtain.result: "(Proof.context -> tactic) -> thm list ->

411 Proof.context -> ((string * cterm) list * thm list) * Proof.context"} \\

412 \end{mldecls}

414 \begin{description}

416 \item @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure

417 of the specified sub-goal, producing an extended context and a

418 reduced goal, which needs to be solved by the given tactic. All

419 schematic parameters of the goal are imported into the context as

420 fixed ones, which may not be instantiated in the sub-proof.

422 \item @{ML Subgoal.FOCUS}, @{ML Subgoal.FOCUS_PREMS}, and @{ML

423 Subgoal.FOCUS_PARAMS} are similar to @{ML SUBPROOF}, but are

424 slightly more flexible: only the specified parts of the subgoal are

425 imported into the context, and the body tactic may introduce new

426 subgoals and schematic variables.

428 \item @{ML Subgoal.focus}, @{ML Subgoal.focus_prems}, @{ML

429 Subgoal.focus_params} extract the focus information from a goal

430 state in the same way as the corresponding tacticals above. This is

431 occasionally useful to experiment without writing actual tactics

432 yet.

434 \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text

435 "C"} in the context augmented by fixed variables @{text "xs"} and

436 assumptions @{text "As"}, and applies tactic @{text "tac"} to solve

437 it. The latter may depend on the local assumptions being presented

438 as facts. The result is in HHF normal form.

440 \item @{ML Goal.prove_common}~@{text "ctxt fork_pri"} is the common form

441 to state and prove a simultaneous goal statement, where @{ML Goal.prove}

442 is a convenient shorthand that is most frequently used in applications.

444 The given list of simultaneous conclusions is encoded in the goal state by

445 means of Pure conjunction: @{ML Goal.conjunction_tac} will turn this into

446 a collection of individual subgoals, but note that the original multi-goal

447 state is usually required for advanced induction.

449 It is possible to provide an optional priority for a forked proof,

450 typically @{ML "SOME ~1"}, while @{ML NONE} means the proof is immediate

451 (sequential) as for @{ML Goal.prove}. Note that a forked proof does not

452 exhibit any failures in the usual way via exceptions in ML, but

453 accumulates error situations under the execution id of the running

454 transaction. Thus the system is able to expose error messages ultimately

455 to the end-user, even though the subsequent ML code misses them.

457 \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the

458 given facts using a tactic, which results in additional fixed

459 variables and assumptions in the context. Final results need to be

460 exported explicitly.

462 \end{description}

463 \<close>

465 text %mlex \<open>The following minimal example illustrates how to access

466 the focus information of a structured goal state.\<close>

468 notepad

469 begin

470 fix A B C :: "'a \<Rightarrow> bool"

472 have "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"

473 ML_val

474 \<open>val {goal, context = goal_ctxt, ...} = @{Isar.goal};

475 val (focus as {params, asms, concl, ...}, goal') =

476 Subgoal.focus goal_ctxt 1 goal;

477 val [A, B] = #prems focus;

478 val [(_, x)] = #params focus;\<close>

479 sorry

480 end

482 text \<open>\medskip The next example demonstrates forward-elimination in

483 a local context, using @{ML Obtain.result}.\<close>

485 notepad

486 begin

487 assume ex: "\<exists>x. B x"

489 ML_prf %"ML"

490 \<open>val ctxt0 = @{context};

491 val (([(_, x)], [B]), ctxt1) = ctxt0

492 |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}];\<close>

493 ML_prf %"ML"

494 \<open>singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl};\<close>

495 ML_prf %"ML"

496 \<open>Proof_Context.export ctxt1 ctxt0 [Thm.reflexive x]

497 handle ERROR msg => (warning msg; []);\<close>

498 end

500 end