--- a/NEWS Wed Dec 28 20:03:13 2011 +0100
+++ b/NEWS Wed Dec 28 22:08:44 2011 +0100
@@ -70,7 +70,7 @@
it is often sufficent to prune any tinkering with former theorems mem_def
and Collect_def.
-* Theory HOL/Library/AList has been renamed to AList_Impl. INCOMPABILITY.
+* Theory HOL/Library/AList has been renamed to AList_Impl. INCOMPATIBILITY.
* 'datatype' specifications allow explicit sort constraints.
@@ -113,14 +113,22 @@
word_order_linear ~> linorder_linear
lenw1_zero_neq_one ~> zero_neq_one
word_number_of_eq ~> number_of_eq
-
-* Clarified attribute "mono_set": pure declararation without modifying
+ word_of_int_add_hom ~> wi_hom_add
+ word_of_int_sub_hom ~> wi_hom_sub
+ word_of_int_mult_hom ~> wi_hom_mult
+ word_of_int_minus_hom ~> wi_hom_neg
+ word_of_int_succ_hom ~> wi_hom_succ
+ word_of_int_pred_hom ~> wi_hom_pred
+ word_of_int_0_hom ~> word_0_wi
+ word_of_int_1_hom ~> word_1_wi
+
+* Clarified attribute "mono_set": pure declaration without modifying
the result of the fact expression.
* "Transitive_Closure.ntrancl": bounded transitive closure on
relations.
-* Constant "Set.not_member" now qualifed. INCOMPATIBILITY.
+* Constant "Set.not_member" now qualified. INCOMPATIBILITY.
* "sublists" moved to theory More_List. INCOMPATIBILITY.
--- a/src/HOL/Word/Bit_Int.thy Wed Dec 28 20:03:13 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy Wed Dec 28 22:08:44 2011 +0100
@@ -12,54 +12,6 @@
imports Bit_Representation Bit_Operations
begin
-subsection {* Recursion combinators for bitstrings *}
-
-function bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a" where
- "bin_rec f1 f2 f3 bin = (if bin = 0 then f1
- else if bin = - 1 then f2
- else f3 (bin_rest bin) (bin_last bin) (bin_rec f1 f2 f3 (bin_rest bin)))"
- by pat_completeness auto
-
-termination by (relation "measure (nat o abs o snd o snd o snd)")
- (simp_all add: bin_last_def bin_rest_def)
-
-declare bin_rec.simps [simp del]
-
-lemma bin_rec_PM:
- "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
- by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
-
-lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
- by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
-
-lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
- by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
-
-lemma bin_rec_Bit0:
- "f3 Int.Pls (0::bit) f1 = f1 \<Longrightarrow>
- bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w (0::bit) (bin_rec f1 f2 f3 w)"
- by (unfold Pls_def Min_def Bit0_def Bit1_def) (simp add: bin_rec.simps bin_last_def bin_rest_def)
-
-lemma bin_rec_Bit1:
- "f3 Int.Min (1::bit) f2 = f2 \<Longrightarrow>
- bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w (1::bit) (bin_rec f1 f2 f3 w)"
- apply (cases "w = Int.Min")
- apply (simp add: bin_rec_Min)
- apply (cases "w = Int.Pls")
- apply (simp add: bin_rec_Pls number_of_is_id Pls_def [symmetric] bin_rec.simps)
- apply (subst bin_rec.simps)
- apply auto unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id apply auto
- done
-
-lemma bin_rec_Bit:
- "f = bin_rec f1 f2 f3 ==> f3 Int.Pls (0::bit) f1 = f1 ==>
- f3 Int.Min (1::bit) f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
- by (cases b, simp add: bin_rec_Bit0 BIT_simps, simp add: bin_rec_Bit1 BIT_simps)
-
-lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
- bin_rec_Bit0 bin_rec_Bit1
-
-
subsection {* Logical operations *}
text "bit-wise logical operations on the int type"
@@ -67,21 +19,25 @@
instantiation int :: bit
begin
-definition
- int_not_def: "bitNOT = bin_rec (- 1) 0
- (\<lambda>w b s. s BIT (NOT b))"
+definition int_not_def:
+ "bitNOT = (\<lambda>x::int. - x - 1)"
-definition
- int_and_def: "bitAND = bin_rec (\<lambda>x. 0) (\<lambda>y. y)
- (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
+function bitAND_int where
+ "bitAND_int x y =
+ (if x = 0 then 0 else if x = -1 then y else
+ (bin_rest x AND bin_rest y) BIT (bin_last x AND bin_last y))"
+ by pat_completeness simp
-definition
- int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. - 1)
- (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
+termination
+ by (relation "measure (nat o abs o fst)", simp_all add: bin_rest_def)
+
+declare bitAND_int.simps [simp del]
-definition
- int_xor_def: "bitXOR = bin_rec (\<lambda>x. x) bitNOT
- (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
+definition int_or_def:
+ "bitOR = (\<lambda>x y::int. NOT (NOT x AND NOT y))"
+
+definition int_xor_def:
+ "bitXOR = (\<lambda>x y::int. (x AND NOT y) OR (NOT x AND y))"
instance ..
@@ -89,33 +45,78 @@
subsubsection {* Basic simplification rules *}
+lemma int_not_BIT [simp]:
+ "NOT (w BIT b) = (NOT w) BIT (NOT b)"
+ unfolding int_not_def Bit_def by (cases b, simp_all)
+
lemma int_not_simps [simp]:
"NOT Int.Pls = Int.Min"
"NOT Int.Min = Int.Pls"
"NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
"NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
- "NOT (w BIT b) = (NOT w) BIT (NOT b)"
- unfolding int_not_def Pls_def [symmetric] Min_def [symmetric]
- by (simp_all add: bin_rec_simps BIT_simps)
+ unfolding int_not_def Pls_def Min_def Bit0_def Bit1_def by simp_all
+
+lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
+ unfolding int_not_def by simp
+
+lemma int_and_0 [simp]: "(0::int) AND x = 0"
+ by (simp add: bitAND_int.simps)
+
+lemma int_and_m1 [simp]: "(-1::int) AND x = x"
+ by (simp add: bitAND_int.simps)
+
+lemma int_and_Pls [simp]: "Int.Pls AND x = Int.Pls"
+ unfolding Pls_def by simp
+
+lemma int_and_Min [simp]: "Int.Min AND x = x"
+ unfolding Min_def by simp
+
+lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> b = 0"
+ by (subst BIT_eq_iff [symmetric], simp)
+
+lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b = 1"
+ by (subst BIT_eq_iff [symmetric], simp)
+
+lemma int_and_Bits [simp]:
+ "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"
+ by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
-lemma int_xor_Pls [simp]:
- "Int.Pls XOR x = x"
- unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM)
+lemma int_and_Bits2 [simp]:
+ "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+ "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
+ "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
+ "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
+ unfolding BIT_simps [symmetric] int_and_Bits by simp_all
+
+lemma int_or_Pls [simp]: "Int.Pls OR x = x"
+ unfolding int_or_def by simp
+
+lemma int_or_Min [simp]: "Int.Min OR x = Int.Min"
+ unfolding int_or_def by simp
+
+lemma bit_or_def: "(b::bit) OR c = NOT (NOT b AND NOT c)"
+ by (induct b, simp_all) (* TODO: move *)
-lemma int_xor_Min [simp]:
- "Int.Min XOR x = NOT x"
- unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM)
+lemma int_or_Bits [simp]:
+ "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
+ unfolding int_or_def bit_or_def by simp
+
+lemma int_or_Bits2 [simp]:
+ "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
+ "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
+ "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
+ "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
+ unfolding int_or_def by simp_all
+
+lemma int_xor_Pls [simp]: "Int.Pls XOR x = x"
+ unfolding int_xor_def by simp
+
+lemma bit_xor_def: "(b::bit) XOR c = (b AND NOT c) OR (NOT b AND c)"
+ by (induct b, simp_all) (* TODO: move *)
lemma int_xor_Bits [simp]:
"(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
- apply (unfold int_xor_def Pls_def [symmetric] Min_def [symmetric])
- apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans])
- apply (rule ext, simp)
- prefer 2
- apply simp
- apply (rule ext)
- apply (simp add: int_not_simps [symmetric])
- done
+ unfolding int_xor_def bit_xor_def by simp
lemma int_xor_Bits2 [simp]:
"(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
@@ -124,46 +125,6 @@
"(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
-lemma int_or_Pls [simp]:
- "Int.Pls OR x = x"
- by (unfold int_or_def) (simp add: bin_rec_PM)
-
-lemma int_or_Min [simp]:
- "Int.Min OR x = Int.Min"
- by (unfold int_or_def Pls_def [symmetric] Min_def [symmetric]) (simp add: bin_rec_PM)
-
-lemma int_or_Bits [simp]:
- "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
- unfolding int_or_def Pls_def [symmetric] Min_def [symmetric]
- by (simp add: bin_rec_simps BIT_simps)
-
-lemma int_or_Bits2 [simp]:
- "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
- "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
- "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
- "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
- unfolding BIT_simps [symmetric] int_or_Bits by simp_all
-
-lemma int_and_Pls [simp]:
- "Int.Pls AND x = Int.Pls"
- unfolding int_and_def Pls_def [symmetric] by (simp add: bin_rec_PM)
-
-lemma int_and_Min [simp]:
- "Int.Min AND x = x"
- unfolding int_and_def by (simp add: bin_rec_PM)
-
-lemma int_and_Bits [simp]:
- "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)"
- unfolding int_and_def Pls_def [symmetric] Min_def [symmetric]
- by (simp add: bin_rec_simps BIT_simps)
-
-lemma int_and_Bits2 [simp]:
- "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
- "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
- "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
- "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
- unfolding BIT_simps [symmetric] int_and_Bits by simp_all
-
subsubsection {* Binary destructors *}
lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
@@ -205,6 +166,9 @@
subsubsection {* Derived properties *}
+lemma int_xor_Min [simp]: "Int.Min XOR x = NOT x"
+ by (auto simp add: bin_eq_iff bin_nth_ops)
+
lemma int_xor_extra_simps [simp]:
"w XOR Int.Pls = w"
"w XOR Int.Min = NOT w"
@@ -234,9 +198,6 @@
"(x::int) XOR x = Int.Pls"
by (auto simp add: bin_eq_iff bin_nth_ops)
-lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
- by (auto simp add: bin_eq_iff bin_nth_ops)
-
lemmas bin_log_esimps =
int_and_extra_simps int_or_extra_simps int_xor_extra_simps
int_and_Pls int_and_Min int_or_Pls int_or_Min int_xor_Pls int_xor_Min
@@ -617,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
@@ -630,4 +589,3 @@
by auto
end
-
--- a/src/HOL/Word/Bit_Representation.thy Wed Dec 28 20:03:13 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Wed Dec 28 22:08:44 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/Examples/WordExamples.thy Wed Dec 28 20:03:13 2011 +0100
+++ b/src/HOL/Word/Examples/WordExamples.thy Wed Dec 28 22:08:44 2011 +0100
@@ -14,7 +14,7 @@
type_synonym word8 = "8 word"
type_synonym byte = word8
--- "modulus"
+text "modulus"
lemma "(27 :: 4 word) = -5" by simp
@@ -22,10 +22,12 @@
lemma "27 \<noteq> (11 :: 6 word)" by simp
--- "signed"
+text "signed"
+
lemma "(127 :: 6 word) = -1" by simp
--- "number ring simps"
+text "number ring simps"
+
lemma
"27 + 11 = (38::'a::len word)"
"27 + 11 = (6::5 word)"
@@ -43,57 +45,70 @@
lemma "23 \<le> (27::8 word)" by simp
lemma "\<not> 23 < (27::2 word)" by simp
lemma "0 < (4::3 word)" by simp
+lemma "1 < (4::3 word)" by simp
+lemma "0 < (1::3 word)" by simp
--- "ring operations"
+text "ring operations"
lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp
--- "casting"
+text "casting"
lemma "uint (234567 :: 10 word) = 71" by simp
lemma "uint (-234567 :: 10 word) = 953" by simp
lemma "sint (234567 :: 10 word) = 71" by simp
lemma "sint (-234567 :: 10 word) = -71" by simp
+lemma "uint (1 :: 10 word) = 1" by simp
lemma "unat (-234567 :: 10 word) = 953" by simp
+lemma "unat (1 :: 10 word) = 1" by simp
lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 word)" by simp
lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp
lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp
+lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp
--- "reducing goals to nat or int and arith:"
+text "reducing goals to nat or int and arith:"
lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by unat_arith
lemma "i < x ==> i < (i + 1 :: 'a :: len word)" by uint_arith
--- "bool lists"
+text "bool lists"
lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp
lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
--- "this is not exactly fast, but bearable"
+text "this is not exactly fast, but bearable"
lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp
--- "this works only for replicate n True"
+text "this works only for replicate n True"
lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
by (unfold mask_bl [symmetric]) (simp add: mask_def)
--- "bit operations"
+text "bit operations"
lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp
-
lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp
-
lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp
-
lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp
+lemma "0 AND 5 = (0 :: byte)" by simp
+lemma "1 AND 1 = (1 :: byte)" by simp
+lemma "1 AND 0 = (0 :: byte)" by simp
+lemma "1 AND 5 = (1 :: byte)" apply simp? oops
+lemma "1 OR 6 = (7 :: byte)" apply simp? oops
+lemma "1 OR 1 = (1 :: byte)" by simp
+lemma "1 XOR 7 = (6 :: byte)" apply simp? oops
+lemma "1 XOR 1 = (0 :: byte)" by simp
+lemma "NOT 1 = (254 :: byte)" apply simp? oops
+lemma "NOT 0 = (255 :: byte)" apply simp oops
lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp
lemma "(0b0010 :: 4 word) !! 1" by simp
lemma "\<not> (0b0010 :: 4 word) !! 0" by simp
lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
+lemma "\<not> (1 :: 3 word) !! 2" apply simp? oops
lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
@@ -101,12 +116,18 @@
lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp
+lemma "set_bit 1 3 True = (0b1001::'a::len0 word)" apply simp? oops
+lemma "set_bit 1 0 False = (0::'a::len0 word)" apply simp? oops
lemma "lsb (0b0101::'a::len word)" by simp
lemma "\<not> lsb (0b1000::'a::len word)" by simp
+lemma "lsb (1::'a::len word)" by simp
+lemma "\<not> lsb (0::'a::len word)" by simp
lemma "\<not> msb (0b0101::4 word)" by simp
lemma "msb (0b1000::4 word)" by simp
+lemma "\<not> msb (1::4 word)" apply simp? oops
+lemma "\<not> msb (0::4 word)" apply simp? oops
lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
@@ -115,13 +136,19 @@
lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
lemma "0b1011 >> 2 = (0b10::8 word)" by simp
lemma "0b1011 >>> 2 = (0b10::8 word)" by simp
+lemma "1 << 2 = (0b100::'a::len0 word)" apply simp? oops
lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp
+lemma "slice 3 (1::6 word) = (0::3 word)" apply simp? oops
lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp
lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp
lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp
lemma "word_roti -2 0b0110 = (0b1001::4 word)" by simp
+lemma "word_rotr 2 0 = (0::4 word)" by simp
+lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops
+lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops
+lemma "word_roti -2 1 = (0b0100::4 word)" apply simp? oops
lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
proof -
--- a/src/HOL/Word/Word.thy Wed Dec 28 20:03:13 2011 +0100
+++ b/src/HOL/Word/Word.thy Wed Dec 28 22:08:44 2011 +0100
@@ -132,9 +132,6 @@
lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
by (simp add: sints_def range_sbintrunc)
-lemma mod_in_reps: "m > 0 \<Longrightarrow> y mod m : {0::int ..< m}"
- by auto
-
lemma
uint_0:"0 <= uint x" and
uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
@@ -153,19 +150,17 @@
word.uint_inverse word.Abs_word_inverse int_mod_lem)
done
-lemma int_word_uint:
- "uint (word_of_int x::'a::len0 word) = x mod 2 ^ len_of TYPE('a)"
- by (fact td_ext_uint [THEN td_ext.eq_norm])
-
interpretation word_uint:
td_ext "uint::'a::len0 word \<Rightarrow> int"
word_of_int
"uints (len_of TYPE('a::len0))"
"\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
by (rule td_ext_uint)
-
+
lemmas td_uint = word_uint.td_thm
+lemmas int_word_uint = word_uint.eq_norm
+
lemmas td_ext_ubin = td_ext_uint
[unfolded len_gt_0 no_bintr_alt1 [symmetric]]
@@ -227,8 +222,8 @@
definition
word_number_of_def: "number_of w = word_of_int w"
-lemmas word_arith_wis =
- word_add_def word_mult_def word_minus_def
+lemmas word_arith_wis =
+ word_add_def word_sub_wi word_mult_def word_minus_def
word_succ_def word_pred_def word_0_wi word_1_wi
lemmas arths =
@@ -237,6 +232,7 @@
lemma wi_homs:
shows
wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
+ wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)" and
wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" and
@@ -245,29 +241,9 @@
lemmas wi_hom_syms = wi_homs [symmetric]
-lemma word_of_int_sub_hom:
- "(word_of_int a) - word_of_int b = word_of_int (a - b)"
- by (simp add: word_sub_wi arths)
-
-lemmas new_word_of_int_homs =
- word_of_int_sub_hom wi_homs word_0_wi word_1_wi
-
-lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric]
-
-lemmas word_of_int_hom_syms =
- new_word_of_int_hom_syms (* FIXME: duplicate *)
-
-lemmas word_of_int_homs =
- new_word_of_int_homs (* FIXME: duplicate *)
-
-(* FIXME: provide only one copy of these theorems! *)
-lemmas word_of_int_add_hom = wi_hom_add
-lemmas word_of_int_mult_hom = wi_hom_mult
-lemmas word_of_int_minus_hom = wi_hom_neg
-lemmas word_of_int_succ_hom = wi_hom_succ
-lemmas word_of_int_pred_hom = wi_hom_pred
-lemmas word_of_int_0_hom = word_0_wi
-lemmas word_of_int_1_hom = word_1_wi
+lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi
+
+lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
instance
by default (auto simp: split_word_all word_of_int_homs algebra_simps)
@@ -288,7 +264,7 @@
lemma word_of_int: "of_int = word_of_int"
apply (rule ext)
apply (case_tac x rule: int_diff_cases)
- apply (simp add: word_of_nat word_of_int_sub_hom)
+ apply (simp add: word_of_nat wi_hom_sub)
done
instance word :: (len) number_ring
@@ -462,6 +438,8 @@
(* FIXME: only provide one theorem name *)
lemmas of_nth_def = word_set_bits_def
+subsection {* Theorems about typedefs *}
+
lemma sint_sbintrunc':
"sint (word_of_int bin :: 'a word) =
(sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
@@ -670,6 +648,8 @@
"x \<le> - (2 ^ (size (w::'a::len word) - 1)) \<Longrightarrow> x \<le> sint w"
unfolding word_size by (rule order_trans [OF _ sint_ge])
+subsection {* Testing bits *}
+
lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)"
unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)
@@ -680,17 +660,16 @@
apply fast
done
-lemma word_eqI [rule_format] :
+lemma word_eq_iff:
+ fixes x y :: "'a::len0 word"
+ shows "x = y \<longleftrightarrow> (\<forall>n<len_of TYPE('a). x !! n = y !! n)"
+ unfolding uint_inject [symmetric] bin_eq_iff word_test_bit_def [symmetric]
+ by (metis test_bit_size [unfolded word_size])
+
+lemma word_eqI [rule_format]:
fixes u :: "'a::len0 word"
shows "(ALL n. n < size u --> u !! n = v !! n) \<Longrightarrow> u = v"
- apply (rule test_bit_eq_iff [THEN iffD1])
- apply (rule ext)
- apply (erule allE)
- apply (erule impCE)
- prefer 2
- apply assumption
- apply (auto dest!: test_bit_size simp add: word_size)
- done
+ by (simp add: word_size word_eq_iff)
lemma word_eqD: "(u::'a::len0 word) = v \<Longrightarrow> u !! x = v !! x"
by simp
@@ -810,8 +789,11 @@
lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
unfolding uint_bl by (simp add : word_size)
-
-lemmas uint_bl_bin [simp] = trans [OF bin_bl_bin word_ubin.norm_Rep]
+
+lemma uint_bl_bin:
+ fixes x :: "'a::len0 word"
+ shows "bl_to_bin (bin_to_bl (len_of TYPE('a)) (uint x)) = uint x"
+ by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
(* FIXME: the next two lemmas should be unnecessary, because the lhs
terms should never occur in practice *)
@@ -894,10 +876,21 @@
word_of_int (sbintrunc (len_of TYPE('a) - Suc 0) (number_of w))"
unfolding scast_def by simp
-lemmas source_size = source_size_def [unfolded Let_def word_size]
-lemmas target_size = target_size_def [unfolded Let_def word_size]
-lemmas is_down = is_down_def [unfolded source_size target_size]
-lemmas is_up = is_up_def [unfolded source_size target_size]
+lemma source_size: "source_size (c::'a::len0 word \<Rightarrow> _) = len_of TYPE('a)"
+ unfolding source_size_def word_size Let_def ..
+
+lemma target_size: "target_size (c::_ \<Rightarrow> 'b::len0 word) = len_of TYPE('b)"
+ unfolding target_size_def word_size Let_def ..
+
+lemma is_down:
+ fixes c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
+ shows "is_down c \<longleftrightarrow> len_of TYPE('b) \<le> len_of TYPE('a)"
+ unfolding is_down_def source_size target_size ..
+
+lemma is_up:
+ fixes c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
+ shows "is_up c \<longleftrightarrow> len_of TYPE('a) \<le> len_of TYPE('b)"
+ unfolding is_up_def source_size target_size ..
lemmas is_up_down = trans [OF is_up is_down [symmetric]]
@@ -1041,7 +1034,6 @@
lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
-lemmas word_log_bin_defs = word_log_defs
text {* Executable equality *}
@@ -1060,9 +1052,7 @@
subsection {* Word Arithmetic *}
lemma word_less_alt: "(a < b) = (uint a < uint b)"
- unfolding word_less_def word_le_def
- by (auto simp del: word_uint.Rep_inject
- simp: word_uint.Rep_inject [symmetric])
+ unfolding word_less_def word_le_def by (simp add: less_le)
lemma signed_linorder: "class.linorder word_sle word_sless"
proof
@@ -1100,12 +1090,8 @@
lemma word_0_no: "(0::'a::len0 word) = Numeral0"
by (simp add: word_number_of_alt)
-lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)"
- unfolding Pls_def Bit_def by auto
-
-lemma word_1_no:
- "(1 :: 'a :: len0 word) = number_of (Int.Pls BIT 1)"
- unfolding word_1_wi word_number_of_def int_one_bin by auto
+lemma word_1_no: "(1::'a::len0 word) = Numeral1"
+ by (simp add: word_number_of_alt)
lemma word_m1_wi: "-1 = word_of_int -1"
by (rule word_number_of_alt)
@@ -1204,7 +1190,7 @@
by (rule word_uint.Abs_cases [of b],
rule word_uint.Abs_cases [of a],
simp add: add_commute mult_commute
- ring_distribs new_word_of_int_homs
+ ring_distribs word_of_int_homs
del: word_of_int_0 word_of_int_1)+
lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
@@ -1237,11 +1223,11 @@
"word_succ (number_of bin) = number_of (Int.succ bin) &
word_pred (number_of bin) = number_of (Int.pred bin)"
unfolding word_number_of_def Int.succ_def Int.pred_def
- by (simp add: new_word_of_int_homs)
+ by (simp add: word_of_int_homs)
lemma word_sp_01 [simp] :
"word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
- by (unfold word_0_no word_1_no) (auto simp: BIT_simps)
+ unfolding word_0_no word_1_no by simp
(* alternative approach to lifting arithmetic equalities *)
lemma word_of_int_Ex:
@@ -1502,7 +1488,7 @@
lemmas le_plus = le_plus' [rotated]
-lemmas le_minus = leD [THEN thin_rl, THEN le_minus']
+lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *)
lemma word_plus_mono_right:
"(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
@@ -1774,11 +1760,11 @@
lemma Abs_fnat_hom_mult:
"of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
- by (simp add: word_of_nat word_of_int_mult_hom zmult_int)
+ by (simp add: word_of_nat wi_hom_mult zmult_int)
lemma Abs_fnat_hom_Suc:
"word_succ (of_nat a) = of_nat (Suc a)"
- by (simp add: word_of_nat word_of_int_succ_hom add_ac)
+ by (simp add: word_of_nat wi_hom_succ add_ac)
lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
by simp
@@ -2108,17 +2094,23 @@
folded word_ubin.eq_norm, THEN eq_reflection]
(* the binary operations only *)
+(* BH: why is this needed? *)
lemmas word_log_binary_defs =
word_and_def word_or_def word_xor_def
-lemmas word_no_log_defs [simp] =
- word_not_def [where a="number_of a",
- unfolded word_no_wi wils1, folded word_no_wi]
- word_log_binary_defs [where a="number_of a" and b="number_of b",
- unfolded word_no_wi wils1, folded word_no_wi]
- for a b
-
-lemmas word_wi_log_defs = word_no_log_defs [unfolded word_no_wi]
+lemma word_wi_log_defs:
+ "NOT word_of_int a = word_of_int (NOT a)"
+ "word_of_int a AND word_of_int b = word_of_int (a AND b)"
+ "word_of_int a OR word_of_int b = word_of_int (a OR b)"
+ "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"
+ unfolding word_log_defs wils1 by simp_all
+
+lemma word_no_log_defs [simp]:
+ "NOT number_of a = (number_of (NOT a) :: 'a::len0 word)"
+ "number_of a AND number_of b = (number_of (a AND b) :: 'a word)"
+ "number_of a OR number_of b = (number_of (a OR b) :: 'a word)"
+ "number_of a XOR number_of b = (number_of (a XOR b) :: 'a word)"
+ unfolding word_no_wi word_wi_log_defs by simp_all
lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
by (simp add: word_or_def word_wi_log_defs word_ubin.eq_norm
@@ -2147,11 +2139,24 @@
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 *)
lemmas bwsimps =
- word_of_int_homs(2)
+ wi_hom_add
word_0_wi_Pls
word_m1_wi_Min
word_wi_log_defs
@@ -2162,10 +2167,7 @@
"(x AND y) AND z = x AND y AND z"
"(x OR y) OR z = x OR y OR z"
"(x XOR y) XOR z = x XOR y XOR z"
- using word_of_int_Ex [where x=x]
- word_of_int_Ex [where x=y]
- word_of_int_Ex [where x=z]
- by (auto simp: bwsimps bbw_assocs)
+ by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
lemma word_bw_comms:
fixes x :: "'a::len0 word"
@@ -2173,9 +2175,7 @@
"x AND y = y AND x"
"x OR y = y OR x"
"x XOR y = y XOR x"
- using word_of_int_Ex [where x=x]
- word_of_int_Ex [where x=y]
- by (auto simp: bwsimps bin_ops_comm)
+ by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
lemma word_bw_lcs:
fixes x :: "'a::len0 word"
@@ -2183,10 +2183,7 @@
"y AND x AND z = x AND y AND z"
"y OR x OR z = x OR y OR z"
"y XOR x XOR z = x XOR y XOR z"
- using word_of_int_Ex [where x=x]
- word_of_int_Ex [where x=y]
- word_of_int_Ex [where x=z]
- by (auto simp: bwsimps)
+ by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
lemma word_log_esimps [simp]:
fixes x :: "'a::len0 word"
@@ -2203,17 +2200,14 @@
"-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"
shows
"NOT (x OR y) = NOT x AND NOT y"
"NOT (x AND y) = NOT x OR NOT y"
- using word_of_int_Ex [where x=x]
- word_of_int_Ex [where x=y]
- by (auto simp: bwsimps bbw_not_dist)
+ by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
lemma word_bw_same:
fixes x :: "'a::len0 word"
@@ -2221,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"
@@ -2235,30 +2228,21 @@
"x OR x AND y = x"
"(x OR y) AND x = x"
"x AND y OR x = x"
- using word_of_int_Ex [where x=x]
- word_of_int_Ex [where x=y]
- by (auto simp: bwsimps)
+ by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
lemma word_not_not [simp]:
"NOT NOT (x::'a::len0 word) = 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_ao_dist:
fixes x :: "'a::len0 word"
shows "(x OR y) AND z = x AND z OR y AND z"
- using word_of_int_Ex [where x=x]
- word_of_int_Ex [where x=y]
- word_of_int_Ex [where x=z]
- by (auto simp: bwsimps bbw_ao_dist)
+ by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
lemma word_oa_dist:
fixes x :: "'a::len0 word"
shows "x AND y OR z = (x OR z) AND (y OR z)"
- using word_of_int_Ex [where x=x]
- word_of_int_Ex [where x=y]
- word_of_int_Ex [where x=z]
- by (auto simp: bwsimps bbw_oa_dist)
+ by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
lemma word_add_not [simp]:
fixes x :: "'a::len0 word"
@@ -2328,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)
@@ -2442,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 test_bit_no word_0_no by auto
-
lemma nth_sint:
fixes w :: "'a::len word"
defines "l \<equiv> len_of TYPE ('a)"
@@ -2463,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]:
@@ -2928,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)
@@ -3042,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))"
@@ -3051,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) =
@@ -3152,7 +3121,7 @@
"word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
"word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
- by (auto simp: and_mask_wi bintr_ariths bintr_arith1s new_word_of_int_homs)
+ by (auto simp: and_mask_wi bintr_ariths bintr_arith1s word_of_int_homs)
lemma mask_power_eq:
"(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
@@ -3448,7 +3417,7 @@
"(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
apply (unfold of_bl_def)
apply (simp add: bl_to_bin_app_cat bin_cat_num)
- apply (simp add: word_of_int_power_hom [symmetric] new_word_of_int_hom_syms)
+ apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
done
lemma of_bl_False [simp]:
@@ -3769,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)+
@@ -4141,7 +4110,7 @@
declare word_roti_def [simp]
-subsection {* Miscellaneous *}
+subsection {* Maximum machine word *}
lemma word_int_cases:
"\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len0 word) = word_of_int n; 0 \<le> n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
@@ -4460,6 +4429,8 @@
apply (case_tac "1+n = 0", auto)
done
+subsection {* Recursion combinator for words *}
+
definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
"word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
@@ -4568,7 +4539,7 @@
lemma word_no_1 [simp]: "(Numeral1::'a::len0 word) = 1"
- by (fact word_1_no [symmetric, unfolded BIT_simps])
+ by (fact word_1_no [symmetric])
lemma word_no_0 [simp]: "(Numeral0::'a::len0 word) = 0"
by (fact word_0_no [symmetric])