# HG changeset patch
# User huffman
# Date 1333101743 -7200
# Node ID 172c031ad743c93baebf3433a148707f6a7f2f80
# Parent  2b652cbadde1032020608b066d3cf9fd914f7f60
restate various simp rules for word operations using pred_numeral

diff -r 2b652cbadde1 -r 172c031ad743 src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Fri Mar 30 11:52:26 2012 +0200
+++ b/src/HOL/Word/Bit_Int.thy	Fri Mar 30 12:02:23 2012 +0200
@@ -501,8 +501,8 @@
 
 lemma bin_sc_numeral [simp]:
   "bin_sc (numeral k) b w =
-    bin_sc (numeral k - 1) b (bin_rest w) BIT bin_last w"
-  by (subst expand_Suc, rule bin_sc.Suc)
+    bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
+  by (simp add: numeral_eq_Suc)
 
 
 subsection {* Splitting and concatenation *}
diff -r 2b652cbadde1 -r 172c031ad743 src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Fri Mar 30 11:52:26 2012 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Fri Mar 30 12:02:23 2012 +0200
@@ -229,8 +229,8 @@
   by (cases n) auto
 
 lemma bin_nth_numeral:
-  "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) = bin_nth y (numeral n - 1)"
-  by (subst expand_Suc, simp only: bin_nth.simps)
+  "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) = bin_nth y (pred_numeral n)"
+  by (simp add: numeral_eq_Suc)
 
 lemmas bin_nth_numeral_simps [simp] =
   bin_nth_numeral [OF bin_rest_numeral_simps(2)]
@@ -543,35 +543,35 @@
 
 lemma bintrunc_numeral:
   "bintrunc (numeral k) x =
-    bintrunc (numeral k - 1) (bin_rest x) BIT bin_last x"
-  by (subst expand_Suc, rule bintrunc.simps)
+    bintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
+  by (simp add: numeral_eq_Suc)
 
 lemma sbintrunc_numeral:
   "sbintrunc (numeral k) x =
-    sbintrunc (numeral k - 1) (bin_rest x) BIT bin_last x"
-  by (subst expand_Suc, rule sbintrunc.simps)
+    sbintrunc (pred_numeral k) (bin_rest x) BIT bin_last x"
+  by (simp add: numeral_eq_Suc)
 
 lemma bintrunc_numeral_simps [simp]:
   "bintrunc (numeral k) (numeral (Num.Bit0 w)) =
-    bintrunc (numeral k - 1) (numeral w) BIT 0"
+    bintrunc (pred_numeral k) (numeral w) BIT 0"
   "bintrunc (numeral k) (numeral (Num.Bit1 w)) =
-    bintrunc (numeral k - 1) (numeral w) BIT 1"
+    bintrunc (pred_numeral k) (numeral w) BIT 1"
   "bintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
-    bintrunc (numeral k - 1) (neg_numeral w) BIT 0"
+    bintrunc (pred_numeral k) (neg_numeral w) BIT 0"
   "bintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
-    bintrunc (numeral k - 1) (neg_numeral (w + Num.One)) BIT 1"
+    bintrunc (pred_numeral k) (neg_numeral (w + Num.One)) BIT 1"
   "bintrunc (numeral k) 1 = 1"
   by (simp_all add: bintrunc_numeral)
 
 lemma sbintrunc_numeral_simps [simp]:
   "sbintrunc (numeral k) (numeral (Num.Bit0 w)) =
-    sbintrunc (numeral k - 1) (numeral w) BIT 0"
+    sbintrunc (pred_numeral k) (numeral w) BIT 0"
   "sbintrunc (numeral k) (numeral (Num.Bit1 w)) =
-    sbintrunc (numeral k - 1) (numeral w) BIT 1"
+    sbintrunc (pred_numeral k) (numeral w) BIT 1"
   "sbintrunc (numeral k) (neg_numeral (Num.Bit0 w)) =
-    sbintrunc (numeral k - 1) (neg_numeral w) BIT 0"
+    sbintrunc (pred_numeral k) (neg_numeral w) BIT 0"
   "sbintrunc (numeral k) (neg_numeral (Num.Bit1 w)) =
-    sbintrunc (numeral k - 1) (neg_numeral (w + Num.One)) BIT 1"
+    sbintrunc (pred_numeral k) (neg_numeral (w + Num.One)) BIT 1"
   "sbintrunc (numeral k) 1 = 1"
   by (simp_all add: sbintrunc_numeral)
 
@@ -754,12 +754,12 @@
   by (cases n) simp_all
 
 lemma funpow_numeral [simp]:
-  "f ^^ numeral k = f \<circ> f ^^ (numeral k - 1)"
-  by (subst expand_Suc, rule funpow.simps)
+  "f ^^ numeral k = f \<circ> f ^^ (pred_numeral k)"
+  by (simp add: numeral_eq_Suc)
 
 lemma replicate_numeral [simp]: (* TODO: move to List.thy *)
-  "replicate (numeral k) x = x # replicate (numeral k - 1) x"
-  by (subst expand_Suc, rule replicate_Suc)
+  "replicate (numeral k) x = x # replicate (pred_numeral k) x"
+  by (simp add: numeral_eq_Suc)
 
 lemmas power_minus_simp = 
   trans [OF gen_minus [where f = "power f"] power_Suc] for f
diff -r 2b652cbadde1 -r 172c031ad743 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Mar 30 11:52:26 2012 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Mar 30 12:02:23 2012 +0200
@@ -633,12 +633,12 @@
   takefill_minus [symmetric, THEN trans]]
 
 lemma takefill_numeral_Nil [simp]:
-  "takefill fill (numeral k) [] = fill # takefill fill (numeral k - 1) []"
-  by (subst expand_Suc, rule takefill_Suc_Nil)
+  "takefill fill (numeral k) [] = fill # takefill fill (pred_numeral k) []"
+  by (simp add: numeral_eq_Suc)
 
 lemma takefill_numeral_Cons [simp]:
-  "takefill fill (numeral k) (x # xs) = x # takefill fill (numeral k - 1) xs"
-  by (subst expand_Suc, rule takefill_Suc_Cons)
+  "takefill fill (numeral k) (x # xs) = x # takefill fill (pred_numeral k) xs"
+  by (simp add: numeral_eq_Suc)
 
 (* links with function bl_to_bin *)