added pretty_statement;
authorwenzelm
Tue Mar 14 22:06:36 2006 +0100 (2006-03-14)
changeset 19267fdb4658eab26
parent 19266 2e8ad3f2cd66
child 19268 5a575522fd26
added pretty_statement;
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Tue Mar 14 22:06:35 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Tue Mar 14 22:06:36 2006 +0100
     1.3 @@ -39,6 +39,7 @@
     1.4    val inst_ctxt: theory -> typ Symtab.table * term Symtab.table -> context_i -> context_i
     1.5    val pretty_stmt: ProofContext.context -> statement_i -> Pretty.T list
     1.6    val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list
     1.7 +  val pretty_statement: ProofContext.context -> string -> thm -> Pretty.T
     1.8  end;
     1.9  
    1.10  structure Element: ELEMENT =
    1.11 @@ -229,9 +230,10 @@
    1.12  
    1.13  (** pretty printing **)
    1.14  
    1.15 -fun pretty_items _ _ _ [] = []
    1.16 -  | pretty_items ctxt sep prfx (x :: xs) =
    1.17 -      Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: pretty_items ctxt sep ("  " ^ sep) xs;
    1.18 +fun pretty_items _ _ [] = []
    1.19 +  | pretty_items keyword sep (x :: ys) =
    1.20 +      Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] ::
    1.21 +        map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
    1.22  
    1.23  fun pretty_name_atts ctxt (name, atts) sep =
    1.24    if name = "" andalso null atts then []
    1.25 @@ -245,20 +247,21 @@
    1.26    let
    1.27      val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
    1.28      val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
    1.29 +    val prt_terms = separate (Pretty.keyword "and") o map prt_term;
    1.30      val prt_name_atts = pretty_name_atts ctxt;
    1.31  
    1.32      fun prt_show (a, ts) =
    1.33 -      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
    1.34 +      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
    1.35  
    1.36      fun prt_var (x, SOME T) = Pretty.block [Pretty.str (x ^ " ::"), Pretty.brk 1, prt_typ T]
    1.37        | prt_var (x, NONE) = Pretty.str x;
    1.38  
    1.39 -    fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (map prt_term ts))
    1.40 +    fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
    1.41        | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
    1.42 -          (map prt_var xs @ [Pretty.str "where"] @ map prt_term ts));
    1.43 +          (map prt_var xs @ [Pretty.keyword "where"] @ prt_terms ts));
    1.44    in
    1.45 -    fn Shows shows => pretty_items ctxt "and" "shows" (map prt_show shows)
    1.46 -     | Obtains obtains => pretty_items ctxt "|" "obtains" (map prt_obtain obtains)
    1.47 +    fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
    1.48 +     | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
    1.49    end;
    1.50  
    1.51  
    1.52 @@ -270,11 +273,10 @@
    1.53      val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
    1.54      val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
    1.55      val prt_name_atts = pretty_name_atts ctxt;
    1.56 -    val prt_items = pretty_items ctxt "and";
    1.57  
    1.58 -    fun prt_mixfix mx =
    1.59 -      let val s = Syntax.string_of_mixfix mx
    1.60 -      in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
    1.61 +    fun prt_mixfix NoSyn = []
    1.62 +      | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx];
    1.63 +
    1.64      fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
    1.65            prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
    1.66        | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_mixfix mx);
    1.67 @@ -291,11 +293,69 @@
    1.68      fun prt_note (a, ths) =
    1.69        Pretty.block (Pretty.breaks (List.concat (prt_name_atts a "=" :: map prt_fact ths)));
    1.70    in
    1.71 -    fn Fixes fixes => prt_items "fixes" (map prt_fix fixes)
    1.72 -     | Constrains xs => prt_items "constrains" (map prt_constrain xs)
    1.73 -     | Assumes asms => prt_items "assumes" (map prt_asm asms)
    1.74 -     | Defines defs => prt_items "defines" (map prt_def defs)
    1.75 -     | Notes facts => prt_items "notes" (map prt_note facts)
    1.76 +    fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes)
    1.77 +     | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)
    1.78 +     | Assumes asms => pretty_items "assumes" "and" (map prt_asm asms)
    1.79 +     | Defines defs => pretty_items "defines" "and" (map prt_def defs)
    1.80 +     | Notes facts => pretty_items "notes" "and" (map prt_note facts)
    1.81    end;
    1.82  
    1.83 +
    1.84 +(* pretty_statement *)
    1.85 +
    1.86 +local
    1.87 +
    1.88 +fun thm_name kind th prts =
    1.89 +  let val head =
    1.90 +    (case #1 (Thm.get_name_tags th) of
    1.91 +      "" => Pretty.command kind
    1.92 +    | a => Pretty.block [Pretty.command kind, Pretty.brk 1, Pretty.str (Sign.base_name a ^ ":")])
    1.93 +  in Pretty.block (Pretty.fbreaks (head :: prts)) end;
    1.94 +
    1.95 +fun obtain prop ctxt =
    1.96 +  let
    1.97 +    val xs = ProofContext.rename_frees ctxt [] (Logic.strip_params prop);
    1.98 +    val args = rev (map Free xs);
    1.99 +    val As = Logic.strip_assums_hyp prop |> map (fn t => Term.subst_bounds (args, t));
   1.100 +    val ctxt' = ctxt |> fold ProofContext.declare_term args;
   1.101 +  in (("", (map (apsnd SOME) xs, As)), ctxt') end;
   1.102 +
   1.103 +in
   1.104 +
   1.105 +fun pretty_statement ctxt kind raw_th =
   1.106 +  let
   1.107 +    val thy = ProofContext.theory_of ctxt;
   1.108 +    val th = Goal.norm_hhf raw_th;
   1.109 +    val maxidx = #maxidx (Thm.rep_thm th);
   1.110 +
   1.111 +    fun standard_thesis t =
   1.112 +      let
   1.113 +        val C = ObjectLogic.drop_judgment thy (Thm.concl_of th);
   1.114 +        val C' = Var ((AutoBind.thesisN, maxidx + 1), Term.fastype_of C);
   1.115 +      in Term.subst_atomic [(C, C')] t end;
   1.116 +
   1.117 +    val raw_prop =
   1.118 +      Thm.prop_of th
   1.119 +      |> singleton (ProofContext.monomorphic ctxt)
   1.120 +      |> K (ObjectLogic.is_elim th) ? standard_thesis
   1.121 +      |> Term.zero_var_indexes;
   1.122 +
   1.123 +    val vars = Term.add_vars raw_prop [];
   1.124 +    val frees = ProofContext.rename_frees ctxt [raw_prop] (map (apfst fst) vars);
   1.125 +    val fixes = rev (filter_out (equal AutoBind.thesisN o #1) frees);
   1.126 +
   1.127 +    val prop = Term.instantiate ([], vars ~~ map Free frees) raw_prop;
   1.128 +    val (prems, concl) = Logic.strip_horn prop;
   1.129 +    val thesis = ObjectLogic.fixed_judgment thy AutoBind.thesisN;
   1.130 +    val (asms, cases) = take_suffix (fn prem => thesis aconv Logic.strip_assums_concl prem) prems;
   1.131 +  in
   1.132 +    pretty_ctxt ctxt (Fixes (map (fn (x, T) => (x, SOME T, NoSyn)) fixes)) @
   1.133 +    pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, ([], []))])) asms)) @
   1.134 +    pretty_stmt ctxt
   1.135 +     (if null cases then Shows [(("", []), [(concl, ([], []))])]
   1.136 +      else Obtains (#1 (fold_map obtain cases (ctxt |> ProofContext.declare_term prop))))
   1.137 +  end |> thm_name kind raw_th;
   1.138 +
   1.139  end;
   1.140 +
   1.141 +end;