prefer plain bool over dedicated type for binary digits
authorhaftmann
Mon Dec 23 14:24:20 2013 +0100 (2013-12-23)
changeset 54847d6cf9a5b9be9
parent 54846 bf86b2002c96
child 54848 a303daddebbf
prefer plain bool over dedicated type for binary digits
src/HOL/Word/Bit_Comparison.thy
src/HOL/Word/Bit_Int.thy
src/HOL/Word/Bit_Operations.thy
src/HOL/Word/Bit_Representation.thy
src/HOL/Word/Bool_List_Representation.thy
src/HOL/Word/Misc_Numeric.thy
src/HOL/Word/Word.thy
src/HOL/Word/WordBitwise.thy
     1.1 --- a/src/HOL/Word/Bit_Comparison.thy	Mon Dec 23 09:21:38 2013 +0100
     1.2 +++ b/src/HOL/Word/Bit_Comparison.thy	Mon Dec 23 14:24:20 2013 +0100
     1.3 @@ -20,10 +20,10 @@
     1.4    proof (cases y rule: bin_exhaust)
     1.5      case (1 bin' bit')
     1.6      from 3 have "0 \<le> bin"
     1.7 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
     1.8 +      by (cases bit) (simp_all add: Bit_def)
     1.9      then have "0 \<le> bin AND bin'" by (rule 3)
    1.10      with 1 show ?thesis
    1.11 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    1.12 +      by simp (simp add: Bit_def)
    1.13    qed
    1.14  next
    1.15    case 2
    1.16 @@ -41,12 +41,12 @@
    1.17    proof (cases y rule: bin_exhaust)
    1.18      case (1 bin' bit')
    1.19      from 3 have "0 \<le> bin"
    1.20 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.21 +      by (cases bit) (simp_all add: Bit_def)
    1.22      moreover from 1 3 have "0 \<le> bin'"
    1.23 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.24 +      by (cases bit') (simp_all add: Bit_def)
    1.25      ultimately have "0 \<le> bin OR bin'" by (rule 3)
    1.26      with 1 show ?thesis
    1.27 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    1.28 +      by simp (simp add: Bit_def)
    1.29    qed
    1.30  qed simp_all
    1.31  
    1.32 @@ -61,12 +61,12 @@
    1.33    proof (cases y rule: bin_exhaust)
    1.34      case (1 bin' bit')
    1.35      from 3 have "0 \<le> bin"
    1.36 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.37 +      by (cases bit) (simp_all add: Bit_def)
    1.38      moreover from 1 3 have "0 \<le> bin'"
    1.39 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.40 +      by (cases bit') (simp_all add: Bit_def)
    1.41      ultimately have "0 \<le> bin XOR bin'" by (rule 3)
    1.42      with 1 show ?thesis
    1.43 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    1.44 +      by simp (simp add: Bit_def)
    1.45    qed
    1.46  next
    1.47    case 2
    1.48 @@ -84,10 +84,10 @@
    1.49    proof (cases y rule: bin_exhaust)
    1.50      case (1 bin' bit')
    1.51      from 3 have "0 \<le> bin"
    1.52 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.53 +      by (cases bit) (simp_all add: Bit_def)
    1.54      then have "bin AND bin' \<le> bin" by (rule 3)
    1.55      with 1 show ?thesis
    1.56 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    1.57 +      by simp (simp add: Bit_def)
    1.58    qed
    1.59  next
    1.60    case 2
    1.61 @@ -108,10 +108,10 @@
    1.62    proof (cases x rule: bin_exhaust)
    1.63      case (1 bin' bit')
    1.64      from 3 have "0 \<le> bin"
    1.65 -      by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.66 +      by (cases bit) (simp_all add: Bit_def)
    1.67      then have "bin' AND bin \<le> bin" by (rule 3)
    1.68      with 1 show ?thesis
    1.69 -      by simp (simp add: Bit_def bitval_def split add: bit.split)
    1.70 +      by simp (simp add: Bit_def)
    1.71    qed
    1.72  next
    1.73    case 2
    1.74 @@ -135,21 +135,21 @@
    1.75      proof (cases n)
    1.76        case 0
    1.77        with 3 have "bin BIT bit = 0" by simp
    1.78 -      then have "bin = 0" "bit = 0"
    1.79 -        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
    1.80 +      then have "bin = 0" and "\<not> bit"
    1.81 +        by (auto simp add: Bit_def split: if_splits) arith
    1.82        then show ?thesis using 0 1 `y < 2 ^ n`
    1.83          by simp
    1.84      next
    1.85        case (Suc m)
    1.86        from 3 have "0 \<le> bin"
    1.87 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.88 +        by (cases bit) (simp_all add: Bit_def)
    1.89        moreover from 3 Suc have "bin < 2 ^ m"
    1.90 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.91 +        by (cases bit) (simp_all add: Bit_def)
    1.92        moreover from 1 3 Suc have "bin' < 2 ^ m"
    1.93 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
    1.94 +        by (cases bit') (simp_all add: Bit_def)
    1.95        ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
    1.96        with 1 Suc show ?thesis
    1.97 -        by simp (simp add: Bit_def bitval_def split add: bit.split)
    1.98 +        by simp (simp add: Bit_def)
    1.99      qed
   1.100    qed
   1.101  qed simp_all
   1.102 @@ -168,21 +168,21 @@
   1.103      proof (cases n)
   1.104        case 0
   1.105        with 3 have "bin BIT bit = 0" by simp
   1.106 -      then have "bin = 0" "bit = 0"
   1.107 -        by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
   1.108 +      then have "bin = 0" and "\<not> bit"
   1.109 +        by (auto simp add: Bit_def split: if_splits) arith
   1.110        then show ?thesis using 0 1 `y < 2 ^ n`
   1.111          by simp
   1.112      next
   1.113        case (Suc m)
   1.114        from 3 have "0 \<le> bin"
   1.115 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.116 +        by (cases bit) (simp_all add: Bit_def)
   1.117        moreover from 3 Suc have "bin < 2 ^ m"
   1.118 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.119 +        by (cases bit) (simp_all add: Bit_def)
   1.120        moreover from 1 3 Suc have "bin' < 2 ^ m"
   1.121 -        by (simp add: Bit_def bitval_def split add: bit.split_asm)
   1.122 +        by (cases bit') (simp_all add: Bit_def)
   1.123        ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
   1.124        with 1 Suc show ?thesis
   1.125 -        by simp (simp add: Bit_def bitval_def split add: bit.split)
   1.126 +        by simp (simp add: Bit_def)
   1.127      qed
   1.128    qed
   1.129  next
     2.1 --- a/src/HOL/Word/Bit_Int.thy	Mon Dec 23 09:21:38 2013 +0100
     2.2 +++ b/src/HOL/Word/Bit_Int.thy	Mon Dec 23 14:24:20 2013 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  header {* Bitwise Operations on Binary Integers *}
     2.5  
     2.6  theory Bit_Int
     2.7 -imports Bit_Representation Bit_Bit
     2.8 +imports Bit_Representation Bit_Operations
     2.9  begin
    2.10  
    2.11  subsection {* Logical operations *}
    2.12 @@ -25,7 +25,7 @@
    2.13  function bitAND_int where
    2.14    "bitAND_int x y =
    2.15      (if x = 0 then 0 else if x = -1 then y else
    2.16 -      (bin_rest x AND bin_rest y) BIT (bin_last x AND bin_last y))"
    2.17 +      (bin_rest x AND bin_rest y) BIT (bin_last x \<and> bin_last y))"
    2.18    by pat_completeness simp
    2.19  
    2.20  termination
    2.21 @@ -46,7 +46,7 @@
    2.22  subsubsection {* Basic simplification rules *}
    2.23  
    2.24  lemma int_not_BIT [simp]:
    2.25 -  "NOT (w BIT b) = (NOT w) BIT (NOT b)"
    2.26 +  "NOT (w BIT b) = (NOT w) BIT (\<not> b)"
    2.27    unfolding int_not_def Bit_def by (cases b, simp_all)
    2.28  
    2.29  lemma int_not_simps [simp]:
    2.30 @@ -68,7 +68,7 @@
    2.31    by (simp add: bitAND_int.simps)
    2.32  
    2.33  lemma int_and_Bits [simp]: 
    2.34 -  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
    2.35 +  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b \<and> c)" 
    2.36    by (subst bitAND_int.simps, simp add: Bit_eq_0_iff Bit_eq_m1_iff)
    2.37  
    2.38  lemma int_or_zero [simp]: "(0::int) OR x = x"
    2.39 @@ -78,40 +78,40 @@
    2.40    unfolding int_or_def by simp
    2.41  
    2.42  lemma int_or_Bits [simp]: 
    2.43 -  "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
    2.44 -  unfolding int_or_def bit_or_def by simp
    2.45 +  "(x BIT b) OR (y BIT c) = (x OR y) BIT (b \<or> c)"
    2.46 +  unfolding int_or_def by simp
    2.47  
    2.48  lemma int_xor_zero [simp]: "(0::int) XOR x = x"
    2.49    unfolding int_xor_def by simp
    2.50  
    2.51  lemma int_xor_Bits [simp]: 
    2.52 -  "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
    2.53 -  unfolding int_xor_def bit_xor_def by simp
    2.54 +  "(x BIT b) XOR (y BIT c) = (x XOR y) BIT ((b \<or> c) \<and> \<not> (b \<and> c))"
    2.55 +  unfolding int_xor_def by auto
    2.56  
    2.57  subsubsection {* Binary destructors *}
    2.58  
    2.59  lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
    2.60    by (cases x rule: bin_exhaust, simp)
    2.61  
    2.62 -lemma bin_last_NOT [simp]: "bin_last (NOT x) = NOT (bin_last x)"
    2.63 +lemma bin_last_NOT [simp]: "bin_last (NOT x) \<longleftrightarrow> \<not> bin_last x"
    2.64    by (cases x rule: bin_exhaust, simp)
    2.65  
    2.66  lemma bin_rest_AND [simp]: "bin_rest (x AND y) = bin_rest x AND bin_rest y"
    2.67    by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
    2.68  
    2.69 -lemma bin_last_AND [simp]: "bin_last (x AND y) = bin_last x AND bin_last y"
    2.70 +lemma bin_last_AND [simp]: "bin_last (x AND y) \<longleftrightarrow> bin_last x \<and> bin_last y"
    2.71    by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
    2.72  
    2.73  lemma bin_rest_OR [simp]: "bin_rest (x OR y) = bin_rest x OR bin_rest y"
    2.74    by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
    2.75  
    2.76 -lemma bin_last_OR [simp]: "bin_last (x OR y) = bin_last x OR bin_last y"
    2.77 +lemma bin_last_OR [simp]: "bin_last (x OR y) \<longleftrightarrow> bin_last x \<or> bin_last y"
    2.78    by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
    2.79  
    2.80  lemma bin_rest_XOR [simp]: "bin_rest (x XOR y) = bin_rest x XOR bin_rest y"
    2.81    by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
    2.82  
    2.83 -lemma bin_last_XOR [simp]: "bin_last (x XOR y) = bin_last x XOR bin_last y"
    2.84 +lemma bin_last_XOR [simp]: "bin_last (x XOR y) \<longleftrightarrow> (bin_last x \<or> bin_last y) \<and> \<not> (bin_last x \<and> bin_last y)"
    2.85    by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
    2.86  
    2.87  lemma bin_nth_ops:
    2.88 @@ -225,36 +225,36 @@
    2.89    other simp rules. *}
    2.90  
    2.91  lemma bin_rl_eqI: "\<lbrakk>bin_rest x = bin_rest y; bin_last x = bin_last y\<rbrakk> \<Longrightarrow> x = y"
    2.92 -  by (metis bin_rl_simp)
    2.93 +  by (metis (mono_tags) BIT_eq_iff bin_ex_rl bin_last_BIT bin_rest_BIT)
    2.94  
    2.95  lemma bin_rest_neg_numeral_BitM [simp]:
    2.96    "bin_rest (- numeral (Num.BitM w)) = - numeral w"
    2.97    by (simp only: BIT_bin_simps [symmetric] bin_rest_BIT)
    2.98  
    2.99  lemma bin_last_neg_numeral_BitM [simp]:
   2.100 -  "bin_last (-  numeral (Num.BitM w)) = 1"
   2.101 +  "bin_last (- numeral (Num.BitM w))"
   2.102    by (simp only: BIT_bin_simps [symmetric] bin_last_BIT)
   2.103  
   2.104  text {* FIXME: The rule sets below are very large (24 rules for each
   2.105    operator). Is there a simpler way to do this? *}
   2.106  
   2.107  lemma int_and_numerals [simp]:
   2.108 -  "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT 0"
   2.109 -  "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 0"
   2.110 -  "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT 0"
   2.111 -  "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT 1"
   2.112 -  "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT 0"
   2.113 -  "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT 0"
   2.114 -  "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT 0"
   2.115 -  "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT 1"
   2.116 -  "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (- numeral x AND numeral y) BIT 0"
   2.117 -  "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (- numeral x AND numeral y) BIT 0"
   2.118 -  "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND numeral y) BIT 0"
   2.119 -  "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND numeral y) BIT 1"
   2.120 -  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (- numeral x AND - numeral y) BIT 0"
   2.121 -  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (- numeral x AND - numeral (y + Num.One)) BIT 0"
   2.122 -  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND - numeral y) BIT 0"
   2.123 -  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND - numeral (y + Num.One)) BIT 1"
   2.124 +  "numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
   2.125 +  "numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT False"
   2.126 +  "numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (numeral x AND numeral y) BIT False"
   2.127 +  "numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (numeral x AND numeral y) BIT True"
   2.128 +  "numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT False"
   2.129 +  "numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT False"
   2.130 +  "numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (numeral x AND - numeral y) BIT False"
   2.131 +  "numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (numeral x AND - numeral (y + Num.One)) BIT True"
   2.132 +  "- numeral (Num.Bit0 x) AND numeral (Num.Bit0 y) = (- numeral x AND numeral y) BIT False"
   2.133 +  "- numeral (Num.Bit0 x) AND numeral (Num.Bit1 y) = (- numeral x AND numeral y) BIT False"
   2.134 +  "- numeral (Num.Bit1 x) AND numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND numeral y) BIT False"
   2.135 +  "- numeral (Num.Bit1 x) AND numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND numeral y) BIT True"
   2.136 +  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit0 y) = (- numeral x AND - numeral y) BIT False"
   2.137 +  "- numeral (Num.Bit0 x) AND - numeral (Num.Bit1 y) = (- numeral x AND - numeral (y + Num.One)) BIT False"
   2.138 +  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit0 y) = (- numeral (x + Num.One) AND - numeral y) BIT False"
   2.139 +  "- numeral (Num.Bit1 x) AND - numeral (Num.Bit1 y) = (- numeral (x + Num.One) AND - numeral (y + Num.One)) BIT True"
   2.140    "(1::int) AND numeral (Num.Bit0 y) = 0"
   2.141    "(1::int) AND numeral (Num.Bit1 y) = 1"
   2.142    "(1::int) AND - numeral (Num.Bit0 y) = 0"
   2.143 @@ -266,22 +266,22 @@
   2.144    by (rule bin_rl_eqI, simp, simp)+
   2.145  
   2.146  lemma int_or_numerals [simp]:
   2.147 -  "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT 0"
   2.148 -  "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
   2.149 -  "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT 1"
   2.150 -  "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT 1"
   2.151 -  "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT 0"
   2.152 -  "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT 1"
   2.153 -  "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT 1"
   2.154 -  "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT 1"
   2.155 -  "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (- numeral x OR numeral y) BIT 0"
   2.156 -  "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (- numeral x OR numeral y) BIT 1"
   2.157 -  "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR numeral y) BIT 1"
   2.158 -  "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR numeral y) BIT 1"
   2.159 -  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (- numeral x OR - numeral y) BIT 0"
   2.160 -  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (- numeral x OR - numeral (y + Num.One)) BIT 1"
   2.161 -  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR - numeral y) BIT 1"
   2.162 -  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR - numeral (y + Num.One)) BIT 1"
   2.163 +  "numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT False"
   2.164 +  "numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT True"
   2.165 +  "numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (numeral x OR numeral y) BIT True"
   2.166 +  "numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (numeral x OR numeral y) BIT True"
   2.167 +  "numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT False"
   2.168 +  "numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT True"
   2.169 +  "numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (numeral x OR - numeral y) BIT True"
   2.170 +  "numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (numeral x OR - numeral (y + Num.One)) BIT True"
   2.171 +  "- numeral (Num.Bit0 x) OR numeral (Num.Bit0 y) = (- numeral x OR numeral y) BIT False"
   2.172 +  "- numeral (Num.Bit0 x) OR numeral (Num.Bit1 y) = (- numeral x OR numeral y) BIT True"
   2.173 +  "- numeral (Num.Bit1 x) OR numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR numeral y) BIT True"
   2.174 +  "- numeral (Num.Bit1 x) OR numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR numeral y) BIT True"
   2.175 +  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit0 y) = (- numeral x OR - numeral y) BIT False"
   2.176 +  "- numeral (Num.Bit0 x) OR - numeral (Num.Bit1 y) = (- numeral x OR - numeral (y + Num.One)) BIT True"
   2.177 +  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) OR - numeral y) BIT True"
   2.178 +  "- numeral (Num.Bit1 x) OR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) OR - numeral (y + Num.One)) BIT True"
   2.179    "(1::int) OR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
   2.180    "(1::int) OR numeral (Num.Bit1 y) = numeral (Num.Bit1 y)"
   2.181    "(1::int) OR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
   2.182 @@ -293,22 +293,22 @@
   2.183    by (rule bin_rl_eqI, simp, simp)+
   2.184  
   2.185  lemma int_xor_numerals [simp]:
   2.186 -  "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT 0"
   2.187 -  "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 1"
   2.188 -  "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT 1"
   2.189 -  "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT 0"
   2.190 -  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT 0"
   2.191 -  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT 1"
   2.192 -  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT 1"
   2.193 -  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT 0"
   2.194 -  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (- numeral x XOR numeral y) BIT 0"
   2.195 -  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (- numeral x XOR numeral y) BIT 1"
   2.196 -  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR numeral y) BIT 1"
   2.197 -  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR numeral y) BIT 0"
   2.198 -  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (- numeral x XOR - numeral y) BIT 0"
   2.199 -  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (- numeral x XOR - numeral (y + Num.One)) BIT 1"
   2.200 -  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR - numeral y) BIT 1"
   2.201 -  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR - numeral (y + Num.One)) BIT 0"
   2.202 +  "numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT False"
   2.203 +  "numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT True"
   2.204 +  "numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (numeral x XOR numeral y) BIT True"
   2.205 +  "numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (numeral x XOR numeral y) BIT False"
   2.206 +  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT False"
   2.207 +  "numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT True"
   2.208 +  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (numeral x XOR - numeral y) BIT True"
   2.209 +  "numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (numeral x XOR - numeral (y + Num.One)) BIT False"
   2.210 +  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit0 y) = (- numeral x XOR numeral y) BIT False"
   2.211 +  "- numeral (Num.Bit0 x) XOR numeral (Num.Bit1 y) = (- numeral x XOR numeral y) BIT True"
   2.212 +  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR numeral y) BIT True"
   2.213 +  "- numeral (Num.Bit1 x) XOR numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR numeral y) BIT False"
   2.214 +  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit0 y) = (- numeral x XOR - numeral y) BIT False"
   2.215 +  "- numeral (Num.Bit0 x) XOR - numeral (Num.Bit1 y) = (- numeral x XOR - numeral (y + Num.One)) BIT True"
   2.216 +  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit0 y) = (- numeral (x + Num.One) XOR - numeral y) BIT True"
   2.217 +  "- numeral (Num.Bit1 x) XOR - numeral (Num.Bit1 y) = (- numeral (x + Num.One) XOR - numeral (y + Num.One)) BIT False"
   2.218    "(1::int) XOR numeral (Num.Bit0 y) = numeral (Num.Bit1 y)"
   2.219    "(1::int) XOR numeral (Num.Bit1 y) = numeral (Num.Bit0 y)"
   2.220    "(1::int) XOR - numeral (Num.Bit0 y) = - numeral (Num.BitM y)"
   2.221 @@ -332,7 +332,7 @@
   2.222    apply (unfold Bit_def)
   2.223    apply clarsimp
   2.224    apply (erule_tac x = "x" in allE)
   2.225 -  apply (simp add: bitval_def split: bit.split)
   2.226 +  apply simp
   2.227    done
   2.228  
   2.229  lemma le_int_or:
   2.230 @@ -385,7 +385,7 @@
   2.231  subsection {* Setting and clearing bits *}
   2.232  
   2.233  primrec
   2.234 -  bin_sc :: "nat => bit => int => int"
   2.235 +  bin_sc :: "nat => bool => int => int"
   2.236  where
   2.237    Z: "bin_sc 0 b w = bin_rest w BIT b"
   2.238    | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
   2.239 @@ -393,7 +393,7 @@
   2.240  (** nth bit, set/clear **)
   2.241  
   2.242  lemma bin_nth_sc [simp]: 
   2.243 -  "bin_nth (bin_sc n b w) n = (b = 1)"
   2.244 +  "bin_nth (bin_sc n b w) n \<longleftrightarrow> b"
   2.245    by (induct n arbitrary: w) auto
   2.246  
   2.247  lemma bin_sc_sc_same [simp]: 
   2.248 @@ -409,11 +409,11 @@
   2.249    done
   2.250  
   2.251  lemma bin_nth_sc_gen: 
   2.252 -  "bin_nth (bin_sc n b w) m = (if m = n then b = 1 else bin_nth w m)"
   2.253 +  "bin_nth (bin_sc n b w) m = (if m = n then b else bin_nth w m)"
   2.254    by (induct n arbitrary: w m) (case_tac [!] m, auto)
   2.255    
   2.256  lemma bin_sc_nth [simp]:
   2.257 -  "(bin_sc n (If (bin_nth w n) 1 0) w) = w"
   2.258 +  "(bin_sc n (bin_nth w n) w) = w"
   2.259    by (induct n arbitrary: w) auto
   2.260  
   2.261  lemma bin_sign_sc [simp]:
   2.262 @@ -428,21 +428,21 @@
   2.263    done
   2.264  
   2.265  lemma bin_clr_le:
   2.266 -  "bin_sc n 0 w <= w"
   2.267 +  "bin_sc n False w <= w"
   2.268    apply (induct n arbitrary: w)
   2.269     apply (case_tac [!] w rule: bin_exhaust)
   2.270     apply (auto simp: le_Bits)
   2.271    done
   2.272  
   2.273  lemma bin_set_ge:
   2.274 -  "bin_sc n 1 w >= w"
   2.275 +  "bin_sc n True w >= w"
   2.276    apply (induct n arbitrary: w)
   2.277     apply (case_tac [!] w rule: bin_exhaust)
   2.278     apply (auto simp: le_Bits)
   2.279    done
   2.280  
   2.281  lemma bintr_bin_clr_le:
   2.282 -  "bintrunc n (bin_sc m 0 w) <= bintrunc n w"
   2.283 +  "bintrunc n (bin_sc m False w) <= bintrunc n w"
   2.284    apply (induct n arbitrary: w m)
   2.285     apply simp
   2.286    apply (case_tac w rule: bin_exhaust)
   2.287 @@ -451,7 +451,7 @@
   2.288    done
   2.289  
   2.290  lemma bintr_bin_set_ge:
   2.291 -  "bintrunc n (bin_sc m 1 w) >= bintrunc n w"
   2.292 +  "bintrunc n (bin_sc m True w) >= bintrunc n w"
   2.293    apply (induct n arbitrary: w m)
   2.294     apply simp
   2.295    apply (case_tac w rule: bin_exhaust)
   2.296 @@ -459,10 +459,10 @@
   2.297     apply (auto simp: le_Bits)
   2.298    done
   2.299  
   2.300 -lemma bin_sc_FP [simp]: "bin_sc n 0 0 = 0"
   2.301 +lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
   2.302    by (induct n) auto
   2.303  
   2.304 -lemma bin_sc_TM [simp]: "bin_sc n 1 -1 = -1"
   2.305 +lemma bin_sc_TM [simp]: "bin_sc n True -1 = -1"
   2.306    by (induct n) auto
   2.307    
   2.308  lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
   2.309 @@ -611,8 +611,7 @@
   2.310    apply (simp add: bin_rest_def zdiv_zmult2_eq)
   2.311    apply (case_tac b rule: bin_exhaust)
   2.312    apply simp
   2.313 -  apply (simp add: Bit_def mod_mult_mult1 p1mod22k bitval_def
   2.314 -              split: bit.split)
   2.315 +  apply (simp add: Bit_def mod_mult_mult1 p1mod22k)
   2.316    done
   2.317  
   2.318  subsection {* Miscellaneous lemmas *}
   2.319 @@ -632,7 +631,7 @@
   2.320    "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
   2.321    by auto
   2.322  
   2.323 -lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT 1"
   2.324 +lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT True"
   2.325    unfolding Bit_B1
   2.326    by (induct n) simp_all
   2.327  
   2.328 @@ -645,8 +644,8 @@
   2.329      by (rule mult_left_mono) simp
   2.330    then have "2 * (bin mod 2 ^ n) + 1 < 2 * 2 ^ n" by simp
   2.331    then show ?thesis
   2.332 -    by (auto simp add: Bit_def bitval_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
   2.333 -      mod_pos_pos_trivial split add: bit.split)
   2.334 +    by (auto simp add: Bit_def mod_mult_mult1 mod_add_left_eq [of "2 * bin"]
   2.335 +      mod_pos_pos_trivial)
   2.336  qed
   2.337  
   2.338  lemma AND_mod:
   2.339 @@ -665,7 +664,7 @@
   2.340    show ?case
   2.341    proof (cases n)
   2.342      case 0
   2.343 -    then show ?thesis by (simp add: int_and_extra_simps)
   2.344 +    then show ?thesis by simp
   2.345    next
   2.346      case (Suc m)
   2.347      with 3 show ?thesis
     3.1 --- a/src/HOL/Word/Bit_Operations.thy	Mon Dec 23 09:21:38 2013 +0100
     3.2 +++ b/src/HOL/Word/Bit_Operations.thy	Mon Dec 23 14:24:20 2013 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Syntactic classes for bitwise operations *}
     3.5  
     3.6  theory Bit_Operations
     3.7 -imports "~~/src/HOL/Library/Bit"
     3.8 +imports Main
     3.9  begin
    3.10  
    3.11  class bit =
     4.1 --- a/src/HOL/Word/Bit_Representation.thy	Mon Dec 23 09:21:38 2013 +0100
     4.2 +++ b/src/HOL/Word/Bit_Representation.thy	Mon Dec 23 14:24:20 2013 +0100
     4.3 @@ -5,38 +5,34 @@
     4.4  header {* Integers as implict bit strings *}
     4.5  
     4.6  theory Bit_Representation
     4.7 -imports "~~/src/HOL/Library/Bit" Misc_Numeric
     4.8 +imports Misc_Numeric
     4.9  begin
    4.10  
    4.11  subsection {* Constructors and destructors for binary integers *}
    4.12  
    4.13 -definition bitval :: "bit \<Rightarrow> 'a\<Colon>zero_neq_one" where
    4.14 -  "bitval = bit_case 0 1"
    4.15 -
    4.16 -lemma bitval_simps [simp]:
    4.17 -  "bitval 0 = 0"
    4.18 -  "bitval 1 = 1"
    4.19 -  by (simp_all add: bitval_def)
    4.20 -
    4.21 -definition Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
    4.22 -  "k BIT b = bitval b + k + k"
    4.23 +definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int" (infixl "BIT" 90) where
    4.24 +  "k BIT b = (if b then 1 else 0) + k + k"
    4.25  
    4.26  lemma Bit_B0:
    4.27 -  "k BIT (0::bit) = k + k"
    4.28 +  "k BIT False = k + k"
    4.29     by (unfold Bit_def) simp
    4.30  
    4.31  lemma Bit_B1:
    4.32 -  "k BIT (1::bit) = k + k + 1"
    4.33 +  "k BIT True = k + k + 1"
    4.34     by (unfold Bit_def) simp
    4.35    
    4.36 -lemma Bit_B0_2t: "k BIT (0::bit) = 2 * k"
    4.37 +lemma Bit_B0_2t: "k BIT False = 2 * k"
    4.38    by (rule trans, rule Bit_B0) simp
    4.39  
    4.40 -lemma Bit_B1_2t: "k BIT (1::bit) = 2 * k + 1"
    4.41 +lemma Bit_B1_2t: "k BIT True = 2 * k + 1"
    4.42    by (rule trans, rule Bit_B1) simp
    4.43  
    4.44 -definition bin_last :: "int \<Rightarrow> bit" where
    4.45 -  "bin_last w = (if w mod 2 = 0 then (0::bit) else (1::bit))"
    4.46 +definition bin_last :: "int \<Rightarrow> bool" where
    4.47 +  "bin_last w \<longleftrightarrow> w mod 2 = 1"
    4.48 +
    4.49 +lemma bin_last_odd:
    4.50 +  "bin_last = odd"
    4.51 +  by (rule ext) (simp add: bin_last_def even_def)
    4.52  
    4.53  definition bin_rest :: "int \<Rightarrow> int" where
    4.54    "bin_rest w = w div 2"
    4.55 @@ -56,48 +52,55 @@
    4.56    by (cases b, simp_all add: z1pmod2)
    4.57  
    4.58  lemma BIT_eq_iff [iff]: "u BIT b = v BIT c \<longleftrightarrow> u = v \<and> b = c"
    4.59 -  by (metis bin_rest_BIT bin_last_BIT)
    4.60 +  apply (auto simp add: Bit_def)
    4.61 +  apply arith
    4.62 +  apply arith
    4.63 +  done
    4.64  
    4.65  lemma BIT_bin_simps [simp]:
    4.66 -  "numeral k BIT 0 = numeral (Num.Bit0 k)"
    4.67 -  "numeral k BIT 1 = numeral (Num.Bit1 k)"
    4.68 -  "(- numeral k) BIT 0 = - numeral (Num.Bit0 k)"
    4.69 -  "(- numeral k) BIT 1 = - numeral (Num.BitM k)"
    4.70 +  "numeral k BIT False = numeral (Num.Bit0 k)"
    4.71 +  "numeral k BIT True = numeral (Num.Bit1 k)"
    4.72 +  "(- numeral k) BIT False = - numeral (Num.Bit0 k)"
    4.73 +  "(- numeral k) BIT True = - numeral (Num.BitM k)"
    4.74    unfolding numeral.simps numeral_BitM
    4.75 -  unfolding Bit_def bitval_simps
    4.76 +  unfolding Bit_def
    4.77    by (simp_all del: arith_simps add_numeral_special diff_numeral_special)
    4.78  
    4.79  lemma BIT_special_simps [simp]:
    4.80 -  shows "0 BIT 0 = 0" and "0 BIT 1 = 1"
    4.81 -  and "1 BIT 0 = 2" and "1 BIT 1 = 3"
    4.82 -  and "(- 1) BIT 0 = - 2" and "(- 1) BIT 1 = - 1"
    4.83 +  shows "0 BIT False = 0" and "0 BIT True = 1"
    4.84 +  and "1 BIT False = 2" and "1 BIT True = 3"
    4.85 +  and "(- 1) BIT False = - 2" and "(- 1) BIT True = - 1"
    4.86    unfolding Bit_def by simp_all
    4.87  
    4.88 -lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> b = 0"
    4.89 -  by (subst BIT_eq_iff [symmetric], simp)
    4.90 +lemma Bit_eq_0_iff: "w BIT b = 0 \<longleftrightarrow> w = 0 \<and> \<not> b"
    4.91 +  apply (auto simp add: Bit_def)
    4.92 +  apply arith
    4.93 +  done
    4.94  
    4.95 -lemma Bit_eq_m1_iff: "w BIT b = - 1 \<longleftrightarrow> w = - 1 \<and> b = 1"
    4.96 -  by (cases b) (auto simp add: Bit_def, arith)
    4.97 +lemma Bit_eq_m1_iff: "w BIT b = -1 \<longleftrightarrow> w = -1 \<and> b"
    4.98 +  apply (auto simp add: Bit_def)
    4.99 +  apply arith
   4.100 +  done
   4.101  
   4.102  lemma BitM_inc: "Num.BitM (Num.inc w) = Num.Bit1 w"
   4.103    by (induct w, simp_all)
   4.104  
   4.105  lemma expand_BIT:
   4.106 -  "numeral (Num.Bit0 w) = numeral w BIT 0"
   4.107 -  "numeral (Num.Bit1 w) = numeral w BIT 1"
   4.108 -  "- numeral (Num.Bit0 w) = - numeral w BIT 0"
   4.109 -  "- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT 1"
   4.110 +  "numeral (Num.Bit0 w) = numeral w BIT False"
   4.111 +  "numeral (Num.Bit1 w) = numeral w BIT True"
   4.112 +  "- numeral (Num.Bit0 w) = (- numeral w) BIT False"
   4.113 +  "- numeral (Num.Bit1 w) = (- numeral (w + Num.One)) BIT True"
   4.114    unfolding add_One by (simp_all add: BitM_inc)
   4.115  
   4.116  lemma bin_last_numeral_simps [simp]:
   4.117 -  "bin_last 0 = 0"
   4.118 -  "bin_last 1 = 1"
   4.119 -  "bin_last -1 = 1"
   4.120 -  "bin_last Numeral1 = 1"
   4.121 -  "bin_last (numeral (Num.Bit0 w)) = 0"
   4.122 -  "bin_last (numeral (Num.Bit1 w)) = 1"
   4.123 -  "bin_last (- numeral (Num.Bit0 w)) = 0"
   4.124 -  "bin_last (- numeral (Num.Bit1 w)) = 1"
   4.125 +  "\<not> bin_last 0"
   4.126 +  "bin_last 1"
   4.127 +  "bin_last -1"
   4.128 +  "bin_last Numeral1"
   4.129 +  "\<not> bin_last (numeral (Num.Bit0 w))"
   4.130 +  "bin_last (numeral (Num.Bit1 w))"
   4.131 +  "\<not> bin_last (- numeral (Num.Bit0 w))"
   4.132 +  "bin_last (- numeral (Num.Bit1 w))"
   4.133    unfolding expand_BIT bin_last_BIT by (simp_all add: bin_last_def zmod_zminus1_eq_if)
   4.134  
   4.135  lemma bin_rest_numeral_simps [simp]:
   4.136 @@ -112,51 +115,42 @@
   4.137    unfolding expand_BIT bin_rest_BIT by (simp_all add: bin_rest_def zdiv_zminus1_eq_if)
   4.138  
   4.139  lemma less_Bits: 
   4.140 -  "(v BIT b < w BIT c) = (v < w | v <= w & b = (0::bit) & c = (1::bit))"
   4.141 -  unfolding Bit_def by (auto simp add: bitval_def split: bit.split)
   4.142 +  "v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"
   4.143 +  unfolding Bit_def by auto
   4.144  
   4.145  lemma le_Bits: 
   4.146 -  "(v BIT b <= w BIT c) = (v < w | v <= w & (b ~= (1::bit) | c ~= (0::bit)))" 
   4.147 -  unfolding Bit_def by (auto simp add: bitval_def split: bit.split)
   4.148 +  "v BIT b \<le> w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> (\<not> b \<or> c)" 
   4.149 +  unfolding Bit_def by auto
   4.150  
   4.151  lemma pred_BIT_simps [simp]:
   4.152 -  "x BIT 0 - 1 = (x - 1) BIT 1"
   4.153 -  "x BIT 1 - 1 = x BIT 0"
   4.154 +  "x BIT False - 1 = (x - 1) BIT True"
   4.155 +  "x BIT True - 1 = x BIT False"
   4.156    by (simp_all add: Bit_B0_2t Bit_B1_2t)
   4.157  
   4.158  lemma succ_BIT_simps [simp]:
   4.159 -  "x BIT 0 + 1 = x BIT 1"
   4.160 -  "x BIT 1 + 1 = (x + 1) BIT 0"
   4.161 +  "x BIT False + 1 = x BIT True"
   4.162 +  "x BIT True + 1 = (x + 1) BIT False"
   4.163    by (simp_all add: Bit_B0_2t Bit_B1_2t)
   4.164  
   4.165  lemma add_BIT_simps [simp]:
   4.166 -  "x BIT 0 + y BIT 0 = (x + y) BIT 0"
   4.167 -  "x BIT 0 + y BIT 1 = (x + y) BIT 1"
   4.168 -  "x BIT 1 + y BIT 0 = (x + y) BIT 1"
   4.169 -  "x BIT 1 + y BIT 1 = (x + y + 1) BIT 0"
   4.170 +  "x BIT False + y BIT False = (x + y) BIT False"
   4.171 +  "x BIT False + y BIT True = (x + y) BIT True"
   4.172 +  "x BIT True + y BIT False = (x + y) BIT True"
   4.173 +  "x BIT True + y BIT True = (x + y + 1) BIT False"
   4.174    by (simp_all add: Bit_B0_2t Bit_B1_2t)
   4.175  
   4.176  lemma mult_BIT_simps [simp]:
   4.177 -  "x BIT 0 * y = (x * y) BIT 0"
   4.178 -  "x * y BIT 0 = (x * y) BIT 0"
   4.179 -  "x BIT 1 * y = (x * y) BIT 0 + y"
   4.180 +  "x BIT False * y = (x * y) BIT False"
   4.181 +  "x * y BIT False = (x * y) BIT False"
   4.182 +  "x BIT True * y = (x * y) BIT False + y"
   4.183    by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps)
   4.184  
   4.185  lemma B_mod_2': 
   4.186 -  "X = 2 ==> (w BIT (1::bit)) mod X = 1 & (w BIT (0::bit)) mod X = 0"
   4.187 +  "X = 2 ==> (w BIT True) mod X = 1 & (w BIT False) mod X = 0"
   4.188    apply (simp (no_asm) only: Bit_B0 Bit_B1)
   4.189    apply (simp add: z1pmod2)
   4.190    done
   4.191  
   4.192 -lemma neB1E [elim!]:
   4.193 -  assumes ne: "y \<noteq> (1::bit)"
   4.194 -  assumes y: "y = (0::bit) \<Longrightarrow> P"
   4.195 -  shows "P"
   4.196 -  apply (rule y)
   4.197 -  apply (cases y rule: bit.exhaust, simp)
   4.198 -  apply (simp add: ne)
   4.199 -  done
   4.200 -
   4.201  lemma bin_ex_rl: "EX w b. w BIT b = bin"
   4.202    by (metis bin_rl_simp)
   4.203  
   4.204 @@ -170,8 +164,10 @@
   4.205    done
   4.206  
   4.207  primrec bin_nth where
   4.208 -  Z: "bin_nth w 0 = (bin_last w = (1::bit))"
   4.209 -  | Suc: "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
   4.210 +  Z: "bin_nth w 0 \<longleftrightarrow> bin_last w"
   4.211 +  | Suc: "bin_nth w (Suc n) \<longleftrightarrow> bin_nth (bin_rest w) n"
   4.212 +
   4.213 +find_theorems "bin_rest _ = _"
   4.214  
   4.215  lemma bin_abs_lem:
   4.216    "bin = (w BIT b) ==> bin ~= -1 --> bin ~= 0 -->
   4.217 @@ -248,7 +244,7 @@
   4.218  lemma bin_nth_minus1 [simp]: "bin_nth -1 n"
   4.219    by (induct n) auto
   4.220  
   4.221 -lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = (1::bit))"
   4.222 +lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 \<longleftrightarrow> b"
   4.223    by auto
   4.224  
   4.225  lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n"
   4.226 @@ -285,8 +281,8 @@
   4.227    "bin_sign (numeral k) = 0"
   4.228    "bin_sign (- numeral k) = -1"
   4.229    "bin_sign (w BIT b) = bin_sign w"
   4.230 -  unfolding bin_sign_def Bit_def bitval_def
   4.231 -  by (simp_all split: bit.split)
   4.232 +  unfolding bin_sign_def Bit_def
   4.233 +  by simp_all
   4.234  
   4.235  lemma bin_sign_rest [simp]: 
   4.236    "bin_sign (bin_rest w) = bin_sign w"
   4.237 @@ -297,7 +293,7 @@
   4.238  | Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
   4.239  
   4.240  primrec sbintrunc :: "nat => int => int" where
   4.241 -  Z : "sbintrunc 0 bin = (case bin_last bin of (1::bit) \<Rightarrow> -1 | (0::bit) \<Rightarrow> 0)"
   4.242 +  Z : "sbintrunc 0 bin = (if bin_last bin then -1 else 0)"
   4.243  | Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
   4.244  
   4.245  lemma sign_bintr: "bin_sign (bintrunc n w) = 0"
   4.246 @@ -313,7 +309,8 @@
   4.247     apply simp
   4.248     apply (subst mod_add_left_eq)
   4.249     apply (simp add: bin_last_def)
   4.250 -  apply (simp add: bin_last_def bin_rest_def Bit_def)
   4.251 +   apply arith
   4.252 +  apply (simp add: bin_last_def bin_rest_def Bit_def mod_2_neq_1_eq_eq_0)
   4.253    apply (clarsimp simp: mod_mult_mult1 [symmetric] 
   4.254           zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
   4.255    apply (rule trans [symmetric, OF _ emep1])
   4.256 @@ -334,13 +331,13 @@
   4.257  
   4.258  lemma bintrunc_Suc_numeral:
   4.259    "bintrunc (Suc n) 1 = 1"
   4.260 -  "bintrunc (Suc n) -1 = bintrunc n -1 BIT 1"
   4.261 -  "bintrunc (Suc n) (numeral (Num.Bit0 w)) = bintrunc n (numeral w) BIT 0"
   4.262 -  "bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT 1"
   4.263 +  "bintrunc (Suc n) -1 = bintrunc n -1 BIT True"
   4.264 +  "bintrunc (Suc n) (numeral (Num.Bit0 w)) = bintrunc n (numeral w) BIT False"
   4.265 +  "bintrunc (Suc n) (numeral (Num.Bit1 w)) = bintrunc n (numeral w) BIT True"
   4.266    "bintrunc (Suc n) (- numeral (Num.Bit0 w)) =
   4.267 -    bintrunc n (- numeral w) BIT 0"
   4.268 +    bintrunc n (- numeral w) BIT False"
   4.269    "bintrunc (Suc n) (- numeral (Num.Bit1 w)) =
   4.270 -    bintrunc n (- numeral (w + Num.One)) BIT 1"
   4.271 +    bintrunc n (- numeral (w + Num.One)) BIT True"
   4.272    by simp_all
   4.273  
   4.274  lemma sbintrunc_0_numeral [simp]:
   4.275 @@ -354,21 +351,15 @@
   4.276  lemma sbintrunc_Suc_numeral:
   4.277    "sbintrunc (Suc n) 1 = 1"
   4.278    "sbintrunc (Suc n) (numeral (Num.Bit0 w)) =
   4.279 -    sbintrunc n (numeral w) BIT 0"
   4.280 +    sbintrunc n (numeral w) BIT False"
   4.281    "sbintrunc (Suc n) (numeral (Num.Bit1 w)) =
   4.282 -    sbintrunc n (numeral w) BIT 1"
   4.283 +    sbintrunc n (numeral w) BIT True"
   4.284    "sbintrunc (Suc n) (- numeral (Num.Bit0 w)) =
   4.285 -    sbintrunc n (- numeral w) BIT 0"
   4.286 +    sbintrunc n (- numeral w) BIT False"
   4.287    "sbintrunc (Suc n) (- numeral (Num.Bit1 w)) =
   4.288 -    sbintrunc n (- numeral (w + Num.One)) BIT 1"
   4.289 +    sbintrunc n (- numeral (w + Num.One)) BIT True"
   4.290    by simp_all
   4.291  
   4.292 -lemma bit_bool:
   4.293 -  "(b = (b' = (1::bit))) = (b' = (if b then (1::bit) else (0::bit)))"
   4.294 -  by (cases b') auto
   4.295 -
   4.296 -lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
   4.297 -
   4.298  lemma bin_sign_lem: "(bin_sign (sbintrunc n bin) = -1) = bin_nth bin n"
   4.299    apply (induct n arbitrary: bin)
   4.300    apply (case_tac bin rule: bin_exhaust, case_tac b, auto)
   4.301 @@ -384,23 +375,25 @@
   4.302    "bin_nth (sbintrunc m w) n = 
   4.303            (if n < m then bin_nth w n else bin_nth w m)"
   4.304    apply (induct n arbitrary: w m)
   4.305 -   apply (case_tac m, simp_all split: bit.splits)[1]
   4.306 -  apply (case_tac m, simp_all split: bit.splits)[1]
   4.307 +  apply (case_tac m)
   4.308 +  apply simp_all
   4.309 +  apply (case_tac m)
   4.310 +  apply simp_all
   4.311    done
   4.312  
   4.313  lemma bin_nth_Bit:
   4.314 -  "bin_nth (w BIT b) n = (n = 0 & b = (1::bit) | (EX m. n = Suc m & bin_nth w m))"
   4.315 +  "bin_nth (w BIT b) n = (n = 0 & b | (EX m. n = Suc m & bin_nth w m))"
   4.316    by (cases n) auto
   4.317  
   4.318  lemma bin_nth_Bit0:
   4.319    "bin_nth (numeral (Num.Bit0 w)) n \<longleftrightarrow>
   4.320      (\<exists>m. n = Suc m \<and> bin_nth (numeral w) m)"
   4.321 -  using bin_nth_Bit [where w="numeral w" and b="(0::bit)"] by simp
   4.322 +  using bin_nth_Bit [where w="numeral w" and b="False"] by simp
   4.323  
   4.324  lemma bin_nth_Bit1:
   4.325    "bin_nth (numeral (Num.Bit1 w)) n \<longleftrightarrow>
   4.326      n = 0 \<or> (\<exists>m. n = Suc m \<and> bin_nth (numeral w) m)"
   4.327 -  using bin_nth_Bit [where w="numeral w" and b="(1::bit)"] by simp
   4.328 +  using bin_nth_Bit [where w="numeral w" and b="True"] by simp
   4.329  
   4.330  lemma bintrunc_bintrunc_l:
   4.331    "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
   4.332 @@ -452,19 +445,19 @@
   4.333  
   4.334  lemmas sbintrunc_Pls = 
   4.335    sbintrunc.Z [where bin="0", 
   4.336 -               simplified bin_last_numeral_simps bin_rest_numeral_simps bit.simps]
   4.337 +               simplified bin_last_numeral_simps bin_rest_numeral_simps]
   4.338  
   4.339  lemmas sbintrunc_Min = 
   4.340    sbintrunc.Z [where bin="-1",
   4.341 -               simplified bin_last_numeral_simps bin_rest_numeral_simps bit.simps]
   4.342 +               simplified bin_last_numeral_simps bin_rest_numeral_simps]
   4.343  
   4.344  lemmas sbintrunc_0_BIT_B0 [simp] = 
   4.345 -  sbintrunc.Z [where bin="w BIT (0::bit)", 
   4.346 -               simplified bin_last_numeral_simps bin_rest_numeral_simps bit.simps] for w
   4.347 +  sbintrunc.Z [where bin="w BIT False", 
   4.348 +               simplified bin_last_numeral_simps bin_rest_numeral_simps] for w
   4.349  
   4.350  lemmas sbintrunc_0_BIT_B1 [simp] = 
   4.351 -  sbintrunc.Z [where bin="w BIT (1::bit)", 
   4.352 -               simplified bin_last_BIT bin_rest_numeral_simps bit.simps] for w
   4.353 +  sbintrunc.Z [where bin="w BIT True", 
   4.354 +               simplified bin_last_BIT bin_rest_numeral_simps] for w
   4.355  
   4.356  lemmas sbintrunc_0_simps =
   4.357    sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
   4.358 @@ -583,25 +576,25 @@
   4.359  
   4.360  lemma bintrunc_numeral_simps [simp]:
   4.361    "bintrunc (numeral k) (numeral (Num.Bit0 w)) =
   4.362 -    bintrunc (pred_numeral k) (numeral w) BIT 0"
   4.363 +    bintrunc (pred_numeral k) (numeral w) BIT False"
   4.364    "bintrunc (numeral k) (numeral (Num.Bit1 w)) =
   4.365 -    bintrunc (pred_numeral k) (numeral w) BIT 1"
   4.366 +    bintrunc (pred_numeral k) (numeral w) BIT True"
   4.367    "bintrunc (numeral k) (- numeral (Num.Bit0 w)) =
   4.368 -    bintrunc (pred_numeral k) (- numeral w) BIT 0"
   4.369 +    bintrunc (pred_numeral k) (- numeral w) BIT False"
   4.370    "bintrunc (numeral k) (- numeral (Num.Bit1 w)) =
   4.371 -    bintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT 1"
   4.372 +    bintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT True"
   4.373    "bintrunc (numeral k) 1 = 1"
   4.374    by (simp_all add: bintrunc_numeral)
   4.375  
   4.376  lemma sbintrunc_numeral_simps [simp]:
   4.377    "sbintrunc (numeral k) (numeral (Num.Bit0 w)) =
   4.378 -    sbintrunc (pred_numeral k) (numeral w) BIT 0"
   4.379 +    sbintrunc (pred_numeral k) (numeral w) BIT False"
   4.380    "sbintrunc (numeral k) (numeral (Num.Bit1 w)) =
   4.381 -    sbintrunc (pred_numeral k) (numeral w) BIT 1"
   4.382 +    sbintrunc (pred_numeral k) (numeral w) BIT True"
   4.383    "sbintrunc (numeral k) (- numeral (Num.Bit0 w)) =
   4.384 -    sbintrunc (pred_numeral k) (- numeral w) BIT 0"
   4.385 +    sbintrunc (pred_numeral k) (- numeral w) BIT False"
   4.386    "sbintrunc (numeral k) (- numeral (Num.Bit1 w)) =
   4.387 -    sbintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT 1"
   4.388 +    sbintrunc (pred_numeral k) (- numeral (w + Num.One)) BIT True"
   4.389    "sbintrunc (numeral k) 1 = 1"
   4.390    by (simp_all add: sbintrunc_numeral)
   4.391  
   4.392 @@ -728,7 +721,7 @@
   4.393    "sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
   4.394    apply (induct n arbitrary: bin, simp)
   4.395    apply (case_tac bin rule: bin_exhaust)
   4.396 -  apply (auto simp: bintrunc_bintrunc_l split: bit.splits)
   4.397 +  apply (auto simp: bintrunc_bintrunc_l split: bool.splits)
   4.398    done
   4.399  
   4.400  lemma bintrunc_rest':
     5.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Mon Dec 23 09:21:38 2013 +0100
     5.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Mon Dec 23 14:24:20 2013 +0100
     5.3 @@ -34,7 +34,7 @@
     5.4  primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
     5.5    Nil: "bl_to_bin_aux [] w = w"
     5.6    | Cons: "bl_to_bin_aux (b # bs) w = 
     5.7 -      bl_to_bin_aux bs (w BIT (if b then 1 else 0))"
     5.8 +      bl_to_bin_aux bs (w BIT b)"
     5.9  
    5.10  definition bl_to_bin :: "bool list \<Rightarrow> int" where
    5.11    bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
    5.12 @@ -42,7 +42,7 @@
    5.13  primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
    5.14    Z: "bin_to_bl_aux 0 w bl = bl"
    5.15    | Suc: "bin_to_bl_aux (Suc n) w bl =
    5.16 -      bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)"
    5.17 +      bin_to_bl_aux n (bin_rest w) ((bin_last w) # bl)"
    5.18  
    5.19  definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
    5.20    bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
    5.21 @@ -106,7 +106,7 @@
    5.22  
    5.23  lemma bin_to_bl_aux_Bit_minus_simp [simp]:
    5.24    "0 < n ==> bin_to_bl_aux n (w BIT b) bl = 
    5.25 -    bin_to_bl_aux (n - 1) w ((b = 1) # bl)"
    5.26 +    bin_to_bl_aux (n - 1) w (b # bl)"
    5.27    by (cases n) auto
    5.28  
    5.29  lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
    5.30 @@ -253,8 +253,7 @@
    5.31    apply (induct n arbitrary: w bs)
    5.32     apply clarsimp
    5.33     apply (cases w rule: bin_exhaust)
    5.34 -   apply (simp split add : bit.split)
    5.35 -  apply clarsimp
    5.36 +   apply simp
    5.37    done
    5.38      
    5.39  lemma bl_sbin_sign: 
    5.40 @@ -317,7 +316,6 @@
    5.41    apply (induct bs arbitrary: w)
    5.42     apply clarsimp
    5.43    apply clarsimp
    5.44 -  apply safe
    5.45    apply (drule meta_spec, erule xtrans(8) [rotated], simp add: Bit_def)+
    5.46    done
    5.47  
    5.48 @@ -334,9 +332,9 @@
    5.49    apply (induct bs arbitrary: w)
    5.50     apply clarsimp
    5.51    apply clarsimp
    5.52 -  apply safe
    5.53     apply (drule meta_spec, erule order_trans [rotated],
    5.54            simp add: Bit_B0_2t Bit_B1_2t algebra_simps)+
    5.55 +   apply (simp add: Bit_def)
    5.56    done
    5.57  
    5.58  lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
    5.59 @@ -422,15 +420,15 @@
    5.60    by (cases xs) auto
    5.61  
    5.62  lemma last_bin_last': 
    5.63 -  "size xs > 0 \<Longrightarrow> last xs = (bin_last (bl_to_bin_aux xs w) = 1)" 
    5.64 +  "size xs > 0 \<Longrightarrow> last xs \<longleftrightarrow> bin_last (bl_to_bin_aux xs w)" 
    5.65    by (induct xs arbitrary: w) auto
    5.66  
    5.67  lemma last_bin_last: 
    5.68 -  "size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = 1)" 
    5.69 +  "size xs > 0 ==> last xs \<longleftrightarrow> bin_last (bl_to_bin xs)" 
    5.70    unfolding bl_to_bin_def by (erule last_bin_last')
    5.71    
    5.72  lemma bin_last_last: 
    5.73 -  "bin_last w = (if last (bin_to_bl (Suc n) w) then 1 else 0)" 
    5.74 +  "bin_last w \<longleftrightarrow> last (bin_to_bl (Suc n) w)" 
    5.75    apply (unfold bin_to_bl_def)
    5.76    apply simp
    5.77    apply (auto simp add: bin_to_bl_aux_alt)
    5.78 @@ -447,7 +445,7 @@
    5.79    apply (case_tac w rule: bin_exhaust)
    5.80    apply clarsimp
    5.81    apply (case_tac b)
    5.82 -  apply (case_tac ba, safe, simp_all)+
    5.83 +  apply auto
    5.84    done
    5.85  
    5.86  lemma bl_or_aux_bin:
    5.87 @@ -458,8 +456,6 @@
    5.88    apply (case_tac v rule: bin_exhaust)
    5.89    apply (case_tac w rule: bin_exhaust)
    5.90    apply clarsimp
    5.91 -  apply (case_tac b)
    5.92 -  apply (case_tac ba, safe, simp_all)+
    5.93    done
    5.94      
    5.95  lemma bl_and_aux_bin:
    5.96 @@ -846,7 +842,7 @@
    5.97  lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
    5.98  
    5.99  lemma rbbl_Cons: 
   5.100 -  "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT If b 1 0))"
   5.101 +  "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT b))"
   5.102    apply (unfold bin_to_bl_def)
   5.103    apply simp
   5.104    apply (simp add: bin_to_bl_aux_alt)
     6.1 --- a/src/HOL/Word/Misc_Numeric.thy	Mon Dec 23 09:21:38 2013 +0100
     6.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Mon Dec 23 14:24:20 2013 +0100
     6.3 @@ -22,6 +22,11 @@
     6.4    
     6.5  lemmas min_minus' [simp] = trans [OF min_max.inf_commute min_minus]
     6.6  
     6.7 +lemma mod_2_neq_1_eq_eq_0:
     6.8 +  fixes k :: int
     6.9 +  shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
    6.10 +  by arith
    6.11 +
    6.12  lemma z1pmod2:
    6.13    "(2 * b + 1) mod 2 = (1::int)" by arith
    6.14  
     7.1 --- a/src/HOL/Word/Word.thy	Mon Dec 23 09:21:38 2013 +0100
     7.2 +++ b/src/HOL/Word/Word.thy	Mon Dec 23 14:24:20 2013 +0100
     7.3 @@ -390,16 +390,16 @@
     7.4  
     7.5  definition
     7.6    word_set_bit_def: "set_bit a n x =
     7.7 -   word_of_int (bin_sc n (If x 1 0) (uint a))"
     7.8 +   word_of_int (bin_sc n x (uint a))"
     7.9  
    7.10  definition
    7.11    word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE ('a)) f)"
    7.12  
    7.13  definition
    7.14 -  word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a) = 1"
    7.15 +  word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
    7.16  
    7.17  definition shiftl1 :: "'a word \<Rightarrow> 'a word" where
    7.18 -  "shiftl1 w = word_of_int (uint w BIT 0)"
    7.19 +  "shiftl1 w = word_of_int (uint w BIT False)"
    7.20  
    7.21  definition shiftr1 :: "'a word \<Rightarrow> 'a word" where
    7.22    -- "shift right as unsigned or as signed, ie logical or arithmetic"
    7.23 @@ -2524,15 +2524,15 @@
    7.24    by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
    7.25  
    7.26  lemma word_lsb_numeral [simp]:
    7.27 -  "lsb (numeral bin :: 'a :: len word) = (bin_last (numeral bin) = 1)"
    7.28 +  "lsb (numeral bin :: 'a :: len word) \<longleftrightarrow> bin_last (numeral bin)"
    7.29    unfolding word_lsb_alt test_bit_numeral by simp
    7.30  
    7.31  lemma word_lsb_neg_numeral [simp]:
    7.32 -  "lsb (- numeral bin :: 'a :: len word) = (bin_last (- numeral bin) = 1)"
    7.33 +  "lsb (- numeral bin :: 'a :: len word) \<longleftrightarrow> bin_last (- numeral bin)"
    7.34    unfolding word_lsb_alt test_bit_neg_numeral by simp
    7.35  
    7.36  lemma set_bit_word_of_int:
    7.37 -  "set_bit (word_of_int x) n b = word_of_int (bin_sc n (if b then 1 else 0) x)"
    7.38 +  "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
    7.39    unfolding word_set_bit_def
    7.40    apply (rule word_eqI)
    7.41    apply (simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
    7.42 @@ -2540,28 +2540,28 @@
    7.43  
    7.44  lemma word_set_numeral [simp]:
    7.45    "set_bit (numeral bin::'a::len0 word) n b = 
    7.46 -    word_of_int (bin_sc n (if b then 1 else 0) (numeral bin))"
    7.47 +    word_of_int (bin_sc n b (numeral bin))"
    7.48    unfolding word_numeral_alt by (rule set_bit_word_of_int)
    7.49  
    7.50  lemma word_set_neg_numeral [simp]:
    7.51    "set_bit (- numeral bin::'a::len0 word) n b = 
    7.52 -    word_of_int (bin_sc n (if b then 1 else 0) (- numeral bin))"
    7.53 +    word_of_int (bin_sc n b (- numeral bin))"
    7.54    unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
    7.55  
    7.56  lemma word_set_bit_0 [simp]:
    7.57 -  "set_bit 0 n b = word_of_int (bin_sc n (if b then 1 else 0) 0)"
    7.58 +  "set_bit 0 n b = word_of_int (bin_sc n b 0)"
    7.59    unfolding word_0_wi by (rule set_bit_word_of_int)
    7.60  
    7.61  lemma word_set_bit_1 [simp]:
    7.62 -  "set_bit 1 n b = word_of_int (bin_sc n (if b then 1 else 0) 1)"
    7.63 +  "set_bit 1 n b = word_of_int (bin_sc n b 1)"
    7.64    unfolding word_1_wi by (rule set_bit_word_of_int)
    7.65  
    7.66  lemma setBit_no [simp]:
    7.67 -  "setBit (numeral bin) n = word_of_int (bin_sc n 1 (numeral bin))"
    7.68 +  "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
    7.69    by (simp add: setBit_def)
    7.70  
    7.71  lemma clearBit_no [simp]:
    7.72 -  "clearBit (numeral bin) n = word_of_int (bin_sc n 0 (numeral bin))"
    7.73 +  "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
    7.74    by (simp add: clearBit_def)
    7.75  
    7.76  lemma to_bl_n1: 
    7.77 @@ -2645,7 +2645,6 @@
    7.78    fixes w :: "'a::len0 word"
    7.79    shows "w >= set_bit w n False"
    7.80    apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
    7.81 -  apply simp
    7.82    apply (rule order_trans)
    7.83     apply (rule bintr_bin_clr_le)
    7.84    apply simp
    7.85 @@ -2655,7 +2654,6 @@
    7.86    fixes w :: "'a::len word"
    7.87    shows "w <= set_bit w n True"
    7.88    apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
    7.89 -  apply simp
    7.90    apply (rule order_trans [OF _ bintr_bin_set_ge])
    7.91    apply simp
    7.92    done
    7.93 @@ -2663,7 +2661,7 @@
    7.94  
    7.95  subsection {* Shifting, Rotating, and Splitting Words *}
    7.96  
    7.97 -lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT 0)"
    7.98 +lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT False)"
    7.99    unfolding shiftl1_def
   7.100    apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
   7.101    apply (subst refl [THEN bintrunc_BIT_I, symmetric])
   7.102 @@ -2682,10 +2680,10 @@
   7.103  lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
   7.104    unfolding shiftl1_def by simp
   7.105  
   7.106 -lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT 0)"
   7.107 +lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT False)"
   7.108    by (simp only: shiftl1_def) (* FIXME: duplicate *)
   7.109  
   7.110 -lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT 0)"
   7.111 +lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT False)"
   7.112    unfolding shiftl1_def Bit_B0 wi_hom_syms by simp
   7.113  
   7.114  lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
     8.1 --- a/src/HOL/Word/WordBitwise.thy	Mon Dec 23 09:21:38 2013 +0100
     8.2 +++ b/src/HOL/Word/WordBitwise.thy	Mon Dec 23 14:24:20 2013 +0100
     8.3 @@ -364,8 +364,7 @@
     8.4              = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
     8.5    apply (induct xs ys rule: list_induct2)
     8.6     apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat)
     8.7 -  apply (simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq)
     8.8 -  apply arith?
     8.9 +  apply (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def)
    8.10    done
    8.11  
    8.12  lemma word_le_rbl: