# HG changeset patch # User wenzelm # Date 1330010299 -3600 # Node ID cd0e6841ab9cf8f153af453f965ad7da696688a4 # Parent 0c3a5e28f425dacad12b7d1e01cc1023cf2d1efb# Parent c29bf6741acea7866b355e8948b683d8d5a4dd0d merged; diff -r c29bf6741ace -r cd0e6841ab9c src/HOL/Word/Bit_Int.thy --- 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 diff -r c29bf6741ace -r cd0e6841ab9c src/HOL/Word/Bit_Representation.thy --- 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 \ (1::bit)" assumes y: "y = (0::bit) \ 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]] diff -r c29bf6741ace -r cd0e6841ab9c src/HOL/Word/Word.thy --- 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 \ + "bin_sign (number_of b) = 0 \ 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 \ 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)"