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.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