more precise imports;
authorhaftmann
Sat Mar 01 17:08:39 2014 +0100 (2014-03-01)
changeset 55818d8b2f50705d0
parent 55817 0bc0217387a5
child 55819 e21d83c8e1c7
more precise imports;
avoid duplicated simp rules in fact collections;
dropped redundancy
NEWS
src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy
src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
src/HOL/Word/Word.thy
     1.1 --- a/NEWS	Sat Mar 01 09:34:08 2014 +0100
     1.2 +++ b/NEWS	Sat Mar 01 17:08:39 2014 +0100
     1.3 @@ -91,6 +91,13 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* HOL-Word:
     1.8 +  * Abandoned fact collection "word_arith_alts", which is a
     1.9 +  duplicate of "word_arith_wis".
    1.10 +  * Dropped first (duplicated) element in fact collections
    1.11 +  "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
    1.12 +  "uint_word_arith_bintrs".
    1.13 +
    1.14  * Code generator: explicit proof contexts in many ML interfaces.
    1.15  INCOMPATIBILITY.
    1.16  
     2.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Sat Mar 01 09:34:08 2014 +0100
     2.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy	Sat Mar 01 17:08:39 2014 +0100
     2.3 @@ -5,7 +5,7 @@
     2.4  *)
     2.5  
     2.6  theory RMD
     2.7 -imports Word
     2.8 +imports "~~/src/HOL/Word/Word"
     2.9  begin
    2.10  
    2.11  
     3.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Sat Mar 01 09:34:08 2014 +0100
     3.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Sat Mar 01 17:08:39 2014 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  *)
     3.5  
     3.6  theory RMD_Specification
     3.7 -imports RMD SPARK
     3.8 +imports RMD "~~/src/HOL/SPARK/SPARK"
     3.9  begin
    3.10  
    3.11  (* bit operations *)
     4.1 --- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Mar 01 09:34:08 2014 +0100
     4.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Mar 01 17:08:39 2014 +0100
     4.3 @@ -456,7 +456,7 @@
     4.4      unfolding round_def
     4.5      unfolding steps_to_steps'
     4.6      unfolding H1[symmetric]
     4.7 -    by (simp add: uint_word_ariths(2) rdmods
     4.8 +    by (simp add: uint_word_ariths(1) rdmods
     4.9        uint_word_of_int_id)
    4.10  qed
    4.11  
     5.1 --- a/src/HOL/Word/Word.thy	Sat Mar 01 09:34:08 2014 +0100
     5.2 +++ b/src/HOL/Word/Word.thy	Sat Mar 01 17:08:39 2014 +0100
     5.3 @@ -1192,7 +1192,7 @@
     5.4  subsection {* Word Arithmetic *}
     5.5  
     5.6  lemma word_less_alt: "(a < b) = (uint a < uint b)"
     5.7 -  unfolding word_less_def word_le_def by (simp add: less_le)
     5.8 +  by (fact word_less_def)
     5.9  
    5.10  lemma signed_linorder: "class.linorder word_sle word_sless"
    5.11    by default (unfold word_sle_def word_sless_def, auto)
    5.12 @@ -1236,16 +1236,20 @@
    5.13    unfolding uint_bl
    5.14    by (simp add: word_size bin_to_bl_zero)
    5.15  
    5.16 -lemma uint_0_iff: "(uint x = 0) = (x = 0)"
    5.17 -  by (auto intro!: word_uint.Rep_eqD)
    5.18 -
    5.19 -lemma unat_0_iff: "(unat x = 0) = (x = 0)"
    5.20 +lemma uint_0_iff:
    5.21 +  "uint x = 0 \<longleftrightarrow> x = 0"
    5.22 +  by (simp add: word_uint_eq_iff)
    5.23 +
    5.24 +lemma unat_0_iff:
    5.25 +  "unat x = 0 \<longleftrightarrow> x = 0"
    5.26    unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)
    5.27  
    5.28 -lemma unat_0 [simp]: "unat 0 = 0"
    5.29 +lemma unat_0 [simp]:
    5.30 +  "unat 0 = 0"
    5.31    unfolding unat_def by auto
    5.32  
    5.33 -lemma size_0_same': "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
    5.34 +lemma size_0_same':
    5.35 +  "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
    5.36    apply (unfold word_size)
    5.37    apply (rule box_equals)
    5.38      defer
    5.39 @@ -1278,8 +1282,7 @@
    5.40    unfolding scast_def by simp
    5.41  
    5.42  lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
    5.43 -  unfolding word_1_wi
    5.44 -  by (simp add: word_ubin.eq_norm bintrunc_minus_simps del: word_of_int_1)
    5.45 +  by (simp only: word_1_wi word_ubin.eq_norm) (simp add: bintrunc_minus_simps(4))
    5.46  
    5.47  lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
    5.48    unfolding unat_def by simp
    5.49 @@ -1289,10 +1292,6 @@
    5.50  
    5.51  (* now, to get the weaker results analogous to word_div/mod_def *)
    5.52  
    5.53 -lemmas word_arith_alts = 
    5.54 -  word_sub_wi
    5.55 -  word_arith_wis (* FIXME: duplicate *)
    5.56 -
    5.57  
    5.58  subsection {* Transferring goals from words to ints *}
    5.59  
    5.60 @@ -1308,16 +1307,44 @@
    5.61  lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
    5.62    by simp
    5.63  
    5.64 -lemmas uint_word_ariths = 
    5.65 -  word_arith_alts [THEN trans [OF uint_cong int_word_uint]]
    5.66 -
    5.67 -lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p]
    5.68 -
    5.69 -(* similar expressions for sint (arith operations) *)
    5.70 -lemmas sint_word_ariths = uint_word_arith_bintrs
    5.71 -  [THEN uint_sint [symmetric, THEN trans],
    5.72 -  unfolded uint_sint bintr_arith1s bintr_ariths 
    5.73 -    len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep]
    5.74 +lemma uint_word_ariths:
    5.75 +  fixes a b :: "'a::len0 word"
    5.76 +  shows "uint (a + b) = (uint a + uint b) mod 2 ^ len_of TYPE('a::len0)"
    5.77 +    and "uint (a - b) = (uint a - uint b) mod 2 ^ len_of TYPE('a)"
    5.78 +    and "uint (a * b) = uint a * uint b mod 2 ^ len_of TYPE('a)"
    5.79 +    and "uint (- a) = - uint a mod 2 ^ len_of TYPE('a)"
    5.80 +    and "uint (word_succ a) = (uint a + 1) mod 2 ^ len_of TYPE('a)"
    5.81 +    and "uint (word_pred a) = (uint a - 1) mod 2 ^ len_of TYPE('a)"
    5.82 +    and "uint (0 :: 'a word) = 0 mod 2 ^ len_of TYPE('a)"
    5.83 +    and "uint (1 :: 'a word) = 1 mod 2 ^ len_of TYPE('a)"
    5.84 +  by (simp_all add: word_arith_wis [THEN trans [OF uint_cong int_word_uint]])
    5.85 +
    5.86 +lemma uint_word_arith_bintrs:
    5.87 +  fixes a b :: "'a::len0 word"
    5.88 +  shows "uint (a + b) = bintrunc (len_of TYPE('a)) (uint a + uint b)"
    5.89 +    and "uint (a - b) = bintrunc (len_of TYPE('a)) (uint a - uint b)"
    5.90 +    and "uint (a * b) = bintrunc (len_of TYPE('a)) (uint a * uint b)"
    5.91 +    and "uint (- a) = bintrunc (len_of TYPE('a)) (- uint a)"
    5.92 +    and "uint (word_succ a) = bintrunc (len_of TYPE('a)) (uint a + 1)"
    5.93 +    and "uint (word_pred a) = bintrunc (len_of TYPE('a)) (uint a - 1)"
    5.94 +    and "uint (0 :: 'a word) = bintrunc (len_of TYPE('a)) 0"
    5.95 +    and "uint (1 :: 'a word) = bintrunc (len_of TYPE('a)) 1"
    5.96 +  by (simp_all add: uint_word_ariths bintrunc_mod2p)
    5.97 +
    5.98 +lemma sint_word_ariths:
    5.99 +  fixes a b :: "'a::len word"
   5.100 +  shows "sint (a + b) = sbintrunc (len_of TYPE('a) - 1) (sint a + sint b)"
   5.101 +    and "sint (a - b) = sbintrunc (len_of TYPE('a) - 1) (sint a - sint b)"
   5.102 +    and "sint (a * b) = sbintrunc (len_of TYPE('a) - 1) (sint a * sint b)"
   5.103 +    and "sint (- a) = sbintrunc (len_of TYPE('a) - 1) (- sint a)"
   5.104 +    and "sint (word_succ a) = sbintrunc (len_of TYPE('a) - 1) (sint a + 1)"
   5.105 +    and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)"
   5.106 +    and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0"
   5.107 +    and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1"
   5.108 +  by (simp_all add: uint_word_arith_bintrs
   5.109 +    [THEN uint_sint [symmetric, THEN trans],
   5.110 +    unfolded uint_sint bintr_arith1s bintr_ariths 
   5.111 +      len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep])
   5.112  
   5.113  lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
   5.114  lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
   5.115 @@ -1417,7 +1444,7 @@
   5.116    with `1 \<le> uint w` have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
   5.117      by auto
   5.118    then show ?thesis
   5.119 -    by (simp only: unat_def int_word_uint word_arith_alts mod_diff_right_eq [symmetric])
   5.120 +    by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq [symmetric])
   5.121  qed
   5.122  
   5.123  lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
   5.124 @@ -3930,7 +3957,7 @@
   5.125       apply (clarsimp simp: word_size)+
   5.126    apply (rule trans)
   5.127    apply (rule test_bit_rcat [OF refl refl])
   5.128 -  apply (simp add: word_size msrevs)
   5.129 +  apply (simp add: word_size)
   5.130    apply (subst nth_rev)
   5.131     apply arith
   5.132    apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
   5.133 @@ -4480,7 +4507,7 @@
   5.134        uint x + uint y 
   5.135     else 
   5.136        uint x + uint y - 2^size x)" 
   5.137 -  by (simp add: word_arith_alts int_word_uint mod_add_if_z 
   5.138 +  by (simp add: word_arith_wis int_word_uint mod_add_if_z 
   5.139                  word_size)
   5.140  
   5.141  lemma unat_plus_if_size:
   5.142 @@ -4501,16 +4528,7 @@
   5.143  
   5.144  lemma max_lt:
   5.145    "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
   5.146 -  apply (subst word_arith_nat_defs)
   5.147 -  apply (subst word_unat.eq_norm)
   5.148 -  apply (subst mod_if)
   5.149 -  apply clarsimp
   5.150 -  apply (erule notE)
   5.151 -  apply (insert div_le_dividend [of "unat (max a b)" "unat c"])
   5.152 -  apply (erule order_le_less_trans)
   5.153 -  apply (insert unat_lt2p [of "max a b"])
   5.154 -  apply simp
   5.155 -  done
   5.156 +  by (fact unat_div)
   5.157  
   5.158  lemma uint_sub_if_size:
   5.159    "uint (x - y) = 
   5.160 @@ -4518,7 +4536,7 @@
   5.161        uint x - uint y 
   5.162     else 
   5.163        uint x - uint y + 2^size x)"
   5.164 -  by (simp add: word_arith_alts int_word_uint mod_sub_if_z 
   5.165 +  by (simp add: word_arith_wis int_word_uint mod_sub_if_z 
   5.166                  word_size)
   5.167  
   5.168  lemma unat_sub:
   5.169 @@ -4725,5 +4743,3 @@
   5.170  
   5.171  end
   5.172  
   5.173 -
   5.174 -