HOL-Word: removed more duplicate theorems
authorhuffman
Thu Nov 17 15:07:46 2011 +0100 (2011-11-17)
changeset 4554794c37f3df10f
parent 45546 6dd3e88de4c2
child 45548 3e2722d66169
HOL-Word: removed more duplicate theorems
NEWS
src/HOL/Word/Word.thy
     1.1 --- a/NEWS	Thu Nov 17 14:52:05 2011 +0100
     1.2 +++ b/NEWS	Thu Nov 17 15:07:46 2011 +0100
     1.3 @@ -57,6 +57,10 @@
     1.4    word_mult_ac ~> mult_ac
     1.5    word_plus_ac0 ~> add_0_left add_0_right add_ac
     1.6    word_times_ac1 ~> mult_1_left mult_1_right mult_ac
     1.7 +  word_order_trans ~> order_trans
     1.8 +  word_order_refl ~> order_refl
     1.9 +  word_order_antisym ~> order_antisym
    1.10 +  word_order_linear ~> linorder_linear
    1.11  
    1.12  * Clarified attribute "mono_set": pure declararation without modifying
    1.13  the result of the fact expression.
     2.1 --- a/src/HOL/Word/Word.thy	Thu Nov 17 14:52:05 2011 +0100
     2.2 +++ b/src/HOL/Word/Word.thy	Thu Nov 17 15:07:46 2011 +0100
     2.3 @@ -199,7 +199,7 @@
     2.4  where
     2.5    "word_pred a = word_of_int (Int.pred (uint a))"
     2.6  
     2.7 -instantiation word :: (len0) "{number, Divides.div, ord, comm_monoid_mult, comm_ring}"
     2.8 +instantiation word :: (len0) "{number, Divides.div, comm_monoid_mult, comm_ring}"
     2.9  begin
    2.10  
    2.11  definition
    2.12 @@ -229,12 +229,6 @@
    2.13  definition
    2.14    word_number_of_def: "number_of w = word_of_int w"
    2.15  
    2.16 -definition
    2.17 -  word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
    2.18 -
    2.19 -definition
    2.20 -  word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
    2.21 -
    2.22  lemmas word_arith_wis = 
    2.23    word_add_def word_mult_def word_minus_def 
    2.24    word_succ_def word_pred_def word_0_wi word_1_wi
    2.25 @@ -316,6 +310,23 @@
    2.26  definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
    2.27    "a udvd b = (EX n>=0. uint b = n * uint a)"
    2.28  
    2.29 +
    2.30 +subsection "Ordering"
    2.31 +
    2.32 +instantiation word :: (len0) linorder
    2.33 +begin
    2.34 +
    2.35 +definition
    2.36 +  word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
    2.37 +
    2.38 +definition
    2.39 +  word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
    2.40 +
    2.41 +instance
    2.42 +  by default (auto simp: word_less_def word_le_def)
    2.43 +
    2.44 +end
    2.45 +
    2.46  definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
    2.47    "a <=s b = (sint a <= sint b)"
    2.48  
    2.49 @@ -1265,26 +1276,10 @@
    2.50  
    2.51  subsection "Order on fixed-length words"
    2.52  
    2.53 -lemma word_order_trans: "x <= y \<Longrightarrow> y <= z \<Longrightarrow> x <= (z :: 'a :: len0 word)"
    2.54 -  unfolding word_le_def by auto
    2.55 -
    2.56 -lemma word_order_refl: "z <= (z :: 'a :: len0 word)"
    2.57 -  unfolding word_le_def by auto
    2.58 -
    2.59 -lemma word_order_antisym: "x <= y \<Longrightarrow> y <= x \<Longrightarrow> x = (y :: 'a :: len0 word)"
    2.60 -  unfolding word_le_def by (auto intro!: word_uint.Rep_eqD)
    2.61 -
    2.62 -lemma word_order_linear:
    2.63 -  "y <= x | x <= (y :: 'a :: len0 word)"
    2.64 -  unfolding word_le_def by auto
    2.65 -
    2.66  lemma word_zero_le [simp] :
    2.67    "0 <= (y :: 'a :: len0 word)"
    2.68    unfolding word_le_def by auto
    2.69    
    2.70 -instance word :: (len0) linorder
    2.71 -  by intro_classes (auto simp: word_less_def word_le_def)
    2.72 -
    2.73  lemma word_m1_ge [simp] : "word_pred 0 >= y"
    2.74    unfolding word_le_def
    2.75    by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto