# HG changeset patch
# User huffman
# Date 1324988182 -3600
# Node ID 871bdab23f5c9d36dd3510ac68d45cc72ba13a2c
# Parent  cce7e6197a46b905e30e9b17c3ec98bcf348fcb1
remove some uses of Int.succ and Int.pred

diff -r cce7e6197a46 -r 871bdab23f5c src/HOL/Word/Bit_Representation.thy
--- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 27 12:49:03 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 27 13:16:22 2011 +0100
@@ -723,9 +723,9 @@
   zmod_zsub_left_eq [where b = "1"]
 
 lemmas bintr_arith1s =
-  brdmod1s' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n
+  brdmod1s' [where c="2^n::int", folded bintrunc_mod2p] for n
 lemmas bintr_ariths =
-  brdmods' [where c="2^n::int", folded pred_def succ_def bintrunc_mod2p] for n
+  brdmods' [where c="2^n::int", folded bintrunc_mod2p] for n
 
 lemmas m2pths = pos_mod_sign pos_mod_bound [OF zless2p]
 
diff -r cce7e6197a46 -r 871bdab23f5c src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Dec 27 12:49:03 2011 +0100
+++ b/src/HOL/Word/Word.thy	Tue Dec 27 13:16:22 2011 +0100
@@ -190,12 +190,12 @@
 definition
   word_succ :: "'a :: len0 word => 'a word"
 where
-  "word_succ a = word_of_int (Int.succ (uint a))"
+  "word_succ a = word_of_int (uint a + 1)"
 
 definition
   word_pred :: "'a :: len0 word => 'a word"
 where
-  "word_pred a = word_of_int (Int.pred (uint a))"
+  "word_pred a = word_of_int (uint a - 1)"
 
 instantiation word :: (len0) "{number, Divides.div, comm_monoid_mult, comm_ring}"
 begin
@@ -239,8 +239,8 @@
   wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
   wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
   wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
-  wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Int.succ a)" and
-  wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
+  wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" and
+  wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)"
   by (auto simp: word_arith_wis arths)
 
 lemmas wi_hom_syms = wi_homs [symmetric]
@@ -255,17 +255,17 @@
 lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric]
 
 lemmas word_of_int_hom_syms =
-  new_word_of_int_hom_syms [unfolded succ_def pred_def]
+  new_word_of_int_hom_syms (* FIXME: duplicate *)
 
 lemmas word_of_int_homs =
-  new_word_of_int_homs [unfolded succ_def pred_def]
+  new_word_of_int_homs (* FIXME: duplicate *)
 
 (* FIXME: provide only one copy of these theorems! *)
 lemmas word_of_int_add_hom = wi_hom_add
 lemmas word_of_int_mult_hom = wi_hom_mult
 lemmas word_of_int_minus_hom = wi_hom_neg
-lemmas word_of_int_succ_hom = wi_hom_succ [unfolded succ_def]
-lemmas word_of_int_pred_hom = wi_hom_pred [unfolded pred_def]
+lemmas word_of_int_succ_hom = wi_hom_succ
+lemmas word_of_int_pred_hom = wi_hom_pred
 lemmas word_of_int_0_hom = word_0_wi
 lemmas word_of_int_1_hom = word_1_wi
 
@@ -1192,11 +1192,11 @@
 (* now, to get the weaker results analogous to word_div/mod_def *)
 
 lemmas word_arith_alts = 
-  word_sub_wi [unfolded succ_def pred_def]
-  word_arith_wis [unfolded succ_def pred_def]
-
-lemmas word_succ_alt = word_arith_alts (5)
-lemmas word_pred_alt = word_arith_alts (6)
+  word_sub_wi
+  word_arith_wis (* FIXME: duplicate *)
+
+lemmas word_succ_alt = word_succ_def (* FIXME: duplicate *)
+lemmas word_pred_alt = word_pred_def (* FIXME: duplicate *)
 
 subsection  "Transferring goals from words to ints"
 
@@ -1209,7 +1209,7 @@
   word_mult_succ: "word_succ a * b = b + a * b"
   by (rule word_uint.Abs_cases [of b],
       rule word_uint.Abs_cases [of a],
-      simp add: pred_def succ_def add_commute mult_commute 
+      simp add: add_commute mult_commute 
                 ring_distribs new_word_of_int_homs
            del: word_of_int_0 word_of_int_1)+
 
@@ -1242,7 +1242,8 @@
 lemma succ_pred_no [simp]:
   "word_succ (number_of bin) = number_of (Int.succ bin) & 
     word_pred (number_of bin) = number_of (Int.pred bin)"
-  unfolding word_number_of_def by (simp add : new_word_of_int_homs)
+  unfolding word_number_of_def Int.succ_def Int.pred_def
+  by (simp add: new_word_of_int_homs)
 
 lemma word_sp_01 [simp] : 
   "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
@@ -1638,7 +1639,7 @@
   apply (unfold word_succ_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
-  apply (simp add: to_bl_def rbl_succ)
+  apply (simp add: to_bl_def rbl_succ Int.succ_def)
   done
 
 lemma word_pred_rbl:
@@ -1646,7 +1647,7 @@
   apply (unfold word_pred_def)
   apply clarify
   apply (simp add: to_bl_of_bin)
-  apply (simp add: to_bl_def rbl_pred)
+  apply (simp add: to_bl_def rbl_pred Int.pred_def)
   done
 
 lemma word_add_rbl: