src/HOL/Rings.thy
changeset 66810 cc2b490f9dc4
parent 66808 1907167b6038
child 66816 212a3334e7da
     1.1 --- a/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
     1.2 +++ b/src/HOL/Rings.thy	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -1624,8 +1624,39 @@
     1.4    "b dvd a - a mod b"
     1.5    by (simp add: minus_mod_eq_div_mult)
     1.6  
     1.7 +lemma cancel_div_mod_rules:
     1.8 +  "((a div b) * b + a mod b) + c = a + c"
     1.9 +  "(b * (a div b) + a mod b) + c = a + c"
    1.10 +  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
    1.11 +
    1.12  end
    1.13  
    1.14 +text \<open>Interlude: basic tool support for algebraic and arithmetic calculations\<close>
    1.15 +
    1.16 +named_theorems arith "arith facts -- only ground formulas"
    1.17 +ML_file "Tools/arith_data.ML"
    1.18 +
    1.19 +ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
    1.20 +
    1.21 +ML \<open>
    1.22 +structure Cancel_Div_Mod_Ring = Cancel_Div_Mod
    1.23 +(
    1.24 +  val div_name = @{const_name divide};
    1.25 +  val mod_name = @{const_name modulo};
    1.26 +  val mk_binop = HOLogic.mk_binop;
    1.27 +  val mk_sum = Arith_Data.mk_sum;
    1.28 +  val dest_sum = Arith_Data.dest_sum;
    1.29 +
    1.30 +  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
    1.31 +
    1.32 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
    1.33 +    @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
    1.34 +)
    1.35 +\<close>
    1.36 +
    1.37 +simproc_setup cancel_div_mod_int ("(a::'a::semidom_modulo) + b") =
    1.38 +  \<open>K Cancel_Div_Mod_Ring.proc\<close>
    1.39 +
    1.40  class idom_modulo = idom + semidom_modulo
    1.41  begin
    1.42