simplified simproc programming interfaces;
authorwenzelm
Wed Sep 09 20:57:21 2015 +0200 (2015-09-09)
changeset 611445e94dfead1c2
parent 61143 5f898411ce87
child 61145 497eb43a3064
simplified simproc programming interfaces;
NEWS
src/HOL/Decision_Procs/langford.ML
src/HOL/HOL.thy
src/HOL/HOLCF/Tools/cont_proc.ML
src/HOL/Int.thy
src/HOL/Library/Old_SMT/old_smt_real.ML
src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
src/HOL/NSA/HyperDef.thy
src/HOL/Nat.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Product_Type.thy
src/HOL/Rat.thy
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/z3_replay_util.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/record.ML
src/HOL/Word/WordBitwise.thy
src/Provers/Arith/cancel_numeral_factor.ML
src/Provers/Arith/cancel_numerals.ML
src/Provers/Arith/combine_numerals.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
src/Tools/induct.ML
src/ZF/Datatype_ZF.thy
src/ZF/arith_data.ML
src/ZF/int_arith.ML
     1.1 --- a/NEWS	Wed Sep 09 14:47:41 2015 +0200
     1.2 +++ b/NEWS	Wed Sep 09 20:57:21 2015 +0200
     1.3 @@ -315,6 +315,12 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Simproc programming interfaces have been simplified:
     1.8 +Simplifier.make_simproc and Simplifier.define_simproc supersede various
     1.9 +forms of Simplifier.mk_simproc, Simplifier.simproc_global etc. Note that
    1.10 +term patterns for the left-hand sides are specified with implicitly
    1.11 +fixed variables, like top-level theorem statements. INCOMPATIBILITY.
    1.12 +
    1.13  * Instantiation rules have been re-organized as follows:
    1.14  
    1.15    Thm.instantiate  (*low-level instantiation with named arguments*)
     2.1 --- a/src/HOL/Decision_Procs/langford.ML	Wed Sep 09 14:47:41 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/langford.ML	Wed Sep 09 20:57:21 2015 +0200
     2.3 @@ -170,11 +170,8 @@
     2.4  in
     2.5  
     2.6  val reduce_ex_simproc =
     2.7 -  Simplifier.make_simproc
     2.8 -    {lhss = [@{cpat "\<exists>x. ?P x"}],
     2.9 -     name = "reduce_ex_simproc",
    2.10 -     proc = K proc,
    2.11 -     identifier = []};
    2.12 +  Simplifier.make_simproc @{context} "reduce_ex_simproc"
    2.13 +    {lhss = [@{term "\<exists>x. P x"}], proc = K proc, identifier = []};
    2.14  
    2.15  end;
    2.16  
     3.1 --- a/src/HOL/HOL.thy	Wed Sep 09 14:47:41 2015 +0200
     3.2 +++ b/src/HOL/HOL.thy	Wed Sep 09 20:57:21 2015 +0200
     3.3 @@ -1446,25 +1446,29 @@
     3.4  declaration \<open>
     3.5    fn _ => Induct.map_simpset (fn ss => ss
     3.6      addsimprocs
     3.7 -      [Simplifier.simproc_global @{theory} "swap_induct_false"
     3.8 -         ["induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"]
     3.9 -         (fn _ =>
    3.10 -            (fn _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
    3.11 -                  if P <> Q then SOME Drule.swap_prems_eq else NONE
    3.12 -              | _ => NONE)),
    3.13 -       Simplifier.simproc_global @{theory} "induct_equal_conj_curry"
    3.14 -         ["induct_conj P Q \<Longrightarrow> PROP R"]
    3.15 -         (fn _ =>
    3.16 -            (fn _ $ (_ $ P) $ _ =>
    3.17 -                let
    3.18 -                  fun is_conj (@{const induct_conj} $ P $ Q) =
    3.19 -                        is_conj P andalso is_conj Q
    3.20 -                    | is_conj (Const (@{const_name induct_equal}, _) $ _ $ _) = true
    3.21 -                    | is_conj @{const induct_true} = true
    3.22 -                    | is_conj @{const induct_false} = true
    3.23 -                    | is_conj _ = false
    3.24 -                in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
    3.25 -              | _ => NONE))]
    3.26 +      [Simplifier.make_simproc @{context} "swap_induct_false"
    3.27 +        {lhss = [@{term "induct_false \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"}],
    3.28 +         proc = fn _ => fn _ => fn ct =>
    3.29 +          (case Thm.term_of ct of
    3.30 +            _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
    3.31 +              if P <> Q then SOME Drule.swap_prems_eq else NONE
    3.32 +          | _ => NONE),
    3.33 +         identifier = []},
    3.34 +       Simplifier.make_simproc @{context} "induct_equal_conj_curry"
    3.35 +        {lhss = [@{term "induct_conj P Q \<Longrightarrow> PROP R"}],
    3.36 +         proc = fn _ => fn _ => fn ct =>
    3.37 +          (case Thm.term_of ct of
    3.38 +            _ $ (_ $ P) $ _ =>
    3.39 +              let
    3.40 +                fun is_conj (@{const induct_conj} $ P $ Q) =
    3.41 +                      is_conj P andalso is_conj Q
    3.42 +                  | is_conj (Const (@{const_name induct_equal}, _) $ _ $ _) = true
    3.43 +                  | is_conj @{const induct_true} = true
    3.44 +                  | is_conj @{const induct_false} = true
    3.45 +                  | is_conj _ = false
    3.46 +              in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
    3.47 +            | _ => NONE),
    3.48 +          identifier = []}]
    3.49      |> Simplifier.set_mksimps (fn ctxt =>
    3.50          Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
    3.51          map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
    3.52 @@ -1731,8 +1735,14 @@
    3.53  
    3.54  setup \<open>
    3.55    Code_Preproc.map_pre (fn ctxt =>
    3.56 -    ctxt addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
    3.57 -      (fn _ => fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)])
    3.58 +    ctxt addsimprocs
    3.59 +      [Simplifier.make_simproc @{context} "equal"
    3.60 +        {lhss = [@{term HOL.eq}],
    3.61 +         proc = fn _ => fn _ => fn ct =>
    3.62 +          (case Thm.term_of ct of
    3.63 +            Const (_, Type (@{type_name fun}, [Type _, _])) => SOME @{thm eq_equal}
    3.64 +          | _ => NONE),
    3.65 +         identifier = []}])
    3.66  \<close>
    3.67  
    3.68  
     4.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Wed Sep 09 14:47:41 2015 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Wed Sep 09 20:57:21 2015 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4    val cont_thms: term -> thm list
     4.5    val all_cont_thms: term -> thm list
     4.6    val cont_tac: Proof.context -> int -> tactic
     4.7 -  val cont_proc: theory -> simproc
     4.8 +  val cont_proc: simproc
     4.9    val setup: theory -> theory
    4.10  end
    4.11  
    4.12 @@ -119,15 +119,17 @@
    4.13    end
    4.14  
    4.15  local
    4.16 -  fun solve_cont ctxt t =
    4.17 +  fun solve_cont ctxt ct =
    4.18      let
    4.19 +      val t = Thm.term_of ct
    4.20        val tr = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
    4.21      in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end
    4.22  in
    4.23 -  fun cont_proc thy =
    4.24 -    Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont
    4.25 +  val cont_proc =
    4.26 +    Simplifier.make_simproc @{context} "cont_proc"
    4.27 +     {lhss = [@{term "cont f"}], proc = K solve_cont, identifier = []}
    4.28  end
    4.29  
    4.30 -fun setup thy = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc thy]) thy
    4.31 +val setup = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc])
    4.32  
    4.33  end
     5.1 --- a/src/HOL/Int.thy	Wed Sep 09 14:47:41 2015 +0200
     5.2 +++ b/src/HOL/Int.thy	Wed Sep 09 20:57:21 2015 +0200
     5.3 @@ -775,9 +775,9 @@
     5.4  declaration \<open>K Int_Arith.setup\<close>
     5.5  
     5.6  simproc_setup fast_arith ("(m::'a::linordered_idom) < n" |
     5.7 -  "(m::'a::linordered_idom) <= n" |
     5.8 +  "(m::'a::linordered_idom) \<le> n" |
     5.9    "(m::'a::linordered_idom) = n") =
    5.10 -  \<open>fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct)\<close>
    5.11 +  \<open>K Lin_Arith.simproc\<close>
    5.12  
    5.13  
    5.14  subsection\<open>More Inequality Reasoning\<close>
     6.1 --- a/src/HOL/Library/Old_SMT/old_smt_real.ML	Wed Sep 09 14:47:41 2015 +0200
     6.2 +++ b/src/HOL/Library/Old_SMT/old_smt_real.ML	Wed Sep 09 20:57:21 2015 +0200
     6.3 @@ -114,8 +114,10 @@
     6.4    "x + y = y + x"
     6.5    by auto}
     6.6  
     6.7 -val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
     6.8 -  "(m::real) < n", "(m::real) <= n", "(m::real) = n"] Lin_Arith.simproc
     6.9 +val real_linarith_proc =
    6.10 +  Simplifier.make_simproc @{context} "fast_real_arith"
    6.11 +   {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \<le> n"}, @{term "(m::real) = n"}],
    6.12 +    proc = K Lin_Arith.simproc, identifier = []}
    6.13  
    6.14  
    6.15  (* setup *)
     7.1 --- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Wed Sep 09 14:47:41 2015 +0200
     7.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML	Wed Sep 09 20:57:21 2015 +0200
     7.3 @@ -304,9 +304,9 @@
     7.4    fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
     7.5      | dest_binop t = raise TERM ("dest_binop", [t])
     7.6  
     7.7 -  fun prove_antisym_le ctxt t =
     7.8 +  fun prove_antisym_le ctxt ct =
     7.9      let
    7.10 -      val (le, r, s) = dest_binop t
    7.11 +      val (le, r, s) = dest_binop (Thm.term_of ct)
    7.12        val less = Const (@{const_name less}, Term.fastype_of le)
    7.13        val prems = Simplifier.prems_of ctxt
    7.14      in
    7.15 @@ -318,9 +318,9 @@
    7.16      end
    7.17      handle THM _ => NONE
    7.18  
    7.19 -  fun prove_antisym_less ctxt t =
    7.20 +  fun prove_antisym_less ctxt ct =
    7.21      let
    7.22 -      val (less, r, s) = dest_binop (HOLogic.dest_not t)
    7.23 +      val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct))
    7.24        val le = Const (@{const_name less_eq}, Term.fastype_of less)
    7.25        val prems = Simplifier.prems_of ctxt
    7.26      in
    7.27 @@ -343,12 +343,15 @@
    7.28        addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
    7.29        addsimprocs [@{simproc numeral_divmod}]
    7.30        addsimprocs [
    7.31 -        Simplifier.simproc_global @{theory} "fast_int_arith" [
    7.32 -          "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc,
    7.33 -        Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"]
    7.34 -          prove_antisym_le,
    7.35 -        Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
    7.36 -          prove_antisym_less])
    7.37 +        Simplifier.make_simproc @{context} "fast_int_arith"
    7.38 +         {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
    7.39 +          proc = K Lin_Arith.simproc, identifier = []},
    7.40 +        Simplifier.make_simproc @{context} "antisym_le"
    7.41 +         {lhss = [@{term "(x::'a::order) \<le> y"}],
    7.42 +          proc = K prove_antisym_le, identifier = []},
    7.43 +        Simplifier.make_simproc @{context} "antisym_less"
    7.44 +         {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
    7.45 +          proc = K prove_antisym_less, identifier = []}])
    7.46  
    7.47    structure Simpset = Generic_Data
    7.48    (
     8.1 --- a/src/HOL/NSA/HyperDef.thy	Wed Sep 09 14:47:41 2015 +0200
     8.2 +++ b/src/HOL/NSA/HyperDef.thy	Wed Sep 09 20:57:21 2015 +0200
     8.3 @@ -337,7 +337,7 @@
     8.4  *}
     8.5  
     8.6  simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = n") =
     8.7 -  {* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct) *}
     8.8 +  {* K Lin_Arith.simproc *}
     8.9  
    8.10  
    8.11  subsection {* Exponentials on the Hyperreals *}
     9.1 --- a/src/HOL/Nat.thy	Wed Sep 09 14:47:41 2015 +0200
     9.2 +++ b/src/HOL/Nat.thy	Wed Sep 09 20:57:21 2015 +0200
     9.3 @@ -1664,8 +1664,8 @@
     9.4  setup \<open>Lin_Arith.global_setup\<close>
     9.5  declaration \<open>K Lin_Arith.setup\<close>
     9.6  
     9.7 -simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) <= n" | "(m::nat) = n") =
     9.8 -  \<open>fn _ => fn ss => fn ct => Lin_Arith.simproc ss (Thm.term_of ct)\<close>
     9.9 +simproc_setup fast_arith_nat ("(m::nat) < n" | "(m::nat) \<le> n" | "(m::nat) = n") =
    9.10 +  \<open>K Lin_Arith.simproc\<close>
    9.11  (* Because of this simproc, the arithmetic solver is really only
    9.12  useful to detect inconsistencies among the premises for subgoals which are
    9.13  *not* themselves (in)equalities, because the latter activate
    10.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Sep 09 14:47:41 2015 +0200
    10.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Sep 09 20:57:21 2015 +0200
    10.3 @@ -98,12 +98,15 @@
    10.4  fun permTs_of (Const (@{const_name Nominal.perm}, T) $ t $ u) = fst (dest_permT T) :: permTs_of u
    10.5    | permTs_of _ = [];
    10.6  
    10.7 -fun perm_simproc' ctxt (Const (@{const_name Nominal.perm}, T) $ t $ (u as Const (@{const_name Nominal.perm}, U) $ r $ s)) =
    10.8 +fun perm_simproc' ctxt ct =
    10.9 +  (case Thm.term_of ct of
   10.10 +    Const (@{const_name Nominal.perm}, T) $ t $ (u as Const (@{const_name Nominal.perm}, U) $ r $ s) =>
   10.11        let
   10.12          val thy = Proof_Context.theory_of ctxt;
   10.13          val (aT as Type (a, []), S) = dest_permT T;
   10.14          val (bT as Type (b, []), _) = dest_permT U;
   10.15 -      in if member (op =) (permTs_of u) aT andalso aT <> bT then
   10.16 +      in
   10.17 +        if member (op =) (permTs_of u) aT andalso aT <> bT then
   10.18            let
   10.19              val cp = cp_inst_of thy a b;
   10.20              val dj = dj_thm_of thy b a;
   10.21 @@ -115,10 +118,11 @@
   10.22            end
   10.23          else NONE
   10.24        end
   10.25 -  | perm_simproc' _ _ = NONE;
   10.26 +  | _ => NONE);
   10.27  
   10.28  val perm_simproc =
   10.29 -  Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
   10.30 +  Simplifier.make_simproc @{context} "perm_simp"
   10.31 +   {lhss = [@{term "pi1 \<bullet> (pi2 \<bullet> x)"}], proc = K perm_simproc', identifier = []};
   10.32  
   10.33  fun projections ctxt rule =
   10.34    Project_Rule.projections ctxt rule
    11.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Sep 09 14:47:41 2015 +0200
    11.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Sep 09 20:57:21 2015 +0200
    11.3 @@ -40,11 +40,15 @@
    11.4    th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
    11.5  
    11.6  fun mk_perm_bool_simproc names =
    11.7 -  Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
    11.8 -    fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
    11.9 -         if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
   11.10 -         then SOME perm_bool else NONE
   11.11 -     | _ => NONE);
   11.12 +  Simplifier.make_simproc @{context} "perm_bool"
   11.13 +   {lhss = [@{term "perm pi x"}],
   11.14 +    proc = fn _ => fn _ => fn ct =>
   11.15 +      (case Thm.term_of ct of
   11.16 +        Const (@{const_name Nominal.perm}, _) $ _ $ t =>
   11.17 +          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
   11.18 +          then SOME perm_bool else NONE
   11.19 +      | _ => NONE),
   11.20 +    identifier = []};
   11.21  
   11.22  fun transp ([] :: _) = []
   11.23    | transp xs = map hd xs :: transp (map tl xs);
    12.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Sep 09 14:47:41 2015 +0200
    12.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Sep 09 20:57:21 2015 +0200
    12.3 @@ -44,11 +44,15 @@
    12.4    th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI;
    12.5  
    12.6  fun mk_perm_bool_simproc names =
    12.7 -  Simplifier.simproc_global_i @{theory} "perm_bool" [@{term "perm pi x"}] (fn ctxt =>
    12.8 -    fn Const (@{const_name Nominal.perm}, _) $ _ $ t =>
    12.9 -         if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
   12.10 -         then SOME perm_bool else NONE
   12.11 -     | _ => NONE);
   12.12 +  Simplifier.make_simproc @{context} "perm_bool"
   12.13 +   {lhss = [@{term "perm pi x"}],
   12.14 +    proc = fn _ => fn _ => fn ct =>
   12.15 +      (case Thm.term_of ct of
   12.16 +        Const (@{const_name Nominal.perm}, _) $ _ $ t =>
   12.17 +          if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
   12.18 +          then SOME perm_bool else NONE
   12.19 +       | _ => NONE),
   12.20 +    identifier = []};
   12.21  
   12.22  fun transp ([] :: _) = []
   12.23    | transp xs = map hd xs :: transp (map tl xs);
    13.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Sep 09 14:47:41 2015 +0200
    13.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Sep 09 20:57:21 2015 +0200
    13.3 @@ -3,7 +3,7 @@
    13.4      Author:     Julien Narboux, TU Muenchen
    13.5  
    13.6  Methods for simplifying permutations and for analysing equations
    13.7 -involving permutations. 
    13.8 +involving permutations.
    13.9  *)
   13.10  
   13.11  (*
   13.12 @@ -18,8 +18,8 @@
   13.13  
   13.14        [(a,b)] o pi1 o pi2 = ....
   13.15  
   13.16 -   rather it tries to permute pi1 over pi2, which 
   13.17 -   results in a failure when used with the 
   13.18 +   rather it tries to permute pi1 over pi2, which
   13.19 +   results in a failure when used with the
   13.20     perm_(full)_simp tactics
   13.21  
   13.22  *)
   13.23 @@ -67,7 +67,7 @@
   13.24  val supp_unit     = @{thm "supp_unit"};
   13.25  val pt_perm_compose_aux = @{thm "pt_perm_compose_aux"};
   13.26  val cp1_aux             = @{thm "cp1_aux"};
   13.27 -val perm_aux_fold       = @{thm "perm_aux_fold"}; 
   13.28 +val perm_aux_fold       = @{thm "perm_aux_fold"};
   13.29  val supports_fresh_rule = @{thm "supports_fresh"};
   13.30  
   13.31  (* needed in the process of fully simplifying permutations *)
   13.32 @@ -76,31 +76,32 @@
   13.33  val weak_congs   = [@{thm "if_weak_cong"}]
   13.34  
   13.35  (* debugging *)
   13.36 -fun DEBUG ctxt (msg,tac) = 
   13.37 -    CHANGED (EVERY [print_tac ctxt ("before "^msg), tac, print_tac ctxt ("after "^msg)]); 
   13.38 -fun NO_DEBUG _ (_,tac) = CHANGED tac; 
   13.39 +fun DEBUG ctxt (msg,tac) =
   13.40 +    CHANGED (EVERY [print_tac ctxt ("before "^msg), tac, print_tac ctxt ("after "^msg)]);
   13.41 +fun NO_DEBUG _ (_,tac) = CHANGED tac;
   13.42  
   13.43  
   13.44  (* simproc that deals with instances of permutations in front *)
   13.45  (* of applications; just adding this rule to the simplifier   *)
   13.46  (* would loop; it also needs careful tuning with the simproc  *)
   13.47  (* for functions to avoid further possibilities for looping   *)
   13.48 -fun perm_simproc_app' ctxt redex =
   13.49 -  let 
   13.50 -    val thy = Proof_Context.theory_of ctxt;
   13.51 +fun perm_simproc_app' ctxt ct =
   13.52 +  let
   13.53 +    val thy = Proof_Context.theory_of ctxt
   13.54 +    val redex = Thm.term_of ct
   13.55      (* the "application" case is only applicable when the head of f is not a *)
   13.56      (* constant or when (f x) is a permuation with two or more arguments     *)
   13.57 -    fun applicable_app t = 
   13.58 +    fun applicable_app t =
   13.59            (case (strip_comb t) of
   13.60                (Const (@{const_name Nominal.perm},_),ts) => (length ts) >= 2
   13.61              | (Const _,_) => false
   13.62              | _ => true)
   13.63    in
   13.64 -    case redex of 
   13.65 +    case redex of
   13.66          (* case pi o (f x) == (pi o f) (pi o x)          *)
   13.67          (Const(@{const_name Nominal.perm},
   13.68            Type(@{type_name fun},
   13.69 -            [Type(@{type_name list}, [Type(@{type_name prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
   13.70 +            [Type(@{type_name list}, [Type(@{type_name prod},[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
   13.71              (if (applicable_app f) then
   13.72                let
   13.73                  val name = Long_Name.base_name n
   13.74 @@ -111,12 +112,14 @@
   13.75        | _ => NONE
   13.76    end
   13.77  
   13.78 -val perm_simproc_app = Simplifier.simproc_global @{theory} "perm_simproc_app"
   13.79 -  ["Nominal.perm pi x"] perm_simproc_app';
   13.80 +val perm_simproc_app =
   13.81 +  Simplifier.make_simproc @{context} "perm_simproc_app"
   13.82 +   {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_app', identifier = []}
   13.83  
   13.84  (* a simproc that deals with permutation instances in front of functions  *)
   13.85 -fun perm_simproc_fun' ctxt redex = 
   13.86 -   let 
   13.87 +fun perm_simproc_fun' ctxt ct =
   13.88 +   let
   13.89 +     val redex = Thm.term_of ct
   13.90       fun applicable_fun t =
   13.91         (case (strip_comb t) of
   13.92            (Abs _ ,[]) => true
   13.93 @@ -124,20 +127,21 @@
   13.94          | (Const _, _) => true
   13.95          | _ => false)
   13.96     in
   13.97 -     case redex of 
   13.98 -       (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)     
   13.99 -       (Const(@{const_name Nominal.perm},_) $ pi $ f)  => 
  13.100 +     case redex of
  13.101 +       (* case pi o f == (%x. pi o (f ((rev pi)o x))) *)
  13.102 +       (Const(@{const_name Nominal.perm},_) $ pi $ f)  =>
  13.103            (if applicable_fun f then SOME perm_fun_def else NONE)
  13.104        | _ => NONE
  13.105     end
  13.106  
  13.107 -val perm_simproc_fun = Simplifier.simproc_global @{theory} "perm_simproc_fun"
  13.108 -  ["Nominal.perm pi x"] perm_simproc_fun';
  13.109 +val perm_simproc_fun =
  13.110 +  Simplifier.make_simproc @{context} "perm_simproc_fun"
  13.111 +   {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_fun', identifier = []}
  13.112  
  13.113  (* function for simplyfying permutations          *)
  13.114  (* stac contains the simplifiation tactic that is *)
  13.115  (* applied (see (no_asm) options below            *)
  13.116 -fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i = 
  13.117 +fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i =
  13.118      ("general simplification of permutations", fn st => SUBGOAL (fn _ =>
  13.119      let
  13.120         val ctxt' = ctxt
  13.121 @@ -150,23 +154,23 @@
  13.122      end) i st);
  13.123  
  13.124  (* general simplification of permutations and permutation that arose from eqvt-problems *)
  13.125 -fun perm_simp stac ctxt = 
  13.126 +fun perm_simp stac ctxt =
  13.127      let val simps = ["perm_swap","perm_fresh_fresh","perm_bij","perm_pi_simp","swap_simps"]
  13.128 -    in 
  13.129 +    in
  13.130          perm_simp_gen stac simps [] ctxt
  13.131      end;
  13.132  
  13.133 -fun eqvt_simp stac ctxt = 
  13.134 +fun eqvt_simp stac ctxt =
  13.135      let val simps = ["perm_swap","perm_fresh_fresh","perm_pi_simp"]
  13.136          val eqvts_thms = NominalThmDecls.get_eqvt_thms ctxt;
  13.137 -    in 
  13.138 +    in
  13.139          perm_simp_gen stac simps eqvts_thms ctxt
  13.140      end;
  13.141  
  13.142  
  13.143  (* main simplification tactics for permutations *)
  13.144  fun perm_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (perm_simp stac ctxt i));
  13.145 -fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (eqvt_simp stac ctxt i)); 
  13.146 +fun eqvt_simp_tac_gen_i stac tactical ctxt i = DETERM (tactical ctxt (eqvt_simp stac ctxt i));
  13.147  
  13.148  val perm_simp_tac_i          = perm_simp_tac_gen_i simp_tac
  13.149  val perm_asm_simp_tac_i      = perm_simp_tac_gen_i asm_simp_tac
  13.150 @@ -177,18 +181,18 @@
  13.151  
  13.152  (* applies the perm_compose rule such that                             *)
  13.153  (*   pi o (pi' o lhs) = rhs                                            *)
  13.154 -(* is transformed to                                                   *) 
  13.155 +(* is transformed to                                                   *)
  13.156  (*  (pi o pi') o (pi' o lhs) = rhs                                     *)
  13.157  (*                                                                     *)
  13.158  (* this rule would loop in the simplifier, so some trick is used with  *)
  13.159  (* generating perm_aux'es for the outermost permutation and then un-   *)
  13.160  (* folding the definition                                              *)
  13.161  
  13.162 -fun perm_compose_simproc' ctxt redex =
  13.163 -  (case redex of
  13.164 +fun perm_compose_simproc' ctxt ct =
  13.165 +  (case Thm.term_of ct of
  13.166       (Const (@{const_name Nominal.perm}, Type (@{type_name fun}, [Type (@{type_name list},
  13.167 -       [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (@{const_name Nominal.perm}, 
  13.168 -         Type (@{type_name fun}, [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $ 
  13.169 +       [Type (@{type_name Product_Type.prod}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const (@{const_name Nominal.perm},
  13.170 +         Type (@{type_name fun}, [Type (@{type_name list}, [Type (@{type_name Product_Type.prod}, [U as Type (uname,_),_])]),_])) $
  13.171            pi2 $ t)) =>
  13.172      let
  13.173        val thy = Proof_Context.theory_of ctxt
  13.174 @@ -196,7 +200,7 @@
  13.175        val uname' = Long_Name.base_name uname
  13.176      in
  13.177        if pi1 <> pi2 then  (* only apply the composition rule in this case *)
  13.178 -        if T = U then    
  13.179 +        if T = U then
  13.180            SOME (Thm.instantiate'
  13.181              [SOME (Thm.global_ctyp_of thy (fastype_of t))]
  13.182              [SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
  13.183 @@ -206,16 +210,18 @@
  13.184            SOME (Thm.instantiate'
  13.185              [SOME (Thm.global_ctyp_of thy (fastype_of t))]
  13.186              [SOME (Thm.global_cterm_of thy pi1), SOME (Thm.global_cterm_of thy pi2), SOME (Thm.global_cterm_of thy t)]
  13.187 -            (mk_meta_eq (Global_Theory.get_thm thy ("cp_"^tname'^"_"^uname'^"_inst") RS 
  13.188 +            (mk_meta_eq (Global_Theory.get_thm thy ("cp_"^tname'^"_"^uname'^"_inst") RS
  13.189               cp1_aux)))
  13.190        else NONE
  13.191      end
  13.192    | _ => NONE);
  13.193  
  13.194 -val perm_compose_simproc = Simplifier.simproc_global @{theory} "perm_compose"
  13.195 -  ["Nominal.perm pi1 (Nominal.perm pi2 t)"] perm_compose_simproc';
  13.196 +val perm_compose_simproc =
  13.197 +  Simplifier.make_simproc @{context} "perm_compose"
  13.198 +   {lhss = [@{term "Nominal.perm pi1 (Nominal.perm pi2 t)"}],
  13.199 +    proc = K perm_compose_simproc', identifier = []}
  13.200  
  13.201 -fun perm_compose_tac ctxt i = 
  13.202 +fun perm_compose_tac ctxt i =
  13.203    ("analysing permutation compositions on the lhs",
  13.204     fn st => EVERY
  13.205       [resolve_tac ctxt [trans] i,
  13.206 @@ -227,11 +233,11 @@
  13.207  
  13.208  (* unfolds the definition of permutations     *)
  13.209  (* applied to functions such that             *)
  13.210 -(*     pi o f = rhs                           *)  
  13.211 +(*     pi o f = rhs                           *)
  13.212  (* is transformed to                          *)
  13.213  (*     %x. pi o (f ((rev pi) o x)) = rhs      *)
  13.214  fun unfold_perm_fun_def_tac ctxt i =
  13.215 -    ("unfolding of permutations on functions", 
  13.216 +    ("unfolding of permutations on functions",
  13.217        resolve_tac ctxt [perm_fun_def RS meta_eq_to_obj_eq RS trans] i)
  13.218  
  13.219  (* applies the ext-rule such that      *)
  13.220 @@ -246,14 +252,14 @@
  13.221  (* since it contains looping rules the "recursion" - depth is set *)
  13.222  (* to 10 - this seems to be sufficient in most cases              *)
  13.223  fun perm_extend_simp_tac_i tactical ctxt =
  13.224 -  let fun perm_extend_simp_tac_aux tactical ctxt n = 
  13.225 +  let fun perm_extend_simp_tac_aux tactical ctxt n =
  13.226            if n=0 then K all_tac
  13.227 -          else DETERM o 
  13.228 +          else DETERM o
  13.229                 (FIRST'
  13.230                   [fn i => tactical ctxt ("splitting conjunctions on the rhs", resolve_tac ctxt [conjI] i),
  13.231                    fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i),
  13.232                    fn i => tactical ctxt (perm_compose_tac ctxt i),
  13.233 -                  fn i => tactical ctxt (apply_cong_tac ctxt i), 
  13.234 +                  fn i => tactical ctxt (apply_cong_tac ctxt i),
  13.235                    fn i => tactical ctxt (unfold_perm_fun_def_tac ctxt i),
  13.236                    fn i => tactical ctxt (ext_fun_tac ctxt i)]
  13.237                  THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1))))
  13.238 @@ -264,7 +270,7 @@
  13.239  (* unfolds the support definition and strips off the     *)
  13.240  (* intros, then applies eqvt_simp_tac                    *)
  13.241  fun supports_tac_i tactical ctxt i =
  13.242 -  let 
  13.243 +  let
  13.244       val simps        = [supports_def, Thm.symmetric fresh_def, fresh_prod]
  13.245    in
  13.246        EVERY [tactical ctxt ("unfolding of supports   ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i),
  13.247 @@ -323,11 +329,11 @@
  13.248  
  13.249  
  13.250  (* tactic that guesses whether an atom is fresh for an expression  *)
  13.251 -(* it first collects all free variables and tries to show that the *) 
  13.252 +(* it first collects all free variables and tries to show that the *)
  13.253  (* support of these free variables (op supports) the goal          *)
  13.254  (* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
  13.255  fun fresh_guess_tac_i tactical ctxt i st =
  13.256 -    let 
  13.257 +    let
  13.258          val goal = nth (cprems_of st) (i - 1)
  13.259          val fin_supp = Proof_Context.get_thms ctxt "fin_supp"
  13.260          val fresh_atm = Proof_Context.get_thms ctxt "fresh_atm"
  13.261 @@ -335,7 +341,7 @@
  13.262          val ctxt2 = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
  13.263      in
  13.264        case Logic.strip_assums_concl (Thm.term_of goal) of
  13.265 -          _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) => 
  13.266 +          _ $ (Const (@{const_name Nominal.fresh}, Type ("fun", [T, _])) $ _ $ t) =>
  13.267            let
  13.268              val ps = Logic.strip_params (Thm.term_of goal);
  13.269              val Ts = rev (map snd ps);
  13.270 @@ -353,15 +359,15 @@
  13.271                infer_instantiate ctxt
  13.272                  [(#1 (dest_Var (head_of S)), Thm.cterm_of ctxt s')] supports_fresh_rule';
  13.273            in
  13.274 -            (tactical ctxt ("guessing of the right set that supports the goal", 
  13.275 +            (tactical ctxt ("guessing of the right set that supports the goal",
  13.276                        (EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i,
  13.277                               asm_full_simp_tac ctxt1 (i+2),
  13.278 -                             asm_full_simp_tac ctxt2 (i+1), 
  13.279 +                             asm_full_simp_tac ctxt2 (i+1),
  13.280                               supports_tac_i tactical ctxt i]))) st
  13.281            end
  13.282 -          (* when a term-constructor contains more than one binder, it is useful    *) 
  13.283 +          (* when a term-constructor contains more than one binder, it is useful    *)
  13.284            (* in nominal_primrecs to try whether the goal can be solved by an hammer *)
  13.285 -        | _ => (tactical ctxt ("if it is not of the form _\<sharp>_, then try the simplifier",   
  13.286 +        | _ => (tactical ctxt ("if it is not of the form _\<sharp>_, then try the simplifier",
  13.287                            (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps [fresh_prod]@fresh_atm) i))) st
  13.288      end
  13.289      handle General.Subscript => Seq.empty;
  13.290 @@ -383,7 +389,7 @@
  13.291  
  13.292  (* Code opied from the Simplifer for setting up the perm_simp method   *)
  13.293  (* behaves nearly identical to the simp-method, for example can handle *)
  13.294 -(* options like (no_asm) etc.                                          *) 
  13.295 +(* options like (no_asm) etc.                                          *)
  13.296  val no_asmN = "no_asm";
  13.297  val no_asm_useN = "no_asm_use";
  13.298  val no_asm_simpN = "no_asm_simp";
    14.1 --- a/src/HOL/Product_Type.thy	Wed Sep 09 14:47:41 2015 +0200
    14.2 +++ b/src/HOL/Product_Type.thy	Wed Sep 09 20:57:21 2015 +0200
    14.3 @@ -1261,8 +1261,10 @@
    14.4  
    14.5  setup \<open>
    14.6    Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
    14.7 -    [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
    14.8 -    proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
    14.9 +    [Simplifier.make_simproc @{context} "set comprehension"
   14.10 +      {lhss = [@{term "Collect P"}],
   14.11 +       proc = K Set_Comprehension_Pointfree.code_simproc,
   14.12 +       identifier = []}])
   14.13  \<close>
   14.14  
   14.15  
    15.1 --- a/src/HOL/Rat.thy	Wed Sep 09 14:47:41 2015 +0200
    15.2 +++ b/src/HOL/Rat.thy	Wed Sep 09 20:57:21 2015 +0200
    15.3 @@ -629,7 +629,7 @@
    15.4        @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
    15.5        @{thm of_int_minus}, @{thm of_int_diff},
    15.6        @{thm of_int_of_nat_eq}]
    15.7 -  #> Lin_Arith.add_simprocs Numeral_Simprocs.field_divide_cancel_numeral_factor
    15.8 +  #> Lin_Arith.add_simprocs [Numeral_Simprocs.field_divide_cancel_numeral_factor]
    15.9    #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"})
   15.10    #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"}))
   15.11  \<close>
    16.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Wed Sep 09 14:47:41 2015 +0200
    16.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Wed Sep 09 20:57:21 2015 +0200
    16.3 @@ -353,12 +353,15 @@
    16.4    mk_solver "distinctFieldSolver" (distinctTree_tac names);
    16.5  
    16.6  fun distinct_simproc names =
    16.7 -  Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
    16.8 -    (fn ctxt =>
    16.9 -      (fn Const (@{const_name HOL.eq}, _) $ x $ y =>
   16.10 +  Simplifier.make_simproc @{context} "DistinctTreeProver.distinct_simproc"
   16.11 +   {lhss = [@{term "x = y"}],
   16.12 +    proc = fn _ => fn ctxt => fn ct =>
   16.13 +      (case Thm.term_of ct of
   16.14 +        Const (@{const_name HOL.eq}, _) $ x $ y =>
   16.15            Option.map (fn neq => @{thm neq_to_eq_False} OF [neq])
   16.16              (get_fst_success (neq_x_y ctxt x y) names)
   16.17 -        | _ => NONE));
   16.18 +      | _ => NONE),
   16.19 +    identifier = []};
   16.20  
   16.21  end;
   16.22  
    17.1 --- a/src/HOL/Statespace/state_fun.ML	Wed Sep 09 14:47:41 2015 +0200
    17.2 +++ b/src/HOL/Statespace/state_fun.ML	Wed Sep 09 20:57:21 2015 +0200
    17.3 @@ -51,26 +51,29 @@
    17.4  in
    17.5  
    17.6  val lazy_conj_simproc =
    17.7 -  Simplifier.simproc_global @{theory HOL} "lazy_conj_simp" ["P & Q"]
    17.8 -    (fn ctxt => fn t =>
    17.9 -      (case t of (Const (@{const_name HOL.conj},_) $ P $ Q) =>
   17.10 -        let
   17.11 -          val P_P' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt P);
   17.12 -          val P' = P_P' |> Thm.prop_of |> Logic.dest_equals |> #2;
   17.13 -        in
   17.14 -          if isFalse P' then SOME (conj1_False OF [P_P'])
   17.15 -          else
   17.16 -            let
   17.17 -              val Q_Q' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt Q);
   17.18 -              val Q' = Q_Q' |> Thm.prop_of |> Logic.dest_equals |> #2;
   17.19 -            in
   17.20 -              if isFalse Q' then SOME (conj2_False OF [Q_Q'])
   17.21 -              else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q'])
   17.22 -              else if P aconv P' andalso Q aconv Q' then NONE
   17.23 -              else SOME (conj_cong OF [P_P', Q_Q'])
   17.24 -            end
   17.25 -         end
   17.26 -      | _ => NONE));
   17.27 +  Simplifier.make_simproc @{context} "lazy_conj_simp"
   17.28 +   {lhss = [@{term "P & Q"}],
   17.29 +    proc = fn _ => fn ctxt => fn ct =>
   17.30 +      (case Thm.term_of ct of
   17.31 +        Const (@{const_name HOL.conj},_) $ P $ Q =>
   17.32 +          let
   17.33 +            val P_P' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt P);
   17.34 +            val P' = P_P' |> Thm.prop_of |> Logic.dest_equals |> #2;
   17.35 +          in
   17.36 +            if isFalse P' then SOME (conj1_False OF [P_P'])
   17.37 +            else
   17.38 +              let
   17.39 +                val Q_Q' = Simplifier.rewrite ctxt (Thm.cterm_of ctxt Q);
   17.40 +                val Q' = Q_Q' |> Thm.prop_of |> Logic.dest_equals |> #2;
   17.41 +              in
   17.42 +                if isFalse Q' then SOME (conj2_False OF [Q_Q'])
   17.43 +                else if isTrue P' andalso isTrue Q' then SOME (conj_True OF [P_P', Q_Q'])
   17.44 +                else if P aconv P' andalso Q aconv Q' then NONE
   17.45 +                else SOME (conj_cong OF [P_P', Q_Q'])
   17.46 +              end
   17.47 +           end
   17.48 +      | _ => NONE),
   17.49 +    identifier = []};
   17.50  
   17.51  fun string_eq_simp_tac ctxt =
   17.52    simp_tac (put_simpset HOL_basic_ss ctxt
   17.53 @@ -106,13 +109,14 @@
   17.54  val _ = Theory.setup (Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false)));
   17.55  
   17.56  val lookup_simproc =
   17.57 -  Simplifier.simproc_global @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
   17.58 -    (fn ctxt => fn t =>
   17.59 -      (case t of (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $
   17.60 +  Simplifier.make_simproc @{context} "lookup_simp"
   17.61 +   {lhss = [@{term "lookup d n (update d' c m v s)"}],
   17.62 +    proc = fn _ => fn ctxt => fn ct =>
   17.63 +      (case Thm.term_of ct of (Const (@{const_name StateFun.lookup}, lT) $ destr $ n $
   17.64                     (s as Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _)) =>
   17.65          (let
   17.66            val (_::_::_::_::sT::_) = binder_types uT;
   17.67 -          val mi = maxidx_of_term t;
   17.68 +          val mi = Term.maxidx_of_term (Thm.term_of ct);
   17.69            fun mk_upds (Const (@{const_name StateFun.update}, uT) $ d' $ c $ m $ v $ s) =
   17.70                  let
   17.71                    val (_ :: _ :: _ :: fT :: _ :: _) = binder_types uT;
   17.72 @@ -149,7 +153,8 @@
   17.73            else SOME thm
   17.74          end
   17.75          handle Option.Option => NONE)
   17.76 -      | _ => NONE ));
   17.77 +      | _ => NONE),
   17.78 +  identifier = []};
   17.79  
   17.80  
   17.81  local
   17.82 @@ -165,9 +170,10 @@
   17.83  in
   17.84  
   17.85  val update_simproc =
   17.86 -  Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
   17.87 -    (fn ctxt => fn t =>
   17.88 -      (case t of
   17.89 +  Simplifier.make_simproc @{context} "update_simp"
   17.90 +   {lhss = [@{term "update d c n v s"}],
   17.91 +    proc = fn _ => fn ctxt => fn ct =>
   17.92 +      (case Thm.term_of ct of
   17.93          Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _ =>
   17.94            let
   17.95              val (_ :: _ :: _ :: _ :: sT :: _) = binder_types uT;
   17.96 @@ -242,7 +248,7 @@
   17.97              val ctxt1 = put_simpset ss' ctxt0;
   17.98              val ctxt2 = put_simpset (#1 (Data.get (Context.Proof ctxt0))) ctxt0;
   17.99            in
  17.100 -            (case mk_updterm [] t of
  17.101 +            (case mk_updterm [] (Thm.term_of ct) of
  17.102                (trm, trm', vars, _, true) =>
  17.103                  let
  17.104                    val eq1 =
  17.105 @@ -253,7 +259,8 @@
  17.106                  in SOME (Thm.transitive eq1 eq2) end
  17.107              | _ => NONE)
  17.108            end
  17.109 -      | _ => NONE));
  17.110 +      | _ => NONE),
  17.111 +  identifier = []};
  17.112  
  17.113  end;
  17.114  
  17.115 @@ -269,10 +276,12 @@
  17.116  in
  17.117  
  17.118  val ex_lookup_eq_simproc =
  17.119 -  Simplifier.simproc_global @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
  17.120 -    (fn ctxt => fn t =>
  17.121 +  Simplifier.make_simproc @{context} "ex_lookup_eq_simproc"
  17.122 +   {lhss = [@{term "Ex t"}],
  17.123 +    proc = fn _ => fn ctxt => fn ct =>
  17.124        let
  17.125          val thy = Proof_Context.theory_of ctxt;
  17.126 +        val t = Thm.term_of ct;
  17.127  
  17.128          val ex_lookup_ss = #2 (Data.get (Context.Proof ctxt));
  17.129          val ctxt' = ctxt |> Config.put simp_depth_limit 100 |> put_simpset ex_lookup_ss;
  17.130 @@ -316,7 +325,8 @@
  17.131                val thm' = if swap then swap_ex_eq OF [thm] else thm
  17.132              in SOME thm' end handle TERM _ => NONE)
  17.133          | _ => NONE)
  17.134 -      end handle Option.Option => NONE);
  17.135 +      end handle Option.Option => NONE,
  17.136 +  identifier = []};
  17.137  
  17.138  end;
  17.139  
    18.1 --- a/src/HOL/Statespace/state_space.ML	Wed Sep 09 14:47:41 2015 +0200
    18.2 +++ b/src/HOL/Statespace/state_space.ML	Wed Sep 09 20:57:21 2015 +0200
    18.3 @@ -211,10 +211,15 @@
    18.4  val distinctNameSolver = mk_solver "distinctNameSolver" distinctTree_tac;
    18.5  
    18.6  val distinct_simproc =
    18.7 -  Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
    18.8 -    (fn ctxt => (fn (Const (@{const_name HOL.eq},_)$(x as Free _)$(y as Free _)) =>
    18.9 -        Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq]) (neq_x_y ctxt x y)
   18.10 -      | _ => NONE));
   18.11 +  Simplifier.make_simproc @{context} "StateSpace.distinct_simproc"
   18.12 +   {lhss = [@{term "x = y"}],
   18.13 +    proc = fn _ => fn ctxt => fn ct =>
   18.14 +      (case Thm.term_of ct of
   18.15 +        Const (@{const_name HOL.eq},_) $ (x as Free _) $ (y as Free _) =>
   18.16 +          Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
   18.17 +            (neq_x_y ctxt x y)
   18.18 +      | _ => NONE),
   18.19 +    identifier = []};
   18.20  
   18.21  fun interprete_parent name dist_thm_name parent_expr thy =
   18.22    let
    19.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Sep 09 14:47:41 2015 +0200
    19.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Sep 09 20:57:21 2015 +0200
    19.3 @@ -102,13 +102,13 @@
    19.4      (case try (Thm.instantiate' ty_inst trm_inst) ball_bex_thm of
    19.5        NONE => NONE
    19.6      | SOME thm' =>
    19.7 -        (case try (get_match_inst thy (get_lhs thm')) redex of
    19.8 +        (case try (get_match_inst thy (get_lhs thm')) (Thm.term_of redex) of
    19.9            NONE => NONE
   19.10          | SOME inst2 => try (Drule.instantiate_normalize inst2) thm'))
   19.11    end
   19.12  
   19.13  fun ball_bex_range_simproc ctxt redex =
   19.14 -  case redex of
   19.15 +  (case Thm.term_of redex of
   19.16      (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $
   19.17        (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
   19.18          calculate_inst ctxt @{thm ball_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   19.19 @@ -117,7 +117,7 @@
   19.20        (Const (@{const_name "rel_fun"}, _) $ R1 $ R2)) $ _) =>
   19.21          calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2
   19.22  
   19.23 -  | _ => NONE
   19.24 +  | _ => NONE)
   19.25  
   19.26  (* Regularize works as follows:
   19.27  
   19.28 @@ -147,17 +147,19 @@
   19.29  fun eq_imp_rel_get ctxt =
   19.30    map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))
   19.31  
   19.32 +val regularize_simproc =
   19.33 +  Simplifier.make_simproc @{context} "regularize"
   19.34 +    {lhss = [@{term "Ball (Respects (R1 ===> R2)) P"}, @{term "Bex (Respects (R1 ===> R2)) P"}],
   19.35 +     proc = K ball_bex_range_simproc,
   19.36 +     identifier = []};
   19.37 +
   19.38  fun regularize_tac ctxt =
   19.39    let
   19.40      val thy = Proof_Context.theory_of ctxt
   19.41 -    val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"}
   19.42 -    val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"}
   19.43 -    val simproc =
   19.44 -      Simplifier.simproc_global_i thy "" [ball_pat, bex_pat] ball_bex_range_simproc
   19.45      val simpset =
   19.46        mk_minimal_simpset ctxt
   19.47        addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
   19.48 -      addsimprocs [simproc]
   19.49 +      addsimprocs [regularize_simproc]
   19.50        addSolver equiv_solver addSolver quotient_solver
   19.51      val eq_eqvs = eq_imp_rel_get ctxt
   19.52    in
    20.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Wed Sep 09 14:47:41 2015 +0200
    20.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Sep 09 20:57:21 2015 +0200
    20.3 @@ -98,8 +98,10 @@
    20.4  
    20.5  (* Z3 proof replay *)
    20.6  
    20.7 -val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
    20.8 -  "(m::real) < n", "(m::real) <= n", "(m::real) = n"] Lin_Arith.simproc
    20.9 +val real_linarith_proc =
   20.10 +  Simplifier.make_simproc @{context} "fast_real_arith"
   20.11 +   {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \<le> n"}, @{term "(m::real) = n"}],
   20.12 +    proc = K Lin_Arith.simproc, identifier = []}
   20.13  
   20.14  
   20.15  (* setup *)
    21.1 --- a/src/HOL/Tools/SMT/z3_replay_util.ML	Wed Sep 09 14:47:41 2015 +0200
    21.2 +++ b/src/HOL/Tools/SMT/z3_replay_util.ML	Wed Sep 09 20:57:21 2015 +0200
    21.3 @@ -91,9 +91,9 @@
    21.4    fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
    21.5      | dest_binop t = raise TERM ("dest_binop", [t])
    21.6  
    21.7 -  fun prove_antisym_le ctxt t =
    21.8 +  fun prove_antisym_le ctxt ct =
    21.9      let
   21.10 -      val (le, r, s) = dest_binop t
   21.11 +      val (le, r, s) = dest_binop (Thm.term_of ct)
   21.12        val less = Const (@{const_name less}, Term.fastype_of le)
   21.13        val prems = Simplifier.prems_of ctxt
   21.14      in
   21.15 @@ -105,9 +105,9 @@
   21.16      end
   21.17      handle THM _ => NONE
   21.18  
   21.19 -  fun prove_antisym_less ctxt t =
   21.20 +  fun prove_antisym_less ctxt ct =
   21.21      let
   21.22 -      val (less, r, s) = dest_binop (HOLogic.dest_not t)
   21.23 +      val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct))
   21.24        val le = Const (@{const_name less_eq}, Term.fastype_of less)
   21.25        val prems = Simplifier.prems_of ctxt
   21.26      in
   21.27 @@ -124,11 +124,15 @@
   21.28        addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
   21.29          arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
   21.30        addsimprocs [@{simproc numeral_divmod},
   21.31 -        Simplifier.simproc_global @{theory} "fast_int_arith" [
   21.32 -          "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc,
   21.33 -        Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"] prove_antisym_le,
   21.34 -        Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
   21.35 -          prove_antisym_less])
   21.36 +        Simplifier.make_simproc @{context} "fast_int_arith"
   21.37 +         {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
   21.38 +          proc = K Lin_Arith.simproc, identifier = []},
   21.39 +        Simplifier.make_simproc @{context} "antisym_le"
   21.40 +         {lhss = [@{term "(x::'a::order) \<le> y"}],
   21.41 +          proc = K prove_antisym_le, identifier = []},
   21.42 +        Simplifier.make_simproc @{context} "antisym_less"
   21.43 +         {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
   21.44 +          proc = K prove_antisym_less, identifier = []}])
   21.45  
   21.46    structure Simpset = Generic_Data
   21.47    (
    22.1 --- a/src/HOL/Tools/groebner.ML	Wed Sep 09 14:47:41 2015 +0200
    22.2 +++ b/src/HOL/Tools/groebner.ML	Wed Sep 09 20:57:21 2015 +0200
    22.3 @@ -778,17 +778,20 @@
    22.4   in Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv ring_normalize_conv))
    22.5       (Thm.instantiate' [] [SOME a, SOME b] idl_sub)
    22.6   end
    22.7 - val poly_eq_simproc =
    22.8 +
    22.9 +val poly_eq_simproc =
   22.10    let
   22.11 -   fun proc phi ctxt t =
   22.12 -    let val th = poly_eq_conv t
   22.13 -    in if Thm.is_reflexive th then NONE else SOME th
   22.14 -    end
   22.15 -   in make_simproc {lhss = [Thm.lhs_of idl_sub],
   22.16 -                name = "poly_eq_simproc", proc = proc, identifier = []}
   22.17 -   end;
   22.18 - val poly_eq_ss =
   22.19 -   simpset_of (put_simpset HOL_basic_ss @{context}
   22.20 +    fun proc ct =
   22.21 +      let val th = poly_eq_conv ct
   22.22 +      in if Thm.is_reflexive th then NONE else SOME th end
   22.23 +  in
   22.24 +    Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc"
   22.25 +     {lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
   22.26 +      proc = fn _ => fn _ => proc, identifier = []}
   22.27 +  end;
   22.28 +
   22.29 +val poly_eq_ss =
   22.30 +  simpset_of (put_simpset HOL_basic_ss @{context}
   22.31      addsimps @{thms simp_thms}
   22.32      addsimprocs [poly_eq_simproc])
   22.33  
    23.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Sep 09 14:47:41 2015 +0200
    23.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Sep 09 20:57:21 2015 +0200
    23.3 @@ -38,65 +38,68 @@
    23.4  val anyt = Free ("t", TFree ("'t", []));
    23.5  
    23.6  fun strong_ind_simproc tab =
    23.7 -  Simplifier.simproc_global_i @{theory HOL} "strong_ind" [anyt] (fn ctxt => fn t =>
    23.8 -    let
    23.9 -      fun close p t f =
   23.10 -        let val vs = Term.add_vars t []
   23.11 -        in Thm.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
   23.12 -          (p (fold (Logic.all o Var) vs t) f)
   23.13 -        end;
   23.14 -      fun mkop @{const_name HOL.conj} T x =
   23.15 -            SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
   23.16 -        | mkop @{const_name HOL.disj} T x =
   23.17 -            SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
   23.18 -        | mkop _ _ _ = NONE;
   23.19 -      fun mk_collect p T t =
   23.20 -        let val U = HOLogic.dest_setT T
   23.21 -        in HOLogic.Collect_const U $
   23.22 -          HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
   23.23 -        end;
   23.24 -      fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member},
   23.25 -            Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
   23.26 -              mkop s T (m, p, S, mk_collect p T (head_of u))
   23.27 -        | decomp (Const (s, _) $ u $ ((m as Const (@{const_name Set.member},
   23.28 -            Type (_, [_, Type (_, [T, _])]))) $ p $ S)) =
   23.29 -              mkop s T (m, p, mk_collect p T (head_of u), S)
   23.30 -        | decomp _ = NONE;
   23.31 -      val simp =
   23.32 -        full_simp_tac
   23.33 -          (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]) 1;
   23.34 -      fun mk_rew t = (case strip_abs_vars t of
   23.35 -          [] => NONE
   23.36 -        | xs => (case decomp (strip_abs_body t) of
   23.37 -            NONE => NONE
   23.38 -          | SOME (bop, (m, p, S, S')) =>
   23.39 -              SOME (close (Goal.prove ctxt [] [])
   23.40 -                (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
   23.41 -                (K (EVERY
   23.42 -                  [resolve_tac ctxt [eq_reflection] 1,
   23.43 -                   REPEAT (resolve_tac ctxt @{thms ext} 1),
   23.44 -                   resolve_tac ctxt [iffI] 1,
   23.45 -                   EVERY [eresolve_tac ctxt [conjE] 1, resolve_tac ctxt [IntI] 1, simp, simp,
   23.46 -                     eresolve_tac ctxt [IntE] 1, resolve_tac ctxt [conjI] 1, simp, simp] ORELSE
   23.47 -                   EVERY [eresolve_tac ctxt [disjE] 1, resolve_tac ctxt [UnI1] 1, simp,
   23.48 -                     resolve_tac ctxt [UnI2] 1, simp,
   23.49 -                     eresolve_tac ctxt [UnE] 1, resolve_tac ctxt [disjI1] 1, simp,
   23.50 -                     resolve_tac ctxt [disjI2] 1, simp]])))
   23.51 -                handle ERROR _ => NONE))
   23.52 -    in
   23.53 -      case strip_comb t of
   23.54 -        (h as Const (name, _), ts) => (case Symtab.lookup tab name of
   23.55 -          SOME _ =>
   23.56 -            let val rews = map mk_rew ts
   23.57 -            in
   23.58 -              if forall is_none rews then NONE
   23.59 -              else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1)
   23.60 -                (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.cterm_of ctxt)
   23.61 -                   rews ts) (Thm.reflexive (Thm.cterm_of ctxt h)))
   23.62 -            end
   23.63 -        | NONE => NONE)
   23.64 -      | _ => NONE
   23.65 -    end);
   23.66 +  Simplifier.make_simproc @{context} "strong_ind"
   23.67 +   {lhss = [@{term "x::'a::{}"}],
   23.68 +    proc = fn _ => fn ctxt => fn ct =>
   23.69 +      let
   23.70 +        fun close p t f =
   23.71 +          let val vs = Term.add_vars t []
   23.72 +          in Thm.instantiate' [] (rev (map (SOME o Thm.cterm_of ctxt o Var) vs))
   23.73 +            (p (fold (Logic.all o Var) vs t) f)
   23.74 +          end;
   23.75 +        fun mkop @{const_name HOL.conj} T x =
   23.76 +              SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
   23.77 +          | mkop @{const_name HOL.disj} T x =
   23.78 +              SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
   23.79 +          | mkop _ _ _ = NONE;
   23.80 +        fun mk_collect p T t =
   23.81 +          let val U = HOLogic.dest_setT T
   23.82 +          in HOLogic.Collect_const U $
   23.83 +            HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
   23.84 +          end;
   23.85 +        fun decomp (Const (s, _) $ ((m as Const (@{const_name Set.member},
   23.86 +              Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
   23.87 +                mkop s T (m, p, S, mk_collect p T (head_of u))
   23.88 +          | decomp (Const (s, _) $ u $ ((m as Const (@{const_name Set.member},
   23.89 +              Type (_, [_, Type (_, [T, _])]))) $ p $ S)) =
   23.90 +                mkop s T (m, p, mk_collect p T (head_of u), S)
   23.91 +          | decomp _ = NONE;
   23.92 +        val simp =
   23.93 +          full_simp_tac
   23.94 +            (put_simpset HOL_basic_ss ctxt addsimps [mem_Collect_eq, @{thm split_conv}]) 1;
   23.95 +        fun mk_rew t = (case strip_abs_vars t of
   23.96 +            [] => NONE
   23.97 +          | xs => (case decomp (strip_abs_body t) of
   23.98 +              NONE => NONE
   23.99 +            | SOME (bop, (m, p, S, S')) =>
  23.100 +                SOME (close (Goal.prove ctxt [] [])
  23.101 +                  (Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
  23.102 +                  (K (EVERY
  23.103 +                    [resolve_tac ctxt [eq_reflection] 1,
  23.104 +                     REPEAT (resolve_tac ctxt @{thms ext} 1),
  23.105 +                     resolve_tac ctxt [iffI] 1,
  23.106 +                     EVERY [eresolve_tac ctxt [conjE] 1, resolve_tac ctxt [IntI] 1, simp, simp,
  23.107 +                       eresolve_tac ctxt [IntE] 1, resolve_tac ctxt [conjI] 1, simp, simp] ORELSE
  23.108 +                     EVERY [eresolve_tac ctxt [disjE] 1, resolve_tac ctxt [UnI1] 1, simp,
  23.109 +                       resolve_tac ctxt [UnI2] 1, simp,
  23.110 +                       eresolve_tac ctxt [UnE] 1, resolve_tac ctxt [disjI1] 1, simp,
  23.111 +                       resolve_tac ctxt [disjI2] 1, simp]])))
  23.112 +                  handle ERROR _ => NONE))
  23.113 +      in
  23.114 +        (case strip_comb (Thm.term_of ct) of
  23.115 +          (h as Const (name, _), ts) =>
  23.116 +            if Symtab.defined tab name then
  23.117 +              let val rews = map mk_rew ts
  23.118 +              in
  23.119 +                if forall is_none rews then NONE
  23.120 +                else SOME (fold (fn th1 => fn th2 => Thm.combination th2 th1)
  23.121 +                  (map2 (fn SOME r => K r | NONE => Thm.reflexive o Thm.cterm_of ctxt)
  23.122 +                     rews ts) (Thm.reflexive (Thm.cterm_of ctxt h)))
  23.123 +              end
  23.124 +            else NONE
  23.125 +        | _ => NONE)
  23.126 +      end,
  23.127 +    identifier = []};
  23.128  
  23.129  (* only eta contract terms occurring as arguments of functions satisfying p *)
  23.130  fun eta_contract p =
  23.131 @@ -312,9 +315,12 @@
  23.132  fun to_pred_simproc rules =
  23.133    let val rules' = map mk_meta_eq rules
  23.134    in
  23.135 -    Simplifier.simproc_global_i @{theory HOL} "to_pred" [anyt]
  23.136 -      (fn ctxt =>
  23.137 -        lookup_rule (Proof_Context.theory_of ctxt) (Thm.prop_of #> Logic.dest_equals) rules')
  23.138 +    Simplifier.make_simproc @{context} "to_pred"
  23.139 +      {lhss = [anyt],
  23.140 +       proc = fn _ => fn ctxt => fn ct =>
  23.141 +        lookup_rule (Proof_Context.theory_of ctxt)
  23.142 +          (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct),
  23.143 +       identifier = []}
  23.144    end;
  23.145  
  23.146  fun to_pred_proc thy rules t =
    24.1 --- a/src/HOL/Tools/int_arith.ML	Wed Sep 09 14:47:41 2015 +0200
    24.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Sep 09 20:57:21 2015 +0200
    24.3 @@ -20,33 +20,29 @@
    24.4     That is, m and n consist only of 1s combined with "+", "-" and "*".
    24.5  *)
    24.6  
    24.7 -val zeroth = (Thm.symmetric o mk_meta_eq) @{thm of_int_0};
    24.8 -
    24.9 -val lhss0 = [@{cpat "0::?'a::ring"}];
   24.10 -
   24.11 -fun proc0 phi ctxt ct =
   24.12 -  let val T = Thm.ctyp_of_cterm ct
   24.13 -  in if Thm.typ_of T = @{typ int} then NONE else
   24.14 -     SOME (Thm.instantiate' [SOME T] [] zeroth)
   24.15 -  end;
   24.16 +val zeroth = Thm.symmetric (mk_meta_eq @{thm of_int_0});
   24.17  
   24.18  val zero_to_of_int_zero_simproc =
   24.19 -  make_simproc {lhss = lhss0, name = "zero_to_of_int_zero_simproc",
   24.20 -  proc = proc0, identifier = []};
   24.21 -
   24.22 -val oneth = (Thm.symmetric o mk_meta_eq) @{thm of_int_1};
   24.23 +  Simplifier.make_simproc @{context} "zero_to_of_int_zero_simproc"
   24.24 +   {lhss = [@{term "0::'a::ring"}],
   24.25 +    proc = fn _ => fn ctxt => fn ct =>
   24.26 +      let val T = Thm.ctyp_of_cterm ct in
   24.27 +        if Thm.typ_of T = @{typ int} then NONE
   24.28 +        else SOME (Thm.instantiate' [SOME T] [] zeroth)
   24.29 +      end,
   24.30 +     identifier = []};
   24.31  
   24.32 -val lhss1 = [@{cpat "1::?'a::ring_1"}];
   24.33 -
   24.34 -fun proc1 phi ctxt ct =
   24.35 -  let val T = Thm.ctyp_of_cterm ct
   24.36 -  in if Thm.typ_of T = @{typ int} then NONE else
   24.37 -     SOME (Thm.instantiate' [SOME T] [] oneth)
   24.38 -  end;
   24.39 +val oneth = Thm.symmetric (mk_meta_eq @{thm of_int_1});
   24.40  
   24.41  val one_to_of_int_one_simproc =
   24.42 -  make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   24.43 -  proc = proc1, identifier = []};
   24.44 +  Simplifier.make_simproc @{context} "one_to_of_int_one_simproc"
   24.45 +   {lhss = [@{term "1::'a::ring_1"}],
   24.46 +    proc = fn _ => fn ctxt => fn ct =>
   24.47 +      let val T = Thm.ctyp_of_cterm ct in
   24.48 +        if Thm.typ_of T = @{typ int} then NONE
   24.49 +        else SOME (Thm.instantiate' [SOME T] [] oneth)
   24.50 +      end,
   24.51 +    identifier = []};
   24.52  
   24.53  fun check (Const (@{const_name Groups.one}, @{typ int})) = false
   24.54    | check (Const (@{const_name Groups.one}, _)) = true
   24.55 @@ -66,18 +62,18 @@
   24.56        [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}])
   24.57       addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]);
   24.58  
   24.59 -fun sproc phi ctxt ct =
   24.60 -  if check (Thm.term_of ct) then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
   24.61 -  else NONE;
   24.62 +val zero_one_idom_simproc =
   24.63 +  Simplifier.make_simproc @{context} "zero_one_idom_simproc"
   24.64 +   {lhss =
   24.65 +      [@{term "(x::'a::ring_char_0) = y"},
   24.66 +       @{term "(x::'a::linordered_idom) < y"},
   24.67 +       @{term "(x::'a::linordered_idom) \<le> y"}],
   24.68 +    proc = fn _ => fn ctxt => fn ct =>
   24.69 +      if check (Thm.term_of ct)
   24.70 +      then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
   24.71 +      else NONE,
   24.72 +    identifier = []};
   24.73  
   24.74 -val lhss' =
   24.75 -  [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"},
   24.76 -   @{cpat "(?x::?'a::linordered_idom) < (?y::?'a)"},
   24.77 -   @{cpat "(?x::?'a::linordered_idom) <= (?y::?'a)"}]
   24.78 -
   24.79 -val zero_one_idom_simproc =
   24.80 -  make_simproc {lhss = lhss' , name = "zero_one_idom_simproc",
   24.81 -  proc = sproc, identifier = []}
   24.82  
   24.83  fun number_of ctxt T n =
   24.84    if not (Sign.of_sort (Proof_Context.theory_of ctxt) (T, @{sort numeral}))
    25.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Sep 09 14:47:41 2015 +0200
    25.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Sep 09 20:57:21 2015 +0200
    25.3 @@ -9,7 +9,7 @@
    25.4    val pre_tac: Proof.context -> int -> tactic
    25.5    val simple_tac: Proof.context -> int -> tactic
    25.6    val tac: Proof.context -> int -> tactic
    25.7 -  val simproc: Proof.context -> term -> thm option
    25.8 +  val simproc: Proof.context -> cterm -> thm option
    25.9    val add_inj_thms: thm list -> Context.generic -> Context.generic
   25.10    val add_lessD: thm -> Context.generic -> Context.generic
   25.11    val add_simps: thm list -> Context.generic -> Context.generic
    26.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Sep 09 14:47:41 2015 +0200
    26.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Sep 09 20:57:21 2015 +0200
    26.3 @@ -216,10 +216,10 @@
    26.4    val bal_add2 = @{thm nat_diff_add_eq2} RS trans
    26.5  );
    26.6  
    26.7 -fun eq_cancel_numerals ctxt ct = EqCancelNumerals.proc ctxt (Thm.term_of ct)
    26.8 -fun less_cancel_numerals ctxt ct = LessCancelNumerals.proc ctxt (Thm.term_of ct)
    26.9 -fun le_cancel_numerals ctxt ct = LeCancelNumerals.proc ctxt (Thm.term_of ct)
   26.10 -fun diff_cancel_numerals ctxt ct = DiffCancelNumerals.proc ctxt (Thm.term_of ct)
   26.11 +val eq_cancel_numerals = EqCancelNumerals.proc
   26.12 +val less_cancel_numerals = LessCancelNumerals.proc
   26.13 +val le_cancel_numerals = LeCancelNumerals.proc
   26.14 +val diff_cancel_numerals = DiffCancelNumerals.proc
   26.15  
   26.16  
   26.17  (*** Applying CombineNumeralsFun ***)
   26.18 @@ -257,7 +257,7 @@
   26.19  
   26.20  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   26.21  
   26.22 -fun combine_numerals ctxt ct = CombineNumerals.proc ctxt (Thm.term_of ct)
   26.23 +val combine_numerals = CombineNumerals.proc
   26.24  
   26.25  
   26.26  (*** Applying CancelNumeralFactorFun ***)
   26.27 @@ -311,7 +311,8 @@
   26.28  );
   26.29  
   26.30  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   26.31 - (open CancelNumeralFactorCommon
   26.32 +(
   26.33 +  open CancelNumeralFactorCommon
   26.34    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   26.35    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   26.36    val cancel = @{thm nat_mult_less_cancel1} RS trans
   26.37 @@ -319,18 +320,19 @@
   26.38  );
   26.39  
   26.40  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   26.41 - (open CancelNumeralFactorCommon
   26.42 +(
   26.43 +  open CancelNumeralFactorCommon
   26.44    val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   26.45    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   26.46    val cancel = @{thm nat_mult_le_cancel1} RS trans
   26.47    val neg_exchanges = true
   26.48  )
   26.49  
   26.50 -fun eq_cancel_numeral_factor ctxt ct = EqCancelNumeralFactor.proc ctxt (Thm.term_of ct)
   26.51 -fun less_cancel_numeral_factor ctxt ct = LessCancelNumeralFactor.proc ctxt (Thm.term_of ct)
   26.52 -fun le_cancel_numeral_factor ctxt ct = LeCancelNumeralFactor.proc ctxt (Thm.term_of ct)
   26.53 -fun div_cancel_numeral_factor ctxt ct = DivCancelNumeralFactor.proc ctxt (Thm.term_of ct)
   26.54 -fun dvd_cancel_numeral_factor ctxt ct = DvdCancelNumeralFactor.proc ctxt (Thm.term_of ct)
   26.55 +val eq_cancel_numeral_factor = EqCancelNumeralFactor.proc
   26.56 +val less_cancel_numeral_factor = LessCancelNumeralFactor.proc
   26.57 +val le_cancel_numeral_factor = LeCancelNumeralFactor.proc
   26.58 +val div_cancel_numeral_factor = DivCancelNumeralFactor.proc
   26.59 +val dvd_cancel_numeral_factor = DvdCancelNumeralFactor.proc
   26.60  
   26.61  
   26.62  (*** Applying ExtractCommonTermFun ***)
    27.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Sep 09 14:47:41 2015 +0200
    27.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Sep 09 20:57:21 2015 +0200
    27.3 @@ -16,8 +16,6 @@
    27.4  
    27.5  signature NUMERAL_SIMPROCS =
    27.6  sig
    27.7 -  val prep_simproc: theory -> string * string list * (Proof.context -> term -> thm option)
    27.8 -    -> simproc
    27.9    val trans_tac: Proof.context -> thm option -> tactic
   27.10    val assoc_fold: Proof.context -> cterm -> thm option
   27.11    val combine_numerals: Proof.context -> cterm -> thm option
   27.12 @@ -37,7 +35,7 @@
   27.13    val div_cancel_numeral_factor: Proof.context -> cterm -> thm option
   27.14    val divide_cancel_numeral_factor: Proof.context -> cterm -> thm option
   27.15    val field_combine_numerals: Proof.context -> cterm -> thm option
   27.16 -  val field_divide_cancel_numeral_factor: simproc list
   27.17 +  val field_divide_cancel_numeral_factor: simproc
   27.18    val num_ss: simpset
   27.19    val field_comp_conv: Proof.context -> conv
   27.20  end;
   27.21 @@ -45,9 +43,6 @@
   27.22  structure Numeral_Simprocs : NUMERAL_SIMPROCS =
   27.23  struct
   27.24  
   27.25 -fun prep_simproc thy (name, pats, proc) =
   27.26 -  Simplifier.simproc_global thy name pats proc;
   27.27 -
   27.28  fun trans_tac _ NONE  = all_tac
   27.29    | trans_tac ctxt (SOME th) = ALLGOALS (resolve_tac ctxt [th RS trans]);
   27.30  
   27.31 @@ -65,7 +60,7 @@
   27.32     which is not required for cancellation of common factors in divisions.
   27.33     UPDATE: this reasoning no longer applies (number_ring is gone)
   27.34  *)
   27.35 -fun mk_prod T = 
   27.36 +fun mk_prod T =
   27.37    let val one = one_of T
   27.38    fun mk [] = one
   27.39      | mk [t] = t
   27.40 @@ -141,7 +136,7 @@
   27.41    ordering is not well-founded.*)
   27.42  fun num_ord (i,j) =
   27.43    (case int_ord (abs i, abs j) of
   27.44 -    EQUAL => int_ord (Int.sign i, Int.sign j) 
   27.45 +    EQUAL => int_ord (Int.sign i, Int.sign j)
   27.46    | ord => ord);
   27.47  
   27.48  (*This resembles Term_Ord.term_ord, but it puts binary numerals before other
   27.49 @@ -190,7 +185,7 @@
   27.50  
   27.51  val field_post_simps =
   27.52      post_simps @ [@{thm divide_zero_left}, @{thm divide_1}]
   27.53 -                      
   27.54 +
   27.55  (*Simplify inverse Numeral1*)
   27.56  val inverse_1s = [@{thm inverse_numeral_1}];
   27.57  
   27.58 @@ -202,7 +197,7 @@
   27.59      @{thms add_neg_numeral_left} @
   27.60      @{thms mult_numeral_left} @
   27.61      @{thms arith_simps} @ @{thms rel_simps};
   27.62 -    
   27.63 +
   27.64  (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
   27.65    during re-arrangement*)
   27.66  val non_add_simps =
   27.67 @@ -288,9 +283,9 @@
   27.68    val bal_add2 = @{thm le_add_iff2} RS trans
   27.69  );
   27.70  
   27.71 -fun eq_cancel_numerals ctxt ct = EqCancelNumerals.proc ctxt (Thm.term_of ct)
   27.72 -fun less_cancel_numerals ctxt ct = LessCancelNumerals.proc ctxt (Thm.term_of ct)
   27.73 -fun le_cancel_numerals ctxt ct = LeCancelNumerals.proc ctxt (Thm.term_of ct)
   27.74 +val eq_cancel_numerals = EqCancelNumerals.proc
   27.75 +val less_cancel_numerals = LessCancelNumerals.proc
   27.76 +val le_cancel_numerals = LeCancelNumerals.proc
   27.77  
   27.78  structure CombineNumeralsData =
   27.79  struct
   27.80 @@ -350,9 +345,9 @@
   27.81  
   27.82  structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
   27.83  
   27.84 -fun combine_numerals ctxt ct = CombineNumerals.proc ctxt (Thm.term_of ct)
   27.85 +val combine_numerals = CombineNumerals.proc
   27.86  
   27.87 -fun field_combine_numerals ctxt ct = FieldCombineNumerals.proc ctxt (Thm.term_of ct)
   27.88 +val field_combine_numerals = FieldCombineNumerals.proc
   27.89  
   27.90  
   27.91  (** Constant folding for multiplication in semirings **)
   27.92 @@ -433,37 +428,40 @@
   27.93  )
   27.94  
   27.95  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   27.96 - (open CancelNumeralFactorCommon
   27.97 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   27.98 +(
   27.99 +  open CancelNumeralFactorCommon
  27.100 +  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
  27.101    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
  27.102    val cancel = @{thm mult_le_cancel_left} RS trans
  27.103    val neg_exchanges = true
  27.104  )
  27.105  
  27.106 -fun eq_cancel_numeral_factor ctxt ct = EqCancelNumeralFactor.proc ctxt (Thm.term_of ct)
  27.107 -fun less_cancel_numeral_factor ctxt ct = LessCancelNumeralFactor.proc ctxt (Thm.term_of ct)
  27.108 -fun le_cancel_numeral_factor ctxt ct = LeCancelNumeralFactor.proc ctxt (Thm.term_of ct)
  27.109 -fun div_cancel_numeral_factor ctxt ct = DivCancelNumeralFactor.proc ctxt (Thm.term_of ct)
  27.110 -fun divide_cancel_numeral_factor ctxt ct = DivideCancelNumeralFactor.proc ctxt (Thm.term_of ct)
  27.111 +val eq_cancel_numeral_factor = EqCancelNumeralFactor.proc
  27.112 +val less_cancel_numeral_factor = LessCancelNumeralFactor.proc
  27.113 +val le_cancel_numeral_factor = LeCancelNumeralFactor.proc
  27.114 +val div_cancel_numeral_factor = DivCancelNumeralFactor.proc
  27.115 +val divide_cancel_numeral_factor = DivideCancelNumeralFactor.proc
  27.116  
  27.117  val field_divide_cancel_numeral_factor =
  27.118 -  [prep_simproc @{theory}
  27.119 -    ("field_divide_cancel_numeral_factor",
  27.120 -     ["((l::'a::field) * m) / n",
  27.121 -      "(l::'a::field) / (m * n)",
  27.122 -      "((numeral v)::'a::field) / (numeral w)",
  27.123 -      "((numeral v)::'a::field) / (- numeral w)",
  27.124 -      "((- numeral v)::'a::field) / (numeral w)",
  27.125 -      "((- numeral v)::'a::field) / (- numeral w)"],
  27.126 -     DivideCancelNumeralFactor.proc)];
  27.127 +  Simplifier.make_simproc @{context} "field_divide_cancel_numeral_factor"
  27.128 +   {lhss =
  27.129 +     [@{term "((l::'a::field) * m) / n"},
  27.130 +      @{term "(l::'a::field) / (m * n)"},
  27.131 +      @{term "((numeral v)::'a::field) / (numeral w)"},
  27.132 +      @{term "((numeral v)::'a::field) / (- numeral w)"},
  27.133 +      @{term "((- numeral v)::'a::field) / (numeral w)"},
  27.134 +      @{term "((- numeral v)::'a::field) / (- numeral w)"}],
  27.135 +    proc = K DivideCancelNumeralFactor.proc,
  27.136 +    identifier = []}
  27.137  
  27.138  val field_cancel_numeral_factors =
  27.139 -  prep_simproc @{theory}
  27.140 -    ("field_eq_cancel_numeral_factor",
  27.141 -     ["(l::'a::field) * m = n",
  27.142 -      "(l::'a::field) = m * n"],
  27.143 -     EqCancelNumeralFactor.proc)
  27.144 -   :: field_divide_cancel_numeral_factor;
  27.145 +  [Simplifier.make_simproc @{context} "field_eq_cancel_numeral_factor"
  27.146 +    {lhss =
  27.147 +       [@{term "(l::'a::field) * m = n"},
  27.148 +        @{term "(l::'a::field) = m * n"}],
  27.149 +      proc = K EqCancelNumeralFactor.proc,
  27.150 +      identifier = []},
  27.151 +   field_divide_cancel_numeral_factor]
  27.152  
  27.153  
  27.154  (** Declarations for ExtractCommonTerm **)
  27.155 @@ -476,7 +474,7 @@
  27.156          handle TERM _ => find_first_t (t::past) u terms;
  27.157  
  27.158  (** Final simplification for the CancelFactor simprocs **)
  27.159 -val simplify_one = Arith_Data.simplify_meta_eq  
  27.160 +val simplify_one = Arith_Data.simplify_meta_eq
  27.161    [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
  27.162  
  27.163  fun cancel_simplify_meta_eq ctxt cancel_th th =
  27.164 @@ -484,7 +482,7 @@
  27.165  
  27.166  local
  27.167    val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory_context HOL} HOLogic.Trueprop)
  27.168 -  fun Eq_True_elim Eq = 
  27.169 +  fun Eq_True_elim Eq =
  27.170      Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
  27.171  in
  27.172  fun sign_conv pos_th neg_th ctxt t =
  27.173 @@ -515,7 +513,7 @@
  27.174      simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms ac_simps minus_mult_commute})
  27.175    fun norm_tac ctxt =
  27.176      ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
  27.177 -  val simplify_meta_eq  = cancel_simplify_meta_eq 
  27.178 +  val simplify_meta_eq  = cancel_simplify_meta_eq
  27.179    fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
  27.180  end;
  27.181  
  27.182 @@ -585,25 +583,26 @@
  27.183  fun divide_cancel_factor ctxt ct = DivideCancelFactor.proc ctxt (Thm.term_of ct)
  27.184  
  27.185  local
  27.186 - val zr = @{cpat "0"}
  27.187 - val zT = Thm.ctyp_of_cterm zr
  27.188 - val geq = @{cpat HOL.eq}
  27.189 - val eqT = Thm.dest_ctyp (Thm.ctyp_of_cterm geq) |> hd
  27.190 - val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
  27.191 - val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
  27.192 - val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
  27.193 +
  27.194 +val zr = @{cpat "0"}
  27.195 +val zT = Thm.ctyp_of_cterm zr
  27.196 +val geq = @{cpat HOL.eq}
  27.197 +val eqT = Thm.dest_ctyp (Thm.ctyp_of_cterm geq) |> hd
  27.198 +val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
  27.199 +val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
  27.200 +val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
  27.201  
  27.202 - fun prove_nz ctxt T t =
  27.203 -    let
  27.204 -      val z = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of zT), T)],[]) zr
  27.205 -      val eq = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of eqT), T)],[]) geq
  27.206 -      val th = Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
  27.207 -           (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"}
  27.208 -                  (Thm.apply (Thm.apply eq t) z)))
  27.209 -    in Thm.equal_elim (Thm.symmetric th) TrueI
  27.210 -    end
  27.211 +fun prove_nz ctxt T t =
  27.212 +  let
  27.213 +    val z = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of zT), T)],[]) zr
  27.214 +    val eq = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of eqT), T)],[]) geq
  27.215 +    val th = Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
  27.216 +         (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"}
  27.217 +                (Thm.apply (Thm.apply eq t) z)))
  27.218 +  in Thm.equal_elim (Thm.symmetric th) TrueI
  27.219 +  end
  27.220  
  27.221 - fun proc phi ctxt ct =
  27.222 +fun proc ctxt ct =
  27.223    let
  27.224      val ((x,y),(w,z)) =
  27.225           (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
  27.226 @@ -611,11 +610,10 @@
  27.227      val T = Thm.ctyp_of_cterm x
  27.228      val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z]
  27.229      val th = Thm.instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
  27.230 -  in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz)
  27.231 -  end
  27.232 +  in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) end
  27.233    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
  27.234  
  27.235 - fun proc2 phi ctxt ct =
  27.236 +fun proc2 ctxt ct =
  27.237    let
  27.238      val (l,r) = Thm.dest_binop ct
  27.239      val T = Thm.ctyp_of_cterm l
  27.240 @@ -636,12 +634,12 @@
  27.241    end
  27.242    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
  27.243  
  27.244 - fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
  27.245 -   | is_number t = can HOLogic.dest_number t
  27.246 +fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
  27.247 +  | is_number t = can HOLogic.dest_number t
  27.248  
  27.249 - val is_number = is_number o Thm.term_of
  27.250 +val is_number = is_number o Thm.term_of
  27.251  
  27.252 - fun proc3 phi ctxt ct =
  27.253 +fun proc3 ctxt ct =
  27.254    (case Thm.term_of ct of
  27.255      Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
  27.256        let
  27.257 @@ -685,41 +683,42 @@
  27.258          val T = Thm.ctyp_of_cterm c
  27.259          val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
  27.260        in SOME (mk_meta_eq th) end
  27.261 -  | _ => NONE)
  27.262 -  handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
  27.263 +  | _ => NONE) handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
  27.264  
  27.265  val add_frac_frac_simproc =
  27.266 -       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
  27.267 -                     name = "add_frac_frac_simproc",
  27.268 -                     proc = proc, identifier = []}
  27.269 +  Simplifier.make_simproc @{context} "add_frac_frac_simproc"
  27.270 +   {lhss = [@{term "(x::'a::field) / y + (w::'a::field) / z"}],
  27.271 +    proc = K proc, identifier = []}
  27.272  
  27.273  val add_frac_num_simproc =
  27.274 -       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
  27.275 -                     name = "add_frac_num_simproc",
  27.276 -                     proc = proc2, identifier = []}
  27.277 +  Simplifier.make_simproc @{context} "add_frac_num_simproc"
  27.278 +   {lhss = [@{term "(x::'a::field) / y + z"}, @{term "z + (x::'a::field) / y"}],
  27.279 +    proc = K proc2, identifier = []}
  27.280  
  27.281  val ord_frac_simproc =
  27.282 -  make_simproc
  27.283 -    {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
  27.284 -             @{cpat "(?a::(?'a::{field, ord}))/?b <= ?c"},
  27.285 -             @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
  27.286 -             @{cpat "?c <= (?a::(?'a::{field, ord}))/?b"},
  27.287 -             @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
  27.288 -             @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
  27.289 -             name = "ord_frac_simproc", proc = proc3, identifier = []}
  27.290 +  Simplifier.make_simproc @{context} "ord_frac_simproc"
  27.291 +   {lhss =
  27.292 +     [@{term "(a::'a::{field,ord}) / b < c"},
  27.293 +      @{term "(a::'a::{field,ord}) / b \<le> c"},
  27.294 +      @{term "c < (a::'a::{field,ord}) / b"},
  27.295 +      @{term "c \<le> (a::'a::{field,ord}) / b"},
  27.296 +      @{term "c = (a::'a::{field,ord}) / b"},
  27.297 +      @{term "(a::'a::{field, ord}) / b = c"}],
  27.298 +    proc = K proc3, identifier = []}
  27.299  
  27.300 -val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
  27.301 -           @{thm "divide_numeral_1"},
  27.302 -           @{thm "divide_zero"}, @{thm divide_zero_left},
  27.303 -           @{thm "divide_divide_eq_left"}, 
  27.304 -           @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
  27.305 -           @{thm "times_divide_times_eq"},
  27.306 -           @{thm "divide_divide_eq_right"},
  27.307 -           @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"},
  27.308 -           @{thm "add_divide_distrib"} RS sym,
  27.309 -           @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide}, 
  27.310 -           Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute}))))   
  27.311 -           (@{thm Fields.field_divide_inverse} RS sym)]
  27.312 +val ths =
  27.313 + [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
  27.314 +  @{thm "divide_numeral_1"},
  27.315 +  @{thm "divide_zero"}, @{thm divide_zero_left},
  27.316 +  @{thm "divide_divide_eq_left"},
  27.317 +  @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
  27.318 +  @{thm "times_divide_times_eq"},
  27.319 +  @{thm "divide_divide_eq_right"},
  27.320 +  @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"},
  27.321 +  @{thm "add_divide_distrib"} RS sym,
  27.322 +  @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide},
  27.323 +  Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute}))))
  27.324 +  (@{thm Fields.field_divide_inverse} RS sym)]
  27.325  
  27.326  val field_comp_ss =
  27.327    simpset_of
  27.328 @@ -740,4 +739,3 @@
  27.329  end
  27.330  
  27.331  end;
  27.332 -
    28.1 --- a/src/HOL/Tools/record.ML	Wed Sep 09 14:47:41 2015 +0200
    28.2 +++ b/src/HOL/Tools/record.ML	Wed Sep 09 20:57:21 2015 +0200
    28.3 @@ -1059,9 +1059,13 @@
    28.4      subrecord.
    28.5  *)
    28.6  val simproc =
    28.7 -  Simplifier.simproc_global @{theory HOL} "record" ["x"]
    28.8 -    (fn ctxt => fn t =>
    28.9 -      let val thy = Proof_Context.theory_of ctxt in
   28.10 +  Simplifier.make_simproc @{context} "record"
   28.11 +   {lhss = [@{term "x"}],
   28.12 +    proc = fn _ => fn ctxt => fn ct =>
   28.13 +      let
   28.14 +        val thy = Proof_Context.theory_of ctxt;
   28.15 +        val t = Thm.term_of ct;
   28.16 +      in
   28.17          (case t of
   28.18            (sel as Const (s, Type (_, [_, rangeS]))) $
   28.19                ((upd as Const (u, Type (_, [_, Type (_, [rT, _])]))) $ k $ r) =>
   28.20 @@ -1109,7 +1113,8 @@
   28.21                end
   28.22              else NONE
   28.23          | _ => NONE)
   28.24 -      end);
   28.25 +      end,
   28.26 +    identifier = []};
   28.27  
   28.28  fun get_upd_acc_cong_thm upd acc thy ss =
   28.29    let
   28.30 @@ -1139,10 +1144,12 @@
   28.31    we omit considering further updates if doing so would introduce
   28.32    both a more update and an update to a field within it.*)
   28.33  val upd_simproc =
   28.34 -  Simplifier.simproc_global @{theory HOL} "record_upd" ["x"]
   28.35 -    (fn ctxt => fn t =>
   28.36 +  Simplifier.make_simproc @{context} "record_upd"
   28.37 +   {lhss = [@{term "x"}],
   28.38 +    proc = fn _ => fn ctxt => fn ct =>
   28.39        let
   28.40          val thy = Proof_Context.theory_of ctxt;
   28.41 +        val t = Thm.term_of ct;
   28.42          (*We can use more-updators with other updators as long
   28.43            as none of the other updators go deeper than any more
   28.44            updator. min here is the depth of the deepest other
   28.45 @@ -1240,7 +1247,8 @@
   28.46              (prove_unfold_defs thy noops' [simproc]
   28.47                (Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
   28.48          else NONE
   28.49 -      end);
   28.50 +      end,
   28.51 +    identifier = []};
   28.52  
   28.53  end;
   28.54  
   28.55 @@ -1260,16 +1268,19 @@
   28.56   Complexity: #components * #updates     #updates
   28.57  *)
   28.58  val eq_simproc =
   28.59 -  Simplifier.simproc_global @{theory HOL} "record_eq" ["r = s"]
   28.60 -    (fn ctxt => fn t =>
   28.61 -      (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
   28.62 -        (case rec_id ~1 T of
   28.63 -          "" => NONE
   28.64 -        | name =>
   28.65 -            (case get_equalities (Proof_Context.theory_of ctxt) name of
   28.66 -              NONE => NONE
   28.67 -            | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
   28.68 -      | _ => NONE));
   28.69 +  Simplifier.make_simproc @{context} "record_eq"
   28.70 +   {lhss = [@{term "r = s"}],
   28.71 +    proc = fn _ => fn ctxt => fn ct =>
   28.72 +      (case Thm.term_of ct of
   28.73 +        Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
   28.74 +          (case rec_id ~1 T of
   28.75 +            "" => NONE
   28.76 +          | name =>
   28.77 +              (case get_equalities (Proof_Context.theory_of ctxt) name of
   28.78 +                NONE => NONE
   28.79 +              | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
   28.80 +      | _ => NONE),
   28.81 +    identifier = []};
   28.82  
   28.83  
   28.84  (* split_simproc *)
   28.85 @@ -1280,9 +1291,10 @@
   28.86      P t = ~1: completely split
   28.87      P t > 0: split up to given bound of record extensions.*)
   28.88  fun split_simproc P =
   28.89 -  Simplifier.simproc_global @{theory HOL} "record_split" ["x"]
   28.90 -    (fn ctxt => fn t =>
   28.91 -      (case t of
   28.92 +  Simplifier.make_simproc @{context} "record_split"
   28.93 +   {lhss = [@{term x}],
   28.94 +    proc = fn _ => fn ctxt => fn ct =>
   28.95 +      (case Thm.term_of ct of
   28.96          Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
   28.97            if quantifier = @{const_name Pure.all} orelse
   28.98              quantifier = @{const_name All} orelse
   28.99 @@ -1291,7 +1303,7 @@
  28.100              (case rec_id ~1 T of
  28.101                "" => NONE
  28.102              | _ =>
  28.103 -                let val split = P t in
  28.104 +                let val split = P (Thm.term_of ct) in
  28.105                    if split <> 0 then
  28.106                      (case get_splits (Proof_Context.theory_of ctxt) (rec_id split T) of
  28.107                        NONE => NONE
  28.108 @@ -1305,13 +1317,16 @@
  28.109                    else NONE
  28.110                  end)
  28.111            else NONE
  28.112 -      | _ => NONE));
  28.113 +      | _ => NONE),
  28.114 +    identifier = []};
  28.115  
  28.116  val ex_sel_eq_simproc =
  28.117 -  Simplifier.simproc_global @{theory HOL} "ex_sel_eq" ["Ex t"]
  28.118 -    (fn ctxt => fn t =>
  28.119 +  Simplifier.make_simproc @{context} "ex_sel_eq"
  28.120 +   {lhss = [@{term "Ex t"}],
  28.121 +    proc = fn _ => fn ctxt => fn ct =>
  28.122        let
  28.123          val thy = Proof_Context.theory_of ctxt;
  28.124 +        val t = Thm.term_of ct;
  28.125          fun mkeq (lr, Teq, (sel, Tsel), x) i =
  28.126            if is_selector thy sel then
  28.127              let
  28.128 @@ -1344,7 +1359,8 @@
  28.129                      addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
  28.130              end handle TERM _ => NONE)
  28.131          | _ => NONE)
  28.132 -      end);
  28.133 +      end,
  28.134 +    identifier = []};
  28.135  
  28.136  
  28.137  (* split_simp_tac *)
    29.1 --- a/src/HOL/Word/WordBitwise.thy	Wed Sep 09 14:47:41 2015 +0200
    29.2 +++ b/src/HOL/Word/WordBitwise.thy	Wed Sep 09 20:57:21 2015 +0200
    29.3 @@ -497,8 +497,8 @@
    29.4  text {* Tactic definition *}
    29.5  
    29.6  ML {*
    29.7 -
    29.8 -structure Word_Bitwise_Tac = struct
    29.9 +structure Word_Bitwise_Tac =
   29.10 +struct
   29.11  
   29.12  val word_ss = simpset_of @{theory_context Word};
   29.13  
   29.14 @@ -523,10 +523,9 @@
   29.15        end
   29.16    | _ => NONE;
   29.17  
   29.18 -val expand_upt_simproc = Simplifier.make_simproc
   29.19 -  {lhss = [@{cpat "upt _ _"}],
   29.20 -   name = "expand_upt", identifier = [],
   29.21 -   proc = K upt_conv};
   29.22 +val expand_upt_simproc =
   29.23 +  Simplifier.make_simproc @{context} "expand_upt"
   29.24 +   {lhss = [@{term "upt x y"}], proc = K upt_conv, identifier = []};
   29.25  
   29.26  fun word_len_simproc_fn ctxt ct =
   29.27    case Thm.term_of ct of
   29.28 @@ -540,10 +539,9 @@
   29.29      handle TERM _ => NONE | TYPE _ => NONE)
   29.30    | _ => NONE;
   29.31  
   29.32 -val word_len_simproc = Simplifier.make_simproc
   29.33 -  {lhss = [@{cpat "len_of _"}],
   29.34 -   name = "word_len", identifier = [],
   29.35 -   proc = K word_len_simproc_fn};
   29.36 +val word_len_simproc =
   29.37 +  Simplifier.make_simproc @{context} "word_len"
   29.38 +   {lhss = [@{term "len_of x"}], proc = K word_len_simproc_fn, identifier = []};
   29.39  
   29.40  (* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2,
   29.41     or just 5 (discarding nat) when n_sucs = 0 *)
   29.42 @@ -567,10 +565,10 @@
   29.43         |> mk_meta_eq |> SOME end
   29.44      handle TERM _ => NONE;
   29.45  
   29.46 -fun nat_get_Suc_simproc n_sucs cts = Simplifier.make_simproc
   29.47 -  {lhss = map (fn t => Thm.apply t @{cpat "?n :: nat"}) cts,
   29.48 -   name = "nat_get_Suc", identifier = [],
   29.49 -   proc = K (nat_get_Suc_simproc_fn n_sucs)};
   29.50 +fun nat_get_Suc_simproc n_sucs ts =
   29.51 +  Simplifier.make_simproc @{context} "nat_get_Suc"
   29.52 +   {lhss = map (fn t => t $ @{term "n :: nat"}) ts,
   29.53 +    proc = K (nat_get_Suc_simproc_fn n_sucs), identifier = []};
   29.54  
   29.55  val no_split_ss =
   29.56    simpset_of (put_simpset HOL_ss @{context}
   29.57 @@ -601,10 +599,10 @@
   29.58                                  rev_bl_order_simps}
   29.59            addsimprocs [expand_upt_simproc,
   29.60                         nat_get_Suc_simproc 4
   29.61 -                         [@{cpat replicate}, @{cpat "takefill ?x"},
   29.62 -                          @{cpat drop}, @{cpat "bin_to_bl"},
   29.63 -                          @{cpat "takefill_last ?x"},
   29.64 -                          @{cpat "drop_nonempty ?x"}]],
   29.65 +                         [@{term replicate}, @{term "takefill x"},
   29.66 +                          @{term drop}, @{term "bin_to_bl"},
   29.67 +                          @{term "takefill_last x"},
   29.68 +                          @{term "drop_nonempty x"}]],
   29.69      put_simpset no_split_ss @{context} addsimps @{thms xor3_simps carry_simps if_bool_simps}
   29.70    ])
   29.71  
    30.1 --- a/src/Provers/Arith/cancel_numeral_factor.ML	Wed Sep 09 14:47:41 2015 +0200
    30.2 +++ b/src/Provers/Arith/cancel_numeral_factor.ML	Wed Sep 09 20:57:21 2015 +0200
    30.3 @@ -37,16 +37,14 @@
    30.4  
    30.5  
    30.6  functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
    30.7 -  sig
    30.8 -  val proc: Proof.context -> term -> thm option
    30.9 -  end
   30.10 -=
   30.11 +  sig val proc: Proof.context -> cterm -> thm option end =
   30.12  struct
   30.13  
   30.14  (*the simplification procedure*)
   30.15 -fun proc ctxt t =
   30.16 +fun proc ctxt ct =
   30.17    let
   30.18      val prems = Simplifier.prems_of ctxt;
   30.19 +    val t = Thm.term_of ct;
   30.20      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
   30.21      val export = singleton (Variable.export ctxt' ctxt)
   30.22      (* FIXME ctxt vs. ctxt' *)
    31.1 --- a/src/Provers/Arith/cancel_numerals.ML	Wed Sep 09 14:47:41 2015 +0200
    31.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Wed Sep 09 20:57:21 2015 +0200
    31.3 @@ -44,7 +44,7 @@
    31.4  
    31.5  signature CANCEL_NUMERALS =
    31.6  sig
    31.7 -  val proc: Proof.context -> term -> thm option
    31.8 +  val proc: Proof.context -> cterm -> thm option
    31.9  end;
   31.10  
   31.11  functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
   31.12 @@ -65,9 +65,10 @@
   31.13    in  seek terms1 end;
   31.14  
   31.15  (*the simplification procedure*)
   31.16 -fun proc ctxt t =
   31.17 +fun proc ctxt ct =
   31.18    let
   31.19      val prems = Simplifier.prems_of ctxt
   31.20 +    val t = Thm.term_of ct
   31.21      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
   31.22      val export = singleton (Variable.export ctxt' ctxt)
   31.23      (* FIXME ctxt vs. ctxt' (!?) *)
    32.1 --- a/src/Provers/Arith/combine_numerals.ML	Wed Sep 09 14:47:41 2015 +0200
    32.2 +++ b/src/Provers/Arith/combine_numerals.ML	Wed Sep 09 20:57:21 2015 +0200
    32.3 @@ -38,7 +38,7 @@
    32.4  
    32.5  functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
    32.6    sig
    32.7 -  val proc: Proof.context -> term -> thm option
    32.8 +  val proc: Proof.context -> cterm -> thm option
    32.9    end
   32.10  =
   32.11  struct
   32.12 @@ -65,8 +65,9 @@
   32.13          | NONE => find_repeated (tab, t::past, terms);
   32.14  
   32.15  (*the simplification procedure*)
   32.16 -fun proc ctxt t =
   32.17 +fun proc ctxt ct =
   32.18    let
   32.19 +    val t = Thm.term_of ct
   32.20      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
   32.21      val export = singleton (Variable.export ctxt' ctxt)
   32.22      (* FIXME ctxt vs. ctxt' (!?) *)
    33.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Sep 09 14:47:41 2015 +0200
    33.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Sep 09 20:57:21 2015 +0200
    33.3 @@ -87,7 +87,7 @@
    33.4  sig
    33.5    val prems_lin_arith_tac: Proof.context -> int -> tactic
    33.6    val lin_arith_tac: Proof.context -> int -> tactic
    33.7 -  val lin_arith_simproc: Proof.context -> term -> thm option
    33.8 +  val lin_arith_simproc: Proof.context -> cterm -> thm option
    33.9    val map_data:
   33.10      ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
   33.11        lessD: thm list, neqE: thm list, simpset: simpset,
   33.12 @@ -775,7 +775,7 @@
   33.13    let
   33.14      val thms = maps LA_Logic.atomize (Simplifier.prems_of ctxt)
   33.15      val Hs = map Thm.prop_of thms
   33.16 -    val Tconcl = LA_Logic.mk_Trueprop concl
   33.17 +    val Tconcl = LA_Logic.mk_Trueprop (Thm.term_of concl)
   33.18    in
   33.19      case prove ctxt [] false Hs Tconcl of (* concl provable? *)
   33.20        (split_neq, SOME js) => prover ctxt thms Tconcl js split_neq true
    34.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Sep 09 14:47:41 2015 +0200
    34.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Sep 09 20:57:21 2015 +0200
    34.3 @@ -168,8 +168,9 @@
    34.4    ML_Lex.read_source false source
    34.5    |> ML_Context.expression (Input.range_of source) "proc"
    34.6      "Morphism.morphism -> Proof.context -> cterm -> thm option"
    34.7 -    ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
    34.8 -      \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
    34.9 +    ("Context.map_proof (Simplifier.define_simproc_cmd " ^
   34.10 +      ML_Syntax.atomic (ML_Syntax.make_binding name) ^
   34.11 +      "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
   34.12        \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
   34.13    |> Context.proof_map;
   34.14  
    35.1 --- a/src/Pure/raw_simplifier.ML	Wed Sep 09 14:47:41 2015 +0200
    35.2 +++ b/src/Pure/raw_simplifier.ML	Wed Sep 09 20:57:21 2015 +0200
    35.3 @@ -35,10 +35,10 @@
    35.4      safe_solvers: string list}
    35.5    type simproc
    35.6    val eq_simproc: simproc * simproc -> bool
    35.7 +  val cert_simproc: theory -> string ->
    35.8 +    {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list}
    35.9 +    -> simproc
   35.10    val transform_simproc: morphism -> simproc -> simproc
   35.11 -  val make_simproc: {name: string, lhss: cterm list,
   35.12 -    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} -> simproc
   35.13 -  val mk_simproc: string -> cterm list -> (Proof.context -> term -> thm option) -> simproc
   35.14    val simpset_of: Proof.context -> simpset
   35.15    val put_simpset: simpset -> Proof.context -> Proof.context
   35.16    val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset
   35.17 @@ -105,10 +105,6 @@
   35.18    val solver: Proof.context -> solver -> int -> tactic
   35.19    val simp_depth_limit_raw: Config.raw
   35.20    val default_mk_sym: Proof.context -> thm -> thm option
   35.21 -  val simproc_global_i: theory -> string -> term list ->
   35.22 -    (Proof.context -> term -> thm option) -> simproc
   35.23 -  val simproc_global: theory -> string -> string list ->
   35.24 -    (Proof.context -> term -> thm option) -> simproc
   35.25    val simp_trace_depth_limit_raw: Config.raw
   35.26    val simp_trace_raw: Config.raw
   35.27    val simp_debug_raw: Config.raw
   35.28 @@ -675,6 +671,10 @@
   35.29  
   35.30  fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
   35.31  
   35.32 +fun cert_simproc thy name {lhss, proc, identifier} =
   35.33 +  Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc,
   35.34 +    id = (stamp (), map Thm.trim_context identifier)};
   35.35 +
   35.36  fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
   35.37    Simproc
   35.38     {name = name,
   35.39 @@ -682,19 +682,6 @@
   35.40      proc = Morphism.transform phi proc,
   35.41      id = (s, Morphism.fact phi ths)};
   35.42  
   35.43 -fun make_simproc {name, lhss, proc, identifier} =
   35.44 -  Simproc {name = name, lhss = map Thm.term_of lhss, proc = proc,
   35.45 -    id = (stamp (), map Thm.trim_context identifier)};
   35.46 -
   35.47 -fun mk_simproc name lhss proc =
   35.48 -  make_simproc {name = name, lhss = lhss, proc = fn _ => fn ctxt => fn ct =>
   35.49 -    proc ctxt (Thm.term_of ct), identifier = []};
   35.50 -
   35.51 -(* FIXME avoid global thy and Logic.varify_global *)
   35.52 -fun simproc_global_i thy name = mk_simproc name o map (Thm.global_cterm_of thy o Logic.varify_global);
   35.53 -fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy);
   35.54 -
   35.55 -
   35.56  local
   35.57  
   35.58  fun add_proc (proc as Proc {name, lhs, ...}) ctxt =
    36.1 --- a/src/Pure/simplifier.ML	Wed Sep 09 14:47:41 2015 +0200
    36.2 +++ b/src/Pure/simplifier.ML	Wed Sep 09 20:57:21 2015 +0200
    36.3 @@ -36,12 +36,11 @@
    36.4    val cong_del: attribute
    36.5    val check_simproc: Proof.context -> xstring * Position.T -> string
    36.6    val the_simproc: Proof.context -> string -> simproc
    36.7 -  val def_simproc: {name: binding, lhss: term list,
    36.8 -    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
    36.9 -    local_theory -> local_theory
   36.10 -  val def_simproc_cmd: {name: binding, lhss: string list,
   36.11 -    proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list} ->
   36.12 -    local_theory -> local_theory
   36.13 +  type 'a simproc_spec =
   36.14 +    {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list}
   36.15 +  val make_simproc: Proof.context -> string -> term simproc_spec -> simproc
   36.16 +  val define_simproc: binding -> term simproc_spec -> local_theory -> local_theory
   36.17 +  val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory
   36.18    val pretty_simpset: bool -> Proof.context -> Pretty.T
   36.19    val default_mk_sym: Proof.context -> thm -> thm option
   36.20    val prems_of: Proof.context -> thm list
   36.21 @@ -61,10 +60,6 @@
   36.22    val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
   36.23    type trace_ops
   36.24    val set_trace_ops: trace_ops -> theory -> theory
   36.25 -  val simproc_global_i: theory -> string -> term list ->
   36.26 -    (Proof.context -> term -> thm option) -> simproc
   36.27 -  val simproc_global: theory -> string -> string list ->
   36.28 -    (Proof.context -> term -> thm option) -> simproc
   36.29    val rewrite: Proof.context -> conv
   36.30    val asm_rewrite: Proof.context -> conv
   36.31    val full_rewrite: Proof.context -> conv
   36.32 @@ -122,19 +117,25 @@
   36.33  
   36.34  (* define simprocs *)
   36.35  
   36.36 +type 'a simproc_spec =
   36.37 +  {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list};
   36.38 +
   36.39 +fun make_simproc ctxt name {lhss, proc, identifier} =
   36.40 +  let
   36.41 +    val ctxt' = fold Variable.auto_fixes lhss ctxt;
   36.42 +    val lhss' = Variable.export_terms ctxt' ctxt lhss;
   36.43 +  in
   36.44 +    cert_simproc (Proof_Context.theory_of ctxt) name
   36.45 +      {lhss = lhss', proc = proc, identifier = identifier}
   36.46 +  end;
   36.47 +
   36.48  local
   36.49  
   36.50 -fun gen_simproc prep {name = b, lhss, proc, identifier} lthy =
   36.51 +fun def_simproc prep b {lhss, proc, identifier} lthy =
   36.52    let
   36.53 -    val simproc = make_simproc
   36.54 -      {name = Local_Theory.full_name lthy b,
   36.55 -       lhss =
   36.56 -        let
   36.57 -          val lhss' = prep lthy lhss;
   36.58 -          val ctxt' = fold Variable.auto_fixes lhss' lthy;
   36.59 -        in Variable.export_terms ctxt' lthy lhss' end |> map (Thm.cterm_of lthy),
   36.60 -       proc = proc,
   36.61 -       identifier = identifier};
   36.62 +    val simproc =
   36.63 +      make_simproc lthy (Local_Theory.full_name lthy b)
   36.64 +        {lhss = prep lthy lhss, proc = proc, identifier = identifier};
   36.65    in
   36.66      lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
   36.67        let
   36.68 @@ -149,8 +150,8 @@
   36.69  
   36.70  in
   36.71  
   36.72 -val def_simproc = gen_simproc Syntax.check_terms;
   36.73 -val def_simproc_cmd = gen_simproc Syntax.read_terms;
   36.74 +val define_simproc = def_simproc Syntax.check_terms;
   36.75 +val define_simproc_cmd = def_simproc Syntax.read_terms;
   36.76  
   36.77  end;
   36.78  
    37.1 --- a/src/Tools/induct.ML	Wed Sep 09 14:47:41 2015 +0200
    37.2 +++ b/src/Tools/induct.ML	Wed Sep 09 20:57:21 2015 +0200
    37.3 @@ -158,8 +158,10 @@
    37.4    | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct));
    37.5  
    37.6  val rearrange_eqs_simproc =
    37.7 -  Simplifier.simproc_global Pure.thy "rearrange_eqs" ["Pure.all t"]
    37.8 -    (fn ctxt => fn t => mk_swap_rrule ctxt (Thm.cterm_of ctxt t));
    37.9 +  Simplifier.make_simproc @{context} "rearrange_eqs"
   37.10 +   {lhss = [@{term "Pure.all(t)"}],
   37.11 +    proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct,
   37.12 +    identifier = []};
   37.13  
   37.14  
   37.15  (* rotate k premises to the left by j, skipping over first j premises *)
    38.1 --- a/src/ZF/Datatype_ZF.thy	Wed Sep 09 14:47:41 2015 +0200
    38.2 +++ b/src/ZF/Datatype_ZF.thy	Wed Sep 09 20:57:21 2015 +0200
    38.3 @@ -70,8 +70,9 @@
    38.4  
    38.5   val datatype_ss = simpset_of @{context};
    38.6  
    38.7 - fun proc ctxt old =
    38.8 -   let val thy = Proof_Context.theory_of ctxt
    38.9 + fun proc ctxt ct =
   38.10 +   let val old = Thm.term_of ct
   38.11 +       val thy = Proof_Context.theory_of ctxt
   38.12         val _ =
   38.13           if !trace then writeln ("data_free: OLD = " ^ Syntax.string_of_term ctxt old)
   38.14           else ()
   38.15 @@ -104,7 +105,9 @@
   38.16     handle Match => NONE;
   38.17  
   38.18  
   38.19 - val conv = Simplifier.simproc_global @{theory} "data_free" ["(x::i) = y"] proc;
   38.20 +  val conv =
   38.21 +    Simplifier.make_simproc @{context} "data_free"
   38.22 +     {lhss = [@{term "(x::i) = y"}], proc = K proc, identifier = []};
   38.23  
   38.24  end;
   38.25  \<close>
    39.1 --- a/src/ZF/arith_data.ML	Wed Sep 09 14:47:41 2015 +0200
    39.2 +++ b/src/ZF/arith_data.ML	Wed Sep 09 20:57:21 2015 +0200
    39.3 @@ -76,9 +76,6 @@
    39.4          (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
    39.5    end;
    39.6  
    39.7 -fun prep_simproc thy (name, pats, proc) =
    39.8 -  Simplifier.simproc_global thy name pats proc;
    39.9 -
   39.10  
   39.11  (*** Use CancelNumerals simproc without binary numerals,
   39.12       just for cancellation ***)
   39.13 @@ -202,22 +199,24 @@
   39.14  
   39.15  
   39.16  val nat_cancel =
   39.17 -  map (prep_simproc @{theory})
   39.18 -   [("nateq_cancel_numerals",
   39.19 -     ["l #+ m = n", "l = m #+ n",
   39.20 -      "l #* m = n", "l = m #* n",
   39.21 -      "succ(m) = n", "m = succ(n)"],
   39.22 -     EqCancelNumerals.proc),
   39.23 -    ("natless_cancel_numerals",
   39.24 -     ["l #+ m < n", "l < m #+ n",
   39.25 -      "l #* m < n", "l < m #* n",
   39.26 -      "succ(m) < n", "m < succ(n)"],
   39.27 -     LessCancelNumerals.proc),
   39.28 -    ("natdiff_cancel_numerals",
   39.29 -     ["(l #+ m) #- n", "l #- (m #+ n)",
   39.30 -      "(l #* m) #- n", "l #- (m #* n)",
   39.31 -      "succ(m) #- n", "m #- succ(n)"],
   39.32 -     DiffCancelNumerals.proc)];
   39.33 + [Simplifier.make_simproc @{context} "nateq_cancel_numerals"
   39.34 +   {lhss =
   39.35 +     [@{term "l #+ m = n"}, @{term "l = m #+ n"},
   39.36 +      @{term "l #* m = n"}, @{term "l = m #* n"},
   39.37 +      @{term "succ(m) = n"}, @{term "m = succ(n)"}],
   39.38 +    proc = K EqCancelNumerals.proc, identifier = []},
   39.39 +  Simplifier.make_simproc @{context} "natless_cancel_numerals"
   39.40 +   {lhss =
   39.41 +     [@{term "l #+ m < n"}, @{term "l < m #+ n"},
   39.42 +      @{term "l #* m < n"}, @{term "l < m #* n"},
   39.43 +      @{term "succ(m) < n"}, @{term "m < succ(n)"}],
   39.44 +    proc = K LessCancelNumerals.proc, identifier = []},
   39.45 +  Simplifier.make_simproc @{context} "natdiff_cancel_numerals"
   39.46 +   {lhss =
   39.47 +     [@{term "(l #+ m) #- n"}, @{term "l #- (m #+ n)"},
   39.48 +      @{term "(l #* m) #- n"}, @{term "l #- (m #* n)"},
   39.49 +      @{term "succ(m) #- n"}, @{term "m #- succ(n)"}],
   39.50 +    proc = K DiffCancelNumerals.proc, identifier = []}];
   39.51  
   39.52  end;
   39.53  
    40.1 --- a/src/ZF/int_arith.ML	Wed Sep 09 14:47:41 2015 +0200
    40.2 +++ b/src/ZF/int_arith.ML	Wed Sep 09 20:57:21 2015 +0200
    40.3 @@ -146,9 +146,6 @@
    40.4  val int_mult_minus_simps =
    40.5      [@{thm zmult_assoc}, @{thm zmult_zminus} RS @{thm sym}, int_minus_mult_eq_1_to_2];
    40.6  
    40.7 -fun prep_simproc thy (name, pats, proc) =
    40.8 -  Simplifier.simproc_global thy name pats proc;
    40.9 -
   40.10  structure CancelNumeralsCommon =
   40.11    struct
   40.12    val mk_sum = (fn _ : typ => mk_sum)
   40.13 @@ -210,22 +207,24 @@
   40.14  );
   40.15  
   40.16  val cancel_numerals =
   40.17 -  map (prep_simproc @{theory})
   40.18 -   [("inteq_cancel_numerals",
   40.19 -     ["l $+ m = n", "l = m $+ n",
   40.20 -      "l $- m = n", "l = m $- n",
   40.21 -      "l $* m = n", "l = m $* n"],
   40.22 -     EqCancelNumerals.proc),
   40.23 -    ("intless_cancel_numerals",
   40.24 -     ["l $+ m $< n", "l $< m $+ n",
   40.25 -      "l $- m $< n", "l $< m $- n",
   40.26 -      "l $* m $< n", "l $< m $* n"],
   40.27 -     LessCancelNumerals.proc),
   40.28 -    ("intle_cancel_numerals",
   40.29 -     ["l $+ m $<= n", "l $<= m $+ n",
   40.30 -      "l $- m $<= n", "l $<= m $- n",
   40.31 -      "l $* m $<= n", "l $<= m $* n"],
   40.32 -     LeCancelNumerals.proc)];
   40.33 + [Simplifier.make_simproc @{context} "inteq_cancel_numerals"
   40.34 +   {lhss =
   40.35 +     [@{term "l $+ m = n"}, @{term "l = m $+ n"},
   40.36 +      @{term "l $- m = n"}, @{term "l = m $- n"},
   40.37 +      @{term "l $* m = n"}, @{term "l = m $* n"}],
   40.38 +    proc = K EqCancelNumerals.proc, identifier = []},
   40.39 +  Simplifier.make_simproc @{context} "intless_cancel_numerals"
   40.40 +   {lhss =
   40.41 +     [@{term "l $+ m $< n"}, @{term "l $< m $+ n"},
   40.42 +      @{term "l $- m $< n"}, @{term "l $< m $- n"},
   40.43 +      @{term "l $* m $< n"}, @{term "l $< m $* n"}],
   40.44 +    proc = K LessCancelNumerals.proc, identifier = []},
   40.45 +  Simplifier.make_simproc @{context} "intle_cancel_numerals"
   40.46 +   {lhss =
   40.47 +     [@{term "l $+ m $<= n"}, @{term "l $<= m $+ n"},
   40.48 +      @{term "l $- m $<= n"}, @{term "l $<= m $- n"},
   40.49 +      @{term "l $* m $<= n"}, @{term "l $<= m $* n"}],
   40.50 +    proc = K LeCancelNumerals.proc, identifier = []}];
   40.51  
   40.52  
   40.53  (*version without the hyps argument*)
   40.54 @@ -268,8 +267,9 @@
   40.55  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   40.56  
   40.57  val combine_numerals =
   40.58 -  prep_simproc @{theory}
   40.59 -    ("int_combine_numerals", ["i $+ j", "i $- j"], CombineNumerals.proc);
   40.60 +  Simplifier.make_simproc @{context} "int_combine_numerals"
   40.61 +    {lhss = [@{term "i $+ j"}, @{term "i $- j"}],
   40.62 +     proc = K CombineNumerals.proc, identifier = []};
   40.63  
   40.64  
   40.65  
   40.66 @@ -314,8 +314,8 @@
   40.67  structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
   40.68  
   40.69  val combine_numerals_prod =
   40.70 -  prep_simproc @{theory}
   40.71 -    ("int_combine_numerals_prod", ["i $* j"], CombineNumeralsProd.proc);
   40.72 +  Simplifier.make_simproc @{context} "int_combine_numerals_prod"
   40.73 +   {lhss = [@{term "i $* j"}], proc = K CombineNumeralsProd.proc, identifier = []};
   40.74  
   40.75  end;
   40.76