author  wenzelm 
Mon, 24 May 1999 21:55:34 +0200  
changeset 6721  dcee829f8e21 
parent 6560  1436349f8b28 
child 6762  a9a515a43ae0 
permissions  rwrr 
5819  1 
(* Title: Pure/Isar/proof_context.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Proof context information. 

6 

7 
TODO: 

8 
 pretty_bind: use syntax (!?) (show_types etc.); 

9 
 smash_unifiers: ever invents new vars (???); 

10 
*) 

11 

12 
signature PROOF_CONTEXT = 

13 
sig 

14 
type context 

15 
exception CONTEXT of string * context 

16 
val theory_of: context > theory 

17 
val sign_of: context > Sign.sg 

6528  18 
val verbose: bool ref 
5819  19 
val print_binds: context > unit 
20 
val print_thms: context > unit 

21 
val print_context: context > unit 

22 
val print_proof_data: theory > unit 

5874  23 
val init: theory > context 
5819  24 
val read_typ: context > string > typ 
25 
val cert_typ: context > typ > typ 

5874  26 
val read_termTs: context > (string * typ) list > term list * (indexname * typ) list 
5819  27 
val read_term: context > string > term 
28 
val read_prop: context > string > term 

5935  29 
val read_term_pat: context > string > term 
30 
val read_prop_pat: context > string > term 

5819  31 
val cert_term: context > term > term 
32 
val cert_prop: context > term > term 

33 
val declare_term: term > context > context 

34 
val declare_terms: term list > context > context 

5874  35 
val declare_thm: thm > context > context 
5819  36 
val add_binds: (indexname * string) list > context > context 
37 
val add_binds_i: (indexname * term) list > context > context 

5935  38 
val match_binds: (string list * string) list > context > context 
39 
val match_binds_i: (term list * term) list > context > context 

40 
val bind_propp: context * (string * string list) > context * term 

41 
val bind_propp_i: context * (term * term list) > context * term 

6091  42 
val thms_closure: context > xstring > thm list option 
43 
val get_thm: context > string > thm 

44 
val get_thms: context > string > thm list 

45 
val get_thmss: context > string list > thm list 

46 
val put_thm: string * thm > context > context 

47 
val put_thms: string * thm list > context > context 

48 
val put_thmss: (string * thm list) list > context > context 

49 
val have_thmss: string > context attribute list 

50 
> (thm list * context attribute list) list > context > context * (string * thm list) 

51 
val assumptions: context > thm list 

5819  52 
val fixed_names: context > string list 
5935  53 
val assume: string > context attribute list > (string * string list) list > context 
6091  54 
> context * (string * thm list) 
5935  55 
val assume_i: string > context attribute list > (term * term list) list > context 
6091  56 
> context * (string * thm list) 
5819  57 
val fix: (string * string option) list > context > context 
58 
val fix_i: (string * typ) list > context > context 

59 
val setup: (theory > theory) list 

60 
end; 

61 

62 
signature PROOF_CONTEXT_PRIVATE = 

63 
sig 

64 
include PROOF_CONTEXT 

65 
val init_data: Object.kind > (theory > Object.T) * (context > Object.T > unit) 

66 
> theory > theory 

67 
val print_data: Object.kind > context > unit 

68 
val get_data: Object.kind > (Object.T > 'a) > context > 'a 

69 
val put_data: Object.kind > ('a > Object.T) > 'a > context > context 

70 
end; 

71 

72 
structure ProofContext: PROOF_CONTEXT_PRIVATE = 

73 
struct 

74 

75 

76 
(** datatype context **) 

77 

78 
datatype context = 

79 
Context of 

80 
{thy: theory, (*current theory*) 

81 
data: Object.T Symtab.table, (*user data*) 

82 
asms: 

6091  83 
(string * thm list) list * (*assumes: A ==> _*) 
5819  84 
((string * string) list * string list), (*fixes: !!x. _*) 
85 
binds: (term * typ) Vartab.table, (*term bindings*) 

6091  86 
thms: thm list Symtab.table, (*local thms*) 
5819  87 
defs: 
88 
typ Vartab.table * (*type constraints*) 

89 
sort Vartab.table * (*default sorts*) 

90 
int * (*maxidx*) 

91 
string list}; (*used type variable names*) 

92 

93 
exception CONTEXT of string * context; 

94 

95 

96 
fun make_context (thy, data, asms, binds, thms, defs) = 

97 
Context {thy = thy, data = data, asms = asms, binds = binds, thms = thms, defs = defs}; 

98 

99 
fun map_context f (Context {thy, data, asms, binds, thms, defs}) = 

100 
make_context (f (thy, data, asms, binds, thms, defs)); 

101 

102 
fun theory_of (Context {thy, ...}) = thy; 

103 
val sign_of = Theory.sign_of o theory_of; 

104 

105 

106 

107 
(** print context information **) 

108 

6528  109 
val verbose = ref false; 
110 
fun verb f x = if ! verbose then f x else (); 

5819  111 

112 
fun print_items prt name items = 

113 
let 

114 
fun pretty_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x] 

115 
 pretty_itms (name, xs) = Pretty.big_list (name ^ ":") (map prt xs); 

6721  116 
in 
117 
if null items andalso not (! verbose) then () 

118 
else Pretty.writeln (Pretty.big_list name (map pretty_itms items)) 

119 
end; 

5819  120 

121 

122 
(* term bindings *) 

123 

124 
fun print_binds (Context {thy, binds, ...}) = 

125 
let 

126 
val prt_term = Sign.pretty_term (Theory.sign_of thy); 

127 

128 
fun fix_var (x, i) = 

129 
(case try Syntax.dest_binding x of 

130 
None => Syntax.string_of_vname (x, i) 

131 
 Some x' => if i = 0 then "??" ^ x' else Syntax.string_of_vname (x, i)); 

132 
fun pretty_bind (xi, (t, T)) = Pretty.block 

133 
[Pretty.str (fix_var xi), Pretty.str " ==", Pretty.brk 1, prt_term t]; 

6721  134 
in 
135 
if Vartab.is_empty binds andalso not (! verbose) then () 

136 
else Pretty.writeln (Pretty.big_list "Term bindings:" (map pretty_bind (Vartab.dest binds))) 

137 
end; 

5819  138 

139 

140 
(* local theorems *) 

141 

142 
fun print_thms (Context {thms, ...}) = 

6091  143 
print_items Display.pretty_thm "Local theorems:" (Symtab.dest thms); 
5819  144 

145 

146 
(* main context *) 

147 

148 
fun print_context (ctxt as Context {thy, data = _, asms = (assumes, (fixes, _)), binds = _, 

149 
thms = _, defs = (types, sorts, maxidx, used)}) = 

150 
let 

151 
val sign = Theory.sign_of thy; 

152 

153 
val prt_term = Sign.pretty_term sign; 

154 
val prt_typ = Sign.pretty_typ sign; 

155 
val prt_sort = Sign.pretty_sort sign; 

156 

157 
(*theory*) 

158 
val pretty_thy = Pretty.block [Pretty.str "Theory:", Pretty.brk 1, Sign.pretty_sg sign]; 

159 

160 
(*fixes*) 

161 
fun prt_fix (x, x') = Pretty.str (x ^ " = " ^ x'); 

162 

163 
(* defaults *) 

164 

165 
fun prt_atom prt prtT (x, X) = Pretty.block 

166 
[prt x, Pretty.str " ::", Pretty.brk 1, prtT X]; 

167 

168 
fun prt_var (x, ~1) = prt_term (Syntax.free x) 

169 
 prt_var xi = prt_term (Syntax.var xi); 

170 

171 
fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) 

172 
 prt_varT xi = prt_typ (TVar (xi, [])); 

173 

174 
val prt_defT = prt_atom prt_var prt_typ; 

175 
val prt_defS = prt_atom prt_varT prt_sort; 

176 
in 

6528  177 
verb Pretty.writeln pretty_thy; 
6721  178 
if null fixes andalso not (! verbose) then () 
179 
else Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes))); 

6091  180 
print_items (prt_term o #prop o Thm.rep_thm) "Assumptions:" assumes; 
6528  181 
verb print_binds ctxt; 
182 
verb print_thms ctxt; 

183 
verb Pretty.writeln (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types))); 

184 
verb Pretty.writeln (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts))); 

185 
verb writeln ("Maxidx: " ^ string_of_int maxidx); 

186 
verb Pretty.writeln (Pretty.strs ("Used type variable names:" :: used)) 

5819  187 
end; 
188 

189 

190 

191 
(** user data **) 

192 

193 
(* errors *) 

194 

195 
fun of_theory thy = "\nof theory " ^ Sign.str_of_sg (Theory.sign_of thy); 

196 

197 
fun err_inconsistent kinds = 

198 
error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " proof data"); 

199 

200 
fun err_dup_init thy kind = 

201 
error ("Duplicate initialization of " ^ quote kind ^ " proof data" ^ of_theory thy); 

202 

203 
fun err_undef ctxt kind = 

204 
raise CONTEXT ("Tried to access undefined " ^ quote kind ^ " proof data", ctxt); 

205 

206 
fun err_uninit ctxt kind = 

207 
raise CONTEXT ("Tried to access uninitialized " ^ quote kind ^ " proof data" ^ 

208 
of_theory (theory_of ctxt), ctxt); 

209 

210 
fun err_access ctxt kind = 

211 
raise CONTEXT ("Unauthorized access to " ^ quote kind ^ " proof data" ^ 

212 
of_theory (theory_of ctxt), ctxt); 

213 

214 

215 
(* data kind 'Isar/proof_data' *) 

216 

217 
structure ProofDataDataArgs = 

218 
struct 

219 
val name = "Isar/proof_data"; 

220 
type T = (Object.kind * ((theory > Object.T) * (context > Object.T > unit))) Symtab.table; 

221 

222 
val empty = Symtab.empty; 

6550  223 
val copy = I; 
5819  224 
val prep_ext = I; 
225 
fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs 

226 
handle Symtab.DUPS kinds => err_inconsistent kinds; 

227 
fun print _ tab = Pretty.writeln (Pretty.strs (map #1 (Symtab.dest tab))); 

228 
end; 

229 

230 
structure ProofDataData = TheoryDataFun(ProofDataDataArgs); 

231 
val print_proof_data = ProofDataData.print; 

232 

233 

234 
(* init proof data *) 

235 

236 
fun init_data kind meths thy = 

237 
let 

238 
val name = Object.name_of_kind kind; 

239 
val tab = Symtab.update_new ((name, (kind, meths)), ProofDataData.get thy) 

240 
handle Symtab.DUP _ => err_dup_init thy name; 

241 
in thy > ProofDataData.put tab end; 

242 

243 

244 
(* access data *) 

245 

246 
fun lookup_data (ctxt as Context {data, ...}) kind = 

247 
let 

248 
val thy = theory_of ctxt; 

249 
val name = Object.name_of_kind kind; 

250 
in 

251 
(case Symtab.lookup (ProofDataData.get thy, name) of 

252 
Some (k, meths) => 

253 
if Object.eq_kind (kind, k) then 

254 
(case Symtab.lookup (data, name) of 

255 
Some x => (x, meths) 

256 
 None => err_undef ctxt name) 

257 
else err_access ctxt name 

258 
 None => err_uninit ctxt name) 

259 
end; 

260 

261 
fun get_data kind f ctxt = 

262 
let val (x, _) = lookup_data ctxt kind 

263 
in f x handle Match => Object.kind_error kind end; 

264 

265 
fun print_data kind ctxt = 

266 
let val (x, (_, prt)) = lookup_data ctxt kind 

267 
in prt ctxt x end; 

268 

269 
fun put_data kind f x ctxt = 

270 
(lookup_data ctxt kind; 

271 
ctxt > map_context (fn (thy, data, asms, binds, thms, defs) => 

272 
(thy, Symtab.update ((Object.name_of_kind kind, f x), data), asms, binds, thms, defs))); 

273 

274 

275 
(* init context *) 

276 

5874  277 
fun init thy = 
278 
let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in 

5819  279 
make_context (thy, data, ([], ([], [])), Vartab.empty, Symtab.empty, 
280 
(Vartab.empty, Vartab.empty, ~1, [])) 

281 
end; 

282 

283 

284 

285 
(** prepare types **) 

286 

287 
fun read_typ (ctxt as Context {defs = (_, sorts, _, _), ...}) s = 

288 
let 

289 
val sign = sign_of ctxt; 

290 
fun def_sort xi = Vartab.lookup (sorts, xi); 

291 
in 

292 
transform_error (Sign.read_typ (sign, def_sort)) s 

293 
handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt) 

294 
end; 

295 

296 
fun cert_typ ctxt raw_T = 

297 
Sign.certify_typ (sign_of ctxt) raw_T 

298 
handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt); 

299 

300 

301 

302 
(** prepare terms and propositions **) 

303 

304 
(* 

305 
(1) read / certify wrt. signature of context 

306 
(2) intern Skolem constants 

307 
(3) expand term bindings 

308 
*) 

309 

310 

311 
(* read / certify wrt. signature *) (*exception ERROR*) (*exception TERM*) 

312 

5874  313 
fun read_def_termTs freeze sg (types, sorts, used) sTs = 
314 
let val (cts, env) = Thm.read_def_cterms (sg, types, sorts) used freeze sTs 

315 
in (map Thm.term_of cts, env) end; 

316 

317 
fun read_def_termT freeze sg defs sT = apfst hd (read_def_termTs freeze sg defs [sT]); 

318 

5819  319 

320 
fun read_term_sg sg (defs as (_, _, used)) s = 

5874  321 
#1 (read_def_termT true sg defs (s, TVar ((variant used "'z", 0), logicS))); 
5819  322 

5874  323 
fun read_prop_sg sg defs s = 
324 
#1 (read_def_termT true sg defs (s, propT)); 

5819  325 

326 

327 
fun cert_term_sg sg t = Thm.term_of (Thm.cterm_of sg t); 

328 

329 
fun cert_prop_sg sg tm = 

330 
let 

331 
val ctm = Thm.cterm_of sg tm; 

332 
val {t, T, ...} = Thm.rep_cterm ctm; 

333 
in 

334 
if T = propT then t 

335 
else raise TERM ("Term not of type prop", [t]) 

336 
end; 

337 

338 

339 
(* intern_skolem *) 

340 

341 
fun get_skolem (Context {asms = (_, (fixes, _)), ...}) x = assoc (fixes, x); 

342 

343 
fun check_skolem ctxt check x = 

344 
if check andalso can Syntax.dest_skolem x then 

345 
raise CONTEXT ("Illegal reference to internal Skolem constant: " ^ quote x, ctxt) 

346 
else x; 

347 

348 
fun intern_skolem ctxt check = 

349 
let 

350 
fun intern (t as Free (x, T)) = 

351 
(case get_skolem ctxt (check_skolem ctxt check x) of 

352 
Some x' => Free (x', T) 

353 
 None => t) 

354 
 intern (t $ u) = intern t $ intern u 

355 
 intern (Abs (x, T, t)) = Abs (x, T, intern t) 

356 
 intern a = a; 

357 
in intern end; 

358 

359 

360 
(* norm_term *) 

361 

362 
(*beta normal form for terms (not eta normal form), chase variables in 

363 
bindings environment (code taken from Pure/envir.ML)*) 

364 

365 
fun norm_term (ctxt as Context {binds, ...}) = 

366 
let 

367 
(*raised when norm has no effect on a term, to do sharing instead of copying*) 

368 
exception SAME; 

369 

370 
fun norm (t as Var (xi, T)) = 

371 
(case Vartab.lookup (binds, xi) of 

372 
Some (u, U) => 

373 
if T = U then (norm u handle SAME => u) 

374 
else raise TYPE ("norm_term: illtyped variable assigment", [T, U], [t, u]) 

375 
 None => 

376 
if can Syntax.dest_binding (#1 xi) then 

377 
raise CONTEXT ("Unbound binding: " ^ Syntax.string_of_vname xi, ctxt) 

378 
else raise SAME) 

379 
 norm (Abs (a, T, body)) = Abs (a, T, norm body) 

380 
 norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body)) 

381 
 norm (f $ t) = 

382 
((case norm f of 

383 
Abs (_, _, body) => normh (subst_bound (t, body)) 

384 
 nf => nf $ (norm t handle SAME => t)) handle SAME => f $ norm t) 

385 
 norm _ = raise SAME 

386 
and normh t = norm t handle SAME => t 

387 
in normh end; 

388 

389 

6550  390 
(* dummy patterns *) 
391 

6560
1436349f8b28
renamed 'dummy' to 'dummy_pattern' (less dangerous);
wenzelm
parents:
6550
diff
changeset

392 
fun is_dummy (Const (c, _)) = c = PureThy.dummy_patternN 
6550  393 
 is_dummy _ = false; 
394 

395 
fun reject_dummies ctxt tm = 

396 
if foldl_aterms (fn (ok, t) => ok andalso not (is_dummy t)) (true, tm) then tm 

397 
else raise CONTEXT ("Illegal dummy pattern(s) in term", ctxt); 

398 

399 

6560
1436349f8b28
renamed 'dummy' to 'dummy_pattern' (less dangerous);
wenzelm
parents:
6550
diff
changeset

400 
fun prep_dummy (i, t) = 
1436349f8b28
renamed 'dummy' to 'dummy_pattern' (less dangerous);
wenzelm
parents:
6550
diff
changeset

401 
if is_dummy t then (i + 1, Var (("_dummy_", i), Term.fastype_of t)) else (i, t); 
6550  402 

403 
fun prepare_dummies tm = #2 (Term.foldl_map_aterms prep_dummy (1, tm)); 

404 

405 

5819  406 
(* read terms *) 
407 

5874  408 
fun gen_read read app is_pat (ctxt as Context {binds, defs = (types, sorts, _, used), ...}) s = 
5819  409 
let 
410 
val sign = sign_of ctxt; 

411 

412 
fun def_type xi = 

413 
(case Vartab.lookup (types, xi) of 

414 
None => if is_pat then None else apsome #2 (Vartab.lookup (binds, xi)) 

415 
 some => some); 

416 

417 
fun def_sort xi = Vartab.lookup (sorts, xi); 

418 
in 

419 
(transform_error (read sign (def_type, def_sort, used)) s 

420 
handle TERM (msg, _) => raise CONTEXT (msg, ctxt) 

421 
 ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt)) 

5874  422 
> app (intern_skolem ctxt true) 
423 
> app (if is_pat then I else norm_term ctxt) 

6550  424 
> app (if is_pat then prepare_dummies else (reject_dummies ctxt)) 
5819  425 
end; 
426 

5874  427 
val read_termTs = gen_read (read_def_termTs false) (apfst o map) false; 
428 
val read_term = gen_read read_term_sg I false; 

429 
val read_prop = gen_read read_prop_sg I false; 

5935  430 
val read_term_pat = gen_read read_term_sg I true; 
431 
val read_prop_pat = gen_read read_prop_sg I true; 

5819  432 

433 

434 
(* certify terms *) 

435 

436 
fun gen_cert cert is_pat ctxt t = 

437 
(cert (sign_of ctxt) t handle TERM (msg, _) => raise CONTEXT (msg, ctxt)) 

438 
> intern_skolem ctxt false 

439 
> (if is_pat then I else norm_term ctxt); 

440 

441 
val cert_term = gen_cert cert_term_sg false; 

442 
val cert_prop = gen_cert cert_prop_sg false; 

5935  443 
val cert_term_pat = gen_cert cert_term_sg true; 
444 
val cert_prop_pat = gen_cert cert_prop_sg true; 

5819  445 

446 

447 
(* declare terms *) 

448 

449 
val ins_types = foldl_aterms 

450 
(fn (types, Free (x, T)) => Vartab.update (((x, ~1), T), types) 

451 
 (types, Var v) => Vartab.update (v, types) 

452 
 (types, _) => types); 

453 

454 
val ins_sorts = foldl_types (foldl_atyps 

455 
(fn (sorts, TFree (x, S)) => Vartab.update (((x, ~1), S), sorts) 

456 
 (sorts, TVar v) => Vartab.update (v, sorts) 

457 
 (sorts, _) => sorts)); 

458 

459 
val ins_used = foldl_types (foldl_atyps 

460 
(fn (used, TFree (x, _)) => x ins used 

461 
 (used, TVar ((x, _), _)) => x ins used 

462 
 (used, _) => used)); 

463 

5994  464 
fun ins_skolem def_type = foldr 
465 
(fn ((x, x'), types) => 

466 
(case def_type x' of 

467 
Some T => Vartab.update (((x, ~1), T), types) 

468 
 None => types)); 

469 

5819  470 
fun map_defaults f = map_context 
471 
(fn (thy, data, asms, binds, thms, defs) => (thy, data, asms, binds, thms, f defs)); 

472 

5994  473 
fun declare (ctxt as Context {asms = (_, (fixes, _)), ...}, t) = 
5819  474 
ctxt 
475 
> map_defaults (fn (types, sorts, maxidx, used) => (ins_types (types, t), sorts, maxidx, used)) 

476 
> map_defaults (fn (types, sorts, maxidx, used) => (types, ins_sorts (sorts, t), maxidx, used)) 

477 
> map_defaults (fn (types, sorts, maxidx, used) => (types, sorts, maxidx, ins_used (used, t))) 

478 
> map_defaults (fn (types, sorts, maxidx, used) => 

5994  479 
(types, sorts, Int.max (maxidx, Term.maxidx_of_term t), used)) 
480 
> map_defaults (fn (types, sorts, maxidx, used) => 

481 
(ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes, types), sorts, maxidx, used)); 

5819  482 

483 

484 
fun declare_term t ctxt = declare (ctxt, t); 

485 
fun declare_terms ts ctxt = foldl declare (ctxt, ts); 

486 

5874  487 
fun declare_thm thm ctxt = 
488 
let val {prop, hyps, ...} = Thm.rep_thm thm 

489 
in ctxt > declare_terms (prop :: hyps) end; 

490 

5819  491 

492 

493 
(** bindings **) 

494 

495 
(* update_binds *) 

496 

497 
fun upd_bind (ctxt, (xi, t)) = 

498 
let val T = fastype_of t in 

499 
ctxt 

500 
> declare_term t 

501 
> map_context (fn (thy, data, asms, binds, thms, defs) => 

502 
(thy, data, asms, Vartab.update ((xi, (t, T)), binds), thms, defs)) 

503 
end; 

504 

505 
fun update_binds bs ctxt = foldl upd_bind (ctxt, bs); 

506 
fun update_binds_env env = update_binds (Envir.alist_of env); 

507 

508 

509 
(* add_binds(_i)  sequential *) 

510 

511 
fun gen_bind prep (ctxt, (xi as (x, _), raw_t)) = 

512 
let val t = prep ctxt raw_t in 

513 
if can Syntax.dest_binding x then ctxt > update_binds [(xi, t)] 

514 
else raise CONTEXT ("Illegal variable name for term binding: " ^ 

515 
quote (Syntax.string_of_vname xi), ctxt) 

516 
end; 

517 

518 
fun gen_binds prep binds ctxt = foldl (gen_bind prep) (ctxt, binds); 

519 

520 
val add_binds = gen_binds read_term; 

521 
val add_binds_i = gen_binds cert_term; 

522 

523 

524 
(* match_binds(_i)  parallel *) 

525 

5935  526 
fun prep_declare_match (prep_pat, prep) (ctxt, (raw_pats, raw_t)) = 
5819  527 
let 
5935  528 
val t = prep ctxt raw_t; 
5994  529 
val ctxt' = ctxt > declare_term t; 
530 
val pats = map (prep_pat ctxt') raw_pats; (* FIXME seq / par / simult (??) *) 

531 
in (ctxt', (map (rpair t) pats, t)) end; 

5819  532 

5935  533 
fun gen_match_binds _ [] ctxt = ctxt 
534 
 gen_match_binds prepp raw_pairs ctxt = 

535 
let 

536 
val (ctxt', matches) = foldl_map (prep_declare_match prepp) (ctxt, raw_pairs); 

537 
val pairs = flat (map #1 matches); 

538 
val Context {defs = (_, _, maxidx, _), ...} = ctxt'; 

539 
val envs = Unify.smash_unifiers (sign_of ctxt', Envir.empty maxidx, pairs); 

540 
val env = 

541 
(case Seq.pull envs of 

542 
None => raise CONTEXT ("Pattern match failed!", ctxt') 

543 
 Some (env, _) => env); 

544 
in ctxt' > update_binds_env env end; 

545 

546 
val match_binds = gen_match_binds (read_term_pat, read_term); 

547 
val match_binds_i = gen_match_binds (cert_term_pat, cert_term); 

548 

549 

550 
(* bind proposition patterns *) 

551 

552 
fun gen_bind_propp prepp (ctxt, (raw_prop, raw_pats)) = 

553 
let val (ctxt', (pairs, prop)) = prep_declare_match prepp (ctxt, (raw_pats, raw_prop)) 

554 
in (ctxt' > match_binds_i (map (apfst single) pairs), prop) end; 

555 

556 
val bind_propp = gen_bind_propp (read_prop_pat, read_prop); 

557 
val bind_propp_i = gen_bind_propp (cert_prop_pat, cert_prop); 

5819  558 

559 

560 

561 
(** theorems **) 

562 

563 
(* thms_closure *) 

564 

565 
fun thms_closure (Context {thy, thms, ...}) = 

566 
let 

567 
val global_closure = PureThy.thms_closure thy; 

568 
fun get name = 

569 
(case global_closure name of 

570 
None => Symtab.lookup (thms, name) 

571 
 some => some); 

572 
in get end; 

573 

574 

6091  575 
(* get_thm(s) *) 
5819  576 

6091  577 
fun get_thm (ctxt as Context {thy, thms, ...}) name = 
5819  578 
(case Symtab.lookup (thms, name) of 
579 
Some [th] => th 

580 
 Some _ => raise CONTEXT ("Single theorem expected: " ^ quote name, ctxt) 

6091  581 
 None => (PureThy.get_thm thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt))); 
5819  582 

6091  583 
fun get_thms (ctxt as Context {thy, thms, ...}) name = 
5819  584 
(case Symtab.lookup (thms, name) of 
585 
Some ths => ths 

6091  586 
 None => (PureThy.get_thms thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt))); 
5819  587 

6091  588 
fun get_thmss ctxt names = flat (map (get_thms ctxt) names); 
5819  589 

590 

6091  591 
(* put_thm(s) *) 
5819  592 

6091  593 
fun put_thms (name, ths) = map_context 
5819  594 
(fn (thy, data, asms, binds, thms, defs) => 
595 
(thy, data, asms, binds, Symtab.update ((name, ths), thms), defs)); 

596 

6091  597 
fun put_thm (name, th) = put_thms (name, [th]); 
5819  598 

6091  599 
fun put_thmss [] ctxt = ctxt 
600 
 put_thmss (th :: ths) ctxt = ctxt > put_thms th > put_thmss ths; 

5819  601 

602 

6091  603 
(* have_thmss *) 
5819  604 

6091  605 
fun have_thmss name more_attrs ths_attrs ctxt = 
5819  606 
let 
607 
fun app ((ct, ths), (th, attrs)) = 

6091  608 
let val (ct', th') = Thm.applys_attributes ((ct, th), attrs @ more_attrs) 
5819  609 
in (ct', th' :: ths) end 
610 
val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs); 

5919  611 
val thms = flat (rev rev_thms); 
6091  612 
in (ctxt' > put_thms (name, thms), (name, thms)) end; 
5819  613 

614 

615 

616 
(** assumptions **) 

617 

618 
(* get assumptions *) 

619 

620 
fun assumptions (Context {asms = (asms, _), ...}) = flat (map #2 asms); 

621 
fun fixed_names (Context {asms = (_, (fixes, _)), ...}) = map #2 fixes; 

622 

623 

624 
(* assume *) 

625 

5935  626 
fun gen_assume prepp name attrs raw_prop_pats ctxt = 
5819  627 
let 
5935  628 
val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats); 
5819  629 
val sign = sign_of ctxt'; 
630 

6091  631 
val asms = map (Thm.assume o Thm.cterm_of sign) props; 
5919  632 

633 
val ths = map (fn th => ([th], [])) asms; 

6091  634 
val (ctxt'', (_, thms)) = 
5819  635 
ctxt' 
6091  636 
> have_thmss name (attrs @ [Drule.tag_assumption]) ths; 
5819  637 

638 
val ctxt''' = 

639 
ctxt'' 

640 
> map_context (fn (thy, data, (assumes, fixes), binds, thms, defs) => 

5919  641 
(thy, data, (assumes @ [(name, asms)], fixes), binds, thms, defs)); 
6091  642 
in (ctxt''', (name, thms)) end; 
5819  643 

5935  644 
val assume = gen_assume bind_propp; 
645 
val assume_i = gen_assume bind_propp_i; 

5819  646 

647 

648 
(* fix *) 

649 

650 
fun read_skolemT (Context {defs = (_, _, _, used), ...}) None = Type.param used ("'z", logicS) 

651 
 read_skolemT ctxt (Some s) = read_typ ctxt s; 

652 

653 
fun gen_fix prep check (ctxt, (x, raw_T)) = 

654 
ctxt 

655 
> declare_term (Free (check_skolem ctxt check x, prep ctxt raw_T)) 

656 
> map_context (fn (thy, data, (assumes, (fixes, names)), binds, thms, defs) => 

657 
let val x' = variant names x in 

658 
(thy, data, (assumes, ((x, Syntax.skolem x') :: fixes, x' :: names)), binds, thms, defs) 

659 
end); 

660 

661 
fun gen_fixs prep check xs ctxt = foldl (gen_fix prep check) (ctxt, xs); 

662 

663 

664 
val fix = gen_fixs read_skolemT true; 

665 
val fix_i = gen_fixs cert_typ false; 

666 

667 

668 

669 
(** theory setup **) 

670 

671 
val setup = [ProofDataData.init]; 

672 

673 

674 
end; 