# 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 \<Longrightarrow> 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: