--- a/src/Pure/Isar/element.ML Tue Mar 14 22:06:35 2006 +0100
+++ b/src/Pure/Isar/element.ML Tue Mar 14 22:06:36 2006 +0100
@@ -39,6 +39,7 @@
val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
val pretty_stmt: ProofContext.context -> statement_i -> Pretty.T list
val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list
+ val pretty_statement: ProofContext.context -> string -> thm -> Pretty.T
end;
structure Element: ELEMENT =
@@ -229,9 +230,10 @@
(** pretty printing **)
-fun pretty_items _ _ _ [] = []
- | pretty_items ctxt sep prfx (x :: xs) =
- Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: pretty_items ctxt sep (" " ^ sep) xs;
+fun pretty_items _ _ [] = []
+ | pretty_items keyword sep (x :: ys) =
+ Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] ::
+ map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
fun pretty_name_atts ctxt (name, atts) sep =
if name = "" andalso null atts then []
@@ -245,20 +247,21 @@
let
val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
+ val prt_terms = separate (Pretty.keyword "and") o map prt_term;
val prt_name_atts = pretty_name_atts ctxt;
fun prt_show (a, ts) =
- Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
+ Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
fun prt_var (x, SOME T) = Pretty.block [Pretty.str (x ^ " ::"), Pretty.brk 1, prt_typ T]
| prt_var (x, NONE) = Pretty.str x;
- fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (map prt_term ts))
+ fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
| prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
- (map prt_var xs @ [Pretty.str "where"] @ map prt_term ts));
+ (map prt_var xs @ [Pretty.keyword "where"] @ prt_terms ts));
in
- fn Shows shows => pretty_items ctxt "and" "shows" (map prt_show shows)
- | Obtains obtains => pretty_items ctxt "|" "obtains" (map prt_obtain obtains)
+ fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
+ | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
end;
@@ -270,11 +273,10 @@
val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
val prt_name_atts = pretty_name_atts ctxt;
- val prt_items = pretty_items ctxt "and";
- fun prt_mixfix mx =
- let val s = Syntax.string_of_mixfix mx
- in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
+ fun prt_mixfix NoSyn = []
+ | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx];
+
fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
| prt_fix (x, NONE, mx) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_mixfix mx);
@@ -291,11 +293,69 @@
fun prt_note (a, ths) =
Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths)));
in
- fn Fixes fixes => prt_items "fixes" (map prt_fix fixes)
- | Constrains xs => prt_items "constrains" (map prt_constrain xs)
- | Assumes asms => prt_items "assumes" (map prt_asm asms)
- | Defines defs => prt_items "defines" (map prt_def defs)
- | Notes facts => prt_items "notes" (map prt_note facts)
+ fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes)
+ | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)
+ | Assumes asms => pretty_items "assumes" "and" (map prt_asm asms)
+ | Defines defs => pretty_items "defines" "and" (map prt_def defs)
+ | Notes facts => pretty_items "notes" "and" (map prt_note facts)
end;
+
+(* pretty_statement *)
+
+local
+
+fun thm_name kind th prts =
+ let val head =
+ (case #1 (Thm.get_name_tags th) of
+ "" => Pretty.command kind
+ | a => Pretty.block [Pretty.command kind, Pretty.brk 1, Pretty.str (Sign.base_name a ^ ":")])
+ in Pretty.block (Pretty.fbreaks (head :: prts)) end;
+
+fun obtain prop ctxt =
+ let
+ val xs = ProofContext.rename_frees ctxt [] (Logic.strip_params prop);
+ val args = rev (map Free xs);
+ val As = Logic.strip_assums_hyp prop |> map (fn t => Term.subst_bounds (args, t));
+ val ctxt' = ctxt |> fold ProofContext.declare_term args;
+ in (("", (map (apsnd SOME) xs, As)), ctxt') end;
+
+in
+
+fun pretty_statement ctxt kind raw_th =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val th = Goal.norm_hhf raw_th;
+ val maxidx = #maxidx (Thm.rep_thm th);
+
+ fun standard_thesis t =
+ let
+ val C = ObjectLogic.drop_judgment thy (Thm.concl_of th);
+ val C' = Var ((AutoBind.thesisN, maxidx + 1), Term.fastype_of C);
+ in Term.subst_atomic [(C, C')] t end;
+
+ val raw_prop =
+ Thm.prop_of th
+ |> singleton (ProofContext.monomorphic ctxt)
+ |> K (ObjectLogic.is_elim th) ? standard_thesis
+ |> Term.zero_var_indexes;
+
+ val vars = Term.add_vars raw_prop [];
+ val frees = ProofContext.rename_frees ctxt [raw_prop] (map (apfst fst) vars);
+ val fixes = rev (filter_out (equal AutoBind.thesisN o #1) frees);
+
+ val prop = Term.instantiate ([], vars ~~ map Free frees) raw_prop;
+ val (prems, concl) = Logic.strip_horn prop;
+ val thesis = ObjectLogic.fixed_judgment thy AutoBind.thesisN;
+ val (asms, cases) = take_suffix (fn prem => thesis aconv Logic.strip_assums_concl prem) prems;
+ in
+ pretty_ctxt ctxt (Fixes (map (fn (x, T) => (x, SOME T, NoSyn)) fixes)) @
+ pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, ([], []))])) asms)) @
+ pretty_stmt ctxt
+ (if null cases then Shows [(("", []), [(concl, ([], []))])]
+ else Obtains (#1 (fold_map obtain cases (ctxt |> ProofContext.declare_term prop))))
+ end |> thm_name kind raw_th;
+
end;
+
+end;