# HG changeset patch
# User huffman
# Date 1321448311 -3600
# Node ID 0e1037d4e049e9f20ddf90e349f8bb7950195ffe
# Parent  726b743855ea7506bf9b2ad0fca05b005487fc15
remove redundant lemmas bin_last_mod and bin_rest_div, use bin_last_def and bin_rest_def instead

diff -r 726b743855ea -r 0e1037d4e049 src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Wed Nov 16 12:29:50 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Wed Nov 16 13:58:31 2011 +0100
@@ -657,7 +657,7 @@
 lemma bin_split_num:
   "!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
   apply (induct n, clarsimp)
-  apply (simp add: bin_rest_div zdiv_zmult2_eq)
+  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
diff -r 726b743855ea -r 0e1037d4e049 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Wed Nov 16 12:29:50 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Wed Nov 16 13:58:31 2011 +0100
@@ -227,26 +227,8 @@
   "bin_rest -1 = -1"
   by (simp_all add: bin_last_def bin_rest_def)
 
-lemma bin_last_mod: 
-  "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))"
-  apply (case_tac w rule: bin_exhaust)
-  apply (case_tac b)
-   apply auto
-  done
-
-lemma bin_rest_div: 
-  "bin_rest w = w div 2"
-  apply (case_tac w rule: bin_exhaust)
-  apply (rule trans)
-   apply clarsimp
-   apply (rule refl)
-  apply (drule trans)
-   apply (rule Bit_def)
-  apply (simp add: bitval_def z1pdiv2 split: bit.split)
-  done
-
 lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
-  unfolding bin_rest_div [symmetric] by auto
+  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
@@ -358,7 +340,7 @@
 lemma bintrunc_mod2p:
   "!!w. bintrunc n w = (w mod 2 ^ n :: int)"
   apply (induct n, clarsimp)
-  apply (simp add: bin_last_mod bin_rest_div Bit_def zmod_zmult2_eq
+  apply (simp add: bin_last_def bin_rest_def Bit_def zmod_zmult2_eq
               cong: number_of_False_cong)
   done
 
@@ -367,10 +349,10 @@
   apply (induct n)
    apply clarsimp
    apply (subst mod_add_left_eq)
-   apply (simp add: bin_last_mod)
+   apply (simp add: bin_last_def)
    apply (simp add: number_of_eq)
   apply clarsimp
-  apply (simp add: bin_last_mod bin_rest_div Bit_def 
+  apply (simp add: bin_last_def bin_rest_def Bit_def 
               cong: number_of_False_cong)
   apply (clarsimp simp: mod_mult_mult1 [symmetric] 
          zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
diff -r 726b743855ea -r 0e1037d4e049 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Nov 16 12:29:50 2011 +0100
+++ b/src/HOL/Word/Word.thy	Wed Nov 16 13:58:31 2011 +0100
@@ -2428,7 +2428,7 @@
   done
 
 lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
-  unfolding word_lsb_def bin_last_mod by auto
+  unfolding word_lsb_def bin_last_def by auto
 
 lemma word_msb_sint: "msb w = (sint w < 0)" 
   unfolding word_msb_def
@@ -2823,7 +2823,7 @@
   done
     
 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
-  apply (unfold shiftr1_def bin_rest_div)
+  apply (unfold shiftr1_def bin_rest_def)
   apply (rule word_uint.Abs_inverse)
   apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
   apply (rule xtr7)
@@ -2833,7 +2833,7 @@
   done
 
 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
-  apply (unfold sshiftr1_def bin_rest_div [symmetric])
+  apply (unfold sshiftr1_def bin_rest_def [symmetric])
   apply (simp add: word_sbin.eq_norm)
   apply (rule trans)
    defer