# HG changeset patch
# User huffman
# Date 1323776201 -3600
# Node ID b4254b2e2b4ab7999634c7643b971618650a15d1
# Parent  518a245a1ab6411cd371e242bee84757fc22e2a5
towards removing BIT_simps from the simpset

diff -r 518a245a1ab6 -r b4254b2e2b4a src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Tue Dec 13 12:10:43 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Tue Dec 13 12:36:41 2011 +0100
@@ -54,7 +54,7 @@
 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
@@ -95,7 +95,8 @@
   "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"
@@ -133,7 +134,8 @@
 
 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)"
@@ -152,7 +154,8 @@
 
 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)"
@@ -322,7 +325,7 @@
   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 =
@@ -334,7 +337,7 @@
   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 *}
@@ -447,10 +450,10 @@
   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
 
@@ -566,7 +569,7 @@
 
 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)"
@@ -578,7 +581,7 @@
   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:
@@ -587,7 +590,7 @@
   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:
diff -r 518a245a1ab6 -r b4254b2e2b4a src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 12:10:43 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 13 12:36:41 2011 +0100
@@ -46,10 +46,10 @@
 lemma BIT_eq: "u BIT b = v BIT c ==> u = v & b = c"
   by (metis bin_rest_BIT bin_last_BIT)
 
-lemma BIT_B0_eq_Bit0 [simp]: "w BIT 0 = Int.Bit0 w"
+lemma BIT_B0_eq_Bit0: "w BIT 0 = Int.Bit0 w"
   unfolding Bit_def Bit0_def by simp
 
-lemma BIT_B1_eq_Bit1 [simp]: "w BIT 1 = Int.Bit1 w"
+lemma BIT_B1_eq_Bit1: "w BIT 1 = Int.Bit1 w"
   unfolding Bit_def Bit1_def by simp
 
 lemmas BIT_simps = BIT_B0_eq_Bit0 BIT_B1_eq_Bit1
@@ -147,7 +147,7 @@
   "bin_rl (Int.Bit0 r) = (r, (0::bit))"
   "bin_rl (Int.Bit1 r) = (r, (1::bit))"
   "bin_rl (r BIT b) = (r, b)"
-  unfolding bin_rl_char by simp_all
+  unfolding bin_rl_char by (simp_all add: BIT_simps)
 
 lemma bin_abs_lem:
   "bin = (w BIT b) ==> ~ bin = Int.Min --> ~ bin = Int.Pls -->
@@ -183,11 +183,11 @@
    apply (rule Min)
   apply (case_tac bit)
    apply (case_tac "bin = Int.Pls")
-    apply simp
-   apply (simp add: Bit0)
+    apply (simp add: BIT_simps)
+   apply (simp add: Bit0 BIT_simps)
   apply (case_tac "bin = Int.Min")
-   apply simp
-  apply (simp add: Bit1)
+   apply (simp add: BIT_simps)
+  apply (simp add: Bit1 BIT_simps)
   done
 
 lemma bin_rest_simps [simp]: 
@@ -221,10 +221,10 @@
   unfolding bin_rest_def [symmetric] by auto
 
 lemma Bit0_div2 [simp]: "(Int.Bit0 w) div 2 = w"
-  using Bit_div2 [where b="(0::bit)"] by simp
+  using Bit_div2 [where b="(0::bit)"] by (simp add: BIT_simps)
 
 lemma Bit1_div2 [simp]: "(Int.Bit1 w) div 2 = w"
-  using Bit_div2 [where b="(1::bit)"] by simp
+  using Bit_div2 [where b="(1::bit)"] by (simp add: BIT_simps)
 
 lemma bin_nth_lem [rule_format]:
   "ALL y. bin_nth x = bin_nth y --> x = y"
@@ -236,14 +236,14 @@
       apply (drule_tac x=0 in fun_cong, force)
      apply (erule notE, rule ext, 
             drule_tac x="Suc x" in fun_cong, force)
-    apply (drule_tac x=0 in fun_cong, force)
+    apply (drule_tac x=0 in fun_cong, force simp: BIT_simps)
    apply (erule rev_mp)
    apply (induct_tac y rule: bin_induct)
      apply (safe del: subset_antisym)
      apply (drule_tac x=0 in fun_cong, force)
     apply (erule notE, rule ext, 
            drule_tac x="Suc x" in fun_cong, force)
-   apply (drule_tac x=0 in fun_cong, force)
+   apply (drule_tac x=0 in fun_cong, force simp: BIT_simps)
   apply (case_tac y rule: bin_exhaust)
   apply clarify
   apply (erule allE)
@@ -280,11 +280,11 @@
 
 lemma bin_nth_minus_Bit0 [simp]:
   "0 < n ==> bin_nth (Int.Bit0 w) n = bin_nth w (n - 1)"
-  using bin_nth_minus [where b="(0::bit)"] by simp
+  using bin_nth_minus [where b="(0::bit)"] by (simp add: BIT_simps)
 
 lemma bin_nth_minus_Bit1 [simp]:
   "0 < n ==> bin_nth (Int.Bit1 w) n = bin_nth w (n - 1)"
-  using bin_nth_minus [where b="(1::bit)"] by simp
+  using bin_nth_minus [where b="(1::bit)"] by (simp add: BIT_simps)
 
 lemmas bin_nth_0 = bin_nth.simps(1)
 lemmas bin_nth_Suc = bin_nth.simps(2)
@@ -392,11 +392,11 @@
 
 lemma bin_nth_Bit0:
   "bin_nth (Int.Bit0 w) n = (EX m. n = Suc m & bin_nth w m)"
-  using bin_nth_Bit [where b="(0::bit)"] by simp
+  using bin_nth_Bit [where b="(0::bit)"] by (simp add: BIT_simps)
 
 lemma bin_nth_Bit1:
   "bin_nth (Int.Bit1 w) n = (n = 0 | (EX m. n = Suc m & bin_nth w m))"
-  using bin_nth_Bit [where b="(1::bit)"] by simp
+  using bin_nth_Bit [where b="(1::bit)"] by (simp add: BIT_simps)
 
 lemma bintrunc_bintrunc_l:
   "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
@@ -433,11 +433,11 @@
 
 lemma bintrunc_Bit0 [simp]:
   "bintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (bintrunc n w)"
-  using bintrunc_BIT [where b="(0::bit)"] by simp
+  using bintrunc_BIT [where b="(0::bit)"] by (simp add: BIT_simps)
 
 lemma bintrunc_Bit1 [simp]:
   "bintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (bintrunc n w)"
-  using bintrunc_BIT [where b="(1::bit)"] by simp
+  using bintrunc_BIT [where b="(1::bit)"] by (simp add: BIT_simps)
 
 lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
   bintrunc_Bit0 bintrunc_Bit1
@@ -453,11 +453,11 @@
 
 lemma sbintrunc_Suc_Bit0 [simp]:
   "sbintrunc (Suc n) (Int.Bit0 w) = Int.Bit0 (sbintrunc n w)"
-  using sbintrunc_Suc_BIT [where b="(0::bit)"] by simp
+  using sbintrunc_Suc_BIT [where b="(0::bit)"] by (simp add: BIT_simps)
 
 lemma sbintrunc_Suc_Bit1 [simp]:
   "sbintrunc (Suc n) (Int.Bit1 w) = Int.Bit1 (sbintrunc n w)"
-  using sbintrunc_Suc_BIT [where b="(1::bit)"] by simp
+  using sbintrunc_Suc_BIT [where b="(1::bit)"] by (simp add: BIT_simps)
 
 lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
   sbintrunc_Suc_Bit0 sbintrunc_Suc_Bit1
@@ -506,12 +506,12 @@
 
 lemma bintrunc_n_Pls [simp]:
   "bintrunc n Int.Pls = Int.Pls"
-  by (induct n) auto
+  by (induct n) (auto simp: BIT_simps)
 
 lemma sbintrunc_n_PM [simp]:
   "sbintrunc n Int.Pls = Int.Pls"
   "sbintrunc n Int.Min = Int.Min"
-  by (induct n) auto
+  by (induct n) (auto simp: BIT_simps)
 
 lemmas thobini1 = arg_cong [where f = "%w. w BIT b"] for b
 
diff -r 518a245a1ab6 -r b4254b2e2b4a src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Tue Dec 13 12:10:43 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Tue Dec 13 12:36:41 2011 +0100
@@ -184,7 +184,7 @@
   done
 
 lemma bl_to_bin_False: "bl_to_bin (False # bl) = bl_to_bin bl"
-  unfolding bl_to_bin_def by auto
+  unfolding bl_to_bin_def by (auto simp: BIT_simps)
   
 lemma bl_to_bin_Nil: "bl_to_bin [] = Int.Pls"
   unfolding bl_to_bin_def by auto
@@ -323,7 +323,8 @@
   apply clarsimp
   apply safe
   apply (erule allE, erule xtr8 [rotated],
-         simp add: numeral_simps algebra_simps cong add : number_of_False_cong)+
+         simp add: numeral_simps algebra_simps BIT_simps
+         cong add: number_of_False_cong)+
   done
 
 lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
@@ -341,7 +342,8 @@
   apply clarsimp
   apply safe
    apply (erule allE, erule preorder_class.order_trans [rotated],
-          simp add: numeral_simps algebra_simps cong add : number_of_False_cong)+
+          simp add: numeral_simps algebra_simps BIT_simps
+          cong add: number_of_False_cong)+
   done
 
 lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
@@ -384,13 +386,13 @@
   apply safe
    apply (case_tac "m - size list")
     apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
-   apply simp
+   apply (simp add: BIT_simps)
    apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit1 (bintrunc nat w))" 
                    in arg_cong) 
    apply simp
   apply (case_tac "m - size list")
    apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
-  apply simp
+  apply (simp add: BIT_simps)
   apply (rule_tac f = "%nat. bl_to_bin_aux list (Int.Bit0 (bintrunc nat w))" 
                   in arg_cong) 
   apply simp
@@ -688,10 +690,10 @@
     Int.succ (bl_to_bin (replicate n True))"
   apply (unfold bl_to_bin_def)
   apply (induct n)
-   apply simp
+   apply (simp add: BIT_simps)
   apply (simp only: Suc_eq_plus1 replicate_add
                     append_Cons [symmetric] bl_to_bin_aux_append)
-  apply simp
+  apply (simp add: BIT_simps)
   done
 
 (* function bl_of_nth *)
@@ -754,7 +756,7 @@
   apply clarsimp
   apply (case_tac bin rule: bin_exhaust)
   apply (case_tac b)
-   apply (clarsimp simp: bin_to_bl_aux_alt)+
+   apply (clarsimp simp: bin_to_bl_aux_alt BIT_simps)+
   done
 
 lemma rbl_succ: 
@@ -764,7 +766,7 @@
   apply clarsimp
   apply (case_tac bin rule: bin_exhaust)
   apply (case_tac b)
-   apply (clarsimp simp: bin_to_bl_aux_alt)+
+   apply (clarsimp simp: bin_to_bl_aux_alt BIT_simps)+
   done
 
 lemma rbl_add: 
@@ -777,7 +779,7 @@
   apply (case_tac binb rule: bin_exhaust)
   apply (case_tac b)
    apply (case_tac [!] "ba")
-     apply (auto simp: rbl_succ succ_def bin_to_bl_aux_alt Let_def add_ac)
+     apply (auto simp: rbl_succ succ_def bin_to_bl_aux_alt Let_def add_ac BIT_simps)
   done
 
 lemma rbl_add_app2: 
@@ -863,8 +865,8 @@
   apply (case_tac binb rule: bin_exhaust)
   apply (case_tac b)
    apply (case_tac [!] "ba")
-     apply (auto simp: bin_to_bl_aux_alt Let_def)
-     apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add)
+     apply (auto simp: bin_to_bl_aux_alt Let_def BIT_simps)
+     apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add BIT_simps)
   done
 
 lemma rbl_add_split: 
diff -r 518a245a1ab6 -r b4254b2e2b4a src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Dec 13 12:10:43 2011 +0100
+++ b/src/HOL/Word/Word.thy	Tue Dec 13 12:36:41 2011 +0100
@@ -1255,7 +1255,7 @@
 
 lemma word_sp_01 [simp] : 
   "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
-  by (unfold word_0_no word_1_no) auto
+  by (unfold word_0_no word_1_no) (auto simp: BIT_simps)
 
 (* alternative approach to lifting arithmetic equalities *)
 lemma word_of_int_Ex:
@@ -2541,10 +2541,10 @@
    apply clarsimp
    apply (case_tac "n")
     apply (clarsimp simp add : word_1_wi [symmetric])
-   apply (clarsimp simp add : word_0_wi [symmetric])
+   apply (clarsimp simp add : word_0_wi [symmetric] BIT_simps)
   apply (drule word_gt_0 [THEN iffD1])
   apply (safe intro!: word_eqI bin_nth_lem ext)
-     apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
+     apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric] BIT_simps)
   done
 
 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
@@ -2556,7 +2556,7 @@
    apply (rule box_equals) 
      apply (rule_tac [2] bintr_ariths (1))+ 
    apply (clarsimp simp add : number_of_is_id)
-  apply simp 
+  apply (simp add: BIT_simps)
   done
 
 lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)" 
@@ -2599,7 +2599,7 @@
   done
 
 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
-  unfolding word_0_no shiftl1_number by auto
+  unfolding word_0_no shiftl1_number by (auto simp: BIT_simps)
 
 lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def]
 
@@ -2920,13 +2920,13 @@
 (* note - the following results use 'a :: len word < number_ring *)
 
 lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
-  apply (simp add: shiftl1_def_u)
+  apply (simp add: shiftl1_def_u BIT_simps)
   apply (simp only:  double_number_of_Bit0 [symmetric])
   apply simp
   done
 
 lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
-  apply (simp add: shiftl1_def_u)
+  apply (simp add: shiftl1_def_u BIT_simps)
   apply (simp only: double_number_of_Bit0 [symmetric])
   apply simp
   done
@@ -4599,4 +4599,7 @@
 
 setup {* SMT_Word.setup *}
 
+text {* Legacy simp rules *}
+declare BIT_simps [simp]
+
 end