# HG changeset patch
# User nipkow
# Date 1251481399 -7200
# Node ID 7a91c7bcfe7e7425e1ff8d18982911c1cd1a343b
# Parent  620a5d8cfa78dfe1b516f0156ec9fb58dcda21de
tuned proofs

diff -r 620a5d8cfa78 -r 7a91c7bcfe7e src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Fri Aug 28 19:35:49 2009 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Fri Aug 28 19:43:19 2009 +0200
@@ -918,8 +918,8 @@
   apply (frule asm_rl)
   apply (drule spec)
   apply (erule trans)
-  apply (drule_tac x = "bin_cat y n a" in spec) 
-  apply (simp add : bin_cat_assoc_sym min_def)
+  apply (drule_tac x = "bin_cat y n a" in spec)
+  apply (simp add : bin_cat_assoc_sym)
   done
 
 lemma bin_rcat_bl:
diff -r 620a5d8cfa78 -r 7a91c7bcfe7e src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Fri Aug 28 19:35:49 2009 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Fri Aug 28 19:43:19 2009 +0200
@@ -493,7 +493,7 @@
 
 lemma sbintrunc_sbintrunc_l:
   "n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)"
-  by (rule bin_eqI) (auto simp: nth_sbintr min_def)
+  by (rule bin_eqI) (auto simp: nth_sbintr)
 
 lemma bintrunc_bintrunc_ge:
   "n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)"
@@ -501,14 +501,12 @@
 
 lemma bintrunc_bintrunc_min [simp]:
   "bintrunc m (bintrunc n w) = bintrunc (min m n) w"
-  apply (unfold min_def)
   apply (rule bin_eqI)
   apply (auto simp: nth_bintr)
   done
 
 lemma sbintrunc_sbintrunc_min [simp]:
   "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
-  apply (unfold min_def)
   apply (rule bin_eqI)
   apply (auto simp: nth_sbintr)
   done
diff -r 620a5d8cfa78 -r 7a91c7bcfe7e src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Fri Aug 28 19:35:49 2009 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Fri Aug 28 19:43:19 2009 +0200
@@ -380,7 +380,7 @@
   "n >= size w ==> bintrunc n (uint w) = uint w"
   apply (unfold word_size)
   apply (subst word_ubin.norm_Rep [symmetric]) 
-  apply (simp only: bintrunc_bintrunc_min word_size min_def)
+  apply (simp only: bintrunc_bintrunc_min word_size)
   apply simp
   done
 
@@ -388,7 +388,7 @@
   "wb = word_of_int bin ==> n >= size wb ==> 
     word_of_int (bintrunc n bin) = wb"
   unfolding word_size
-  by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric] min_def)
+  by (clarsimp simp add : word_ubin.norm_eq_iff [symmetric])
 
 lemmas bintr_uint = bintr_uint' [unfolded word_size]
 lemmas wi_bintr = wi_bintr' [unfolded word_size]
diff -r 620a5d8cfa78 -r 7a91c7bcfe7e src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Fri Aug 28 19:35:49 2009 +0200
+++ b/src/HOL/Word/WordShift.thy	Fri Aug 28 19:43:19 2009 +0200
@@ -319,7 +319,7 @@
 
 lemma bl_shiftl:
   "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
-  by (simp add: shiftl_bl word_rep_drop word_size min_def)
+  by (simp add: shiftl_bl word_rep_drop word_size)
 
 lemma shiftl_zero_size: 
   fixes x :: "'a::len0 word"
@@ -1018,8 +1018,7 @@
   word_of_int (bin_cat w (size b) (uint b))"
   apply (unfold word_cat_def word_size) 
   apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
-      word_ubin.eq_norm bintr_cat min_def)
-  apply arith
+      word_ubin.eq_norm bintr_cat)
   done
 
 lemma word_cat_split_alt: