# 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 @@ "\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 \ 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)"