src/Pure/raw_simplifier.ML
changeset 55316 885500f4aa6a
parent 55032 b49366215417
child 55377 d79c057c68f0
     1.1 --- a/src/Pure/raw_simplifier.ML	Tue Feb 04 01:35:48 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Tue Feb 04 09:04:59 2014 +0000
     1.3 @@ -17,6 +17,7 @@
     1.4    val simp_trace: bool Config.T
     1.5    type cong_name = bool * string
     1.6    type rrule
     1.7 +  val mk_rrules: Proof.context -> thm list -> rrule list
     1.8    val eq_rrule: rrule * rrule -> bool
     1.9    type proc
    1.10    type solver
    1.11 @@ -571,6 +572,12 @@
    1.12  fun extract_safe_rrules ctxt thm =
    1.13    maps (orient_rrule ctxt) (extract_rews ctxt [thm]);
    1.14  
    1.15 +fun mk_rrules ctxt thms =
    1.16 +  let
    1.17 +    val rews = extract_rews ctxt thms
    1.18 +    val raw_rrules = flat (map (mk_rrule ctxt) rews)
    1.19 +  in map mk_rrule2 raw_rrules end
    1.20 +
    1.21  
    1.22  (* add/del rules explicitly *)
    1.23  
    1.24 @@ -588,7 +595,6 @@
    1.25  fun add_simp thm ctxt = ctxt addsimps [thm];
    1.26  fun del_simp thm ctxt = ctxt delsimps [thm];
    1.27  
    1.28 -
    1.29  (* congs *)
    1.30  
    1.31  local
    1.32 @@ -814,7 +820,7 @@
    1.33  
    1.34  type trace_ops =
    1.35   {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
    1.36 -  trace_apply: {unconditional: bool, term: term, thm: thm, name: string} ->
    1.37 +  trace_apply: {unconditional: bool, term: term, thm: thm, rrule: rrule} ->
    1.38      Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option};
    1.39  
    1.40  structure Trace_Ops = Theory_Data
    1.41 @@ -919,8 +925,9 @@
    1.42      val eta_thm = Thm.eta_conversion t;
    1.43      val eta_t' = Thm.rhs_of eta_thm;
    1.44      val eta_t = term_of eta_t';
    1.45 -    fun rew {thm, name, lhs, elhs, extra, fo, perm} =
    1.46 +    fun rew rrule =
    1.47        let
    1.48 +        val {thm, name, lhs, elhs, extra, fo, perm} = rrule
    1.49          val prop = Thm.prop_of thm;
    1.50          val (rthm, elhs') =
    1.51            if maxt = ~1 orelse not extra then (thm, elhs)
    1.52 @@ -932,7 +939,7 @@
    1.53          val prop' = Thm.prop_of thm';
    1.54          val unconditional = (Logic.count_prems prop' = 0);
    1.55          val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop');
    1.56 -        val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', name = name};
    1.57 +        val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', rrule = rrule};
    1.58        in
    1.59          if perm andalso not (termless (rhs', lhs'))
    1.60          then