--- 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
--- 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]: "\<not> bin_nth 0 n"
by (induct n) auto
+lemma bin_nth_1 [simp]: "bin_nth 1 n \<longleftrightarrow> 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 \<longleftrightarrow>
+ (\<exists>m. n = Suc m \<and> 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 \<longleftrightarrow>
+ n = 0 \<or> (\<exists>m. n = Suc m \<and> 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)"
--- 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) \<Longrightarrow> 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 \<longleftrightarrow> n < len_of TYPE('a) \<and> 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 \<longleftrightarrow>
+ n < len_of TYPE('a) \<and> 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 \<longleftrightarrow> n < len_of TYPE('a) \<and> 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 \<equiv> n < len_of TYPE('a) \<and> 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 \<equiv> 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 \<Longrightarrow>
- (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 \<Longrightarrow> w >>> n = number_of ((bin_rest ^^ n)
- (sbintrunc (size w - 1) bin))"
+ "w = number_of bin \<Longrightarrow> 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)+