--- 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:
--- 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
--- 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]
--- 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: