# HG changeset patch # User huffman # Date 1187658147 -7200 # Node ID 223622422d7b32645aed816413f21787a99b8845 # Parent e403ab5c9415d06905ba33bf62a861267f9db98b move order-related stuff from WordDefinition to WordArith diff -r e403ab5c9415 -r 223622422d7b src/HOL/Word/WordArith.thy --- 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" ("(_/ 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) diff -r e403ab5c9415 -r 223622422d7b src/HOL/Word/WordDefinition.thy --- 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" ("(_/ nat => 'a word" primrec