1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Wed Jun 29 16:31:50 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Jun 29 17:35:46 2011 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4            @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
     1.5            Suc_eq_plus1]
     1.6        addsimps @{thms add_ac}
     1.7 -      addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
     1.8 +      addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     1.9      val simpset0 = HOL_basic_ss
    1.10        addsimps [mod_div_equality', Suc_eq_plus1]
    1.11        addsimps comp_arith

     2.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Wed Jun 29 16:31:50 2011 +0200
     2.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Wed Jun 29 17:35:46 2011 +0200
     2.3 @@ -104,7 +104,7 @@
     2.4                                    @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
     2.5                                    @{thm "Suc_eq_plus1"}]
     2.6                          addsimps @{thms add_ac}
     2.7 -                        addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
     2.8 +                        addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     2.9      val simpset0 = HOL_basic_ss
    2.10        addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
    2.11        addsimps comp_ths

     3.1 --- a/src/HOL/Divides.thy	Wed Jun 29 16:31:50 2011 +0200
     3.2 +++ b/src/HOL/Divides.thy	Wed Jun 29 17:35:46 2011 +0200
     3.3 @@ -679,9 +679,7 @@
     3.4  text {* Simproc for cancelling @{const div} and @{const mod} *}
     3.5  
     3.6  ML {*
     3.7 -local
     3.8 -
     3.9 -structure CancelDivMod = CancelDivModFun
    3.10 +structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
    3.11  (
    3.12    val div_name = @{const_name div};
    3.13    val mod_name = @{const_name mod};
    3.14 @@ -694,17 +692,10 @@
    3.15    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
    3.16      (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
    3.17  )
    3.18 -
    3.19 -in
    3.20 -
    3.21 -val cancel_div_mod_nat_proc = Simplifier.simproc_global @{theory}
    3.22 -  "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
    3.23 -
    3.24 -val _ = Addsimprocs [cancel_div_mod_nat_proc];
    3.25 -
    3.26 -end
    3.27  *}
    3.28  
    3.29 +simproc_setup cancel_div_mod_nat ("(m::nat) + n") = {* K Cancel_Div_Mod_Nat.proc *}
    3.30 +
    3.31  
    3.32  subsubsection {* Quotient *}
    3.33  
    3.34 @@ -1437,9 +1428,7 @@
    3.35  text {* Tool setup *}
    3.36  
    3.37  ML {*
    3.38 -local
    3.39 -
    3.40 -structure CancelDivMod = CancelDivModFun
    3.41 +structure Cancel_Div_Mod_Int = Cancel_Div_Mod
    3.42  (
    3.43    val div_name = @{const_name div};
    3.44    val mod_name = @{const_name mod};
    3.45 @@ -1452,17 +1441,10 @@
    3.46    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
    3.47      (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
    3.48  )
    3.49 -
    3.50 -in
    3.51 -
    3.52 -val cancel_div_mod_int_proc = Simplifier.simproc_global @{theory}
    3.53 -  "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
    3.54 -
    3.55 -val _ = Addsimprocs [cancel_div_mod_int_proc];
    3.56 -
    3.57 -end
    3.58  *}
    3.59  
    3.60 +simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}
    3.61 +
    3.62  lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
    3.63  apply (cut_tac a = a and b = b in divmod_int_correct)
    3.64  apply (auto simp add: divmod_int_rel_def mod_int_def)

     4.1 --- a/src/HOL/List.thy	Wed Jun 29 16:31:50 2011 +0200
     4.2 +++ b/src/HOL/List.thy	Wed Jun 29 17:35:46 2011 +0200
     4.3 @@ -726,54 +726,44 @@
     4.4  - or both lists end in the same list.
     4.5  *}
     4.6  
     4.7 -ML {*
     4.8 -local
     4.9 -
    4.10 -fun last (cons as Const(@{const_name Cons},_) $ _ $ xs) =
    4.11 -  (case xs of Const(@{const_name Nil},_) => cons | _ => last xs)
    4.12 -  | last (Const(@{const_name append},_) $ _ $ ys) = last ys
    4.13 -  | last t = t;
    4.14 -
    4.15 -fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
    4.16 -  | list1 _ = false;
    4.17 -
    4.18 -fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
    4.19 -  (case xs of Const(@{const_name Nil},_) => xs | _ => cons $ butlast xs)
    4.20 -  | butlast ((app as Const(@{const_name append},_) $ xs) $ ys) = app $ butlast ys
    4.21 -  | butlast xs = Const(@{const_name Nil},fastype_of xs);
    4.22 -
    4.23 -val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
    4.24 -  @{thm append_Nil}, @{thm append_Cons}];
    4.25 -
    4.26 -fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    4.27 +simproc_setup list_eq ("(xs::'a list) = ys")  = {*
    4.28    let
    4.29 -    val lastl = last lhs and lastr = last rhs;
    4.30 -    fun rearr conv =
    4.31 +    fun last (cons as Const (@{const_name Cons}, _) $ _ $ xs) =
    4.32 +          (case xs of Const (@{const_name Nil}, _) => cons | _ => last xs)
    4.33 +      | last (Const(@{const_name append},_) $ _ $ ys) = last ys
    4.34 +      | last t = t;
    4.35 +    
    4.36 +    fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
    4.37 +      | list1 _ = false;
    4.38 +    
    4.39 +    fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
    4.40 +          (case xs of Const (@{const_name Nil}, _) => xs | _ => cons $ butlast xs)
    4.41 +      | butlast ((app as Const (@{const_name append}, _) $ xs) $ ys) = app $ butlast ys
    4.42 +      | butlast xs = Const(@{const_name Nil}, fastype_of xs);
    4.43 +    
    4.44 +    val rearr_ss =
    4.45 +      HOL_basic_ss addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}];
    4.46 +    
    4.47 +    fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    4.48        let
    4.49 -        val lhs1 = butlast lhs and rhs1 = butlast rhs;
    4.50 -        val Type(_,listT::_) = eqT
    4.51 -        val appT = [listT,listT] ---> listT
    4.52 -        val app = Const(@{const_name append},appT)
    4.53 -        val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    4.54 -        val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
    4.55 -        val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
    4.56 -          (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
    4.57 -      in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
    4.58 -
    4.59 -  in
    4.60 -    if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
    4.61 -    else if lastl aconv lastr then rearr @{thm append_same_eq}
    4.62 -    else NONE
    4.63 -  end;
    4.64 -
    4.65 -in
    4.66 -
    4.67 -val list_eq_simproc =
    4.68 -  Simplifier.simproc_global @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
    4.69 -
    4.70 -end;
    4.71 -
    4.72 -Addsimprocs [list_eq_simproc];
    4.73 +        val lastl = last lhs and lastr = last rhs;
    4.74 +        fun rearr conv =
    4.75 +          let
    4.76 +            val lhs1 = butlast lhs and rhs1 = butlast rhs;
    4.77 +            val Type(_,listT::_) = eqT
    4.78 +            val appT = [listT,listT] ---> listT
    4.79 +            val app = Const(@{const_name append},appT)
    4.80 +            val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    4.81 +            val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
    4.82 +            val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
    4.83 +              (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
    4.84 +          in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
    4.85 +      in
    4.86 +        if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
    4.87 +        else if lastl aconv lastr then rearr @{thm append_same_eq}
    4.88 +        else NONE
    4.89 +      end;
    4.90 +  in fn _ => fn ss => fn ct => list_eq ss (term_of ct) end;
    4.91  *}
    4.92  
    4.93  

     5.1 --- a/src/HOL/Product_Type.thy	Wed Jun 29 16:31:50 2011 +0200
     5.2 +++ b/src/HOL/Product_Type.thy	Wed Jun 29 17:35:46 2011 +0200
     5.3 @@ -55,14 +55,10 @@
     5.4    this rule directly --- it loops!
     5.5  *}
     5.6  
     5.7 -ML {*
     5.8 -  val unit_eq_proc =
     5.9 -    let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
    5.10 -      Simplifier.simproc_global @{theory} "unit_eq" ["x::unit"]
    5.11 -      (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
    5.12 -    end;
    5.13 -
    5.14 -  Addsimprocs [unit_eq_proc];
    5.15 +simproc_setup unit_eq ("x::unit") = {*
    5.16 +  fn _ => fn _ => fn ct =>
    5.17 +    if HOLogic.is_unit (term_of ct) then NONE
    5.18 +    else SOME (mk_meta_eq @{thm unit_eq})
    5.19  *}
    5.20  
    5.21  rep_datatype "()" by simp
    5.22 @@ -74,7 +70,7 @@
    5.23    by (rule triv_forall_equality)
    5.24  
    5.25  text {*
    5.26 -  This rewrite counters the effect of @{text unit_eq_proc} on @{term
    5.27 +  This rewrite counters the effect of simproc @{text unit_eq} on @{term
    5.28    [source] "%u::unit. f u"}, replacing it by @{term [source]
    5.29    f} rather than by @{term [source] "%u. f ()"}.
    5.30  *}
    5.31 @@ -497,7 +493,7 @@
    5.32        | exists_paired_all _ = false;
    5.33      val ss = HOL_basic_ss
    5.34        addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}]
    5.35 -      addsimprocs [unit_eq_proc];
    5.36 +      addsimprocs [@{simproc unit_eq}];
    5.37    in
    5.38      val split_all_tac = SUBGOAL (fn (t, i) =>
    5.39        if exists_paired_all t then safe_full_simp_tac ss i else no_tac);

     6.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Jun 29 16:31:50 2011 +0200
     6.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Jun 29 17:35:46 2011 +0200
     6.3 @@ -805,7 +805,7 @@
     6.4       @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
     6.5       @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
     6.6    @ @{thms add_ac}
     6.7 - addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
     6.8 + addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     6.9   val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
    6.10       [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
    6.11        @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]

     7.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Wed Jun 29 16:31:50 2011 +0200
     7.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Wed Jun 29 17:35:46 2011 +0200
     7.3 @@ -27,11 +27,11 @@
     7.4  
     7.5  signature CANCEL_DIV_MOD =
     7.6  sig
     7.7 -  val proc: simpset -> term -> thm option
     7.8 +  val proc: simpset -> cterm -> thm option
     7.9  end;
    7.10  
    7.11  
    7.12 -functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
    7.13 +functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
    7.14  struct
    7.15  
    7.16  fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms =
    7.17 @@ -70,12 +70,16 @@
    7.18    let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
    7.19    in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
    7.20  
    7.21 -fun proc ss t =
    7.22 -  let val (divs,mods) = coll_div_mod t ([],[])
    7.23 -  in if null divs orelse null mods then NONE
    7.24 -     else case inter (op =) mods divs of
    7.25 -            pq :: _ => SOME (cancel ss t pq)
    7.26 -          | [] => NONE
    7.27 -  end
    7.28 +fun proc ss ct =
    7.29 +  let
    7.30 +    val t = term_of ct;
    7.31 +    val (divs, mods) = coll_div_mod t ([], []);
    7.32 +  in
    7.33 +    if null divs orelse null mods then NONE
    7.34 +    else
    7.35 +      (case inter (op =) mods divs of
    7.36 +        pq :: _ => SOME (cancel ss t pq)
    7.37 +      | [] => NONE)
    7.38 +  end;
    7.39  
    7.40  end