# HG changeset patch # User huffman # Date 1325099128 -3600 # Node ID fad87bb608fcceb81a77fb42045c599738d26eba # Parent 657f87b1094451a41a1b9e73a896e8bfab7c6f05 restate some lemmas to respect int/bin distinction diff -r 657f87b10944 -r fad87bb608fc src/HOL/Word/Bit_Int.thy --- a/src/HOL/Word/Bit_Int.thy Wed Dec 28 19:15:28 2011 +0100 +++ b/src/HOL/Word/Bit_Int.thy Wed Dec 28 20:05:28 2011 +0100 @@ -578,8 +578,6 @@ apply (induct n arbitrary: m) apply clarsimp apply safe - apply (case_tac m) - apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq]) apply (case_tac m) apply (auto simp: Bit_B0_2t [symmetric]) done diff -r 657f87b10944 -r fad87bb608fc src/HOL/Word/Bit_Representation.thy --- a/src/HOL/Word/Bit_Representation.thy Wed Dec 28 19:15:28 2011 +0100 +++ b/src/HOL/Word/Bit_Representation.thy Wed Dec 28 20:05:28 2011 +0100 @@ -269,14 +269,17 @@ lemma bin_nth_zero [simp]: "\ bin_nth 0 n" by (induct n) auto +lemma bin_nth_1 [simp]: "bin_nth 1 n \ n = 0" + by (cases n) simp_all + lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n" - by (induct n) auto + by (induct n) auto (* FIXME: delete *) lemma bin_nth_minus1 [simp]: "bin_nth -1 n" by (induct n) auto lemma bin_nth_Min [simp]: "bin_nth Int.Min n" - by (induct n) auto + by (induct n) auto (* FIXME: delete *) lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))" by auto @@ -288,18 +291,18 @@ by (cases n) auto lemma bin_nth_minus_Bit0 [simp]: - "0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)" - using bin_nth_minus [where b="(0::bit)"] by (simp add: BIT_simps) + "0 < n ==> bin_nth (number_of (Int.Bit0 w)) n = bin_nth (number_of w) (n - 1)" + using bin_nth_minus [where w="number_of w" and b="(0::bit)"] by simp lemma bin_nth_minus_Bit1 [simp]: - "0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)" - using bin_nth_minus [where b="(1::bit)"] by (simp add: BIT_simps) + "0 < n ==> bin_nth (number_of (Int.Bit1 w)) n = bin_nth (number_of w) (n - 1)" + using bin_nth_minus [where w="number_of w" and b="(1::bit)"] by simp lemmas bin_nth_0 = bin_nth.simps(1) lemmas bin_nth_Suc = bin_nth.simps(2) lemmas bin_nth_simps = - bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus + bin_nth_0 bin_nth_Suc bin_nth_zero bin_nth_minus1 bin_nth_minus bin_nth_minus_Bit0 bin_nth_minus_Bit1 @@ -416,12 +419,14 @@ by (cases n) auto lemma bin_nth_Bit0: - "bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)" - using bin_nth_Bit [where b="(0::bit)"] by (simp add: BIT_simps) + "bin_nth (number_of (Int.Bit0 w)) n \ + (\m. n = Suc m \ bin_nth (number_of w) m)" + using bin_nth_Bit [where w="number_of w" and b="(0::bit)"] by simp lemma bin_nth_Bit1: - "bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))" - using bin_nth_Bit [where b="(1::bit)"] by (simp add: BIT_simps) + "bin_nth (number_of (Int.Bit1 w)) n \ + n = 0 \ (\m. n = Suc m \ bin_nth (number_of w) m)" + using bin_nth_Bit [where w="number_of w" and b="(1::bit)"] by simp lemma bintrunc_bintrunc_l: "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)" diff -r 657f87b10944 -r fad87bb608fc src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Wed Dec 28 19:15:28 2011 +0100 +++ b/src/HOL/Word/Word.thy Wed Dec 28 20:05:28 2011 +0100 @@ -666,7 +666,7 @@ unfolding uint_inject [symmetric] bin_eq_iff word_test_bit_def [symmetric] by (metis test_bit_size [unfolded word_size]) -lemma word_eqI: +lemma word_eqI [rule_format]: fixes u :: "'a::len0 word" shows "(ALL n. n < size u --> u !! n = v !! n) \ u = v" by (simp add: word_size word_eq_iff) @@ -2139,6 +2139,19 @@ apply (simp add : test_bit_bin word_size) done +lemma test_bit_wi [simp]: + "(word_of_int x::'a::len0 word) !! n \ n < len_of TYPE('a) \ bin_nth x n" + unfolding word_test_bit_def + by (simp add: nth_bintr [symmetric] word_ubin.eq_norm) + +lemma test_bit_no [simp]: + "(number_of w :: 'a::len0 word) !! n \ + n < len_of TYPE('a) \ bin_nth (number_of w) n" + unfolding word_number_of_alt test_bit_wi .. + +lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n" + unfolding word_test_bit_def by simp + (* get from commutativity, associativity etc of int_and etc to same for word_and etc *) @@ -2187,8 +2200,7 @@ "-1 OR x = -1" "0 XOR x = x" "-1 XOR x = NOT x" - using word_of_int_Ex [where x=x] - by (auto simp: bwsimps) + by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) lemma word_not_dist: fixes x :: "'a::len0 word" @@ -2203,8 +2215,7 @@ "x AND x = x" "x OR x = x" "x XOR x = 0" - using word_of_int_Ex [where x=x] - by (auto simp: bwsimps) + by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size]) lemma word_ao_absorbs [simp]: fixes x :: "'a::len0 word" @@ -2301,15 +2312,13 @@ by (simp add : sign_Min_lt_0 number_of_is_id) lemma word_msb_no [simp]: - "msb (number_of bin :: 'a::len word) = bin_nth bin (len_of TYPE('a) - 1)" - unfolding word_msb_def word_number_of_def + "msb (number_of w::'a::len word) = bin_nth (number_of w) (len_of TYPE('a) - 1)" + unfolding word_msb_def word_number_of_alt by (clarsimp simp add: word_sbin.eq_norm bin_sign_lem) lemma word_msb_nth: "msb (w::'a::len word) = bin_nth (uint w) (len_of TYPE('a) - 1)" - apply (rule trans [OF _ word_msb_no]) - apply (simp add : word_number_of_def) - done + unfolding word_msb_def sint_uint by (simp add: bin_sign_lem) lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)" apply (unfold word_msb_nth uint_bl) @@ -2415,19 +2424,6 @@ shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms) -lemma test_bit_wi [simp]: - "(word_of_int x::'a::len0 word) !! n \ n < len_of TYPE('a) \ bin_nth x n" - unfolding word_test_bit_def - by (simp add: nth_bintr [symmetric] word_ubin.eq_norm) - -lemma test_bit_no [simp]: - "(number_of bin :: 'a::len0 word) !! n \ n < len_of TYPE('a) \ bin_nth bin n" - unfolding word_test_bit_def word_number_of_def word_size - by (simp add : nth_bintr [symmetric] word_ubin.eq_norm) - -lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n" - unfolding word_test_bit_def by simp - lemma nth_sint: fixes w :: "'a::len word" defines "l \ len_of TYPE ('a)" @@ -2436,7 +2432,7 @@ by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric]) lemma word_lsb_no [simp]: - "lsb (number_of bin :: 'a :: len word) = (bin_last bin = 1)" + "lsb (number_of bin :: 'a :: len word) = (bin_last (number_of bin) = 1)" unfolding word_lsb_alt test_bit_no by auto lemma word_set_no [simp]: @@ -2901,15 +2897,15 @@ lemma shiftr_no': "w = number_of bin \ - (w::'a::len0 word) >> n = number_of ((bin_rest ^^ n) (bintrunc (size w) bin))" + (w::'a::len0 word) >> n = word_of_int ((bin_rest ^^ n) (bintrunc (size w) (number_of bin)))" apply clarsimp 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 = number_of ((bin_rest ^^ n) - (sbintrunc (size w - 1) bin))" + "w = number_of bin \ w >>> n = word_of_int ((bin_rest ^^ n) + (sbintrunc (size w - 1) (number_of bin)))" apply clarsimp apply (rule word_eqI) apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size) @@ -3015,7 +3011,7 @@ lemma mask_bl: "mask n = of_bl (replicate n True)" by (auto simp add : test_bit_of_bl word_size intro: word_eqI) -lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)" +lemma mask_bin: "mask n = word_of_int (bintrunc n -1)" by (auto simp add: nth_bintr word_size intro: word_eqI) lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))" @@ -3024,11 +3020,11 @@ apply (auto simp add: test_bit_bin) done -lemma and_mask_no: "number_of i AND mask n = number_of (bintrunc n i)" - by (auto simp add : nth_bintr word_size word_ops_nth_size intro: word_eqI) - lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)" - by (fact and_mask_no [unfolded word_number_of_def]) + by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff) + +lemma and_mask_no: "number_of i AND mask n = word_of_int (bintrunc n (number_of i))" + unfolding word_number_of_alt by (rule and_mask_wi) lemma bl_and_mask': "to_bl (w AND mask n :: 'a :: len word) = @@ -3742,7 +3738,7 @@ apply (clarsimp simp add : word_size) apply (rule nth_equalityI, assumption) apply clarsimp - apply (rule word_eqI) + apply (rule word_eqI [rule_format]) apply (rule trans) apply (rule test_bit_rsplit_alt) apply (clarsimp simp: word_size)+