author  wenzelm 
Thu, 01 Jul 1999 21:20:27 +0200  
changeset 6875  df31250ccb3a 
parent 6870  43d64c520d11 
child 6895  450b1f67f099 
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 

6528  14 
val verbose: bool ref 
5819  15 
val print_binds: context > unit 
16 
val print_thms: context > unit 

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

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

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

5935  25 
val read_term_pat: context > string > term 
26 
val read_prop_pat: context > string > term 

5819  27 
val cert_term: context > term > term 
28 
val cert_prop: context > term > term 

29 
val declare_term: term > context > context 

30 
val declare_terms: term list > context > context 

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

5935  34 
val match_binds: (string list * string) list > context > context 
35 
val match_binds_i: (term list * term) list > context > context 

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

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

6789  38 
val auto_bind_goal: term > context > context 
6797  39 
val auto_bind_facts: string > term list > context > context 
6091  40 
val thms_closure: context > xstring > thm list option 
41 
val get_thm: context > string > thm 

42 
val get_thms: context > string > thm list 

43 
val get_thmss: context > string list > thm list 

44 
val put_thm: string * thm > context > context 

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

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

6875  47 
val have_thmss: thm list > string > context attribute list 
6091  48 
> (thm list * context attribute list) list > context > context * (string * thm list) 
6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

49 
val assumptions: context > (cterm * (int > tactic)) list 
5819  50 
val fixed_names: context > string list 
6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

51 
val assume: (int > tactic) > string > context attribute list > (string * string list) list 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

52 
> context > context * ((string * thm list) * thm list) 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

53 
val assume_i: (int > tactic) > string > context attribute list > (term * term list) list 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

54 
> context > context * ((string * thm list) * thm list) 
5819  55 
val fix: (string * string option) list > context > context 
56 
val fix_i: (string * typ) list > context > context 

57 
val setup: (theory > theory) list 

58 
end; 

59 

60 
signature PROOF_CONTEXT_PRIVATE = 

61 
sig 

62 
include PROOF_CONTEXT 

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

64 
> theory > theory 

65 
val print_data: Object.kind > context > unit 

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

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

68 
end; 

69 

70 
structure ProofContext: PROOF_CONTEXT_PRIVATE = 

71 
struct 

72 

73 

74 
(** datatype context **) 

75 

76 
datatype context = 

77 
Context of 

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

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

79 
data: Object.T Symtab.table, (*user data*) 
5819  80 
asms: 
6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

81 
((cterm * (int > tactic)) list * (string * thm list) list) * (*assumes: A ==> _*) 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

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

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

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

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

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

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

89 
string list}; (*used type var names*) 
5819  90 

91 
exception CONTEXT of string * context; 

92 

93 

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

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

96 

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

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

99 

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

101 
val sign_of = Theory.sign_of o theory_of; 

102 

103 

104 

105 
(** print context information **) 

106 

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

108 
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

109 
val verb_string = verb (Library.single o Pretty.string_of); 
5819  110 

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

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

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

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

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

117 
else [Pretty.string_of (Pretty.big_list name (map pretty_itms items))] 
6721  118 
end; 
5819  119 

120 

121 
(* term bindings *) 

122 

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

123 
fun strings_of_binds (Context {thy, binds, ...}) = 
5819  124 
let 
125 
val prt_term = Sign.pretty_term (Theory.sign_of thy); 

126 

127 
fun fix_var (x, i) = 

128 
(case try Syntax.dest_binding x of 

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

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

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

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

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

134 
if Vartab.is_empty binds andalso not (! verbose) then [] 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

135 
else [Pretty.string_of (Pretty.big_list "Term bindings:" (map pretty_bind (Vartab.dest binds)))] 
6721  136 
end; 
5819  137 

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

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

139 

5819  140 

141 
(* local theorems *) 

142 

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

143 
fun strings_of_thms (Context {thms, ...}) = 
6870  144 
strings_of_items (setmp Display.show_hyps false Display.pretty_thm) 
145 
"Local theorems:" (Symtab.dest thms); 

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

146 

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

147 
val print_thms = seq writeln o strings_of_thms; 
5819  148 

149 

150 
(* main context *) 

151 

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

152 
fun strings_of_context (ctxt as Context {thy, data = _, asms = ((_, prems), (fixes, _)), binds = _, 
5819  153 
thms = _, defs = (types, sorts, maxidx, used)}) = 
154 
let 

155 
val sign = Theory.sign_of thy; 

156 

157 
val prt_term = Sign.pretty_term sign; 

158 
val prt_typ = Sign.pretty_typ sign; 

159 
val prt_sort = Sign.pretty_sort sign; 

160 

161 
(*theory*) 

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

163 

164 
(*fixes*) 

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

166 

167 
(* defaults *) 

168 

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

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

171 

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

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

174 

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

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

177 

178 
val prt_defT = prt_atom prt_var prt_typ; 

179 
val prt_defS = prt_atom prt_varT prt_sort; 

180 
in 

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

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

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

183 
else [Pretty.string_of (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)))]) @ 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

184 
strings_of_items (prt_term o #prop o Thm.rep_thm) "Assumptions:" prems @ 
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

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

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

187 
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

188 
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

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

190 
verb_string (Pretty.strs ("Used type variable names:" :: used)) 
5819  191 
end; 
192 

193 

194 

195 
(** user data **) 

196 

197 
(* errors *) 

198 

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

200 

201 
fun err_inconsistent kinds = 

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

203 

204 
fun err_dup_init thy kind = 

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

206 

207 
fun err_undef ctxt kind = 

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

209 

210 
fun err_uninit ctxt kind = 

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

212 
of_theory (theory_of ctxt), ctxt); 

213 

214 
fun err_access ctxt kind = 

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

216 
of_theory (theory_of ctxt), ctxt); 

217 

218 

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

220 

221 
structure ProofDataDataArgs = 

222 
struct 

223 
val name = "Isar/proof_data"; 

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

225 

226 
val empty = Symtab.empty; 

6550  227 
val copy = I; 
5819  228 
val prep_ext = I; 
229 
fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs 

230 
handle Symtab.DUPS kinds => err_inconsistent kinds; 

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

232 
end; 

233 

234 
structure ProofDataData = TheoryDataFun(ProofDataDataArgs); 

235 
val print_proof_data = ProofDataData.print; 

236 

237 

238 
(* init proof data *) 

239 

240 
fun init_data kind meths thy = 

241 
let 

242 
val name = Object.name_of_kind kind; 

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

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

245 
in thy > ProofDataData.put tab end; 

246 

247 

248 
(* access data *) 

249 

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

251 
let 

252 
val thy = theory_of ctxt; 

253 
val name = Object.name_of_kind kind; 

254 
in 

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

256 
Some (k, meths) => 

257 
if Object.eq_kind (kind, k) then 

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

259 
Some x => (x, meths) 

260 
 None => err_undef ctxt name) 

261 
else err_access ctxt name 

262 
 None => err_uninit ctxt name) 

263 
end; 

264 

265 
fun get_data kind f ctxt = 

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

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

268 

269 
fun print_data kind ctxt = 

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

271 
in prt ctxt x end; 

272 

273 
fun put_data kind f x ctxt = 

274 
(lookup_data ctxt kind; 

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

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

277 

278 

279 
(* init context *) 

280 

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

6797  283 
make_context (thy, data, (([], []), ([], [])), Vartab.empty, Symtab.empty, 
5819  284 
(Vartab.empty, Vartab.empty, ~1, [])) 
285 
end; 

286 

287 

288 

289 
(** prepare types **) 

290 

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

292 
let 

293 
val sign = sign_of ctxt; 

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

295 
in 

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

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

298 
end; 

299 

300 
fun cert_typ ctxt raw_T = 

301 
Sign.certify_typ (sign_of ctxt) raw_T 

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

303 

304 

305 

306 
(** prepare terms and propositions **) 

307 

308 
(* 

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

310 
(2) intern Skolem constants 

311 
(3) expand term bindings 

312 
*) 

313 

314 

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

316 

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

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

320 

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

322 

5819  323 

6762  324 
fun read_term_sg freeze sg (defs as (_, _, used)) s = 
325 
#1 (read_def_termT freeze sg defs (s, TVar ((variant used "'z", 0), logicS))); 

5819  326 

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

5819  329 

330 

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

332 

333 
fun cert_prop_sg sg tm = 

334 
let 

335 
val ctm = Thm.cterm_of sg tm; 

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

337 
in 

338 
if T = propT then t 

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

340 
end; 

341 

342 

343 
(* intern_skolem *) 

344 

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

346 

347 
fun check_skolem ctxt check x = 

348 
if check andalso can Syntax.dest_skolem x then 

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

350 
else x; 

351 

352 
fun intern_skolem ctxt check = 

353 
let 

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

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

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

357 
 None => t) 

358 
 intern (t $ u) = intern t $ intern u 

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

360 
 intern a = a; 

361 
in intern end; 

362 

363 

364 
(* norm_term *) 

365 

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

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

368 

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

370 
let 

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

372 
exception SAME; 

373 

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

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

376 
Some (u, U) => 

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

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

379 
 None => 

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

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

382 
else raise SAME) 

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

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

385 
 norm (f $ t) = 

386 
((case norm f of 

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

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

389 
 norm _ = raise SAME 

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

391 
in normh end; 

392 

393 

6550  394 
(* dummy patterns *) 
395 

6762  396 
local 
397 

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

398 
fun is_dummy (Const (c, _)) = c = PureThy.dummy_patternN 
6550  399 
 is_dummy _ = false; 
400 

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

403 

404 
in 

405 

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

407 

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

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

411 

6762  412 
end; 
6550  413 

414 

5819  415 
(* read terms *) 
416 

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

420 

421 
fun def_type xi = 

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

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

424 
 some => some); 

425 

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

427 
in 

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

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

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

5874  431 
> app (intern_skolem ctxt true) 
432 
> app (if is_pat then I else norm_term ctxt) 

6550  433 
> app (if is_pat then prepare_dummies else (reject_dummies ctxt)) 
5819  434 
end; 
435 

5874  436 
val read_termTs = gen_read (read_def_termTs false) (apfst o map) false; 
6762  437 
val read_term = gen_read (read_term_sg true) I false; 
438 
val read_prop = gen_read (read_prop_sg true) I false; 

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

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

5819  441 

442 

443 
(* certify terms *) 

444 

445 
fun gen_cert cert is_pat ctxt t = 

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

447 
> intern_skolem ctxt false 

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

449 

450 
val cert_term = gen_cert cert_term_sg false; 

451 
val cert_prop = gen_cert cert_prop_sg false; 

5935  452 
val cert_term_pat = gen_cert cert_term_sg true; 
453 
val cert_prop_pat = gen_cert cert_prop_sg true; 

5819  454 

455 

456 
(* declare terms *) 

457 

458 
val ins_types = foldl_aterms 

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

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

461 
 (types, _) => types); 

462 

463 
val ins_sorts = foldl_types (foldl_atyps 

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

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

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

467 

468 
val ins_used = foldl_types (foldl_atyps 

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

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

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

472 

5994  473 
fun ins_skolem def_type = foldr 
474 
(fn ((x, x'), types) => 

475 
(case def_type x' of 

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

477 
 None => types)); 

478 

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

481 

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

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

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

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

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

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

5819  491 

492 

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

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

495 

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

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

499 

5819  500 

501 

502 
(** bindings **) 

503 

504 
(* update_binds *) 

505 

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

507 
let val T = fastype_of t in 

508 
ctxt 

509 
> declare_term t 

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

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

512 
end; 

513 

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

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

516 

517 

518 
(* add_binds(_i)  sequential *) 

519 

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

521 
let val t = prep ctxt raw_t in 

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

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

524 
quote (Syntax.string_of_vname xi), ctxt) 

525 
end; 

526 

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

528 

529 
val add_binds = gen_binds read_term; 

530 
val add_binds_i = gen_binds cert_term; 

531 

532 

533 
(* match_binds(_i)  parallel *) 

534 

5935  535 
fun prep_declare_match (prep_pat, prep) (ctxt, (raw_pats, raw_t)) = 
5819  536 
let 
5935  537 
val t = prep ctxt raw_t; 
5994  538 
val ctxt' = ctxt > declare_term t; 
6847
f175f56c57a6
tuned output: print_context replaced by strings_of_context;
wenzelm
parents:
6797
diff
changeset

539 
val pats = map (prep_pat ctxt') raw_pats; (* FIXME seq / par / simult (??) *) 
5994  540 
in (ctxt', (map (rpair t) pats, t)) end; 
5819  541 

5935  542 
fun gen_match_binds _ [] ctxt = ctxt 
543 
 gen_match_binds prepp raw_pairs ctxt = 

544 
let 

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

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

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

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

549 
val env = 

550 
(case Seq.pull envs of 

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

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

553 
in ctxt' > update_binds_env env end; 

554 

555 
val match_binds = gen_match_binds (read_term_pat, read_term); 

556 
val match_binds_i = gen_match_binds (cert_term_pat, cert_term); 

557 

558 

559 
(* bind proposition patterns *) 

560 

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

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

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

564 

565 
val bind_propp = gen_bind_propp (read_prop_pat, read_prop); 

566 
val bind_propp_i = gen_bind_propp (cert_prop_pat, cert_prop); 

5819  567 

568 

6789  569 
(* auto binds *) 
570 

571 
val auto_bind_goal = add_binds_i o AutoBind.goal; 

6797  572 
val auto_bind_facts = add_binds_i oo AutoBind.facts; 
6789  573 

574 

5819  575 

576 
(** theorems **) 

577 

578 
(* thms_closure *) 

579 

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

581 
let 

582 
val global_closure = PureThy.thms_closure thy; 

583 
fun get name = 

584 
(case global_closure name of 

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

586 
 some => some); 

587 
in get end; 

588 

589 

6091  590 
(* get_thm(s) *) 
5819  591 

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

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

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

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

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

6091  603 
fun get_thmss ctxt names = flat (map (get_thms ctxt) names); 
5819  604 

605 

6091  606 
(* put_thm(s) *) 
5819  607 

6091  608 
fun put_thms (name, ths) = map_context 
5819  609 
(fn (thy, data, asms, binds, thms, defs) => 
610 
(thy, data, asms, binds, Symtab.update ((name, ths), thms), defs)); 

611 

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

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

5819  616 

617 

6091  618 
(* have_thmss *) 
5819  619 

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

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

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

629 

630 

631 
(** assumptions **) 

632 

633 
(* get assumptions *) 

634 

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

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

638 

639 
(* assume *) 

640 

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

641 
fun prems (Context {asms = ((_, asms), _), ...}) = flat (map #2 asms); 
6797  642 

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

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

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

650 
val cprops_tac = map (rpair tac) cprops; 
6797  651 
val asms = map (Drule.forall_elim_vars (maxidx + 1) o Thm.assume) cprops; 
5919  652 

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

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

659 
val ctxt''' = 

660 
ctxt'' 

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

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

5935  665 
val assume = gen_assume bind_propp; 
666 
val assume_i = gen_assume bind_propp_i; 

5819  667 

668 

669 
(* fix *) 

670 

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

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

673 

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

675 
ctxt 

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

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

678 
let val x' = variant names x in 

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

680 
end); 

681 

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

683 

684 

685 
val fix = gen_fixs read_skolemT true; 

686 
val fix_i = gen_fixs cert_typ false; 

687 

688 

689 

690 
(** theory setup **) 

691 

692 
val setup = [ProofDataData.init]; 

693 

694 

695 
end; 