# HG changeset patch
# User huffman
# Date 1321537925 -3600
# Node ID 6dd3e88de4c21bbc6c8fc245aa4fa4cb9f48ac22
# Parent  26aebb8ac9c11de7bf19cf324abbf663b9adabf6
HOL-Word: removed many duplicate theorems (see NEWS)

diff -r 26aebb8ac9c1 -r 6dd3e88de4c2 NEWS
--- a/NEWS	Thu Nov 17 14:24:10 2011 +0100
+++ b/NEWS	Thu Nov 17 14:52:05 2011 +0100
@@ -29,6 +29,35 @@
 
 *** HOL ***
 
+* Session HOL-Word: Discontinued many redundant theorems specific to type
+'a word. INCOMPATIBILITY, use the corresponding generic theorems instead.
+
+  word_sub_alt ~> word_sub_wi
+  word_add_alt ~> word_add_def
+  word_mult_alt ~> word_mult_def
+  word_minus_alt ~> word_minus_def
+  word_0_alt ~> word_0_wi
+  word_1_alt ~> word_1_wi
+  word_add_0 ~> add_0_left
+  word_add_0_right ~> add_0_right
+  word_mult_1 ~> mult_1_left
+  word_mult_1_right ~> mult_1_right
+  word_add_commute ~> add_commute
+  word_add_assoc ~> add_assoc
+  word_add_left_commute ~> add_left_commute
+  word_mult_commute ~> mult_commute
+  word_mult_assoc ~> mult_assoc
+  word_mult_left_commute ~> mult_left_commute
+  word_left_distrib ~> left_distrib
+  word_right_distrib ~> right_distrib
+  word_left_minus ~> left_minus
+  word_diff_0_right ~> diff_0_right
+  word_diff_self ~> diff_self
+  word_add_ac ~> add_ac
+  word_mult_ac ~> mult_ac
+  word_plus_ac0 ~> add_0_left add_0_right add_ac
+  word_times_ac1 ~> mult_1_left mult_1_right mult_ac
+
 * Clarified attribute "mono_set": pure declararation without modifying
 the result of the fact expression.
 
diff -r 26aebb8ac9c1 -r 6dd3e88de4c2 src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Thu Nov 17 14:24:10 2011 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Thu Nov 17 14:52:05 2011 +0100
@@ -194,7 +194,7 @@
     have "(?MM::int) = 2 ^ len_of TYPE(32)" by simp
     show ?thesis
       unfolding
-        word_add_alt
+        word_add_def
         uint_word_of_int_id[OF `0 <= a` `a <= ?M`]
         uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`]
         int_word_uint
@@ -237,7 +237,7 @@
       by simp
     show ?thesis
       unfolding
-        word_add_alt
+        word_add_def
         uint_word_of_int_id[OF `0 <= a'` `a' <= ?M`]
         uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`]
         int_word_uint
diff -r 26aebb8ac9c1 -r 6dd3e88de4c2 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Nov 17 14:24:10 2011 +0100
+++ b/src/HOL/Word/Word.thy	Thu Nov 17 14:52:05 2011 +0100
@@ -1203,15 +1203,8 @@
   word_sub_wi [unfolded succ_def pred_def, standard]
   word_arith_wis [unfolded succ_def pred_def, standard]
 
-(* FIXME: Lots of duplicate lemmas *)
-lemmas word_sub_alt = word_arith_alts (1)
-lemmas word_add_alt = word_arith_alts (2)
-lemmas word_mult_alt = word_arith_alts (3)
-lemmas word_minus_alt = word_arith_alts (4)
 lemmas word_succ_alt = word_arith_alts (5)
 lemmas word_pred_alt = word_arith_alts (6)
-lemmas word_0_alt = word_arith_alts (7)
-lemmas word_1_alt = word_arith_alts (8)
 
 subsection  "Transferring goals from words to ints"
 
@@ -1269,40 +1262,6 @@
   "\<exists>y. x = word_of_int y"
   by (rule_tac x="uint x" in exI) simp
 
-(* FIXME: redundant theorems *)
-lemma word_arith_eqs:
-  fixes a :: "'a::len0 word"
-  fixes b :: "'a::len0 word"
-  shows
-  word_add_0: "0 + a = a" and
-  word_add_0_right: "a + 0 = a" and
-  word_mult_1: "1 * a = a" and
-  word_mult_1_right: "a * 1 = a" and
-  word_add_commute: "a + b = b + a" and
-  word_add_assoc: "a + b + c = a + (b + c)" and
-  word_add_left_commute: "a + (b + c) = b + (a + c)" and
-  word_mult_commute: "a * b = b * a" and
-  word_mult_assoc: "a * b * c = a * (b * c)" and
-  word_mult_left_commute: "a * (b * c) = b * (a * c)" and
-  word_left_distrib: "(a + b) * c = a * c + b * c" and
-  word_right_distrib: "a * (b + c) = a * b + a * c" and
-  word_left_minus: "- a + a = 0" and
-  word_diff_0_right: "a - 0 = a" and
-  word_diff_self: "a - a = 0"
-  using word_of_int_Ex [of a] 
-        word_of_int_Ex [of b] 
-        word_of_int_Ex [of c]
-  by (auto simp: word_of_int_hom_syms [symmetric]
-                 add_0_right add_commute add_assoc add_left_commute
-                 mult_commute mult_assoc mult_left_commute
-                 left_distrib right_distrib)
-  
-lemmas word_add_ac = word_add_commute word_add_assoc word_add_left_commute
-lemmas word_mult_ac = word_mult_commute word_mult_assoc word_mult_left_commute
-  
-lemmas word_plus_ac0 = word_add_0 word_add_0_right word_add_ac
-lemmas word_times_ac1 = word_mult_1 word_mult_1_right word_mult_ac
-
 
 subsection "Order on fixed-length words"
 
@@ -1533,7 +1492,7 @@
 lemma no_olen_add':
   fixes x :: "'a::len0 word"
   shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
-  by (simp add: word_add_ac add_ac no_olen_add)
+  by (simp add: add_ac no_olen_add)
 
 lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric], standard]
 
@@ -4412,7 +4371,7 @@
 
 lemma shiftr1_1 [simp]: 
   "shiftr1 (1::'a::len word) = 0"
-  by (simp add: shiftr1_def word_0_alt)
+  by (simp add: shiftr1_def word_0_wi)
 
 lemma shiftr_1[simp]: 
   "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"