src/HOL/Word/Bit_Int.thy

   done
   
 lemma bin_rec_Bit:
   "f = bin_rec f1 f2 f3  ==> f3 Int.Pls (0::bit) f1 = f1 ==> 
     f3 Int.Min (1::bit) f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
-  by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
+  by (cases b, simp add: bin_rec_Bit0 BIT_simps, simp add: bin_rec_Bit1 BIT_simps)
 
 lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
   bin_rec_Bit0 bin_rec_Bit1
 
 

   "NOT Int.Pls = Int.Min"
   "NOT Int.Min = Int.Pls"
   "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
   "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
   "NOT (w BIT b) = (NOT w) BIT (NOT b)"
-  unfolding int_not_def Pls_def [symmetric] Min_def [symmetric] by (simp_all add: bin_rec_simps)
+  unfolding int_not_def Pls_def [symmetric] Min_def [symmetric]
+  by (simp_all add: bin_rec_simps BIT_simps)
 
 lemma int_xor_Pls [simp]: 
   "Int.Pls XOR x = x"
   unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM)
 

   "Int.Min OR x = Int.Min"
   by (unfold int_or_def Pls_def [symmetric] Min_def [symmetric]) (simp add: bin_rec_PM)
 
 lemma int_or_Bits [simp]: 
   "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
-  unfolding int_or_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_simps)
+  unfolding int_or_def Pls_def [symmetric] Min_def [symmetric]
+  by (simp add: bin_rec_simps BIT_simps)
 
 lemma int_or_Bits2 [simp]: 
   "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
   "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
   "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"

   "Int.Min AND x = x"
   unfolding int_and_def by (simp add: bin_rec_PM)
 
 lemma int_and_Bits [simp]: 
   "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
-  unfolding int_and_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_simps)
+  unfolding int_and_def Pls_def [symmetric] Min_def [symmetric]
+  by (simp add: bin_rec_simps BIT_simps)
 
 lemma int_and_Bits2 [simp]: 
   "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
   "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
   "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"

     apply clarsimp
    apply clarsimp
   apply (case_tac x rule: bin_exhaust)
   apply (case_tac b)
    apply (case_tac [!] bit)
-     apply (auto simp: less_eq_int_code)
+     apply (auto simp: less_eq_int_code BIT_simps)
   done
 
 lemmas int_and_le =
   xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or]
 

 (* good example of bin_induction *)
 lemma bin_add_not: "x + NOT x = Int.Min"
   apply (induct x rule: bin_induct)
     apply clarsimp
    apply clarsimp
-  apply (case_tac bit, auto)
+  apply (case_tac bit, auto simp: BIT_simps)
   done
 
 subsubsection {* Truncating results of bit-wise operations *}
 
 lemma bin_trunc_ao: 

    apply (unfold Bit_def)
    apply (simp_all add: bitval_def split: bit.split)
   done
 
 lemma bin_sc_FP [simp]: "bin_sc n 0 Int.Pls = Int.Pls"
-  by (induct n) auto
+  by (induct n) (auto simp: BIT_simps)
 
 lemma bin_sc_TM [simp]: "bin_sc n 1 Int.Min = Int.Min"
-  by (induct n) auto
+  by (induct n) (auto simp: BIT_simps)
   
 lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
 
 lemma bin_sc_minus:
   "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"

   "!!w. bin_split n (bin_cat v n w) = (v, bintrunc n w)"
   by (induct n) auto
 
 lemma bin_split_Pls [simp]:
   "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
-  by (induct n) (auto simp: Let_def split: ls_splits)
+  by (induct n) (auto simp: Let_def BIT_simps split: ls_splits)
 
 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)
 

   "!!m b c. bin_split (min m n) c = (a, b) ==> 
     bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
   apply (induct n, clarsimp)
   apply (simp add: bin_rest_trunc Let_def split: ls_splits)
   apply (case_tac m)
-   apply (auto simp: Let_def split: ls_splits)
+   apply (auto simp: Let_def BIT_simps split: ls_splits)
   done
 
 lemma bin_split_trunc1:
   "!!m b c. bin_split n c = (a, b) ==> 
     bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
   apply (induct n, clarsimp)
   apply (simp add: bin_rest_trunc Let_def split: ls_splits)
   apply (case_tac m)
-   apply (auto simp: Let_def split: ls_splits)
+   apply (auto simp: Let_def BIT_simps split: ls_splits)
   done
 
 lemma bin_cat_num:
   "!!b. bin_cat a n b = a * 2 ^ n + bintrunc n b"
   apply (induct n, clarsimp)