author  wenzelm 
Tue, 07 Sep 1999 16:57:52 +0200  
changeset 7505  a9690e9cc58a 
parent 7486  1f9eceb434db 
child 7557  1b977741f530 
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 

6985  14 
val show_hyps: bool ref 
15 
val pretty_thm: thm > Pretty.T 

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

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

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

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

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

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

31 
val declare_term: term > context > context 

32 
val declare_terms: term list > context > context 

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

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

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

6789  40 
val auto_bind_goal: term > context > context 
6797  41 
val auto_bind_facts: string > term list > context > context 
6091  42 
val get_thm: context > string > thm 
43 
val get_thms: context > string > thm list 

44 
val get_thmss: context > string list > thm list 

45 
val put_thm: string * thm > context > context 

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

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

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

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

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

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

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

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

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

62 

63 
signature PROOF_CONTEXT_PRIVATE = 

64 
sig 

65 
include PROOF_CONTEXT 

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

67 
> theory > theory 

68 
val print_data: Object.kind > context > unit 

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

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

71 
end; 

72 

73 
structure ProofContext: PROOF_CONTEXT_PRIVATE = 

74 
struct 

75 

76 

77 
(** datatype context **) 

78 

79 
datatype context = 

80 
Context of 

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

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

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

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

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

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

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

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

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

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

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

95 
exception CONTEXT of string * context; 

96 

97 

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

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

100 

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

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

103 

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

105 
val sign_of = Theory.sign_of o theory_of; 

106 

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

5819  109 

110 

111 
(** print context information **) 

112 

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

115 

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

117 
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

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

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

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

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

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

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

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

129 

130 
(* term bindings *) 

131 

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

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

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

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

6721  140 
end; 
5819  141 

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

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

143 

5819  144 

145 
(* local theorems *) 

146 

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

147 
fun strings_of_thms (Context {thms, ...}) = 
6985  148 
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

149 

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

150 
val print_thms = seq writeln o strings_of_thms; 
5819  151 

152 

153 
(* main context *) 

154 

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

158 
val sign = Theory.sign_of thy; 

7270  159 
val prems = prems_of ctxt; 
5819  160 

161 
val prt_term = Sign.pretty_term sign; 

162 
val prt_typ = Sign.pretty_typ sign; 

163 
val prt_sort = Sign.pretty_sort sign; 

164 

165 
(*theory*) 

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

167 

168 
(*fixes*) 

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

171 

5819  172 

173 
(* defaults *) 

174 

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

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

177 

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

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

180 

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

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

183 

184 
val prt_defT = prt_atom prt_var prt_typ; 

185 
val prt_defS = prt_atom prt_varT prt_sort; 

186 
in 

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

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

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

192 
(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

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

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

195 
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

196 
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

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

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

201 

202 

203 
(** user data **) 

204 

205 
(* errors *) 

206 

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

208 

209 
fun err_inconsistent kinds = 

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

211 

212 
fun err_dup_init thy kind = 

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

214 

215 
fun err_undef ctxt kind = 

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

217 

218 
fun err_uninit ctxt kind = 

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

220 
of_theory (theory_of ctxt), ctxt); 

221 

222 
fun err_access ctxt kind = 

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

224 
of_theory (theory_of ctxt), ctxt); 

225 

226 

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

228 

229 
structure ProofDataDataArgs = 

230 
struct 

231 
val name = "Isar/proof_data"; 

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

233 

234 
val empty = Symtab.empty; 

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

238 
handle Symtab.DUPS kinds => err_inconsistent kinds; 

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

240 
end; 

241 

242 
structure ProofDataData = TheoryDataFun(ProofDataDataArgs); 

243 
val print_proof_data = ProofDataData.print; 

244 

245 

246 
(* init proof data *) 

247 

248 
fun init_data kind meths thy = 

249 
let 

250 
val name = Object.name_of_kind kind; 

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

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

253 
in thy > ProofDataData.put tab end; 

254 

255 

256 
(* access data *) 

257 

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

259 
let 

260 
val thy = theory_of ctxt; 

261 
val name = Object.name_of_kind kind; 

262 
in 

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

264 
Some (k, meths) => 

265 
if Object.eq_kind (kind, k) then 

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

267 
Some x => (x, meths) 

268 
 None => err_undef ctxt name) 

269 
else err_access ctxt name 

270 
 None => err_uninit ctxt name) 

271 
end; 

272 

273 
fun get_data kind f ctxt = 

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

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

276 

277 
fun print_data kind ctxt = 

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

279 
in prt ctxt x end; 

280 

281 
fun put_data kind f x ctxt = 

282 
(lookup_data ctxt kind; 

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

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

285 

286 

287 
(* init context *) 

288 

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

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

294 

295 

296 

297 
(** prepare types **) 

298 

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

300 
let 

301 
val sign = sign_of ctxt; 

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

303 
in 

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

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

306 
end; 

307 

308 
fun cert_typ ctxt raw_T = 

309 
Sign.certify_typ (sign_of ctxt) raw_T 

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

311 

312 

313 

314 
(** prepare terms and propositions **) 

315 

316 
(* 

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

318 
(2) intern Skolem constants 

319 
(3) expand term bindings 

320 
*) 

321 

322 

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

324 

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

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

328 

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

330 

5819  331 

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

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

5819  337 

338 

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

340 

341 
fun cert_prop_sg sg tm = 

342 
let 

343 
val ctm = Thm.cterm_of sg tm; 

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

345 
in 

346 
if T = propT then t 

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

348 
end; 

349 

350 

351 
(* intern_skolem *) 

352 

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

354 

355 
fun check_skolem ctxt check x = 

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

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

359 
else if can Syntax.dest_skolem x then 

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

362 

363 
fun intern_skolem ctxt check = 

364 
let 

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

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

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

368 
 None => t) 

369 
 intern (t $ u) = intern t $ intern u 

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

371 
 intern a = a; 

372 
in intern end; 

373 

374 

375 
(* norm_term *) 

376 

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

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

379 

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

381 
let 

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

383 
exception SAME; 

384 

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

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

387 
Some (u, U) => 

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

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

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

393 
 norm (f $ t) = 

394 
((case norm f of 

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

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

397 
 norm _ = raise SAME 

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

399 
in normh end; 

400 

401 

6550  402 
(* dummy patterns *) 
403 

6762  404 
local 
405 

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

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

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

411 

412 
in 

413 

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

415 

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

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

419 

6762  420 
end; 
6550  421 

422 

5819  423 
(* read terms *) 
424 

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

428 

429 
fun def_type xi = 

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

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

432 
 some => some); 

433 

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

435 
in 

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

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

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

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

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

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

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

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

5819  449 

450 

451 
(* certify terms *) 

452 

453 
fun gen_cert cert is_pat ctxt t = 

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

455 
> intern_skolem ctxt false 

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

457 

458 
val cert_term = gen_cert cert_term_sg false; 

459 
val cert_prop = gen_cert cert_prop_sg false; 

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

5819  462 

463 

464 
(* declare terms *) 

465 

466 
val ins_types = foldl_aterms 

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

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

469 
 (types, _) => types); 

470 

471 
val ins_sorts = foldl_types (foldl_atyps 

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

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

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

475 

476 
val ins_used = foldl_types (foldl_atyps 

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

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

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

480 

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

483 
(case def_type x' of 

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

485 
 None => types)); 

486 

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

489 

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

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

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

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

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

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

5819  499 

500 

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

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

503 

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

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

507 

5819  508 

509 

510 
(** bindings **) 

511 

512 
(* update_binds *) 

513 

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

515 
let val T = fastype_of t in 

516 
ctxt 

517 
> declare_term t 

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

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

520 
end; 

521 

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

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

5819  525 

526 

527 
(* add_binds(_i)  sequential *) 

528 

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

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

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

533 

534 
val add_binds = gen_binds read_term; 

535 
val add_binds_i = gen_binds cert_term; 

536 

537 

538 
(* match_binds(_i)  parallel *) 

539 

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

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

5819  547 

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

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

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

556 
val env = 

557 
(case Seq.pull envs of 

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

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

560 
in ctxt' > update_binds_env env end; 

561 

562 
val match_binds = gen_match_binds (read_term_pat, read_term); 

563 
val match_binds_i = gen_match_binds (cert_term_pat, cert_term); 

564 

565 

566 
(* bind proposition patterns *) 

567 

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

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

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

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

574 
val bind_propp = gen_bind_propp (read_prop_pat, read_prop); 

575 
val bind_propp_i = gen_bind_propp (cert_prop_pat, cert_prop); 

5819  576 

577 

6789  578 
(* auto binds *) 
579 

580 
val auto_bind_goal = add_binds_i o AutoBind.goal; 

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

583 

5819  584 

585 
(** theorems **) 

586 

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

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

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

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

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

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

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

602 

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

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

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

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

5819  609 

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

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

5819  614 

615 

6091  616 
(* have_thmss *) 
5819  617 

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

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

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

627 

628 

629 
(** assumptions **) 

630 

631 
(* get assumptions *) 

632 

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

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

636 

637 
(* assume *) 

638 

7270  639 
local 
6797  640 

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

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

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

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

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

657 
val ctxt''' = 

658 
ctxt'' 

6797  659 
> 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

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

663 
fun gen_assms prepp tac args ctxt = 

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

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

5819  666 

7270  667 
in 
668 

669 
val assume = gen_assms bind_propp; 

670 
val assume_i = gen_assms bind_propp_i; 

671 

672 
end; 

5819  673 

674 

675 
(* fix *) 

676 

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

7486  678 
(check_skolem ctxt check x; 
679 
ctxt 

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

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

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

7486  684 
end)); 
5819  685 

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

5819  688 

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

5819  691 

6895  692 

5819  693 

694 
(** theory setup **) 

695 

696 
val setup = [ProofDataData.init]; 

697 

698 

699 
end; 