# HG changeset patch
# User wenzelm
# Date 1309361746 -7200
# Node ID ef1ddc59b825071e957e184f2461aed202635c21
# Parent  11140987d4152282ef877a267316e8423d396d54
modernized some simproc setup;

diff -r 11140987d415 -r ef1ddc59b825 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Wed Jun 29 16:31:50 2011 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Jun 29 17:35:46 2011 +0200
@@ -82,7 +82,7 @@
           @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
           Suc_eq_plus1]
       addsimps @{thms add_ac}
-      addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
+      addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_eq_plus1]
       addsimps comp_arith
diff -r 11140987d415 -r ef1ddc59b825 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Wed Jun 29 16:31:50 2011 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Wed Jun 29 17:35:46 2011 +0200
@@ -104,7 +104,7 @@
                                   @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
                                   @{thm "Suc_eq_plus1"}]
                         addsimps @{thms add_ac}
-                        addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
+                        addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
       addsimps comp_ths
diff -r 11140987d415 -r ef1ddc59b825 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Jun 29 16:31:50 2011 +0200
+++ b/src/HOL/Divides.thy	Wed Jun 29 17:35:46 2011 +0200
@@ -679,9 +679,7 @@
 text {* Simproc for cancelling @{const div} and @{const mod} *}
 
 ML {*
-local
-
-structure CancelDivMod = CancelDivModFun
+structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
 (
   val div_name = @{const_name div};
   val mod_name = @{const_name mod};
@@ -694,17 +692,10 @@
   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
     (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
 )
-
-in
-
-val cancel_div_mod_nat_proc = Simplifier.simproc_global @{theory}
-  "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
-
-val _ = Addsimprocs [cancel_div_mod_nat_proc];
-
-end
 *}
 
+simproc_setup cancel_div_mod_nat ("(m::nat) + n") = {* K Cancel_Div_Mod_Nat.proc *}
+
 
 subsubsection {* Quotient *}
 
@@ -1437,9 +1428,7 @@
 text {* Tool setup *}
 
 ML {*
-local
-
-structure CancelDivMod = CancelDivModFun
+structure Cancel_Div_Mod_Int = Cancel_Div_Mod
 (
   val div_name = @{const_name div};
   val mod_name = @{const_name mod};
@@ -1452,17 +1441,10 @@
   val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
     (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
 )
-
-in
-
-val cancel_div_mod_int_proc = Simplifier.simproc_global @{theory}
-  "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
-
-val _ = Addsimprocs [cancel_div_mod_int_proc];
-
-end
 *}
 
+simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}
+
 lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
 apply (cut_tac a = a and b = b in divmod_int_correct)
 apply (auto simp add: divmod_int_rel_def mod_int_def)
diff -r 11140987d415 -r ef1ddc59b825 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jun 29 16:31:50 2011 +0200
+++ b/src/HOL/List.thy	Wed Jun 29 17:35:46 2011 +0200
@@ -726,54 +726,44 @@
 - or both lists end in the same list.
 *}
 
-ML {*
-local
-
-fun last (cons as Const(@{const_name Cons},_) $ _ $ xs) =
-  (case xs of Const(@{const_name Nil},_) => cons | _ => last xs)
-  | last (Const(@{const_name append},_) $ _ $ ys) = last ys
-  | last t = t;
-
-fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
-  | list1 _ = false;
-
-fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
-  (case xs of Const(@{const_name Nil},_) => xs | _ => cons $ butlast xs)
-  | butlast ((app as Const(@{const_name append},_) $ xs) $ ys) = app $ butlast ys
-  | butlast xs = Const(@{const_name Nil},fastype_of xs);
-
-val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
-  @{thm append_Nil}, @{thm append_Cons}];
-
-fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
+simproc_setup list_eq ("(xs::'a list) = ys")  = {*
   let
-    val lastl = last lhs and lastr = last rhs;
-    fun rearr conv =
+    fun last (cons as Const (@{const_name Cons}, _) $ _ $ xs) =
+          (case xs of Const (@{const_name Nil}, _) => cons | _ => last xs)
+      | last (Const(@{const_name append},_) $ _ $ ys) = last ys
+      | last t = t;
+    
+    fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
+      | list1 _ = false;
+    
+    fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
+          (case xs of Const (@{const_name Nil}, _) => xs | _ => cons $ butlast xs)
+      | butlast ((app as Const (@{const_name append}, _) $ xs) $ ys) = app $ butlast ys
+      | butlast xs = Const(@{const_name Nil}, fastype_of xs);
+    
+    val rearr_ss =
+      HOL_basic_ss addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}];
+    
+    fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
       let
-        val lhs1 = butlast lhs and rhs1 = butlast rhs;
-        val Type(_,listT::_) = eqT
-        val appT = [listT,listT] ---> listT
-        val app = Const(@{const_name append},appT)
-        val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
-        val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
-        val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
-          (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
-      in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
-
-  in
-    if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
-    else if lastl aconv lastr then rearr @{thm append_same_eq}
-    else NONE
-  end;
-
-in
-
-val list_eq_simproc =
-  Simplifier.simproc_global @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
-
-end;
-
-Addsimprocs [list_eq_simproc];
+        val lastl = last lhs and lastr = last rhs;
+        fun rearr conv =
+          let
+            val lhs1 = butlast lhs and rhs1 = butlast rhs;
+            val Type(_,listT::_) = eqT
+            val appT = [listT,listT] ---> listT
+            val app = Const(@{const_name append},appT)
+            val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
+            val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
+            val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
+              (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
+          in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
+      in
+        if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
+        else if lastl aconv lastr then rearr @{thm append_same_eq}
+        else NONE
+      end;
+  in fn _ => fn ss => fn ct => list_eq ss (term_of ct) end;
 *}
 
 
diff -r 11140987d415 -r ef1ddc59b825 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Jun 29 16:31:50 2011 +0200
+++ b/src/HOL/Product_Type.thy	Wed Jun 29 17:35:46 2011 +0200
@@ -55,14 +55,10 @@
   this rule directly --- it loops!
 *}
 
-ML {*
-  val unit_eq_proc =
-    let val unit_meta_eq = mk_meta_eq @{thm unit_eq} in
-      Simplifier.simproc_global @{theory} "unit_eq" ["x::unit"]
-      (fn _ => fn _ => fn t => if HOLogic.is_unit t then NONE else SOME unit_meta_eq)
-    end;
-
-  Addsimprocs [unit_eq_proc];
+simproc_setup unit_eq ("x::unit") = {*
+  fn _ => fn _ => fn ct =>
+    if HOLogic.is_unit (term_of ct) then NONE
+    else SOME (mk_meta_eq @{thm unit_eq})
 *}
 
 rep_datatype "()" by simp
@@ -74,7 +70,7 @@
   by (rule triv_forall_equality)
 
 text {*
-  This rewrite counters the effect of @{text unit_eq_proc} on @{term
+  This rewrite counters the effect of simproc @{text unit_eq} on @{term
   [source] "%u::unit. f u"}, replacing it by @{term [source]
   f} rather than by @{term [source] "%u. f ()"}.
 *}
@@ -497,7 +493,7 @@
       | exists_paired_all _ = false;
     val ss = HOL_basic_ss
       addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}]
-      addsimprocs [unit_eq_proc];
+      addsimprocs [@{simproc unit_eq}];
   in
     val split_all_tac = SUBGOAL (fn (t, i) =>
       if exists_paired_all t then safe_full_simp_tac ss i else no_tac);
diff -r 11140987d415 -r ef1ddc59b825 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Wed Jun 29 16:31:50 2011 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Jun 29 17:35:46 2011 +0200
@@ -805,7 +805,7 @@
      @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
      @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
   @ @{thms add_ac}
- addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
+ addsimprocs [@{simproc cancel_div_mod_nat}, @{simproc cancel_div_mod_int}]
  val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
      [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
       @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]
diff -r 11140987d415 -r ef1ddc59b825 src/Provers/Arith/cancel_div_mod.ML
--- a/src/Provers/Arith/cancel_div_mod.ML	Wed Jun 29 16:31:50 2011 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML	Wed Jun 29 17:35:46 2011 +0200
@@ -27,11 +27,11 @@
 
 signature CANCEL_DIV_MOD =
 sig
-  val proc: simpset -> term -> thm option
+  val proc: simpset -> cterm -> thm option
 end;
 
 
-functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
+functor Cancel_Div_Mod(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
 struct
 
 fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms =
@@ -70,12 +70,16 @@
   let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
   in hd (Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
 
-fun proc ss t =
-  let val (divs,mods) = coll_div_mod t ([],[])
-  in if null divs orelse null mods then NONE
-     else case inter (op =) mods divs of
-            pq :: _ => SOME (cancel ss t pq)
-          | [] => NONE
-  end
+fun proc ss ct =
+  let
+    val t = term_of ct;
+    val (divs, mods) = coll_div_mod t ([], []);
+  in
+    if null divs orelse null mods then NONE
+    else
+      (case inter (op =) mods divs of
+        pq :: _ => SOME (cancel ss t pq)
+      | [] => NONE)
+  end;
 
 end