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