src/HOL/Word/Bit_Int.thy

   by (induct n arbitrary: w) auto
 
 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) ==> 
     bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
   apply (induct n arbitrary: m b c, clarsimp)

   apply (simp add: Bit_def)
   done
 
 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
   apply (simp add: Bit_def mod_mult_mult1 p1mod22k bitval_def
               split: bit.split)