37 val inst_term: typ Symtab.table * term Symtab.table -> term -> term |
37 val inst_term: typ Symtab.table * term Symtab.table -> term -> term |
38 val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm |
38 val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm |
39 val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i |
39 val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i |
40 val pretty_stmt: ProofContext.context -> statement_i -> Pretty.T list |
40 val pretty_stmt: ProofContext.context -> statement_i -> Pretty.T list |
41 val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list |
41 val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list |
|
42 val pretty_statement: ProofContext.context -> string -> thm -> Pretty.T |
42 end; |
43 end; |
43 |
44 |
44 structure Element: ELEMENT = |
45 structure Element: ELEMENT = |
45 struct |
46 struct |
46 |
47 |
227 |
228 |
228 |
229 |
229 |
230 |
230 (** pretty printing **) |
231 (** pretty printing **) |
231 |
232 |
232 fun pretty_items _ _ _ [] = [] |
233 fun pretty_items _ _ [] = [] |
233 | pretty_items ctxt sep prfx (x :: xs) = |
234 | pretty_items keyword sep (x :: ys) = |
234 Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: pretty_items ctxt sep (" " ^ sep) xs; |
235 Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] :: |
|
236 map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword sep, Pretty.brk 1, y]) ys; |
235 |
237 |
236 fun pretty_name_atts ctxt (name, atts) sep = |
238 fun pretty_name_atts ctxt (name, atts) sep = |
237 if name = "" andalso null atts then [] |
239 if name = "" andalso null atts then [] |
238 else [Pretty.block (Pretty.breaks (Pretty.str (ProofContext.extern_thm ctxt name) :: |
240 else [Pretty.block (Pretty.breaks (Pretty.str (ProofContext.extern_thm ctxt name) :: |
239 Args.pretty_attribs ctxt atts @ [Pretty.str sep]))]; |
241 Args.pretty_attribs ctxt atts @ [Pretty.str sep]))]; |
243 |
245 |
244 fun pretty_stmt ctxt = |
246 fun pretty_stmt ctxt = |
245 let |
247 let |
246 val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; |
248 val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; |
247 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
249 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
|
250 val prt_terms = separate (Pretty.keyword "and") o map prt_term; |
248 val prt_name_atts = pretty_name_atts ctxt; |
251 val prt_name_atts = pretty_name_atts ctxt; |
249 |
252 |
250 fun prt_show (a, ts) = |
253 fun prt_show (a, ts) = |
251 Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts)); |
254 Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts))); |
252 |
255 |
253 fun prt_var (x, SOME T) = Pretty.block [Pretty.str (x ^ " ::"), Pretty.brk 1, prt_typ T] |
256 fun prt_var (x, SOME T) = Pretty.block [Pretty.str (x ^ " ::"), Pretty.brk 1, prt_typ T] |
254 | prt_var (x, NONE) = Pretty.str x; |
257 | prt_var (x, NONE) = Pretty.str x; |
255 |
258 |
256 fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (map prt_term ts)) |
259 fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts)) |
257 | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks |
260 | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks |
258 (map prt_var xs @ [Pretty.str "where"] @ map prt_term ts)); |
261 (map prt_var xs @ [Pretty.keyword "where"] @ prt_terms ts)); |
259 in |
262 in |
260 fn Shows shows => pretty_items ctxt "and" "shows" (map prt_show shows) |
263 fn Shows shows => pretty_items "shows" "and" (map prt_show shows) |
261 | Obtains obtains => pretty_items ctxt "|" "obtains" (map prt_obtain obtains) |
264 | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains) |
262 end; |
265 end; |
263 |
266 |
264 |
267 |
265 (* pretty_ctxt *) |
268 (* pretty_ctxt *) |
266 |
269 |
268 let |
271 let |
269 val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; |
272 val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt; |
270 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
273 val prt_term = Pretty.quote o ProofContext.pretty_term ctxt; |
271 val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt; |
274 val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt; |
272 val prt_name_atts = pretty_name_atts ctxt; |
275 val prt_name_atts = pretty_name_atts ctxt; |
273 val prt_items = pretty_items ctxt "and"; |
276 |
274 |
277 fun prt_mixfix NoSyn = [] |
275 fun prt_mixfix mx = |
278 | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx]; |
276 let val s = Syntax.string_of_mixfix mx |
279 |
277 in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end; |
|
278 fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: |
280 fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 :: |
279 prt_typ T :: Pretty.brk 1 :: prt_mixfix mx) |
281 prt_typ T :: Pretty.brk 1 :: prt_mixfix mx) |
280 | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_mixfix mx); |
282 | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_mixfix mx); |
281 fun prt_constrain (x, T) = prt_fix (x, SOME T, NoSyn); |
283 fun prt_constrain (x, T) = prt_fix (x, SOME T, NoSyn); |
282 |
284 |
289 | prt_fact (ths, atts) = Pretty.enclose "(" ")" |
291 | prt_fact (ths, atts) = Pretty.enclose "(" ")" |
290 (Pretty.breaks (map prt_thm ths)) :: Args.pretty_attribs ctxt atts; |
292 (Pretty.breaks (map prt_thm ths)) :: Args.pretty_attribs ctxt atts; |
291 fun prt_note (a, ths) = |
293 fun prt_note (a, ths) = |
292 Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths))); |
294 Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths))); |
293 in |
295 in |
294 fn Fixes fixes => prt_items "fixes" (map prt_fix fixes) |
296 fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes) |
295 | Constrains xs => prt_items "constrains" (map prt_constrain xs) |
297 | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs) |
296 | Assumes asms => prt_items "assumes" (map prt_asm asms) |
298 | Assumes asms => pretty_items "assumes" "and" (map prt_asm asms) |
297 | Defines defs => prt_items "defines" (map prt_def defs) |
299 | Defines defs => pretty_items "defines" "and" (map prt_def defs) |
298 | Notes facts => prt_items "notes" (map prt_note facts) |
300 | Notes facts => pretty_items "notes" "and" (map prt_note facts) |
299 end; |
301 end; |
|
302 |
|
303 |
|
304 (* pretty_statement *) |
|
305 |
|
306 local |
|
307 |
|
308 fun thm_name kind th prts = |
|
309 let val head = |
|
310 (case #1 (Thm.get_name_tags th) of |
|
311 "" => Pretty.command kind |
|
312 | a => Pretty.block [Pretty.command kind, Pretty.brk 1, Pretty.str (Sign.base_name a ^ ":")]) |
|
313 in Pretty.block (Pretty.fbreaks (head :: prts)) end; |
|
314 |
|
315 fun obtain prop ctxt = |
|
316 let |
|
317 val xs = ProofContext.rename_frees ctxt [] (Logic.strip_params prop); |
|
318 val args = rev (map Free xs); |
|
319 val As = Logic.strip_assums_hyp prop |> map (fn t => Term.subst_bounds (args, t)); |
|
320 val ctxt' = ctxt |> fold ProofContext.declare_term args; |
|
321 in (("", (map (apsnd SOME) xs, As)), ctxt') end; |
|
322 |
|
323 in |
|
324 |
|
325 fun pretty_statement ctxt kind raw_th = |
|
326 let |
|
327 val thy = ProofContext.theory_of ctxt; |
|
328 val th = Goal.norm_hhf raw_th; |
|
329 val maxidx = #maxidx (Thm.rep_thm th); |
|
330 |
|
331 fun standard_thesis t = |
|
332 let |
|
333 val C = ObjectLogic.drop_judgment thy (Thm.concl_of th); |
|
334 val C' = Var ((AutoBind.thesisN, maxidx + 1), Term.fastype_of C); |
|
335 in Term.subst_atomic [(C, C')] t end; |
|
336 |
|
337 val raw_prop = |
|
338 Thm.prop_of th |
|
339 |> singleton (ProofContext.monomorphic ctxt) |
|
340 |> K (ObjectLogic.is_elim th) ? standard_thesis |
|
341 |> Term.zero_var_indexes; |
|
342 |
|
343 val vars = Term.add_vars raw_prop []; |
|
344 val frees = ProofContext.rename_frees ctxt [raw_prop] (map (apfst fst) vars); |
|
345 val fixes = rev (filter_out (equal AutoBind.thesisN o #1) frees); |
|
346 |
|
347 val prop = Term.instantiate ([], vars ~~ map Free frees) raw_prop; |
|
348 val (prems, concl) = Logic.strip_horn prop; |
|
349 val thesis = ObjectLogic.fixed_judgment thy AutoBind.thesisN; |
|
350 val (asms, cases) = take_suffix (fn prem => thesis aconv Logic.strip_assums_concl prem) prems; |
|
351 in |
|
352 pretty_ctxt ctxt (Fixes (map (fn (x, T) => (x, SOME T, NoSyn)) fixes)) @ |
|
353 pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, ([], []))])) asms)) @ |
|
354 pretty_stmt ctxt |
|
355 (if null cases then Shows [(("", []), [(concl, ([], []))])] |
|
356 else Obtains (#1 (fold_map obtain cases (ctxt |> ProofContext.declare_term prop)))) |
|
357 end |> thm_name kind raw_th; |
300 |
358 |
301 end; |
359 end; |
|
360 |
|
361 end; |