clarified prover-specific rules
authorhaftmann
Sun Oct 16 13:47:37 2016 +0200 (2016-10-16)
changeset 642500cde0b4d4cb5
parent 64249 a3f654f9a46c
child 64262 41e027ab985c
clarified prover-specific rules
src/HOL/Divides.thy
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 16 13:47:36 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Oct 16 13:47:37 2016 +0200
     1.3 @@ -28,12 +28,6 @@
     1.4  
     1.5  text \<open>@{const divide} and @{const modulo}\<close>
     1.6  
     1.7 -lemma div_mod_equality: "((a div b) * b + a mod b) + c = a + c"
     1.8 -  by (simp add: div_mult_mod_eq)
     1.9 -
    1.10 -lemma div_mod_equality2: "(b * (a div b) + a mod b) + c = a + c"
    1.11 -  by (simp add: mult_div_mod_eq)
    1.12 -
    1.13  lemma mod_by_0 [simp]: "a mod 0 = a"
    1.14    using div_mult_mod_eq [of a zero] by simp
    1.15  
    1.16 @@ -345,6 +339,11 @@
    1.17    shows   "(a div d) div (b div d) = a div b"
    1.18    using assms by (subst dvd_div_mult2_eq [symmetric]) simp_all
    1.19  
    1.20 +lemma cancel_div_mod_rules:
    1.21 +  "((a div b) * b + a mod b) + c = a + c"
    1.22 +  "(b * (a div b) + a mod b) + c = a + c"
    1.23 +  by (simp_all add: div_mult_mod_eq mult_div_mod_eq)
    1.24 +
    1.25  end
    1.26  
    1.27  class ring_div = comm_ring_1 + semiring_div
    1.28 @@ -1042,10 +1041,10 @@
    1.29              SOME (t, u) => dest_sum t @ dest_sum u
    1.30            | NONE => [tm]));
    1.31  
    1.32 -  val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
    1.33 -
    1.34 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
    1.35 -    (@{thm add_0_left} :: @{thm add_0_right} :: @{thms ac_simps}))
    1.36 +  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
    1.37 +
    1.38 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
    1.39 +    (Arith_Data.simp_all_tac @{thms add_0_left add_0_right ac_simps})
    1.40  )
    1.41  \<close>
    1.42  
    1.43 @@ -1806,10 +1805,10 @@
    1.44    val mk_sum = Arith_Data.mk_sum HOLogic.intT;
    1.45    val dest_sum = Arith_Data.dest_sum;
    1.46  
    1.47 -  val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
    1.48 -
    1.49 -  val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
    1.50 -    (@{thm diff_conv_add_uminus} :: @{thms add_0_left add_0_right} @ @{thms ac_simps}))
    1.51 +  val div_mod_eqs = map mk_meta_eq @{thms cancel_div_mod_rules};
    1.52 +
    1.53 +  val prove_eq_sums = Arith_Data.prove_conv2 all_tac
    1.54 +    (Arith_Data.simp_all_tac @{thms diff_conv_add_uminus add_0_left add_0_right ac_simps})
    1.55  )
    1.56  \<close>
    1.57