# HG changeset patch
# User huffman
# Date 1330003769 -3600
# Node ID b2563f7cf84459544b5f88f274d0d346d101e2fd
# Parent  9f9e85264e4d7fbe2f268ddc9aa080f3fe06b473
simplify proofs

diff -r 9f9e85264e4d -r b2563f7cf844 src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Thu Feb 23 13:16:18 2012 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Thu Feb 23 14:29:29 2012 +0100
@@ -375,18 +375,14 @@
   "bin_sc n 0 w <= w"
   apply (induct n arbitrary: w)
    apply (case_tac [!] w rule: bin_exhaust)
-   apply (auto simp del: BIT_simps)
-   apply (unfold Bit_def)
-   apply (simp_all add: bitval_def split: bit.split)
+   apply (auto simp: le_Bits)
   done
 
 lemma bin_set_ge:
   "bin_sc n 1 w >= w"
   apply (induct n arbitrary: w)
    apply (case_tac [!] w rule: bin_exhaust)
-   apply (auto simp del: BIT_simps)
-   apply (unfold Bit_def)
-   apply (simp_all add: bitval_def split: bit.split)
+   apply (auto simp: le_Bits)
   done
 
 lemma bintr_bin_clr_le:
@@ -395,9 +391,7 @@
    apply simp
   apply (case_tac w rule: bin_exhaust)
   apply (case_tac m)
-   apply (auto simp del: BIT_simps)
-   apply (unfold Bit_def)
-   apply (simp_all add: bitval_def split: bit.split)
+   apply (auto simp: le_Bits)
   done
 
 lemma bintr_bin_set_ge:
@@ -406,9 +400,7 @@
    apply simp
   apply (case_tac w rule: bin_exhaust)
   apply (case_tac m)
-   apply (auto simp del: BIT_simps)
-   apply (unfold Bit_def)
-   apply (simp_all add: bitval_def split: bit.split)
+   apply (auto simp: le_Bits)
   done
 
 lemma bin_sc_FP [simp]: "bin_sc n 0 Int.Pls = Int.Pls"