1.1 --- a/src/Pure/simplifier.ML	Thu Apr 10 12:00:25 2014 +0200
     1.2 +++ b/src/Pure/simplifier.ML	Thu Apr 10 12:22:29 2014 +0200
     1.3 @@ -29,6 +29,19 @@
     1.4  sig
     1.5    include BASIC_SIMPLIFIER
     1.6    val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic
     1.7 +  val attrib: (thm -> Proof.context -> Proof.context) -> attribute
     1.8 +  val simp_add: attribute
     1.9 +  val simp_del: attribute
    1.10 +  val cong_add: attribute
    1.11 +  val cong_del: attribute
    1.12 +  val check_simproc: Proof.context -> xstring * Position.T -> string
    1.13 +  val the_simproc: Proof.context -> string -> simproc
    1.14 +  val def_simproc: {name: binding, lhss: term list,
    1.15 +    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
    1.16 +    local_theory -> local_theory
    1.17 +  val def_simproc_cmd: {name: binding, lhss: string list,
    1.18 +    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
    1.19 +    local_theory -> local_theory
    1.20    val pretty_simpset: Proof.context -> Pretty.T
    1.21    val default_mk_sym: Proof.context -> thm -> thm option
    1.22    val prems_of: Proof.context -> thm list
    1.23 @@ -57,19 +70,6 @@
    1.24    val full_rewrite: Proof.context -> conv
    1.25    val asm_lr_rewrite: Proof.context -> conv
    1.26    val asm_full_rewrite: Proof.context -> conv
    1.27 -  val attrib: (thm -> Proof.context -> Proof.context) -> attribute
    1.28 -  val simp_add: attribute
    1.29 -  val simp_del: attribute
    1.30 -  val cong_add: attribute
    1.31 -  val cong_del: attribute
    1.32 -  val check_simproc: Proof.context -> xstring * Position.T -> string
    1.33 -  val the_simproc: Proof.context -> string -> simproc
    1.34 -  val def_simproc: {name: binding, lhss: term list,
    1.35 -    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
    1.36 -    local_theory -> local_theory
    1.37 -  val def_simproc_cmd: {name: binding, lhss: string list,
    1.38 -    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
    1.39 -    local_theory -> local_theory
    1.40    val cong_modifiers: Method.modifier parser list
    1.41    val simp_modifiers': Method.modifier parser list
    1.42    val simp_modifiers: Method.modifier parser list
    1.43 @@ -83,36 +83,6 @@
    1.44  open Raw_Simplifier;
    1.45  
    1.46  
    1.47 -(** pretty printing **)
    1.48 -
    1.49 -fun pretty_simpset ctxt =
    1.50 -  let
    1.51 -    val pretty_term = Syntax.pretty_term ctxt;
    1.52 -    val pretty_thm = Display.pretty_thm ctxt;
    1.53 -    val pretty_thm_item = Display.pretty_thm_item ctxt;
    1.54 -
    1.55 -    fun pretty_proc (name, lhss) =
    1.56 -      Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_term o Thm.term_of) lhss);
    1.57 -
    1.58 -    fun pretty_cong_name (const, name) =
    1.59 -      pretty_term ((if const then Const else Free) (name, dummyT));
    1.60 -    fun pretty_cong (name, thm) =
    1.61 -      Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
    1.62 -
    1.63 -    val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
    1.64 -      dest_ss (simpset_of ctxt);
    1.65 -  in
    1.66 -    [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
    1.67 -      Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
    1.68 -      Pretty.big_list "congruences:" (map pretty_cong congs),
    1.69 -      Pretty.strs ("loopers:" :: map quote loopers),
    1.70 -      Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
    1.71 -      Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
    1.72 -    |> Pretty.chunks
    1.73 -  end;
    1.74 -
    1.75 -
    1.76 -
    1.77  (** declarations **)
    1.78  
    1.79  (* attributes *)
    1.80 @@ -187,6 +157,40 @@
    1.81  
    1.82  
    1.83  
    1.84 +(** pretty_simpset **)
    1.85 +
    1.86 +fun pretty_simpset ctxt =
    1.87 +  let
    1.88 +    val pretty_term = Syntax.pretty_term ctxt;
    1.89 +    val pretty_thm = Display.pretty_thm ctxt;
    1.90 +    val pretty_thm_item = Display.pretty_thm_item ctxt;
    1.91 +
    1.92 +    fun pretty_simproc (name, lhss) =
    1.93 +      Pretty.block
    1.94 +        (Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk ::
    1.95 +          Pretty.fbreaks (map (Pretty.item o single o pretty_term o Thm.term_of) lhss));
    1.96 +
    1.97 +    fun pretty_cong_name (const, name) =
    1.98 +      pretty_term ((if const then Const else Free) (name, dummyT));
    1.99 +    fun pretty_cong (name, thm) =
   1.100 +      Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
   1.101 +
   1.102 +    val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} =
   1.103 +      dest_ss (simpset_of ctxt);
   1.104 +    val simprocs =
   1.105 +      Name_Space.markup_entries ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs;
   1.106 +  in
   1.107 +    [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
   1.108 +      Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs),
   1.109 +      Pretty.big_list "congruences:" (map pretty_cong congs),
   1.110 +      Pretty.strs ("loopers:" :: map quote loopers),
   1.111 +      Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers),
   1.112 +      Pretty.strs ("safe solvers:" :: map quote safe_solvers)]
   1.113 +    |> Pretty.chunks
   1.114 +  end;
   1.115 +
   1.116 +
   1.117 +
   1.118  (** simplification tactics and rules **)
   1.119  
   1.120  fun solve_all_tac solvers ctxt =