--- 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.
--- 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
--- 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)"