src/HOL/Word/Word.thy
changeset 55818 d8b2f50705d0
parent 55817 0bc0217387a5
child 55833 6fe16c8a6474
     1.1 --- a/src/HOL/Word/Word.thy	Sat Mar 01 09:34:08 2014 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Sat Mar 01 17:08:39 2014 +0100
     1.3 @@ -1192,7 +1192,7 @@
     1.4  subsection {* Word Arithmetic *}
     1.5  
     1.6  lemma word_less_alt: "(a < b) = (uint a < uint b)"
     1.7 -  unfolding word_less_def word_le_def by (simp add: less_le)
     1.8 +  by (fact word_less_def)
     1.9  
    1.10  lemma signed_linorder: "class.linorder word_sle word_sless"
    1.11    by default (unfold word_sle_def word_sless_def, auto)
    1.12 @@ -1236,16 +1236,20 @@
    1.13    unfolding uint_bl
    1.14    by (simp add: word_size bin_to_bl_zero)
    1.15  
    1.16 -lemma uint_0_iff: "(uint x = 0) = (x = 0)"
    1.17 -  by (auto intro!: word_uint.Rep_eqD)
    1.18 -
    1.19 -lemma unat_0_iff: "(unat x = 0) = (x = 0)"
    1.20 +lemma uint_0_iff:
    1.21 +  "uint x = 0 \<longleftrightarrow> x = 0"
    1.22 +  by (simp add: word_uint_eq_iff)
    1.23 +
    1.24 +lemma unat_0_iff:
    1.25 +  "unat x = 0 \<longleftrightarrow> x = 0"
    1.26    unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)
    1.27  
    1.28 -lemma unat_0 [simp]: "unat 0 = 0"
    1.29 +lemma unat_0 [simp]:
    1.30 +  "unat 0 = 0"
    1.31    unfolding unat_def by auto
    1.32  
    1.33 -lemma size_0_same': "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
    1.34 +lemma size_0_same':
    1.35 +  "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
    1.36    apply (unfold word_size)
    1.37    apply (rule box_equals)
    1.38      defer
    1.39 @@ -1278,8 +1282,7 @@
    1.40    unfolding scast_def by simp
    1.41  
    1.42  lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
    1.43 -  unfolding word_1_wi
    1.44 -  by (simp add: word_ubin.eq_norm bintrunc_minus_simps del: word_of_int_1)
    1.45 +  by (simp only: word_1_wi word_ubin.eq_norm) (simp add: bintrunc_minus_simps(4))
    1.46  
    1.47  lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
    1.48    unfolding unat_def by simp
    1.49 @@ -1289,10 +1292,6 @@
    1.50  
    1.51  (* now, to get the weaker results analogous to word_div/mod_def *)
    1.52  
    1.53 -lemmas word_arith_alts = 
    1.54 -  word_sub_wi
    1.55 -  word_arith_wis (* FIXME: duplicate *)
    1.56 -
    1.57  
    1.58  subsection {* Transferring goals from words to ints *}
    1.59  
    1.60 @@ -1308,16 +1307,44 @@
    1.61  lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
    1.62    by simp
    1.63  
    1.64 -lemmas uint_word_ariths = 
    1.65 -  word_arith_alts [THEN trans [OF uint_cong int_word_uint]]
    1.66 -
    1.67 -lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p]
    1.68 -
    1.69 -(* similar expressions for sint (arith operations) *)
    1.70 -lemmas sint_word_ariths = uint_word_arith_bintrs
    1.71 -  [THEN uint_sint [symmetric, THEN trans],
    1.72 -  unfolded uint_sint bintr_arith1s bintr_ariths 
    1.73 -    len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep]
    1.74 +lemma uint_word_ariths:
    1.75 +  fixes a b :: "'a::len0 word"
    1.76 +  shows "uint (a + b) = (uint a + uint b) mod 2 ^ len_of TYPE('a::len0)"
    1.77 +    and "uint (a - b) = (uint a - uint b) mod 2 ^ len_of TYPE('a)"
    1.78 +    and "uint (a * b) = uint a * uint b mod 2 ^ len_of TYPE('a)"
    1.79 +    and "uint (- a) = - uint a mod 2 ^ len_of TYPE('a)"
    1.80 +    and "uint (word_succ a) = (uint a + 1) mod 2 ^ len_of TYPE('a)"
    1.81 +    and "uint (word_pred a) = (uint a - 1) mod 2 ^ len_of TYPE('a)"
    1.82 +    and "uint (0 :: 'a word) = 0 mod 2 ^ len_of TYPE('a)"
    1.83 +    and "uint (1 :: 'a word) = 1 mod 2 ^ len_of TYPE('a)"
    1.84 +  by (simp_all add: word_arith_wis [THEN trans [OF uint_cong int_word_uint]])
    1.85 +
    1.86 +lemma uint_word_arith_bintrs:
    1.87 +  fixes a b :: "'a::len0 word"
    1.88 +  shows "uint (a + b) = bintrunc (len_of TYPE('a)) (uint a + uint b)"
    1.89 +    and "uint (a - b) = bintrunc (len_of TYPE('a)) (uint a - uint b)"
    1.90 +    and "uint (a * b) = bintrunc (len_of TYPE('a)) (uint a * uint b)"
    1.91 +    and "uint (- a) = bintrunc (len_of TYPE('a)) (- uint a)"
    1.92 +    and "uint (word_succ a) = bintrunc (len_of TYPE('a)) (uint a + 1)"
    1.93 +    and "uint (word_pred a) = bintrunc (len_of TYPE('a)) (uint a - 1)"
    1.94 +    and "uint (0 :: 'a word) = bintrunc (len_of TYPE('a)) 0"
    1.95 +    and "uint (1 :: 'a word) = bintrunc (len_of TYPE('a)) 1"
    1.96 +  by (simp_all add: uint_word_ariths bintrunc_mod2p)
    1.97 +
    1.98 +lemma sint_word_ariths:
    1.99 +  fixes a b :: "'a::len word"
   1.100 +  shows "sint (a + b) = sbintrunc (len_of TYPE('a) - 1) (sint a + sint b)"
   1.101 +    and "sint (a - b) = sbintrunc (len_of TYPE('a) - 1) (sint a - sint b)"
   1.102 +    and "sint (a * b) = sbintrunc (len_of TYPE('a) - 1) (sint a * sint b)"
   1.103 +    and "sint (- a) = sbintrunc (len_of TYPE('a) - 1) (- sint a)"
   1.104 +    and "sint (word_succ a) = sbintrunc (len_of TYPE('a) - 1) (sint a + 1)"
   1.105 +    and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)"
   1.106 +    and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0"
   1.107 +    and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1"
   1.108 +  by (simp_all add: uint_word_arith_bintrs
   1.109 +    [THEN uint_sint [symmetric, THEN trans],
   1.110 +    unfolded uint_sint bintr_arith1s bintr_ariths 
   1.111 +      len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep])
   1.112  
   1.113  lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
   1.114  lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
   1.115 @@ -1417,7 +1444,7 @@
   1.116    with `1 \<le> uint w` have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
   1.117      by auto
   1.118    then show ?thesis
   1.119 -    by (simp only: unat_def int_word_uint word_arith_alts mod_diff_right_eq [symmetric])
   1.120 +    by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq [symmetric])
   1.121  qed
   1.122  
   1.123  lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
   1.124 @@ -3930,7 +3957,7 @@
   1.125       apply (clarsimp simp: word_size)+
   1.126    apply (rule trans)
   1.127    apply (rule test_bit_rcat [OF refl refl])
   1.128 -  apply (simp add: word_size msrevs)
   1.129 +  apply (simp add: word_size)
   1.130    apply (subst nth_rev)
   1.131     apply arith
   1.132    apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
   1.133 @@ -4480,7 +4507,7 @@
   1.134        uint x + uint y 
   1.135     else 
   1.136        uint x + uint y - 2^size x)" 
   1.137 -  by (simp add: word_arith_alts int_word_uint mod_add_if_z 
   1.138 +  by (simp add: word_arith_wis int_word_uint mod_add_if_z 
   1.139                  word_size)
   1.140  
   1.141  lemma unat_plus_if_size:
   1.142 @@ -4501,16 +4528,7 @@
   1.143  
   1.144  lemma max_lt:
   1.145    "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
   1.146 -  apply (subst word_arith_nat_defs)
   1.147 -  apply (subst word_unat.eq_norm)
   1.148 -  apply (subst mod_if)
   1.149 -  apply clarsimp
   1.150 -  apply (erule notE)
   1.151 -  apply (insert div_le_dividend [of "unat (max a b)" "unat c"])
   1.152 -  apply (erule order_le_less_trans)
   1.153 -  apply (insert unat_lt2p [of "max a b"])
   1.154 -  apply simp
   1.155 -  done
   1.156 +  by (fact unat_div)
   1.157  
   1.158  lemma uint_sub_if_size:
   1.159    "uint (x - y) = 
   1.160 @@ -4518,7 +4536,7 @@
   1.161        uint x - uint y 
   1.162     else 
   1.163        uint x - uint y + 2^size x)"
   1.164 -  by (simp add: word_arith_alts int_word_uint mod_sub_if_z 
   1.165 +  by (simp add: word_arith_wis int_word_uint mod_sub_if_z 
   1.166                  word_size)
   1.167  
   1.168  lemma unat_sub:
   1.169 @@ -4725,5 +4743,3 @@
   1.170  
   1.171  end
   1.172  
   1.173 -
   1.174 -