merged

--- a/src/HOL/Word/Bool_List_Representation.thy	Thu Feb 23 16:18:19 2012 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Thu Feb 23 17:27:37 2012 +0100
@@ -90,14 +90,14 @@
     bin_to_bl_aux (n - 1) 0 (False # bl)"
   by (cases n) auto
 
-lemma bin_to_bl_aux_Pls_minus_simp [simp]:
-  "0 < n ==> bin_to_bl_aux n Int.Pls bl = 
-    bin_to_bl_aux (n - 1) Int.Pls (False # bl)"
+lemma bin_to_bl_aux_minus1_minus_simp [simp]:
+  "0 < n ==> bin_to_bl_aux n -1 bl = 
+    bin_to_bl_aux (n - 1) -1 (True # bl)"
   by (cases n) auto
 
-lemma bin_to_bl_aux_Min_minus_simp [simp]:
-  "0 < n ==> bin_to_bl_aux n Int.Min bl = 
-    bin_to_bl_aux (n - 1) Int.Min (True # bl)"
+lemma bin_to_bl_aux_one_minus_simp [simp]:
+  "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = 
+    bin_to_bl_aux (n - 1) 0 (True # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_Bit_minus_simp [simp]:
@@ -106,13 +106,13 @@
   by (cases n) auto
 
 lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
-  "0 < n ==> bin_to_bl_aux n (Int.Bit0 w) bl = 
-    bin_to_bl_aux (n - 1) w (False # bl)"
+  "0 < n ==> bin_to_bl_aux n (number_of (Int.Bit0 w)) bl = 
+    bin_to_bl_aux (n - 1) (number_of w) (False # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
-  "0 < n ==> bin_to_bl_aux n (Int.Bit1 w) bl = 
-    bin_to_bl_aux (n - 1) w (True # bl)"
+  "0 < n ==> bin_to_bl_aux n (number_of (Int.Bit1 w)) bl = 
+    bin_to_bl_aux (n - 1) (number_of w) (True # bl)"
   by (cases n) auto
 
 text {* Link between bin and bool list. *}
@@ -188,19 +188,15 @@
   "bin_to_bl_aux n 0 bl = replicate n False @ bl"
   by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
 
-lemma bin_to_bl_Pls_aux: 
-  "bin_to_bl_aux n Int.Pls bl = replicate n False @ bl"
+lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
+  unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux)
+
+lemma bin_to_bl_minus1_aux:
+  "bin_to_bl_aux n -1 bl = replicate n True @ bl"
   by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
 
-lemma bin_to_bl_Pls: "bin_to_bl n Int.Pls = replicate n False"
-  unfolding bin_to_bl_def by (simp add : bin_to_bl_Pls_aux)
-
-lemma bin_to_bl_Min_aux:
-  "bin_to_bl_aux n Int.Min bl = replicate n True @ bl"
-  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
-
-lemma bin_to_bl_Min: "bin_to_bl n Int.Min = replicate n True"
-  unfolding bin_to_bl_def by (simp add : bin_to_bl_Min_aux)
+lemma bin_to_bl_minus1: "bin_to_bl n -1 = replicate n True"
+  unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux)
 
 lemma bl_to_bin_rep_F: 
   "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
@@ -238,7 +234,7 @@
   by (induct n arbitrary: w bs) auto
 
 lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
-  unfolding bin_to_bl_def len_bin_to_bl_aux by auto
+  by (fact size_bin_to_bl) (* FIXME: duplicate *)
   
 lemma sign_bl_bin': 
   "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
@@ -344,7 +340,7 @@
   apply (unfold bl_to_bin_def)
   apply (rule xtr4)
    apply (rule bl_to_bin_ge2p_aux)
-  apply (simp add: Pls_def)
+  apply simp
   done
 
 lemma butlast_rest_bin: 

--- a/src/HOL/Word/Word.thy	Thu Feb 23 16:18:19 2012 +0100
+++ b/src/HOL/Word/Word.thy	Thu Feb 23 17:27:37 2012 +0100
@@ -779,8 +779,8 @@
   unfolding uint_bl by (clarsimp simp add: word_ubin.eq_norm word_size)
 
 lemma to_bl_no_bin [simp]:
-  "to_bl (number_of bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin"
-  by (fact to_bl_of_bin [folded word_number_of_def])
+  "to_bl (number_of bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) (number_of bin)"
+  unfolding word_number_of_alt by (rule to_bl_of_bin)
 
 lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
   unfolding uint_bl by (simp add : word_size)
@@ -1102,7 +1102,7 @@
 lemma to_bl_0 [simp]:
   "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
   unfolding uint_bl
-  by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric])
+  by (simp add: word_size bin_to_bl_zero)
 
 lemma uint_0_iff: "(uint x = 0) = (x = 0)"
   by (auto intro!: word_uint.Rep_eqD)
@@ -3251,12 +3251,12 @@
 subsubsection "Slices"
 
 lemma slice1_no_bin [simp]:
-  "slice1 n (number_of w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) w))"
+  "slice1 n (number_of w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) (number_of w)))"
   by (simp add: slice1_def)
 
 lemma slice_no_bin [simp]:
   "slice n (number_of w :: 'b word) = of_bl (takefill False (len_of TYPE('b :: len0) - n)
-    (bin_to_bl (len_of TYPE('b :: len0)) w))"
+    (bin_to_bl (len_of TYPE('b :: len0)) (number_of w)))"
   by (simp add: slice_def word_size)
 
 lemma slice1_0 [simp] : "slice1 n 0 = 0"