# HG changeset patch
# User huffman
# Date 1332877706 -7200
# Node ID 8395d7d63fc8a2dee6dc8912ce6b46335f723d64
# Parent  099397de21e3044f4beb13fec0a18e624cc8c925
mark some duplicate lemmas for deletion

diff -r 099397de21e3 -r 8395d7d63fc8 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Mar 27 20:19:23 2012 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Mar 27 21:48:26 2012 +0200
@@ -624,22 +624,22 @@
   "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
   unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
 
-lemmas zmod_uminus' = zmod_uminus [where b=c] for c
+lemmas zmod_uminus' = zminus_zmod [where m=c] for c
 lemmas zpower_zmod' = power_mod [where b=c and n=k] for c k
 
-lemmas brdmod1s' [symmetric] = 
-  mod_add_left_eq mod_add_right_eq 
-  zmod_zsub_left_eq zmod_zsub_right_eq 
-  mod_mult_right_eq zmod_zmult1_eq_rev 
+lemmas brdmod1s' [symmetric] =
+  mod_add_left_eq mod_add_right_eq
+  mod_diff_left_eq mod_diff_right_eq
+  mod_mult_left_eq mod_mult_right_eq
 
 lemmas brdmods' [symmetric] = 
   zpower_zmod' [symmetric]
   trans [OF mod_add_left_eq mod_add_right_eq] 
-  trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] 
-  trans [OF mod_mult_right_eq zmod_zmult1_eq_rev] 
+  trans [OF mod_diff_left_eq mod_diff_right_eq] 
+  trans [OF mod_mult_right_eq mod_mult_left_eq] 
   zmod_uminus' [symmetric]
   mod_add_left_eq [where b = "1::int"]
-  zmod_zsub_left_eq [where b = "1"]
+  mod_diff_left_eq [where b = "1::int"]
 
 lemmas bintr_arith1s =
   brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n
diff -r 099397de21e3 -r 8395d7d63fc8 src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 20:19:23 2012 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Tue Mar 27 21:48:26 2012 +0200
@@ -97,37 +97,28 @@
 lemmas add_diff_cancel2 = add_commute [THEN diff_eq_eq [THEN iffD2]]
 
 lemma zmod_uminus: "- ((a :: int) mod b) mod b = -a mod b"
-  by (simp add : zmod_zminus1_eq_if)
+  by (fact zminus_zmod) (* FIXME: delete *)
 
 lemma zmod_zsub_distrib: "((a::int) - b) mod c = (a mod c - b mod c) mod c"
-  apply (unfold diff_int_def)
-  apply (rule trans [OF _ mod_add_eq [symmetric]])
-  apply (simp add: zmod_uminus mod_add_eq [symmetric])
-  done
+  by (fact mod_diff_eq) (* FIXME: delete *)
 
 lemma zmod_zsub_right_eq: "((a::int) - b) mod c = (a - b mod c) mod c"
-  apply (unfold diff_int_def)
-  apply (rule trans [OF _ mod_add_right_eq [symmetric]])
-  apply (simp add : zmod_uminus mod_add_right_eq [symmetric])
-  done
+  by (fact mod_diff_right_eq) (* FIXME: delete *)
 
 lemma zmod_zsub_left_eq: "((a::int) - b) mod c = (a mod c - b) mod c"
-  by (rule mod_add_left_eq [where b = "- b", simplified diff_int_def [symmetric]])
+  by (fact mod_diff_left_eq) (* FIXME: delete *)
 
 lemma zmod_zsub_self [simp]: 
   "((b :: int) - a) mod a = b mod a"
-  by (simp add: zmod_zsub_right_eq)
+  by (simp add: mod_diff_right_eq)
 
 lemma zmod_zmult1_eq_rev:
   "b * a mod c = b mod c * a mod (c::int)"
-  apply (simp add: mult_commute)
-  apply (subst mod_mult_right_eq)
-  apply simp
-  done
+  by (fact mod_mult_left_eq) (* FIXME: delete *)
 
-lemmas rdmods [symmetric] = zmod_uminus [symmetric]
-  zmod_zsub_left_eq zmod_zsub_right_eq mod_add_left_eq
-  mod_add_right_eq mod_mult_right_eq zmod_zmult1_eq_rev
+lemmas rdmods [symmetric] = mod_minus_eq
+  mod_diff_left_eq mod_diff_right_eq mod_add_left_eq
+  mod_add_right_eq mod_mult_right_eq mod_mult_left_eq
 
 lemma mod_plus_right:
   "((a + x) mod m = (b + x) mod m) = (a mod m = b mod (m :: nat))"
@@ -143,8 +134,8 @@
   THEN mod_plus_right [THEN iffD2], simplified]
 
 lemmas push_mods' = mod_add_eq
-  mod_mult_eq zmod_zsub_distrib
-  zmod_uminus [symmetric]
+  mod_mult_eq mod_diff_eq
+  mod_minus_eq
 
 lemmas push_mods = push_mods' [THEN eq_reflection]
 lemmas pull_mods = push_mods [symmetric] rdmods [THEN eq_reflection]
@@ -198,9 +189,7 @@
 lemmas int_mod_eq' = refl [THEN [3] int_mod_eq]
 
 lemma int_mod_le: "0 <= a ==> 0 < (n :: int) ==> a mod n <= a"
-  apply (cases "a < n")
-   apply (auto dest: mod_pos_pos_trivial pos_mod_bound [where a=a])
-  done
+  by (rule zmod_le_nonneg_dividend)
 
 lemma int_mod_le': "0 <= b - n ==> 0 < (n :: int) ==> b mod n <= b - n"
   by (rule int_mod_le [where a = "b - n" and n = n, simplified])
@@ -289,11 +278,7 @@
 lemmas td_gal_lt = td_gal [simplified not_less [symmetric], simplified]
 
 lemma div_mult_le: "(a :: nat) div b * b <= a"
-  apply (cases b)
-   prefer 2
-   apply (rule order_refl [THEN th2])
-  apply auto
-  done
+  by (fact dtle)
 
 lemmas sdl = split_div_lemma [THEN iffD1, symmetric]
 
diff -r 099397de21e3 -r 8395d7d63fc8 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Mar 27 20:19:23 2012 +0200
+++ b/src/HOL/Word/Word.thy	Tue Mar 27 21:48:26 2012 +0200
@@ -4465,9 +4465,9 @@
       and 4: "x' - y' = z'"
   shows "(x - y) mod b = z' mod b'"
   using assms
-  apply (subst zmod_zsub_left_eq)
-  apply (subst zmod_zsub_right_eq)
-  apply (simp add: zmod_zsub_left_eq [symmetric] zmod_zsub_right_eq [symmetric])
+  apply (subst mod_diff_left_eq)
+  apply (subst mod_diff_right_eq)
+  apply (simp add: mod_diff_left_eq [symmetric] mod_diff_right_eq [symmetric])
   done
 
 lemma word_induct_less: