# HG changeset patch # User huffman # Date 1323774347 -3600 # Node ID 4158f35a5c6ff998d191c45cfb316a54eb990ef0 # Parent 6374cd925b185b29c38b34567b4094c4f242bc19 remove some unwanted numeral-representation-specific simp rules diff -r 6374cd925b18 -r 4158f35a5c6f src/HOL/Word/Bit_Int.thy --- a/src/HOL/Word/Bit_Int.thy Tue Dec 13 11:48:59 2011 +0100 +++ b/src/HOL/Word/Bit_Int.thy Tue Dec 13 12:05:47 2011 +0100 @@ -144,7 +144,7 @@ lemma int_and_Pls [simp]: "Int.Pls AND x = Int.Pls" - unfolding int_and_def by (simp add: bin_rec_PM) + unfolding int_and_def Pls_def [symmetric] by (simp add: bin_rec_PM) lemma int_and_Min [simp]: "Int.Min AND x = x" @@ -598,7 +598,7 @@ lemma bin_split_num: "!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)" - apply (induct n, clarsimp) + apply (induct n, simp add: Pls_def) apply (simp add: bin_rest_def zdiv_zmult2_eq) apply (case_tac b rule: bin_exhaust) apply simp diff -r 6374cd925b18 -r 4158f35a5c6f src/HOL/Word/Bit_Representation.thy --- a/src/HOL/Word/Bit_Representation.thy Tue Dec 13 11:48:59 2011 +0100 +++ b/src/HOL/Word/Bit_Representation.thy Tue Dec 13 12:05:47 2011 +0100 @@ -54,11 +54,6 @@ lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1 -lemmas PlsMin_defs [intro!] = - Pls_def Min_def Pls_def [symmetric] Min_def [symmetric] - -lemmas PlsMin_simps [simp] = PlsMin_defs [THEN Eq_TrueI] - lemma number_of_False_cong: "False \ number_of x = number_of y" by (rule FalseE) @@ -329,7 +324,9 @@ "sbintrunc 0 bin = (case bin_last bin of (1::bit) => - 1 | (0::bit) => 0)" "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)" - apply simp_all apply (cases "bin_last bin") apply simp apply (unfold Min_def number_of_is_id) apply simp done + apply simp_all + apply (simp only: Pls_def Min_def) + done lemma sign_bintr: "!!w. bin_sign (bintrunc n w) = Int.Pls" @@ -337,7 +334,8 @@ lemma bintrunc_mod2p: "!!w. bintrunc n w = (w mod 2 ^ n :: int)" - apply (induct n, clarsimp) + apply (induct n) + apply (simp add: Pls_def) apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq cong: number_of_False_cong) done @@ -349,7 +347,7 @@ apply (subst mod_add_left_eq) apply (simp add: bin_last_def) apply (simp add: number_of_eq) - apply clarsimp + apply (simp add: Pls_def) apply (simp add: bin_last_def bin_rest_def Bit_def cong: number_of_False_cong) apply (clarsimp simp: mod_mult_mult1 [symmetric] diff -r 6374cd925b18 -r 4158f35a5c6f src/HOL/Word/Bool_List_Representation.thy --- a/src/HOL/Word/Bool_List_Representation.thy Tue Dec 13 11:48:59 2011 +0100 +++ b/src/HOL/Word/Bool_List_Representation.thy Tue Dec 13 12:05:47 2011 +0100 @@ -348,7 +348,7 @@ apply (unfold bl_to_bin_def) apply (rule xtr4) apply (rule bl_to_bin_ge2p_aux) - apply simp + apply (simp add: Pls_def) done lemma butlast_rest_bin: