src/HOL/Divides.thy
changeset 49962 a8cc904a6820
parent 48891 c0eafbd55de3
child 50422 ee729dbd1b7f
     1.1 --- a/src/HOL/Divides.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4      "\<dots> = (c + a div b) * b + (a + c * b) mod b"
     1.5        by (simp add: algebra_simps)
     1.6    finally have "a = a div b * b + (a + c * b) mod b"
     1.7 -    by (simp add: add_commute [of a] add_assoc left_distrib)
     1.8 +    by (simp add: add_commute [of a] add_assoc distrib_right)
     1.9    then have "a div b * b + (a + c * b) mod b = a div b * b + a mod b"
    1.10      by (simp add: mod_div_equality)
    1.11    then show ?thesis by simp
    1.12 @@ -1274,9 +1274,9 @@
    1.13   prefer 2 apply (simp add: right_diff_distrib)
    1.14  apply (subgoal_tac "0 < b * (1 + q - q') ")
    1.15  apply (erule_tac [2] order_le_less_trans)
    1.16 - prefer 2 apply (simp add: right_diff_distrib right_distrib)
    1.17 + prefer 2 apply (simp add: right_diff_distrib distrib_left)
    1.18  apply (subgoal_tac "b * q' < b * (1 + q) ")
    1.19 - prefer 2 apply (simp add: right_diff_distrib right_distrib)
    1.20 + prefer 2 apply (simp add: right_diff_distrib distrib_left)
    1.21  apply (simp add: mult_less_cancel_left)
    1.22  done
    1.23  
    1.24 @@ -1332,11 +1332,11 @@
    1.25    apply (induct a b rule: posDivAlg.induct)
    1.26    apply auto
    1.27    apply (simp add: divmod_int_rel_def)
    1.28 -  apply (subst posDivAlg_eqn, simp add: right_distrib)
    1.29 +  apply (subst posDivAlg_eqn, simp add: distrib_left)
    1.30    apply (case_tac "a < b")
    1.31    apply simp_all
    1.32    apply (erule splitE)
    1.33 -  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
    1.34 +  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
    1.35    done
    1.36  
    1.37  
    1.38 @@ -1366,7 +1366,7 @@
    1.39    apply (case_tac "a + b < (0\<Colon>int)")
    1.40    apply simp_all
    1.41    apply (erule splitE)
    1.42 -  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
    1.43 +  apply (auto simp add: distrib_left Let_def mult_ac mult_2_right)
    1.44    done
    1.45  
    1.46  
    1.47 @@ -1732,7 +1732,7 @@
    1.48       "[| 0 \<le> b'*q' + r'; r' < b';  0 < b' |] ==> 0 \<le> (q'::int)"
    1.49  apply (subgoal_tac "0 < b'* (q' + 1) ")
    1.50   apply (simp add: zero_less_mult_iff)
    1.51 -apply (simp add: right_distrib)
    1.52 +apply (simp add: distrib_left)
    1.53  done
    1.54  
    1.55  lemma zdiv_mono2_lemma:
    1.56 @@ -1744,7 +1744,7 @@
    1.57   apply (simp add: mult_less_cancel_left)
    1.58  apply (subgoal_tac "b*q = r' - r + b'*q'")
    1.59   prefer 2 apply simp
    1.60 -apply (simp (no_asm_simp) add: right_distrib)
    1.61 +apply (simp (no_asm_simp) add: distrib_left)
    1.62  apply (subst add_commute, rule add_less_le_mono, arith)
    1.63  apply (rule mult_right_mono, auto)
    1.64  done
    1.65 @@ -1773,7 +1773,7 @@
    1.66  apply (frule q_neg_lemma, assumption+) 
    1.67  apply (subgoal_tac "b*q' < b* (q + 1) ")
    1.68   apply (simp add: mult_less_cancel_left)
    1.69 -apply (simp add: right_distrib)
    1.70 +apply (simp add: distrib_left)
    1.71  apply (subgoal_tac "b*q' \<le> b'*q'")
    1.72   prefer 2 apply (simp add: mult_right_mono_neg, arith)
    1.73  done
    1.74 @@ -1795,7 +1795,7 @@
    1.75  lemma zmult1_lemma:
    1.76       "[| divmod_int_rel b c (q, r) |]  
    1.77        ==> divmod_int_rel (a * b) c (a*q + a*r div c, a*r mod c)"
    1.78 -by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib mult_ac)
    1.79 +by (auto simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left mult_ac)
    1.80  
    1.81  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
    1.82  apply (case_tac "c = 0", simp)
    1.83 @@ -1807,7 +1807,7 @@
    1.84  lemma zadd1_lemma:
    1.85       "[| divmod_int_rel a c (aq, ar);  divmod_int_rel b c (bq, br) |]  
    1.86        ==> divmod_int_rel (a+b) c (aq + bq + (ar+br) div c, (ar+br) mod c)"
    1.87 -by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff right_distrib)
    1.88 +by (force simp add: split_ifs divmod_int_rel_def linorder_neq_iff distrib_left)
    1.89  
    1.90  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
    1.91  lemma zdiv_zadd1_eq:
    1.92 @@ -1900,7 +1900,7 @@
    1.93  lemma zmult2_lemma: "[| divmod_int_rel a b (q, r); 0 < c |]  
    1.94        ==> divmod_int_rel a (b * c) (q div c, b*(q mod c) + r)"
    1.95  by (auto simp add: mult_ac divmod_int_rel_def linorder_neq_iff
    1.96 -                   zero_less_mult_iff right_distrib [symmetric] 
    1.97 +                   zero_less_mult_iff distrib_left [symmetric] 
    1.98                     zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4 mult_less_0_iff split: split_if_asm)
    1.99  
   1.100  lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"