--- a/src/HOL/Word/WordArith.thy Tue Aug 21 02:30:14 2007 +0200
+++ b/src/HOL/Word/WordArith.thy Tue Aug 21 03:02:27 2007 +0200
@@ -12,19 +12,6 @@
theory WordArith imports WordDefinition begin
-lemma word_less_alt: "(a < b) = (uint a < uint b)"
- unfolding word_less_def word_le_def
- by (auto simp del: word_uint.Rep_inject
- simp: word_uint.Rep_inject [symmetric])
-
-lemma signed_linorder: "linorder word_sle word_sless"
- apply unfold_locales
- apply (unfold word_sle_def word_sless_def)
- by auto
-
-interpretation signed: linorder ["word_sle" "word_sless"]
- by (rule signed_linorder)
-
lemmas word_arith_wis [THEN meta_eq_to_obj_eq] =
word_add_def word_mult_def word_minus_def
word_succ_def word_pred_def word_0_wi word_1_wi
@@ -39,18 +26,6 @@
lemmas word_mod_no [simp] =
word_mod_def [of "number_of ?a" "number_of ?b"]
-lemmas word_less_no [simp] =
- word_less_def [of "number_of ?a" "number_of ?b"]
-
-lemmas word_le_no [simp] =
- word_le_def [of "number_of ?a" "number_of ?b"]
-
-lemmas word_sless_no [simp] =
- word_sless_def [of "number_of ?a" "number_of ?b"]
-
-lemmas word_sle_no [simp] =
- word_sle_def [of "number_of ?a" "number_of ?b"]
-
(* following two are available in class number_ring,
but convenient to have them here here;
note - the number_ring versions, numeral_0_eq_0 and numeral_1_eq_1
@@ -308,9 +283,54 @@
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 :: (len0) semigroup_add
+ by intro_classes (simp add: word_add_assoc)
+
+instance word :: (len0) 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 :: (len0) ord
+ word_le_def: "a <= b == uint a <= uint b"
+ word_less_def: "x < y == x <= y & x ~= y"
+ ..
+
+constdefs
+ word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50)
+ "a <=s b == sint a <= sint b"
+
+ word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
+ "(x <s y) == (x <=s y & x ~= y)"
+
+lemma word_less_alt: "(a < b) = (uint a < uint b)"
+ unfolding word_less_def word_le_def
+ by (auto simp del: word_uint.Rep_inject
+ simp: word_uint.Rep_inject [symmetric])
+
+lemma signed_linorder: "linorder word_sle word_sless"
+ apply unfold_locales
+ apply (unfold word_sle_def word_sless_def)
+ by auto
+
+interpretation signed: linorder ["word_sle" "word_sless"]
+ by (rule signed_linorder)
+
+lemmas word_less_no [simp] =
+ word_less_def [of "number_of ?a" "number_of ?b"]
+
+lemmas word_le_no [simp] =
+ word_le_def [of "number_of ?a" "number_of ?b"]
+
+lemmas word_sless_no [simp] =
+ word_sless_def [of "number_of ?a" "number_of ?b"]
+
+lemmas word_sle_no [simp] =
+ word_sle_def [of "number_of ?a" "number_of ?b"]
+
lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a :: len0 word)"
unfolding word_le_def by auto
@@ -327,18 +347,10 @@
lemma word_zero_le [simp] :
"0 <= (y :: 'a :: len0 word)"
unfolding word_le_def by auto
-
-instance word :: (len0) semigroup_add
- by intro_classes (simp add: word_add_assoc)
instance word :: (len0) linorder
by intro_classes (auto simp: word_less_def word_le_def)
-instance word :: (len0) ring
- by intro_classes
- (auto simp: word_arith_eqs word_diff_minus
- word_diff_self [unfolded word_diff_minus])
-
lemma word_m1_ge [simp] : "word_pred 0 >= y"
unfolding word_le_def
by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
@@ -375,6 +387,11 @@
(n mod 2 ^ len_of TYPE('a) <= m mod 2 ^ len_of TYPE('a))"
unfolding word_le_def by (simp add: word_uint.eq_norm)
+lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
+
+
+subsection "Divisibility"
+
lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)"
apply (unfold udvd_def)
apply safe
@@ -391,8 +408,6 @@
lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"
unfolding dvd_def udvd_nat_alt by force
-lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
-
lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
unfolding word_arith_wis
by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
@@ -788,8 +803,6 @@
instance word :: (len0) comm_semiring_0 ..
-instance word :: (len0) order ..
-
instance word :: (len) recpower
by (intro_classes) (simp_all add: word_pow)
--- a/src/HOL/Word/WordDefinition.thy Tue Aug 21 02:30:14 2007 +0200
+++ b/src/HOL/Word/WordDefinition.thy Tue Aug 21 03:02:27 2007 +0200
@@ -21,7 +21,6 @@
instance word :: (type) times ..
instance word :: (type) Divides.div ..
instance word :: (type) power ..
-instance word :: (type) ord ..
instance word :: (type) size ..
instance word :: (type) inverse ..
instance word :: (type) bit ..
@@ -85,9 +84,6 @@
word_1_wi: "(1 :: ('a :: len0) word) == word_of_int 1"
word_0_wi: "(0 :: ('a :: len0) word) == word_of_int 0"
- word_le_def: "a <= b == uint a <= uint b"
- word_less_def: "x < y == x <= y & x ~= (y :: 'a :: len0 word)"
-
constdefs
word_succ :: "'a :: len0 word => 'a word"
"word_succ a == word_of_int (Numeral.succ (uint a))"
@@ -98,12 +94,6 @@
udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)
"a udvd b == EX n>=0. uint b = n * uint a"
- word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50)
- "a <=s b == sint a <= sint b"
-
- word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)
- "(x <s y) == (x <=s y & x ~= y)"
-
consts
word_power :: "'a :: len0 word => nat => 'a word"
primrec