eliminated pointless cterms;
authorwenzelm
Wed Sep 02 23:31:41 2015 +0200 (2015-09-02)
changeset 61098e1b4b24f2ebd
parent 61097 93f08a05abc9
child 61099 64dcd8609962
child 61104 3c2d4636cebc
child 61107 f419f501662c
eliminated pointless cterms;
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Wed Sep 02 23:18:39 2015 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Wed Sep 02 23:31:41 2015 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    val merge_ss: simpset * simpset -> simpset
     1.5    val dest_ss: simpset ->
     1.6     {simps: (string * thm) list,
     1.7 -    procs: (string * cterm list) list,
     1.8 +    procs: (string * term list) list,
     1.9      congs: (cong_name * thm) list,
    1.10      weak_congs: cong_name list,
    1.11      loopers: string list,
    1.12 @@ -222,7 +222,7 @@
    1.13  datatype proc =
    1.14    Proc of
    1.15     {name: string,
    1.16 -    lhs: cterm,
    1.17 +    lhs: term,
    1.18      proc: Proof.context -> cterm -> thm option,
    1.19      id: stamp * thm list};
    1.20  
    1.21 @@ -669,7 +669,7 @@
    1.22  datatype simproc =
    1.23    Simproc of
    1.24      {name: string,
    1.25 -     lhss: cterm list,
    1.26 +     lhss: term list,
    1.27       proc: morphism -> Proof.context -> cterm -> thm option,
    1.28       id: stamp * thm list};
    1.29  
    1.30 @@ -678,12 +678,13 @@
    1.31  fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
    1.32    Simproc
    1.33     {name = name,
    1.34 -    lhss = map (Morphism.cterm phi) lhss,
    1.35 +    lhss = map (Morphism.term phi) lhss,
    1.36      proc = Morphism.transform phi proc,
    1.37      id = (s, Morphism.fact phi ths)};
    1.38  
    1.39  fun make_simproc {name, lhss, proc, identifier} =
    1.40 -  Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)};
    1.41 +  Simproc {name = name, lhss = map Thm.term_of lhss, proc = proc,
    1.42 +    id = (stamp (), map Thm.trim_context identifier)};
    1.43  
    1.44  fun mk_simproc name lhss proc =
    1.45    make_simproc {name = name, lhss = lhss, proc = fn _ => fn ctxt => fn ct =>
    1.46 @@ -698,10 +699,10 @@
    1.47  
    1.48  fun add_proc (proc as Proc {name, lhs, ...}) ctxt =
    1.49   (cond_tracing ctxt (fn () =>
    1.50 -    print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") (Thm.term_of lhs));
    1.51 +    print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") lhs);
    1.52    ctxt |> map_simpset2
    1.53      (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.54 -      (congs, Net.insert_term eq_proc (Thm.term_of lhs, proc) procs,
    1.55 +      (congs, Net.insert_term eq_proc (lhs, proc) procs,
    1.56          mk_rews, termless, subgoal_tac, loop_tacs, solvers))
    1.57    handle Net.INSERT =>
    1.58      (cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name);
    1.59 @@ -710,7 +711,7 @@
    1.60  fun del_proc (proc as Proc {name, lhs, ...}) ctxt =
    1.61    ctxt |> map_simpset2
    1.62      (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.63 -      (congs, Net.delete_term eq_proc (Thm.term_of lhs, proc) procs,
    1.64 +      (congs, Net.delete_term eq_proc (lhs, proc) procs,
    1.65          mk_rews, termless, subgoal_tac, loop_tacs, solvers))
    1.66    handle Net.DELETE =>
    1.67      (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
    1.68 @@ -1006,7 +1007,7 @@
    1.69  
    1.70      fun proc_rews [] = NONE
    1.71        | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
    1.72 -          if Pattern.matches (Proof_Context.theory_of ctxt) (Thm.term_of lhs, Thm.term_of t) then
    1.73 +          if Pattern.matches (Proof_Context.theory_of ctxt) (lhs, Thm.term_of t) then
    1.74              (cond_tracing' ctxt simp_debug (fn () =>
    1.75                print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
    1.76               (case proc ctxt eta_t' of
     2.1 --- a/src/Pure/simplifier.ML	Wed Sep 02 23:18:39 2015 +0200
     2.2 +++ b/src/Pure/simplifier.ML	Wed Sep 02 23:31:41 2015 +0200
     2.3 @@ -167,7 +167,7 @@
     2.4      fun pretty_simproc (name, lhss) =
     2.5        Pretty.block
     2.6          (Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk ::
     2.7 -          Pretty.fbreaks (map (Pretty.item o single o pretty_term o Thm.term_of) lhss));
     2.8 +          Pretty.fbreaks (map (Pretty.item o single o pretty_term) lhss));
     2.9  
    2.10      fun pretty_cong_name (const, name) =
    2.11        pretty_term ((if const then Const else Free) (name, dummyT));