src/HOL/Divides.thy
changeset 43594 ef1ddc59b825
parent 41792 ff3cb0c418b7
child 44766 d4d33a4d7548
     1.1 --- a/src/HOL/Divides.thy	Wed Jun 29 16:31:50 2011 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Jun 29 17:35:46 2011 +0200
     1.3 @@ -679,9 +679,7 @@
     1.4  text {* Simproc for cancelling @{const div} and @{const mod} *}
     1.5  
     1.6  ML {*
     1.7 -local
     1.8 -
     1.9 -structure CancelDivMod = CancelDivModFun
    1.10 +structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
    1.11  (
    1.12    val div_name = @{const_name div};
    1.13    val mod_name = @{const_name mod};
    1.14 @@ -694,17 +692,10 @@
    1.15    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
    1.16      (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
    1.17  )
    1.18 -
    1.19 -in
    1.20 -
    1.21 -val cancel_div_mod_nat_proc = Simplifier.simproc_global @{theory}
    1.22 -  "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
    1.23 -
    1.24 -val _ = Addsimprocs [cancel_div_mod_nat_proc];
    1.25 -
    1.26 -end
    1.27  *}
    1.28  
    1.29 +simproc_setup cancel_div_mod_nat ("(m::nat) + n") = {* K Cancel_Div_Mod_Nat.proc *}
    1.30 +
    1.31  
    1.32  subsubsection {* Quotient *}
    1.33  
    1.34 @@ -1437,9 +1428,7 @@
    1.35  text {* Tool setup *}
    1.36  
    1.37  ML {*
    1.38 -local
    1.39 -
    1.40 -structure CancelDivMod = CancelDivModFun
    1.41 +structure Cancel_Div_Mod_Int = Cancel_Div_Mod
    1.42  (
    1.43    val div_name = @{const_name div};
    1.44    val mod_name = @{const_name mod};
    1.45 @@ -1452,17 +1441,10 @@
    1.46    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
    1.47      (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
    1.48  )
    1.49 -
    1.50 -in
    1.51 -
    1.52 -val cancel_div_mod_int_proc = Simplifier.simproc_global @{theory}
    1.53 -  "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
    1.54 -
    1.55 -val _ = Addsimprocs [cancel_div_mod_int_proc];
    1.56 -
    1.57 -end
    1.58  *}
    1.59  
    1.60 +simproc_setup cancel_div_mod_int ("(k::int) + l") = {* K Cancel_Div_Mod_Int.proc *}
    1.61 +
    1.62  lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
    1.63  apply (cut_tac a = a and b = b in divmod_int_correct)
    1.64  apply (auto simp add: divmod_int_rel_def mod_int_def)