# HG changeset patch # User huffman # Date 1325239917 -3600 # Node ID 8664713db1818a60301a051e0d9caaf2bf103262 # Parent 1e184c0d88be43f471c7598ab21011e18b4ac9fe remove unnecessary intermediate lemmas diff -r 1e184c0d88be -r 8664713db181 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Dec 29 20:32:59 2011 +0100 +++ b/src/HOL/Word/Word.thy Fri Dec 30 11:11:57 2011 +0100 @@ -450,23 +450,19 @@ "uint w = bintrunc (len_of TYPE('a)) (sint (w :: 'a :: len word))" unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le) -lemma bintr_uint': - "n >= size w \ bintrunc n (uint w) = uint w" - apply (unfold word_size) +lemma bintr_uint: + fixes w :: "'a::len0 word" + shows "len_of TYPE('a) \ n \ bintrunc n (uint w) = uint w" apply (subst word_ubin.norm_Rep [symmetric]) apply (simp only: bintrunc_bintrunc_min word_size) apply (simp add: min_max.inf_absorb2) done -lemma wi_bintr': - "wb = word_of_int bin \ n >= size wb \ - word_of_int (bintrunc n bin) = wb" - unfolding word_size +lemma wi_bintr: + "len_of TYPE('a::len0) \ n \ + word_of_int (bintrunc n w) = (word_of_int w :: 'a word)" by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1) -lemmas bintr_uint = bintr_uint' [unfolded word_size] -lemmas wi_bintr = wi_bintr' [unfolded word_size] - lemma td_ext_sbin: "td_ext (sint :: 'a word => int) word_of_int (sints (len_of TYPE('a::len))) (sbintrunc (len_of TYPE('a) - 1))" @@ -682,25 +678,21 @@ lemmas test_bit_bin = test_bit_bin' [unfolded word_size] -lemma bin_nth_uint_imp': "bin_nth (uint w) n --> n < size w" - apply (unfold word_size) - apply (rule impI) +lemma bin_nth_uint_imp: + "bin_nth (uint (w::'a::len0 word)) n \ n < len_of TYPE('a)" apply (rule nth_bintr [THEN iffD1, THEN conjunct1]) apply (subst word_ubin.norm_Rep) apply assumption done -lemma bin_nth_sint': - "n >= size w --> bin_nth (sint w) n = bin_nth (sint w) (size w - 1)" - apply (rule impI) +lemma bin_nth_sint: + fixes w :: "'a::len word" + shows "len_of TYPE('a) \ n \ + bin_nth (sint w) n = bin_nth (sint w) (len_of TYPE('a) - 1)" apply (subst word_sbin.norm_Rep [symmetric]) - apply (simp add : nth_sbintr word_size) - apply auto + apply (auto simp add: nth_sbintr) done -lemmas bin_nth_uint_imp = bin_nth_uint_imp' [rule_format, unfolded word_size] -lemmas bin_nth_sint = bin_nth_sint' [rule_format, unfolded word_size] - (* type definitions theorem for in terms of equivalent bool list *) lemma td_bl: "type_definition (to_bl :: 'a::len0 word => bool list) @@ -2897,29 +2889,21 @@ unfolding sshiftr1_def word_number_of_def by (simp add : word_sbin.eq_norm) -lemma shiftr_no': - "w = number_of bin \ - (w::'a::len0 word) >> n = word_of_int ((bin_rest ^^ n) (bintrunc (size w) (number_of bin)))" - apply clarsimp +lemma shiftr_no [simp]: + "(number_of w::'a::len0 word) >> n = word_of_int + ((bin_rest ^^ n) (bintrunc (len_of TYPE('a)) (number_of w)))" apply (rule word_eqI) apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size) done -lemma sshiftr_no': - "w = number_of bin \ w >>> n = word_of_int ((bin_rest ^^ n) - (sbintrunc (size w - 1) (number_of bin)))" - apply clarsimp +lemma sshiftr_no [simp]: + "(number_of w::'a::len word) >>> n = word_of_int + ((bin_rest ^^ n) (sbintrunc (len_of TYPE('a) - 1) (number_of w)))" apply (rule word_eqI) apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size) apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+ done -lemmas sshiftr_no [simp] = - sshiftr_no' [where w = "number_of w", OF refl, unfolded word_size] for w - -lemmas shiftr_no [simp] = - shiftr_no' [where w = "number_of w", OF refl, unfolded word_size] for w - lemma shiftr1_bl_of: "length bl \ len_of TYPE('a) \ shiftr1 (of_bl bl::'a::len0 word) = of_bl (butlast bl)"