# HG changeset patch
# User huffman
# Date 1187892945 -7200
# Node ID 640b85390ba03853cb07d51703aecd20e3e05720
# Parent  87ef9b486068acb64a411d3587b6142a0e574eac
new instance proofs

diff -r 87ef9b486068 -r 640b85390ba0 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Thu Aug 23 18:53:53 2007 +0200
+++ b/src/HOL/Word/WordArith.thy	Thu Aug 23 20:15:45 2007 +0200
@@ -125,8 +125,7 @@
 lemmas wi_hom_syms = wi_homs [symmetric]
 
 lemma word_sub_def: "a - b == a + - (b :: 'a word)"
-  unfolding word_sub_wi diff_def
-  by (simp only : word_uint.Rep_inverse wi_hom_syms)
+  by (rule diff_def)
     
 lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard]
 
@@ -219,48 +218,6 @@
   "\<exists>y. x = word_of_int y"
   by (rule_tac x="uint x" in exI) simp
 
-lemma word_arith_eqs:
-  fixes a :: "'a word"
-  fixes b :: "'a word"
-  shows
-  word_add_0: "0 + a = a" and
-  word_add_0_right: "a + 0 = a" and
-  word_mult_1: "1 * a = a" and
-  word_mult_1_right: "a * 1 = a" and
-  word_add_commute: "a + b = b + a" and
-  word_add_assoc: "a + b + c = a + (b + c)" and
-  word_add_left_commute: "a + (b + c) = b + (a + c)" and
-  word_mult_commute: "a * b = b * a" and
-  word_mult_assoc: "a * b * c = a * (b * c)" and
-  word_mult_left_commute: "a * (b * c) = b * (a * c)" and
-  word_left_distrib: "(a + b) * c = a * c + b * c" and
-  word_right_distrib: "a * (b + c) = a * b + a * c" and
-  word_left_minus: "- a + a = 0" and
-  word_diff_0_right: "a - 0 = a" and
-  word_diff_self: "a - a = 0"
-  using word_of_int_Ex [of a] 
-        word_of_int_Ex [of b] 
-        word_of_int_Ex [of c]
-  by (auto simp: word_of_int_hom_syms [symmetric]
-                 zadd_0_right add_commute add_assoc add_left_commute
-                 mult_commute mult_assoc mult_left_commute
-                 plus_times.left_distrib plus_times.right_distrib)
-  
-lemmas word_add_ac = word_add_commute word_add_assoc word_add_left_commute
-lemmas word_mult_ac = word_mult_commute word_mult_assoc word_mult_left_commute
-  
-lemmas word_plus_ac0 = word_add_0 word_add_0_right word_add_ac
-lemmas word_times_ac1 = word_mult_1 word_mult_1_right word_mult_ac
-
-instance word :: (type) semigroup_add
-  by intro_classes (simp add: word_add_assoc)
-
-instance word :: (type) ring
-  by intro_classes
-     (auto simp: word_arith_eqs word_diff_minus 
-                 word_diff_self [unfolded word_diff_minus])
-
-
 subsection "Order on fixed-length words"
 
 instance word :: (type) ord
@@ -561,7 +518,7 @@
 lemma no_olen_add':
   fixes x :: "'a word"
   shows "(x \<le> y + x) = (uint y + uint x < 2 ^ CARD('a))"
-  by (simp add: word_add_ac add_ac no_olen_add)
+  by (simp add: add_ac no_olen_add)
 
 lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric], standard]
 
@@ -729,31 +686,6 @@
 
 subsection "Arithmetic type class instantiations"
 
-instance word :: (type) comm_monoid_add ..
-
-instance word :: (type) comm_monoid_mult
-  apply (intro_classes)
-   apply (simp add: word_mult_commute)
-  apply (simp add: word_mult_1)
-  done
-
-instance word :: (type) comm_semiring 
-  by (intro_classes) (simp add : word_left_distrib)
-
-instance word :: (type) ab_group_add ..
-
-instance word :: (type) comm_ring ..
-
-instance word :: (finite) comm_semiring_1 
-  by (intro_classes) (simp add: lenw1_zero_neq_one)
-
-instance word :: (finite) comm_ring_1 ..
-
-instance word :: (type) comm_semiring_0 ..
-
-instance word :: (finite) recpower
-  by (intro_classes) (simp_all add: word_pow)
-
 (* note that iszero_def is only for class comm_semiring_1_cancel,
    which requires word length >= 1, ie 'a :: finite word *) 
 lemma zero_bintrunc:
@@ -772,8 +704,7 @@
 
 lemma word_of_int: "of_int = word_of_int"
   apply (rule ext)
-  apply (case_tac x rule: int_diff_cases)
-  apply (simp add: word_of_nat word_of_int_sub_hom)
+  apply (simp add: word_of_int Abs_word'_eq)
   done
 
 lemma word_of_int_nat: 
diff -r 87ef9b486068 -r 640b85390ba0 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Thu Aug 23 18:53:53 2007 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Thu Aug 23 20:15:45 2007 +0200
@@ -15,16 +15,74 @@
   = "{(0::int) ..< 2^CARD('a)}" by auto
 
 instance word :: (type) number ..
-instance word :: (type) minus ..
-instance word :: (type) plus ..
-instance word :: (type) one ..
-instance word :: (type) zero ..
-instance word :: (type) times ..
-instance word :: (type) power ..
 instance word :: (type) size ..
 instance word :: (type) inverse ..
 instance word :: (type) bit ..
 
+subsection {* Basic arithmetic *}
+
+definition
+  Abs_word' :: "int \<Rightarrow> 'a word"
+  where "Abs_word' x = Abs_word (x mod 2^CARD('a))"
+
+lemma Rep_word_mod: "Rep_word (x::'a word) mod 2^CARD('a) = Rep_word x"
+  by (simp only: mod_pos_pos_trivial Rep_word [simplified])
+
+lemma Rep_word_inverse': "Abs_word' (Rep_word x) = x"
+  unfolding Abs_word'_def Rep_word_mod
+  by (rule Rep_word_inverse)
+
+lemma Abs_word'_inverse: "Rep_word (Abs_word' z::'a word) = z mod 2^CARD('a)"
+  unfolding Abs_word'_def
+  by (simp add: Abs_word_inverse)
+
+lemmas Rep_word_simps =
+  Rep_word_inject [symmetric]
+  Rep_word_mod
+  Rep_word_inverse'
+  Abs_word'_inverse
+
+instance word :: (type) "{zero,one,plus,minus,times,power}"
+  word_zero_def: "0 \<equiv> Abs_word' 0"
+  word_one_def: "1 \<equiv> Abs_word' 1"
+  word_add_def: "x + y \<equiv> Abs_word' (Rep_word x + Rep_word y)"
+  word_mult_def: "x * y \<equiv> Abs_word' (Rep_word x * Rep_word y)"
+  word_diff_def: "x - y \<equiv> Abs_word' (Rep_word x - Rep_word y)"
+  word_minus_def: "- x \<equiv> Abs_word' (- Rep_word x)"
+  word_power_def: "x ^ n \<equiv> Abs_word' (Rep_word x ^ n)"
+  ..
+
+lemmas word_arith_defs =
+  word_zero_def
+  word_one_def
+  word_add_def
+  word_mult_def
+  word_diff_def
+  word_minus_def
+  word_power_def
+
+instance word :: (type) "{comm_ring,comm_monoid_mult,recpower}"
+  apply (intro_classes, unfold word_arith_defs)
+  apply (simp_all add: Rep_word_simps zmod_simps ring_simps
+                       mod_pos_pos_trivial)
+  done
+
+instance word :: (finite) comm_ring_1
+  apply (intro_classes, unfold word_arith_defs)
+  apply (simp_all add: Rep_word_simps zmod_simps ring_simps
+                       mod_pos_pos_trivial one_less_power)
+  done
+
+lemma word_of_nat: "of_nat n = Abs_word' (int n)"
+  apply (induct n)
+  apply (simp add: word_zero_def)
+  apply (simp add: Rep_word_simps word_arith_defs zmod_simps)
+  done
+
+lemma word_of_int: "of_int z = Abs_word' z"
+  apply (cases z rule: int_diff_cases)
+  apply (simp add: Rep_word_simps word_diff_def word_of_nat zmod_simps)
+  done
 
 subsection "Type conversions and casting"
 
@@ -70,9 +128,15 @@
 
 subsection  "Arithmetic operations"
 
-defs (overloaded)
-  word_1_wi: "(1 :: ('a) word) == word_of_int 1"
-  word_0_wi: "(0 :: ('a) word) == word_of_int 0"
+lemma Abs_word'_eq: "Abs_word' = word_of_int"
+  unfolding expand_fun_eq Abs_word'_def word_of_int_def
+  by (simp add: bintrunc_mod2p)
+
+lemma word_1_wi: "(1 :: ('a) word) == word_of_int 1"
+  by (simp only: word_arith_defs Abs_word'_eq)
+
+lemma word_0_wi: "(0 :: ('a) word) == word_of_int 0"
+  by (simp only: word_arith_defs Abs_word'_eq)
 
 constdefs
   word_succ :: "'a word => 'a word"
@@ -87,13 +151,21 @@
   "word_power a 0 = 1"
   "word_power a (Suc n) = a * word_power a n"
 
-defs (overloaded)
+lemma
   word_pow: "power == word_power"
+  apply (rule eq_reflection, rule ext, rule ext)
+  apply (rename_tac n, induct_tac n, simp_all add: power_Suc)
+  done
+
+lemma
   word_add_def: "a + b == word_of_int (uint a + uint b)"
+and
   word_sub_wi: "a - b == word_of_int (uint a - uint b)"
+and
   word_minus_def: "- a == word_of_int (- uint a)"
+and
   word_mult_def: "a * b == word_of_int (uint a * uint b)"
-
+  by (simp_all only: word_arith_defs Abs_word'_eq uint_def)
 
 subsection "Bit-wise operations"