merged

--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 24 19:47:00 2012 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 24 19:47:11 2012 +0100
@@ -331,9 +331,8 @@
    apply clarsimp
   apply clarsimp
   apply safe
-   apply (drule meta_spec, erule preorder_class.order_trans [rotated],
-          simp add: numeral_simps algebra_simps BIT_simps
-          cong add: number_of_False_cong)+
+   apply (drule meta_spec, erule order_trans [rotated],
+          simp add: Bit_B0_2t Bit_B1_2t algebra_simps)+
   done
 
 lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
@@ -377,14 +376,14 @@
   apply safe
    apply (case_tac "m - size bl")
     apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
-   apply (simp add: BIT_simps)
-   apply (rule_tac f = "%nat. bl_to_bin_aux bl (Int.Bit1 (bintrunc nat w))" 
+   apply simp
+   apply (rule_tac f = "%nat. bl_to_bin_aux bl (bintrunc nat w BIT 1)" 
                    in arg_cong)
    apply simp
   apply (case_tac "m - size bl")
    apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
-  apply (simp add: BIT_simps)
-  apply (rule_tac f = "%nat. bl_to_bin_aux bl (Int.Bit0 (bintrunc nat w))" 
+  apply simp
+  apply (rule_tac f = "%nat. bl_to_bin_aux bl (bintrunc nat w BIT 0)"
                   in arg_cong)
   apply simp
   done
@@ -744,26 +743,43 @@
 lemmas rbl_Nils =
   rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
 
-lemma rbl_pred: 
-  "!!bin. rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.pred bin))"
-  apply (induct n, simp)
+lemma pred_BIT_simps [simp]:
+  "x BIT 0 - 1 = (x - 1) BIT 1"
+  "x BIT 1 - 1 = x BIT 0"
+  by (simp_all add: Bit_B0_2t Bit_B1_2t)
+
+lemma rbl_pred:
+  "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
+  apply (induct n arbitrary: bin, simp)
   apply (unfold bin_to_bl_def)
   apply clarsimp
   apply (case_tac bin rule: bin_exhaust)
   apply (case_tac b)
-   apply (clarsimp simp: bin_to_bl_aux_alt BIT_simps)+
+   apply (clarsimp simp: bin_to_bl_aux_alt)+
   done
 
+lemma succ_BIT_simps [simp]:
+  "x BIT 0 + 1 = x BIT 1"
+  "x BIT 1 + 1 = (x + 1) BIT 0"
+  by (simp_all add: Bit_B0_2t Bit_B1_2t)
+
 lemma rbl_succ: 
-  "!!bin. rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (Int.succ bin))"
-  apply (induct n, simp)
+  "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
+  apply (induct n arbitrary: bin, simp)
   apply (unfold bin_to_bl_def)
   apply clarsimp
   apply (case_tac bin rule: bin_exhaust)
   apply (case_tac b)
-   apply (clarsimp simp: bin_to_bl_aux_alt BIT_simps)+
+   apply (clarsimp simp: bin_to_bl_aux_alt)+
   done
 
+lemma add_BIT_simps [simp]: (* FIXME: move *)
+  "x BIT 0 + y BIT 0 = (x + y) BIT 0"
+  "x BIT 0 + y BIT 1 = (x + y) BIT 1"
+  "x BIT 1 + y BIT 0 = (x + y) BIT 1"
+  "x BIT 1 + y BIT 1 = (x + y + 1) BIT 0"
+  by (simp_all add: Bit_B0_2t Bit_B1_2t)
+
 lemma rbl_add: 
   "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 
     rev (bin_to_bl n (bina + binb))"
@@ -774,7 +790,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 BIT_simps)
+     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def add_ac)
   done
 
 lemma rbl_add_app2: 
@@ -848,7 +864,13 @@
   apply simp
   apply (simp add: bin_to_bl_aux_alt)
   done
-  
+
+lemma mult_BIT_simps [simp]:
+  "x BIT 0 * y = (x * y) BIT 0"
+  "x * y BIT 0 = (x * y) BIT 0"
+  "x BIT 1 * y = (x * y) BIT 0 + y"
+  by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps)
+
 lemma rbl_mult: "!!bina binb. 
     rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 
     rev (bin_to_bl n (bina * binb))"
@@ -860,8 +882,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 BIT_simps)
-     apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add BIT_simps)
+     apply (auto simp: bin_to_bl_aux_alt Let_def)
+     apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add)
   done
 
 lemma rbl_add_split: 

--- a/src/HOL/Word/Word.thy	Fri Feb 24 19:47:00 2012 +0100
+++ b/src/HOL/Word/Word.thy	Fri Feb 24 19:47:11 2012 +0100
@@ -1071,9 +1071,6 @@
   (eg) sint (number_of bin) on sint 1, must do
   (simp add: word_1_no del: numeral_1_eq_1) 
   *)
-lemma word_0_wi_Pls: "0 = word_of_int Int.Pls"
-  by (simp only: Pls_def word_0_wi)
-
 lemma word_0_no: "(0::'a::len0 word) = Numeral0"
   by (simp add: word_number_of_alt)
 
@@ -1083,9 +1080,6 @@
 lemma word_m1_wi: "-1 = word_of_int -1" 
   by (rule word_number_of_alt)
 
-lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"
-  by (simp add: word_m1_wi number_of_eq)
-
 lemma word_0_bl [simp]: "of_bl [] = 0"
   unfolding of_bl_def by simp
 
@@ -1598,7 +1592,7 @@
   apply (unfold word_succ_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
-  apply (simp add: to_bl_def rbl_succ Int.succ_def)
+  apply (simp add: to_bl_def rbl_succ)
   done
 
 lemma word_pred_rbl:
@@ -1606,7 +1600,7 @@
   apply (unfold word_pred_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
-  apply (simp add: to_bl_def rbl_pred Int.pred_def)
+  apply (simp add: to_bl_def rbl_pred)
   done
 
 lemma word_add_rbl:
@@ -2140,8 +2134,6 @@
 
 lemmas bwsimps = 
   wi_hom_add
-  word_0_wi_Pls
-  word_m1_wi_Min
   word_wi_log_defs
 
 lemma word_bw_assocs:
@@ -2231,7 +2223,7 @@
   fixes x :: "'a::len0 word"
   shows "x + NOT x = -1"
   using word_of_int_Ex [where x=x] 
-  by (auto simp: bwsimps bin_add_not)
+  by (auto simp: bwsimps bin_add_not [unfolded Min_def])
 
 lemma word_plus_and_or [simp]:
   fixes x :: "'a::len0 word"