author  wenzelm 
Tue, 21 Sep 1999 17:24:50 +0200  
changeset 7557  1b977741f530 
parent 7505  a9690e9cc58a 
child 7575  e1e2d07287d8 
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 

8 
signature PROOF_CONTEXT = 

9 
sig 

10 
type context 

11 
exception CONTEXT of string * context 

12 
val theory_of: context > theory 

13 
val sign_of: context > Sign.sg 

7557  14 
val prems_of: context > thm list 
6985  15 
val show_hyps: bool ref 
16 
val pretty_thm: thm > Pretty.T 

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

6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

20 
val strings_of_context: context > string list 
5819  21 
val print_proof_data: theory > unit 
5874  22 
val init: theory > context 
5819  23 
val read_typ: context > string > typ 
24 
val cert_typ: context > typ > typ 

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

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

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

32 
val declare_term: term > context > context 

33 
val declare_terms: term list > context > context 

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

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

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

6789  41 
val auto_bind_goal: term > context > context 
6797  42 
val auto_bind_facts: string > term list > context > context 
6091  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 

6875  49 
val have_thmss: thm list > string > context attribute list 
6091  50 
> (thm list * context attribute list) list > context > context * (string * thm list) 
6931  51 
val assumptions: context > (cterm * ((int > tactic) * (int > tactic))) list 
5819  52 
val fixed_names: context > string list 
7270  53 
val assume: ((int > tactic) * (int > tactic)) 
54 
> (string * context attribute list * (string * (string list * string list)) list) list 

55 
> context > context * ((string * thm list) list * thm list) 

56 
val assume_i: ((int > tactic) * (int > tactic)) 

57 
> (string * context attribute list * (term * (term list * term list)) list) list 

58 
> context > context * ((string * thm list) list * thm list) 

7411  59 
val fix: (string list * string option) list > context > context 
60 
val fix_i: (string list * typ) list > context > context 

5819  61 
val setup: (theory > theory) list 
62 
end; 

63 

64 
signature PROOF_CONTEXT_PRIVATE = 

65 
sig 

66 
include PROOF_CONTEXT 

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

68 
> theory > theory 

69 
val print_data: Object.kind > context > unit 

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

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

72 
end; 

73 

74 
structure ProofContext: PROOF_CONTEXT_PRIVATE = 

75 
struct 

76 

77 

78 
(** datatype context **) 

79 

80 
datatype context = 

81 
Context of 

6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

82 
{thy: theory, (*current theory*) 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

83 
data: Object.T Symtab.table, (*user data*) 
5819  84 
asms: 
6931  85 
((cterm * ((int > tactic) * (int > tactic))) list * (*assumes: A ==> _*) 
86 
(string * thm list) list) * 

6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

87 
((string * string) list * string list), (*fixes: !!x. _*) 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

88 
binds: (term * typ) Vartab.table, (*term bindings*) 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

89 
thms: thm list Symtab.table, (*local thms*) 
5819  90 
defs: 
6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

91 
typ Vartab.table * (*type constraints*) 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

92 
sort Vartab.table * (*default sorts*) 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

93 
int * (*maxidx*) 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

94 
string list}; (*used type var names*) 
5819  95 

96 
exception CONTEXT of string * context; 

97 

98 

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

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

101 

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

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

104 

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

106 
val sign_of = Theory.sign_of o theory_of; 

107 

7270  108 
fun prems_of (Context {asms = ((_, asms), _), ...}) = flat (map #2 asms); 
109 

5819  110 

111 

112 
(** print context information **) 

113 

6985  114 
val show_hyps = ref false; 
115 
fun pretty_thm th = setmp Display.show_hyps (! show_hyps) Display.pretty_thm th; 

116 

6528  117 
val verbose = ref false; 
6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

118 
fun verb f x = if ! verbose then f x else []; 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

119 
val verb_string = verb (Library.single o Pretty.string_of); 
5819  120 

6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

121 
fun strings_of_items prt name items = 
5819  122 
let 
123 
fun pretty_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x] 

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

6721  125 
in 
6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

126 
if null items andalso not (! verbose) then [] 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

127 
else [Pretty.string_of (Pretty.big_list name (map pretty_itms items))] 
6721  128 
end; 
5819  129 

130 

131 
(* term bindings *) 

132 

6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

133 
fun strings_of_binds (Context {thy, binds, ...}) = 
5819  134 
let 
135 
val prt_term = Sign.pretty_term (Theory.sign_of thy); 

7479  136 
fun pretty_bind (xi, (t, T)) = prt_term (Logic.mk_equals (Var (xi, T), t)); 
6721  137 
in 
6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

138 
if Vartab.is_empty binds andalso not (! verbose) then [] 
7486  139 
else [Pretty.string_of (Pretty.big_list "Term bindings:" 
140 
(map pretty_bind (Vartab.dest binds)))] 

6721  141 
end; 
5819  142 

6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

143 
val print_binds = seq writeln o strings_of_binds; 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

144 

5819  145 

146 
(* local theorems *) 

147 

6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

148 
fun strings_of_thms (Context {thms, ...}) = 
6985  149 
strings_of_items pretty_thm "Local theorems:" (Symtab.dest thms); 
6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

150 

f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

151 
val print_thms = seq writeln o strings_of_thms; 
5819  152 

153 

154 
(* main context *) 

155 

7270  156 
fun strings_of_context (ctxt as Context {thy, data = _, asms = (_, (fixes, _)), binds = _, 
5819  157 
thms = _, defs = (types, sorts, maxidx, used)}) = 
158 
let 

159 
val sign = Theory.sign_of thy; 

7270  160 
val prems = prems_of ctxt; 
5819  161 

162 
val prt_term = Sign.pretty_term sign; 

163 
val prt_typ = Sign.pretty_typ sign; 

164 
val prt_sort = Sign.pretty_sort sign; 

165 

166 
(*theory*) 

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

168 

169 
(*fixes*) 

7200  170 
fun prt_fixes xs = Pretty.block (Pretty.str "Fixed variables:" :: Pretty.brk 1 :: 
171 
Pretty.commas (map (fn (x, x') => Pretty.str (x ^ " = " ^ x')) xs)); 

172 

5819  173 

174 
(* defaults *) 

175 

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

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

178 

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

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

181 

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

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

184 

185 
val prt_defT = prt_atom prt_var prt_typ; 

186 
val prt_defS = prt_atom prt_varT prt_sort; 

187 
in 

6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

188 
verb_string pretty_thy @ 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

189 
(if null fixes andalso not (! verbose) then [] 
7200  190 
else [Pretty.string_of (prt_fixes (rev fixes))]) @ 
7270  191 
(if null prems andalso not (! verbose) then [] 
192 
else [Pretty.string_of (Pretty.big_list "Assumptions:" 

193 
(map (prt_term o #prop o Thm.rep_thm) prems))]) @ 

6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

194 
verb strings_of_binds ctxt @ 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

195 
verb strings_of_thms ctxt @ 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

196 
verb_string (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types))) @ 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

197 
verb_string (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts))) @ 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

198 
verb_string (Pretty.str ("Maxidx: " ^ string_of_int maxidx)) @ 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

199 
verb_string (Pretty.strs ("Used type variable names:" :: used)) 
5819  200 
end; 
201 

202 

203 

204 
(** user data **) 

205 

206 
(* errors *) 

207 

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

209 

210 
fun err_inconsistent kinds = 

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

212 

213 
fun err_dup_init thy kind = 

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

215 

216 
fun err_undef ctxt kind = 

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

218 

219 
fun err_uninit ctxt kind = 

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

221 
of_theory (theory_of ctxt), ctxt); 

222 

223 
fun err_access ctxt kind = 

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

225 
of_theory (theory_of ctxt), ctxt); 

226 

227 

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

229 

230 
structure ProofDataDataArgs = 

231 
struct 

232 
val name = "Isar/proof_data"; 

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

234 

235 
val empty = Symtab.empty; 

6550  236 
val copy = I; 
5819  237 
val prep_ext = I; 
238 
fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs 

239 
handle Symtab.DUPS kinds => err_inconsistent kinds; 

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

241 
end; 

242 

243 
structure ProofDataData = TheoryDataFun(ProofDataDataArgs); 

244 
val print_proof_data = ProofDataData.print; 

245 

246 

247 
(* init proof data *) 

248 

249 
fun init_data kind meths thy = 

250 
let 

251 
val name = Object.name_of_kind kind; 

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

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

254 
in thy > ProofDataData.put tab end; 

255 

256 

257 
(* access data *) 

258 

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

260 
let 

261 
val thy = theory_of ctxt; 

262 
val name = Object.name_of_kind kind; 

263 
in 

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

265 
Some (k, meths) => 

266 
if Object.eq_kind (kind, k) then 

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

268 
Some x => (x, meths) 

269 
 None => err_undef ctxt name) 

270 
else err_access ctxt name 

271 
 None => err_uninit ctxt name) 

272 
end; 

273 

274 
fun get_data kind f ctxt = 

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

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

277 

278 
fun print_data kind ctxt = 

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

280 
in prt ctxt x end; 

281 

282 
fun put_data kind f x ctxt = 

283 
(lookup_data ctxt kind; 

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

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

286 

287 

288 
(* init context *) 

289 

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

6797  292 
make_context (thy, data, (([], []), ([], [])), Vartab.empty, Symtab.empty, 
5819  293 
(Vartab.empty, Vartab.empty, ~1, [])) 
294 
end; 

295 

296 

297 

298 
(** prepare types **) 

299 

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

301 
let 

302 
val sign = sign_of ctxt; 

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

304 
in 

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

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

307 
end; 

308 

309 
fun cert_typ ctxt raw_T = 

310 
Sign.certify_typ (sign_of ctxt) raw_T 

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

312 

313 

314 

315 
(** prepare terms and propositions **) 

316 

317 
(* 

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

319 
(2) intern Skolem constants 

320 
(3) expand term bindings 

321 
*) 

322 

323 

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

325 

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

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

329 

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

331 

5819  332 

6762  333 
fun read_term_sg freeze sg (defs as (_, _, used)) s = 
7505  334 
#1 (read_def_termT freeze sg defs (s, dummyT)); 
5819  335 

6762  336 
fun read_prop_sg freeze sg defs s = 
337 
#1 (read_def_termT freeze sg defs (s, propT)); 

5819  338 

339 

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

341 

342 
fun cert_prop_sg sg tm = 

343 
let 

344 
val ctm = Thm.cterm_of sg tm; 

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

346 
in 

347 
if T = propT then t 

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

349 
end; 

350 

351 

352 
(* intern_skolem *) 

353 

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

355 

356 
fun check_skolem ctxt check x = 

7200  357 
if not check then x 
358 
else if not (Syntax.is_identifier x) then 

359 
raise CONTEXT ("Bad variable name: " ^ quote x, ctxt) 

360 
else if can Syntax.dest_skolem x then 

5819  361 
raise CONTEXT ("Illegal reference to internal Skolem constant: " ^ quote x, ctxt) 
362 
else x; 

363 

364 
fun intern_skolem ctxt check = 

365 
let 

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

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

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

369 
 None => t) 

370 
 intern (t $ u) = intern t $ intern u 

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

372 
 intern a = a; 

373 
in intern end; 

374 

375 

376 
(* norm_term *) 

377 

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

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

380 

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

382 
let 

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

384 
exception SAME; 

385 

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

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

388 
Some (u, U) => 

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

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

7479  391 
 None => raise CONTEXT ("Unbound schematic variable: " ^ Syntax.string_of_vname xi, ctxt)) 
5819  392 
 norm (Abs (a, T, body)) = Abs (a, T, norm body) 
393 
 norm (Abs (_, _, body) $ t) = normh (subst_bound (t, body)) 

394 
 norm (f $ t) = 

395 
((case norm f of 

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

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

398 
 norm _ = raise SAME 

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

400 
in normh end; 

401 

402 

6550  403 
(* dummy patterns *) 
404 

6762  405 
local 
406 

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

407 
fun is_dummy (Const (c, _)) = c = PureThy.dummy_patternN 
6550  408 
 is_dummy _ = false; 
409 

6762  410 
fun prep_dummy (i, t) = 
411 
if is_dummy t then (i + 1, Var (("_dummy_", i), Term.fastype_of t)) else (i, t); 

412 

413 
in 

414 

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

416 

6550  417 
fun reject_dummies ctxt tm = 
418 
if foldl_aterms (fn (ok, t) => ok andalso not (is_dummy t)) (true, tm) then tm 

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

420 

6762  421 
end; 
6550  422 

423 

5819  424 
(* read terms *) 
425 

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

429 

430 
fun def_type xi = 

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

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

433 
 some => some); 

434 

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

436 
in 

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

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

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

5874  440 
> app (intern_skolem ctxt true) 
441 
> app (if is_pat then I else norm_term ctxt) 

6550  442 
> app (if is_pat then prepare_dummies else (reject_dummies ctxt)) 
5819  443 
end; 
444 

5874  445 
val read_termTs = gen_read (read_def_termTs false) (apfst o map) false; 
6762  446 
val read_term = gen_read (read_term_sg true) I false; 
447 
val read_prop = gen_read (read_prop_sg true) I false; 

448 
val read_term_pat = gen_read (read_term_sg false) I true; 

449 
val read_prop_pat = gen_read (read_prop_sg false) I true; 

5819  450 

451 

452 
(* certify terms *) 

453 

454 
fun gen_cert cert is_pat ctxt t = 

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

456 
> intern_skolem ctxt false 

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

458 

459 
val cert_term = gen_cert cert_term_sg false; 

460 
val cert_prop = gen_cert cert_prop_sg false; 

5935  461 
val cert_term_pat = gen_cert cert_term_sg true; 
462 
val cert_prop_pat = gen_cert cert_prop_sg true; 

5819  463 

464 

465 
(* declare terms *) 

466 

467 
val ins_types = foldl_aterms 

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

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

470 
 (types, _) => types); 

471 

472 
val ins_sorts = foldl_types (foldl_atyps 

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

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

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

476 

477 
val ins_used = foldl_types (foldl_atyps 

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

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

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

481 

5994  482 
fun ins_skolem def_type = foldr 
483 
(fn ((x, x'), types) => 

484 
(case def_type x' of 

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

486 
 None => types)); 

487 

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

490 

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

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

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

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

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

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

5819  500 

501 

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

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

504 

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

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

508 

5819  509 

510 

511 
(** bindings **) 

512 

513 
(* update_binds *) 

514 

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

516 
let val T = fastype_of t in 

517 
ctxt 

518 
> declare_term t 

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

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

521 
end; 

522 

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

7479  524 
fun update_binds_env env = (*Envir.norm_term ensures proper type instantiation*) 
525 
update_binds (map (apsnd (Envir.norm_term env)) (Envir.alist_of env)); 

5819  526 

527 

528 
(* add_binds(_i)  sequential *) 

529 

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

7479  531 
ctxt > update_binds [(xi, prep ctxt raw_t)]; 
5819  532 

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

534 

535 
val add_binds = gen_binds read_term; 

536 
val add_binds_i = gen_binds cert_term; 

537 

538 

539 
(* match_binds(_i)  parallel *) 

540 

5935  541 
fun prep_declare_match (prep_pat, prep) (ctxt, (raw_pats, raw_t)) = 
5819  542 
let 
5935  543 
val t = prep ctxt raw_t; 
5994  544 
val ctxt' = ctxt > declare_term t; 
6931  545 
val matches = map (fn (f, raw_pat) => (prep_pat ctxt' raw_pat, f t)) raw_pats; 
546 
(* FIXME seq / par / simult (??) *) 

547 
in (ctxt', (matches, t)) end; 

5819  548 

5935  549 
fun gen_match_binds _ [] ctxt = ctxt 
6931  550 
 gen_match_binds prepp args ctxt = 
5935  551 
let 
6931  552 
val raw_pairs = map (apfst (map (pair I))) args; 
5935  553 
val (ctxt', matches) = foldl_map (prep_declare_match prepp) (ctxt, raw_pairs); 
554 
val pairs = flat (map #1 matches); 

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

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

557 
val env = 

558 
(case Seq.pull envs of 

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

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

561 
in ctxt' > update_binds_env env end; 

562 

563 
val match_binds = gen_match_binds (read_term_pat, read_term); 

564 
val match_binds_i = gen_match_binds (cert_term_pat, cert_term); 

565 

566 

567 
(* bind proposition patterns *) 

568 

6931  569 
fun gen_bind_propp prepp (ctxt, (raw_prop, (raw_pats1, raw_pats2))) = 
570 
let 

571 
val raw_pats = map (pair I) raw_pats1 @ map (pair Logic.strip_imp_concl) raw_pats2; 

572 
val (ctxt', (pairs, prop)) = prep_declare_match prepp (ctxt, (raw_pats, raw_prop)); 

5935  573 
in (ctxt' > match_binds_i (map (apfst single) pairs), prop) end; 
574 

575 
val bind_propp = gen_bind_propp (read_prop_pat, read_prop); 

576 
val bind_propp_i = gen_bind_propp (cert_prop_pat, cert_prop); 

5819  577 

578 

6789  579 
(* auto binds *) 
580 

581 
val auto_bind_goal = add_binds_i o AutoBind.goal; 

6797  582 
val auto_bind_facts = add_binds_i oo AutoBind.facts; 
6789  583 

584 

5819  585 

586 
(** theorems **) 

587 

6091  588 
(* get_thm(s) *) 
5819  589 

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

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

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

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

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

6091  601 
fun get_thmss ctxt names = flat (map (get_thms ctxt) names); 
5819  602 

603 

6091  604 
(* put_thm(s) *) 
5819  605 

7479  606 
fun put_thms ("", _) = I 
607 
 put_thms (name, ths) = map_context 

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

609 
(thy, data, asms, binds, Symtab.update ((name, ths), thms), defs)); 

5819  610 

6091  611 
fun put_thm (name, th) = put_thms (name, [th]); 
5819  612 

6091  613 
fun put_thmss [] ctxt = ctxt 
614 
 put_thmss (th :: ths) ctxt = ctxt > put_thms th > put_thmss ths; 

5819  615 

616 

6091  617 
(* have_thmss *) 
5819  618 

6875  619 
fun have_thmss more_ths name more_attrs ths_attrs ctxt = 
5819  620 
let 
621 
fun app ((ct, ths), (th, attrs)) = 

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

6875  625 
val thms = flat (rev rev_thms) @ more_ths; 
6091  626 
in (ctxt' > put_thms (name, thms), (name, thms)) end; 
5819  627 

628 

629 

630 
(** assumptions **) 

631 

632 
(* get assumptions *) 

633 

6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

634 
fun assumptions (Context {asms = ((asms, _), _), ...}) = asms; 
5819  635 
fun fixed_names (Context {asms = (_, (fixes, _)), ...}) = map #2 fixes; 
636 

637 

638 
(* assume *) 

639 

7270  640 
local 
6797  641 

7270  642 
fun gen_assm prepp tac (ctxt, (name, attrs, raw_prop_pats)) = 
5819  643 
let 
5935  644 
val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats); 
5819  645 
val sign = sign_of ctxt'; 
6797  646 
val Context {defs = (_, _, maxidx, _), ...} = ctxt'; 
5819  647 

6797  648 
val cprops = map (Thm.cterm_of sign) props; 
6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

649 
val cprops_tac = map (rpair tac) cprops; 
6996  650 
val asms = map (Drule.forall_elim_vars (maxidx + 1) o Drule.assume_goal) cprops; 
5919  651 

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

6091  653 
val (ctxt'', (_, thms)) = 
5819  654 
ctxt' 
6797  655 
> auto_bind_facts name props 
6875  656 
> have_thmss [] name (attrs @ [Drule.tag_assumption]) ths; 
5819  657 

658 
val ctxt''' = 

659 
ctxt'' 

6797  660 
> map_context (fn (thy, data, ((asms_ct, asms_th), fixes), binds, thms, defs) => 
6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

661 
(thy, data, ((asms_ct @ cprops_tac, asms_th @ [(name, asms)]), fixes), binds, thms, defs)); 
7270  662 
in (ctxt''', (name, thms)) end; 
663 

664 
fun gen_assms prepp tac args ctxt = 

665 
let val (ctxt', thmss) = foldl_map (gen_assm prepp tac) (ctxt, args) 

666 
in (ctxt', (thmss, prems_of ctxt')) end; 

5819  667 

7270  668 
in 
669 

670 
val assume = gen_assms bind_propp; 

671 
val assume_i = gen_assms bind_propp_i; 

672 

673 
end; 

5819  674 

675 

676 
(* fix *) 

677 

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

7486  679 
(check_skolem ctxt check x; 
680 
ctxt 

681 
> (case prep ctxt raw_T of None => I  Some T => declare_term (Free (x, T))) 

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

5819  683 
let val x' = variant names x in 
684 
(thy, data, (assumes, ((x, Syntax.skolem x') :: fixes, x' :: names)), binds, thms, defs) 

7486  685 
end)); 
5819  686 

7411  687 
fun gen_fixs prep check vars ctxt = 
688 
foldl (gen_fix prep check) (ctxt, flat (map (fn (xs, T) => map (rpair T) xs) vars)); 

5819  689 

7486  690 
val fix = gen_fixs (apsome o read_typ) true; 
691 
val fix_i = gen_fixs (Some oo cert_typ) false; 

5819  692 

6895  693 

5819  694 

695 
(** theory setup **) 

696 

697 
val setup = [ProofDataData.init]; 

698 

699 

700 
end; 