src/HOL/Word/Word.thy
changeset 58410 6d46ad54a2ab
parent 58061 3d060f43accb
child 58874 7172c7ffb047
     1.1 --- a/src/HOL/Word/Word.thy	Sun Sep 21 16:56:06 2014 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Sun Sep 21 16:56:11 2014 +0200
     1.3 @@ -1275,7 +1275,7 @@
     1.4  lemma scast_0 [simp]: "scast 0 = 0"
     1.5    unfolding scast_def by simp
     1.6  
     1.7 -lemma sint_n1 [simp] : "sint -1 = -1"
     1.8 +lemma sint_n1 [simp] : "sint (- 1) = - 1"
     1.9    unfolding word_m1_wi word_sbin.eq_norm by simp
    1.10  
    1.11  lemma scast_n1 [simp]: "scast (- 1) = - 1"
    1.12 @@ -1349,7 +1349,7 @@
    1.13  lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
    1.14  lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
    1.15  
    1.16 -lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
    1.17 +lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)"
    1.18    unfolding word_pred_m1 by simp
    1.19  
    1.20  lemma succ_pred_no [simp]:
    1.21 @@ -1360,7 +1360,7 @@
    1.22    unfolding word_succ_p1 word_pred_m1 by simp_all
    1.23  
    1.24  lemma word_sp_01 [simp] : 
    1.25 -  "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
    1.26 +  "word_succ (- 1) = 0 & word_succ 0 = 1 & word_pred 0 = - 1 & word_pred 1 = 0"
    1.27    unfolding word_succ_p1 word_pred_m1 by simp_all
    1.28  
    1.29  (* alternative approach to lifting arithmetic equalities *)
    1.30 @@ -2803,7 +2803,7 @@
    1.31  lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
    1.32    unfolding sshiftr1_def by simp
    1.33  
    1.34 -lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
    1.35 +lemma sshiftr1_n1 [simp] : "sshiftr1 (- 1) = - 1"
    1.36    unfolding sshiftr1_def by simp
    1.37  
    1.38  lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
    1.39 @@ -3243,7 +3243,7 @@
    1.40  lemma mask_bl: "mask n = of_bl (replicate n True)"
    1.41    by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
    1.42  
    1.43 -lemma mask_bin: "mask n = word_of_int (bintrunc n -1)"
    1.44 +lemma mask_bin: "mask n = word_of_int (bintrunc n (- 1))"
    1.45    by (auto simp add: nth_bintr word_size intro: word_eqI)
    1.46  
    1.47  lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
    1.48 @@ -4729,7 +4729,7 @@
    1.49  done
    1.50  
    1.51  lemma word_rec_max: 
    1.52 -  "\<forall>m\<ge>n. m \<noteq> -1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f -1 = word_rec z f n"
    1.53 +  "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
    1.54  apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
    1.55   apply simp
    1.56  apply simp