src/HOL/Euclidean_Division.thy
 changeset 66810 cc2b490f9dc4 parent 66808 1907167b6038 child 66813 351142796345
```     1.1 --- a/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
1.2 +++ b/src/HOL/Euclidean_Division.thy	Sun Oct 08 22:28:21 2017 +0200
1.3 @@ -9,16 +9,6 @@
1.4    imports Nat_Transfer Lattices_Big
1.5  begin
1.6
1.7 -subsection \<open>Prelude: simproc for cancelling @{const divide} and @{const modulo}\<close>
1.8 -
1.9 -lemma (in semiring_modulo) cancel_div_mod_rules:
1.10 -  "((a div b) * b + a mod b) + c = a + c"
1.11 -  "(b * (a div b) + a mod b) + c = a + c"
1.12 -  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
1.13 -
1.14 -ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
1.15 -
1.16 -
1.17  subsection \<open>Euclidean (semi)rings with explicit division and remainder\<close>
1.18
1.19  class euclidean_semiring = semidom_modulo + normalization_semidom +
1.20 @@ -767,9 +757,10 @@
1.21    val mk_binop = HOLogic.mk_binop;
1.22    val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
1.23    val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
1.24 -  fun mk_sum [] = HOLogic.zero
1.25 -    | mk_sum [t] = t
1.26 -    | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
1.27 +  fun mk_sum' [] = HOLogic.zero
1.28 +    | mk_sum' [t] = t
1.29 +    | mk_sum' (t :: ts) = mk_plus (t, mk_sum' ts);
1.30 +  fun mk_sum _ = mk_sum';
1.31    fun dest_sum tm =
1.32      if HOLogic.is_zero tm then []
1.33      else
```