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