--- a/src/HOL/Word/Bit_Int.thy Thu Feb 23 16:02:07 2012 +0100
+++ b/src/HOL/Word/Bit_Int.thy Thu Feb 23 16:18:19 2012 +0100
@@ -279,14 +279,15 @@
done
lemma le_int_or:
- "bin_sign (y::int) = Int.Pls ==> x <= x OR y"
+ "bin_sign (y::int) = 0 ==> x <= x OR y"
apply (induct y arbitrary: x rule: bin_induct)
apply clarsimp
+ apply (simp only: Min_def)
apply clarsimp
apply (case_tac x rule: bin_exhaust)
apply (case_tac b)
apply (case_tac [!] bit)
- apply (auto simp: less_eq_int_code BIT_simps)
+ apply (auto simp: le_Bits)
done
lemmas int_and_le =
@@ -374,18 +375,14 @@
"bin_sc n 0 w <= w"
apply (induct n arbitrary: w)
apply (case_tac [!] w rule: bin_exhaust)
- apply (auto simp del: BIT_simps)
- apply (unfold Bit_def)
- apply (simp_all add: bitval_def split: bit.split)
+ apply (auto simp: le_Bits)
done
lemma bin_set_ge:
"bin_sc n 1 w >= w"
apply (induct n arbitrary: w)
apply (case_tac [!] w rule: bin_exhaust)
- apply (auto simp del: BIT_simps)
- apply (unfold Bit_def)
- apply (simp_all add: bitval_def split: bit.split)
+ apply (auto simp: le_Bits)
done
lemma bintr_bin_clr_le:
@@ -394,9 +391,7 @@
apply simp
apply (case_tac w rule: bin_exhaust)
apply (case_tac m)
- apply (auto simp del: BIT_simps)
- apply (unfold Bit_def)
- apply (simp_all add: bitval_def split: bit.split)
+ apply (auto simp: le_Bits)
done
lemma bintr_bin_set_ge:
@@ -405,16 +400,14 @@
apply simp
apply (case_tac w rule: bin_exhaust)
apply (case_tac m)
- apply (auto simp del: BIT_simps)
- apply (unfold Bit_def)
- apply (simp_all add: bitval_def split: bit.split)
+ apply (auto simp: le_Bits)
done
-lemma bin_sc_FP [simp]: "bin_sc n 0 Int.Pls = Int.Pls"
- by (induct n) (auto simp: BIT_simps)
+lemma bin_sc_FP [simp]: "bin_sc n 0 0 = 0"
+ by (induct n) auto
-lemma bin_sc_TM [simp]: "bin_sc n 1 Int.Min = Int.Min"
- by (induct n) (auto simp: BIT_simps)
+lemma bin_sc_TM [simp]: "bin_sc n 1 -1 = -1"
+ by (induct n) auto
lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
@@ -495,9 +488,6 @@
lemma bin_cat_zero [simp]: "bin_cat 0 n w = bintrunc n w"
by (induct n arbitrary: w) auto
-lemma bin_cat_Pls [simp]: "bin_cat Int.Pls n w = bintrunc n w"
- unfolding Pls_def by (rule bin_cat_zero)
-
lemma bintr_cat1:
"bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
by (induct n arbitrary: b) auto
@@ -529,13 +519,9 @@
lemma bin_split_zero [simp]: "bin_split n 0 = (0, 0)"
by (induct n) auto
-lemma bin_split_Pls [simp]:
- "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
- unfolding Pls_def by (rule bin_split_zero)
-
-lemma bin_split_Min [simp]:
- "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)"
- by (induct n) (auto simp: Let_def split: ls_splits)
+lemma bin_split_minus1 [simp]:
+ "bin_split n -1 = (-1, bintrunc n -1)"
+ by (induct n) auto
lemma bin_split_trunc:
"bin_split (min m n) c = (a, b) ==>
@@ -563,7 +549,7 @@
lemma bin_split_num:
"bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
- apply (induct n arbitrary: b, simp add: Pls_def)
+ apply (induct n arbitrary: b, simp)
apply (simp add: bin_rest_def zdiv_zmult2_eq)
apply (case_tac b rule: bin_exhaust)
apply simp
--- a/src/HOL/Word/Bit_Representation.thy Thu Feb 23 16:02:07 2012 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Thu Feb 23 16:18:19 2012 +0100
@@ -111,12 +111,6 @@
apply (simp add: z1pmod2)
done
-lemma B1_mod_2 [simp]: "(Int.Bit1 w) mod 2 = 1"
- unfolding numeral_simps number_of_is_id by (simp add: z1pmod2)
-
-lemma B0_mod_2 [simp]: "(Int.Bit0 w) mod 2 = 0"
- unfolding numeral_simps number_of_is_id by simp
-
lemma neB1E [elim!]:
assumes ne: "y \<noteq> (1::bit)"
assumes y: "y = (0::bit) \<Longrightarrow> P"
@@ -291,15 +285,12 @@
lemma bin_sign_simps [simp]:
"bin_sign 0 = 0"
+ "bin_sign 1 = 0"
"bin_sign -1 = -1"
"bin_sign (number_of (Int.Bit0 w)) = bin_sign (number_of w)"
"bin_sign (number_of (Int.Bit1 w)) = bin_sign (number_of w)"
- "bin_sign Int.Pls = Int.Pls"
- "bin_sign Int.Min = Int.Min"
- "bin_sign (Int.Bit0 w) = bin_sign w"
- "bin_sign (Int.Bit1 w) = bin_sign w"
"bin_sign (w BIT b) = bin_sign w"
- unfolding bin_sign_def numeral_simps Bit_def bitval_def number_of_is_id
+ unfolding bin_sign_def Bit_def bitval_def
by (simp_all split: bit.split)
lemma bin_sign_rest [simp]:
@@ -717,17 +708,13 @@
lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)"
by (simp add : no_sbintr m2pths)
-lemma bintrunc_Suc:
- "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT bin_last bin"
- by (case_tac bin rule: bin_exhaust) auto
-
lemma sign_Pls_ge_0:
- "(bin_sign bin = Int.Pls) = (number_of bin >= (0 :: int))"
- by (induct bin rule: numeral_induct) auto
+ "(bin_sign bin = 0) = (bin >= (0 :: int))"
+ unfolding bin_sign_def by simp
lemma sign_Min_lt_0:
- "(bin_sign bin = Int.Min) = (number_of bin < (0 :: int))"
- by (induct bin rule: numeral_induct) auto
+ "(bin_sign bin = -1) = (bin < (0 :: int))"
+ unfolding bin_sign_def by simp
lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]]
--- a/src/HOL/Word/Word.thy Thu Feb 23 16:02:07 2012 +0100
+++ b/src/HOL/Word/Word.thy Thu Feb 23 16:18:19 2012 +0100
@@ -561,7 +561,7 @@
using word_sint.Rep [of x] by (simp add: sints_num)
lemma sign_uint_Pls [simp]:
- "bin_sign (uint x) = Int.Pls"
+ "bin_sign (uint x) = 0"
by (simp add: sign_Pls_ge_0 number_of_eq)
lemma uint_m2p_neg: "uint (x::'a::len0 word) - 2 ^ len_of TYPE('a) < 0"
@@ -587,7 +587,7 @@
by (simp only: int_word_uint)
lemma unat_number_of:
- "bin_sign b = Int.Pls \<Longrightarrow>
+ "bin_sign (number_of b) = 0 \<Longrightarrow>
unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)"
apply (unfold unat_def)
apply (clarsimp simp only: uint_number_of)
@@ -790,14 +790,6 @@
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 *)
-lemma num_AB_u [simp]: "number_of (uint x) = x"
- unfolding word_number_of_def by (rule word_uint.Rep_inverse)
-
-lemma num_AB_s [simp]: "number_of (sint x) = x"
- unfolding word_number_of_def by (rule word_sint.Rep_inverse)
-
(* naturals *)
lemma uints_unats: "uints n = int ` unats n"
apply (unfold unats_def uints_num)
@@ -1653,16 +1645,6 @@
subsection "Arithmetic type class instantiations"
-(* note that iszero_def is only for class comm_semiring_1_cancel,
- which requires word length >= 1, ie 'a :: len word *)
-lemma zero_bintrunc:
- "iszero (number_of x :: 'a :: len word) =
- (bintrunc (len_of TYPE('a)) x = Int.Pls)"
- apply (unfold iszero_def word_0_wi word_no_wi)
- apply (rule word_ubin.norm_eq_iff [symmetric, THEN trans])
- apply (simp add : Pls_def [symmetric])
- done
-
lemmas word_le_0_iff [simp] =
word_zero_le [THEN leD, THEN linorder_antisym_conv1]
@@ -1670,14 +1652,14 @@
"0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
by (simp add: of_nat_nat word_of_int)
-lemma iszero_word_no [simp] :
+(* note that iszero_def is only for class comm_semiring_1_cancel,
+ which requires word length >= 1, ie 'a :: len word *)
+lemma iszero_word_no [simp]:
"iszero (number_of bin :: 'a :: len word) =
iszero (bintrunc (len_of TYPE('a)) (number_of bin))"
- apply (simp add: zero_bintrunc number_of_is_id)
- apply (unfold iszero_def Pls_def)
- apply (rule refl)
- done
-
+ using word_ubin.norm_eq_iff [where 'a='a, of "number_of bin" 0]
+ by (simp add: iszero_def [symmetric])
+
subsection "Word and nat"
@@ -2317,8 +2299,7 @@
unfolding word_lsb_def bin_last_def by auto
lemma word_msb_sint: "msb w = (sint w < 0)"
- unfolding word_msb_def
- by (simp add : sign_Min_lt_0 number_of_is_id)
+ unfolding word_msb_def sign_Min_lt_0 ..
lemma msb_word_of_int:
"msb (word_of_int x::'a::len word) = bin_nth x (len_of TYPE('a) - 1)"