src/HOL/Word/Word.thy
changeset 65363 5eb619751b14
parent 65336 8e5274fc0093
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Word/Word.thy	Mon Apr 03 21:17:47 2017 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Mon Apr 03 23:12:16 2017 +0200
     1.3 @@ -1827,8 +1827,8 @@
     1.4    by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
     1.5  
     1.6  lemma unat_mult_lem:
     1.7 -  "unat x * unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow>
     1.8 -    unat (x * y :: 'a::len word) = unat x * unat y"
     1.9 +  "unat x * unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow> unat (x * y) = unat x * unat y"
    1.10 +  for x y :: "'a::len word"
    1.11    by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
    1.12  
    1.13  lemmas unat_plus_if' =
    1.14 @@ -2002,7 +2002,7 @@
    1.15  
    1.16  lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
    1.17  
    1.18 -lemma word_le_exists': "x \<le> y \<Longrightarrow> (\<exists>z. y = x + z \<and> uint x + uint z < 2 ^ len_of TYPE('a))"
    1.19 +lemma word_le_exists': "x \<le> y \<Longrightarrow> \<exists>z. y = x + z \<and> uint x + uint z < 2 ^ len_of TYPE('a)"
    1.20    for x y z :: "'a::len0 word"
    1.21    apply (rule exI)
    1.22    apply (rule conjI)
    1.23 @@ -2330,13 +2330,15 @@
    1.24    unfolding to_bl_def word_log_defs bl_and_bin
    1.25    by (simp add: word_ubin.eq_norm)
    1.26  
    1.27 -lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
    1.28 +lemma word_lsb_alt: "lsb w = test_bit w 0"
    1.29 +  for w :: "'a::len0 word"
    1.30    by (auto simp: word_test_bit_def word_lsb_def)
    1.31  
    1.32  lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len0 word)"
    1.33    unfolding word_lsb_def uint_eq_0 uint_1 by simp
    1.34  
    1.35 -lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
    1.36 +lemma word_lsb_last: "lsb w = last (to_bl w)"
    1.37 +  for w :: "'a::len word"
    1.38    apply (unfold word_lsb_def uint_bl bin_to_bl_def)
    1.39    apply (rule_tac bin="uint w" in bin_exhaust)
    1.40    apply (cases "size w")
    1.41 @@ -2419,7 +2421,7 @@
    1.42    done
    1.43  
    1.44  lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
    1.45 -  unfolding of_bl_def bl_to_bin_rep_F by auto
    1.46 +  by (auto simp: of_bl_def bl_to_bin_rep_F)
    1.47  
    1.48  lemma msb_nth: "msb w = w !! (len_of TYPE('a) - 1)"
    1.49    for w :: "'a::len word"
    1.50 @@ -2762,7 +2764,8 @@
    1.51  lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
    1.52    by (simp add: of_bl_def bl_to_bin_append)
    1.53  
    1.54 -lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
    1.55 +lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])"
    1.56 +  for w :: "'a::len0 word"
    1.57  proof -
    1.58    have "shiftl1 w = shiftl1 (of_bl (to_bl w))"
    1.59      by simp
    1.60 @@ -2970,7 +2973,7 @@
    1.61    for x :: "'a::len0 word"
    1.62    using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
    1.63  
    1.64 -lemma msb_shift: "msb w \<longleftrightarrow> (w >> (len_of TYPE('a) - 1)) \<noteq> 0"
    1.65 +lemma msb_shift: "msb w \<longleftrightarrow> w >> (len_of TYPE('a) - 1) \<noteq> 0"
    1.66    for w :: "'a::len word"
    1.67    apply (unfold shiftr_bl word_msb_alt)
    1.68    apply (simp add: word_size Suc_le_eq take_Suc)
    1.69 @@ -3091,10 +3094,11 @@
    1.70     apply auto
    1.71    done
    1.72  
    1.73 -lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
    1.74 +lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
    1.75 +  for b n :: int
    1.76    by (simp add: int_mod_lem eq_sym_conv)
    1.77  
    1.78 -lemma mask_eq_iff: "(w AND mask n) = w \<longleftrightarrow> uint w < 2 ^ n"
    1.79 +lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n"
    1.80    apply (simp add: and_mask_bintr)
    1.81    apply (simp add: word_ubin.inverse_norm)
    1.82    apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
    1.83 @@ -3632,8 +3636,9 @@
    1.84        split: prod.split)
    1.85  
    1.86  lemma test_bit_rsplit:
    1.87 -  "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a::len word) \<Longrightarrow>
    1.88 -    k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
    1.89 +  "sw = word_rsplit w \<Longrightarrow> m < size (hd sw) \<Longrightarrow>
    1.90 +    k < length sw \<Longrightarrow> (rev sw ! k) !! m = w !! (k * size (hd sw) + m)"
    1.91 +  for sw :: "'a::len word list"
    1.92    apply (unfold word_rsplit_def word_test_bit_def)
    1.93    apply (rule trans)
    1.94     apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong)
    1.95 @@ -3673,8 +3678,9 @@
    1.96    done
    1.97  
    1.98  lemma test_bit_rcat:
    1.99 -  "sw = size (hd wl :: 'a::len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
   1.100 +  "sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
   1.101      (n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
   1.102 +  for wl :: "'a::len word list"
   1.103    apply (unfold word_rcat_bl word_size)
   1.104    apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
   1.105    apply safe
   1.106 @@ -4266,10 +4272,11 @@
   1.107    by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size)
   1.108  
   1.109  lemma unat_plus_if_size:
   1.110 -  "unat (x + (y::'a::len word)) =
   1.111 +  "unat (x + y) =
   1.112      (if unat x + unat y < 2^size x
   1.113       then unat x + unat y
   1.114       else unat x + unat y - 2^size x)"
   1.115 +  for x y :: "'a::len word"
   1.116    apply (subst word_arith_nat_defs)
   1.117    apply (subst unat_of_nat)
   1.118    apply (simp add:  mod_nat_add word_size)
   1.119 @@ -4339,7 +4346,7 @@
   1.120    shows "(x - y) mod b = z' mod b'"
   1.121    using assms [symmetric] by (auto intro: mod_diff_cong)
   1.122  
   1.123 -lemma word_induct_less: "\<lbrakk>P 0; \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
   1.124 +lemma word_induct_less: "P 0 \<Longrightarrow> (\<And>n. n < m \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
   1.125    for P :: "'a::len word \<Rightarrow> bool"
   1.126    apply (cases m)
   1.127    apply atomize
   1.128 @@ -4362,11 +4369,11 @@
   1.129    apply simp
   1.130    done
   1.131  
   1.132 -lemma word_induct: "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
   1.133 +lemma word_induct: "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
   1.134    for P :: "'a::len word \<Rightarrow> bool"
   1.135    by (erule word_induct_less) simp
   1.136  
   1.137 -lemma word_induct2 [induct type]: "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P n"
   1.138 +lemma word_induct2 [induct type]: "P 0 \<Longrightarrow> (\<And>n. 1 + n \<noteq> 0 \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P n"
   1.139    for P :: "'b::len word \<Rightarrow> bool"
   1.140    apply (rule word_induct)
   1.141     apply simp
   1.142 @@ -4383,16 +4390,15 @@
   1.143  lemma word_rec_0: "word_rec z s 0 = z"
   1.144    by (simp add: word_rec_def)
   1.145  
   1.146 -lemma word_rec_Suc:
   1.147 -  "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
   1.148 +lemma word_rec_Suc: "1 + n \<noteq> 0 \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
   1.149 +  for n :: "'a::len word"
   1.150    apply (simp add: word_rec_def unat_word_ariths)
   1.151    apply (subst nat_mod_eq')
   1.152     apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add)
   1.153    apply simp
   1.154    done
   1.155  
   1.156 -lemma word_rec_Pred:
   1.157 -  "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
   1.158 +lemma word_rec_Pred: "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
   1.159    apply (rule subst[where t="n" and s="1 + (n - 1)"])
   1.160     apply simp
   1.161    apply (subst word_rec_Suc)
   1.162 @@ -4468,7 +4474,8 @@
   1.163    apply simp
   1.164    done
   1.165  
   1.166 -lemma unatSuc: "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
   1.167 +lemma unatSuc: "1 + n \<noteq> 0 \<Longrightarrow> unat (1 + n) = Suc (unat n)"
   1.168 +  for n :: "'a::len word"
   1.169    by unat_arith
   1.170  
   1.171  declare bin_to_bl_def [simp]