clear separation of types for bits (False / True) and Z2 (0 / 1)
authorhaftmann
Fri Jun 14 08:34:27 2019 +0000 (5 weeks ago ago)
changeset 70527e4d626692640
parent 70526 972c0c744e7c
child 70528 e54caaa38ad9
clear separation of types for bits (False / True) and Z2 (0 / 1)
NEWS
src/HOL/Library/Bit.thy
src/HOL/Library/Library.thy
src/HOL/Library/Z2.thy
src/HOL/Word/Bits_Bit.thy
src/HOL/Word/Bits_Z2.thy
src/HOL/Word/Misc_Arithmetic.thy
src/HOL/Word/Word.thy
     1.1 --- a/NEWS	Fri Jun 14 08:34:27 2019 +0000
     1.2 +++ b/NEWS	Fri Jun 14 08:34:27 2019 +0000
     1.3 @@ -14,6 +14,9 @@
     1.4  * ASCII membership syntax concerning big operators for infimum
     1.5  and supremum is gone.  INCOMPATIBILITY.
     1.6  
     1.7 +* Clear distinction between types for bits (False / True) and
     1.8 +Z2 (0 / 1): theory HOL/Library/Bit.thy has been renamed accordingly.
     1.9 +INCOMPATIBILITY.
    1.10  
    1.11  
    1.12  New in Isabelle2019 (June 2019)
     2.1 --- a/src/HOL/Library/Bit.thy	Fri Jun 14 08:34:27 2019 +0000
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,174 +0,0 @@
     2.4 -(*  Title:      HOL/Library/Bit.thy
     2.5 -    Author:     Brian Huffman
     2.6 -*)
     2.7 -
     2.8 -section \<open>The Field of Integers mod 2\<close>
     2.9 -
    2.10 -theory Bit
    2.11 -imports Main
    2.12 -begin
    2.13 -
    2.14 -subsection \<open>Bits as a datatype\<close>
    2.15 -
    2.16 -typedef bit = "UNIV :: bool set"
    2.17 -  morphisms set Bit ..
    2.18 -
    2.19 -instantiation bit :: "{zero, one}"
    2.20 -begin
    2.21 -
    2.22 -definition zero_bit_def: "0 = Bit False"
    2.23 -
    2.24 -definition one_bit_def: "1 = Bit True"
    2.25 -
    2.26 -instance ..
    2.27 -
    2.28 -end
    2.29 -
    2.30 -old_rep_datatype "0::bit" "1::bit"
    2.31 -proof -
    2.32 -  fix P :: "bit \<Rightarrow> bool"
    2.33 -  fix x :: bit
    2.34 -  assume "P 0" and "P 1"
    2.35 -  then have "\<forall>b. P (Bit b)"
    2.36 -    unfolding zero_bit_def one_bit_def
    2.37 -    by (simp add: all_bool_eq)
    2.38 -  then show "P x"
    2.39 -    by (induct x) simp
    2.40 -next
    2.41 -  show "(0::bit) \<noteq> (1::bit)"
    2.42 -    unfolding zero_bit_def one_bit_def
    2.43 -    by (simp add: Bit_inject)
    2.44 -qed
    2.45 -
    2.46 -lemma Bit_set_eq [simp]: "Bit (set b) = b"
    2.47 -  by (fact set_inverse)
    2.48 -
    2.49 -lemma set_Bit_eq [simp]: "set (Bit P) = P"
    2.50 -  by (rule Bit_inverse) rule
    2.51 -
    2.52 -lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
    2.53 -  by (auto simp add: set_inject)
    2.54 -
    2.55 -lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
    2.56 -  by (auto simp add: Bit_inject)
    2.57 -
    2.58 -lemma set [iff]:
    2.59 -  "\<not> set 0"
    2.60 -  "set 1"
    2.61 -  by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
    2.62 -
    2.63 -lemma [code]:
    2.64 -  "set 0 \<longleftrightarrow> False"
    2.65 -  "set 1 \<longleftrightarrow> True"
    2.66 -  by simp_all
    2.67 -
    2.68 -lemma set_iff: "set b \<longleftrightarrow> b = 1"
    2.69 -  by (cases b) simp_all
    2.70 -
    2.71 -lemma bit_eq_iff_set:
    2.72 -  "b = 0 \<longleftrightarrow> \<not> set b"
    2.73 -  "b = 1 \<longleftrightarrow> set b"
    2.74 -  by (simp_all add: bit_eq_iff)
    2.75 -
    2.76 -lemma Bit [simp, code]:
    2.77 -  "Bit False = 0"
    2.78 -  "Bit True = 1"
    2.79 -  by (simp_all add: zero_bit_def one_bit_def)
    2.80 -
    2.81 -lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit
    2.82 -  by (simp add: bit_eq_iff)
    2.83 -
    2.84 -lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit
    2.85 -  by (simp add: bit_eq_iff)
    2.86 -
    2.87 -lemma [code]:
    2.88 -  "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
    2.89 -  "HOL.equal 1 b \<longleftrightarrow> set b"
    2.90 -  by (simp_all add: equal set_iff)
    2.91 -
    2.92 -
    2.93 -subsection \<open>Type \<^typ>\<open>bit\<close> forms a field\<close>
    2.94 -
    2.95 -instantiation bit :: field
    2.96 -begin
    2.97 -
    2.98 -definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x"
    2.99 -
   2.100 -definition times_bit_def: "x * y = case_bit 0 y x"
   2.101 -
   2.102 -definition uminus_bit_def [simp]: "- x = x" for x :: bit
   2.103 -
   2.104 -definition minus_bit_def [simp]: "x - y = x + y" for x y :: bit
   2.105 -
   2.106 -definition inverse_bit_def [simp]: "inverse x = x" for x :: bit
   2.107 -
   2.108 -definition divide_bit_def [simp]: "x div y = x * y" for x y :: bit
   2.109 -
   2.110 -lemmas field_bit_defs =
   2.111 -  plus_bit_def times_bit_def minus_bit_def uminus_bit_def
   2.112 -  divide_bit_def inverse_bit_def
   2.113 -
   2.114 -instance
   2.115 -  by standard (auto simp: field_bit_defs split: bit.split)
   2.116 -
   2.117 -end
   2.118 -
   2.119 -lemma bit_add_self: "x + x = 0" for x :: bit
   2.120 -  unfolding plus_bit_def by (simp split: bit.split)
   2.121 -
   2.122 -lemma bit_mult_eq_1_iff [simp]: "x * y = 1 \<longleftrightarrow> x = 1 \<and> y = 1" for x y :: bit
   2.123 -  unfolding times_bit_def by (simp split: bit.split)
   2.124 -
   2.125 -text \<open>Not sure whether the next two should be simp rules.\<close>
   2.126 -
   2.127 -lemma bit_add_eq_0_iff: "x + y = 0 \<longleftrightarrow> x = y" for x y :: bit
   2.128 -  unfolding plus_bit_def by (simp split: bit.split)
   2.129 -
   2.130 -lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit
   2.131 -  unfolding plus_bit_def by (simp split: bit.split)
   2.132 -
   2.133 -
   2.134 -subsection \<open>Numerals at type \<^typ>\<open>bit\<close>\<close>
   2.135 -
   2.136 -text \<open>All numerals reduce to either 0 or 1.\<close>
   2.137 -
   2.138 -lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
   2.139 -  by (simp only: uminus_bit_def)
   2.140 -
   2.141 -lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
   2.142 -  by (simp only: uminus_bit_def)
   2.143 -
   2.144 -lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   2.145 -  by (simp only: numeral_Bit0 bit_add_self)
   2.146 -
   2.147 -lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
   2.148 -  by (simp only: numeral_Bit1 bit_add_self add_0_left)
   2.149 -
   2.150 -
   2.151 -subsection \<open>Conversion from \<^typ>\<open>bit\<close>\<close>
   2.152 -
   2.153 -context zero_neq_one
   2.154 -begin
   2.155 -
   2.156 -definition of_bit :: "bit \<Rightarrow> 'a"
   2.157 -  where "of_bit b = case_bit 0 1 b"
   2.158 -
   2.159 -lemma of_bit_eq [simp, code]:
   2.160 -  "of_bit 0 = 0"
   2.161 -  "of_bit 1 = 1"
   2.162 -  by (simp_all add: of_bit_def)
   2.163 -
   2.164 -lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y"
   2.165 -  by (cases x) (cases y; simp)+
   2.166 -
   2.167 -end
   2.168 -
   2.169 -lemma (in semiring_1) of_nat_of_bit_eq: "of_nat (of_bit b) = of_bit b"
   2.170 -  by (cases b) simp_all
   2.171 -
   2.172 -lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b"
   2.173 -  by (cases b) simp_all
   2.174 -
   2.175 -hide_const (open) set
   2.176 -
   2.177 -end
     3.1 --- a/src/HOL/Library/Library.thy	Fri Jun 14 08:34:27 2019 +0000
     3.2 +++ b/src/HOL/Library/Library.thy	Fri Jun 14 08:34:27 2019 +0000
     3.3 @@ -4,7 +4,6 @@
     3.4    AList
     3.5    Adhoc_Overloading
     3.6    BigO
     3.7 -  Bit
     3.8    BNF_Axiomatization
     3.9    BNF_Corec
    3.10    Boolean_Algebra
    3.11 @@ -94,6 +93,7 @@
    3.12    Type_Length
    3.13    Uprod
    3.14    While_Combinator
    3.15 +  Z2
    3.16  begin
    3.17  end
    3.18  (*>*)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Z2.thy	Fri Jun 14 08:34:27 2019 +0000
     4.3 @@ -0,0 +1,180 @@
     4.4 +(*  Title:      HOL/Library/Z2.thy
     4.5 +    Author:     Brian Huffman
     4.6 +*)
     4.7 +
     4.8 +section \<open>The Field of Integers mod 2\<close>
     4.9 +
    4.10 +theory Z2
    4.11 +imports Main
    4.12 +begin
    4.13 +
    4.14 +text \<open>
    4.15 +  Note that in most cases \<^typ>\<open>bool\<close> is appropriate hen a binary type is needed; the
    4.16 +  type provided here, for historical reasons named \<guillemotright>bit\<guillemotleft>, is only needed if proper
    4.17 +  field operations are required.
    4.18 +\<close>
    4.19 +
    4.20 +subsection \<open>Bits as a datatype\<close>
    4.21 +
    4.22 +typedef bit = "UNIV :: bool set"
    4.23 +  morphisms set Bit ..
    4.24 +
    4.25 +instantiation bit :: "{zero, one}"
    4.26 +begin
    4.27 +
    4.28 +definition zero_bit_def: "0 = Bit False"
    4.29 +
    4.30 +definition one_bit_def: "1 = Bit True"
    4.31 +
    4.32 +instance ..
    4.33 +
    4.34 +end
    4.35 +
    4.36 +old_rep_datatype "0::bit" "1::bit"
    4.37 +proof -
    4.38 +  fix P :: "bit \<Rightarrow> bool"
    4.39 +  fix x :: bit
    4.40 +  assume "P 0" and "P 1"
    4.41 +  then have "\<forall>b. P (Bit b)"
    4.42 +    unfolding zero_bit_def one_bit_def
    4.43 +    by (simp add: all_bool_eq)
    4.44 +  then show "P x"
    4.45 +    by (induct x) simp
    4.46 +next
    4.47 +  show "(0::bit) \<noteq> (1::bit)"
    4.48 +    unfolding zero_bit_def one_bit_def
    4.49 +    by (simp add: Bit_inject)
    4.50 +qed
    4.51 +
    4.52 +lemma Bit_set_eq [simp]: "Bit (set b) = b"
    4.53 +  by (fact set_inverse)
    4.54 +
    4.55 +lemma set_Bit_eq [simp]: "set (Bit P) = P"
    4.56 +  by (rule Bit_inverse) rule
    4.57 +
    4.58 +lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
    4.59 +  by (auto simp add: set_inject)
    4.60 +
    4.61 +lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
    4.62 +  by (auto simp add: Bit_inject)
    4.63 +
    4.64 +lemma set [iff]:
    4.65 +  "\<not> set 0"
    4.66 +  "set 1"
    4.67 +  by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
    4.68 +
    4.69 +lemma [code]:
    4.70 +  "set 0 \<longleftrightarrow> False"
    4.71 +  "set 1 \<longleftrightarrow> True"
    4.72 +  by simp_all
    4.73 +
    4.74 +lemma set_iff: "set b \<longleftrightarrow> b = 1"
    4.75 +  by (cases b) simp_all
    4.76 +
    4.77 +lemma bit_eq_iff_set:
    4.78 +  "b = 0 \<longleftrightarrow> \<not> set b"
    4.79 +  "b = 1 \<longleftrightarrow> set b"
    4.80 +  by (simp_all add: bit_eq_iff)
    4.81 +
    4.82 +lemma Bit [simp, code]:
    4.83 +  "Bit False = 0"
    4.84 +  "Bit True = 1"
    4.85 +  by (simp_all add: zero_bit_def one_bit_def)
    4.86 +
    4.87 +lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit
    4.88 +  by (simp add: bit_eq_iff)
    4.89 +
    4.90 +lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit
    4.91 +  by (simp add: bit_eq_iff)
    4.92 +
    4.93 +lemma [code]:
    4.94 +  "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
    4.95 +  "HOL.equal 1 b \<longleftrightarrow> set b"
    4.96 +  by (simp_all add: equal set_iff)
    4.97 +
    4.98 +
    4.99 +subsection \<open>Type \<^typ>\<open>bit\<close> forms a field\<close>
   4.100 +
   4.101 +instantiation bit :: field
   4.102 +begin
   4.103 +
   4.104 +definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x"
   4.105 +
   4.106 +definition times_bit_def: "x * y = case_bit 0 y x"
   4.107 +
   4.108 +definition uminus_bit_def [simp]: "- x = x" for x :: bit
   4.109 +
   4.110 +definition minus_bit_def [simp]: "x - y = x + y" for x y :: bit
   4.111 +
   4.112 +definition inverse_bit_def [simp]: "inverse x = x" for x :: bit
   4.113 +
   4.114 +definition divide_bit_def [simp]: "x div y = x * y" for x y :: bit
   4.115 +
   4.116 +lemmas field_bit_defs =
   4.117 +  plus_bit_def times_bit_def minus_bit_def uminus_bit_def
   4.118 +  divide_bit_def inverse_bit_def
   4.119 +
   4.120 +instance
   4.121 +  by standard (auto simp: field_bit_defs split: bit.split)
   4.122 +
   4.123 +end
   4.124 +
   4.125 +lemma bit_add_self: "x + x = 0" for x :: bit
   4.126 +  unfolding plus_bit_def by (simp split: bit.split)
   4.127 +
   4.128 +lemma bit_mult_eq_1_iff [simp]: "x * y = 1 \<longleftrightarrow> x = 1 \<and> y = 1" for x y :: bit
   4.129 +  unfolding times_bit_def by (simp split: bit.split)
   4.130 +
   4.131 +text \<open>Not sure whether the next two should be simp rules.\<close>
   4.132 +
   4.133 +lemma bit_add_eq_0_iff: "x + y = 0 \<longleftrightarrow> x = y" for x y :: bit
   4.134 +  unfolding plus_bit_def by (simp split: bit.split)
   4.135 +
   4.136 +lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit
   4.137 +  unfolding plus_bit_def by (simp split: bit.split)
   4.138 +
   4.139 +
   4.140 +subsection \<open>Numerals at type \<^typ>\<open>bit\<close>\<close>
   4.141 +
   4.142 +text \<open>All numerals reduce to either 0 or 1.\<close>
   4.143 +
   4.144 +lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
   4.145 +  by (simp only: uminus_bit_def)
   4.146 +
   4.147 +lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
   4.148 +  by (simp only: uminus_bit_def)
   4.149 +
   4.150 +lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   4.151 +  by (simp only: numeral_Bit0 bit_add_self)
   4.152 +
   4.153 +lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
   4.154 +  by (simp only: numeral_Bit1 bit_add_self add_0_left)
   4.155 +
   4.156 +
   4.157 +subsection \<open>Conversion from \<^typ>\<open>bit\<close>\<close>
   4.158 +
   4.159 +context zero_neq_one
   4.160 +begin
   4.161 +
   4.162 +definition of_bit :: "bit \<Rightarrow> 'a"
   4.163 +  where "of_bit b = case_bit 0 1 b"
   4.164 +
   4.165 +lemma of_bit_eq [simp, code]:
   4.166 +  "of_bit 0 = 0"
   4.167 +  "of_bit 1 = 1"
   4.168 +  by (simp_all add: of_bit_def)
   4.169 +
   4.170 +lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y"
   4.171 +  by (cases x) (cases y; simp)+
   4.172 +
   4.173 +end
   4.174 +
   4.175 +lemma (in semiring_1) of_nat_of_bit_eq: "of_nat (of_bit b) = of_bit b"
   4.176 +  by (cases b) simp_all
   4.177 +
   4.178 +lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b"
   4.179 +  by (cases b) simp_all
   4.180 +
   4.181 +hide_const (open) set
   4.182 +
   4.183 +end
     5.1 --- a/src/HOL/Word/Bits_Bit.thy	Fri Jun 14 08:34:27 2019 +0000
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,89 +0,0 @@
     5.4 -(*  Title:      HOL/Word/Bits_Bit.thy
     5.5 -    Author:     Author: Brian Huffman, PSU and Gerwin Klein, NICTA
     5.6 -*)
     5.7 -
     5.8 -section \<open>Bit operations in $\cal Z_2$\<close>
     5.9 -
    5.10 -theory Bits_Bit
    5.11 -  imports Bits "HOL-Library.Bit"
    5.12 -begin
    5.13 -
    5.14 -instantiation bit :: bit_operations
    5.15 -begin
    5.16 -
    5.17 -primrec bitNOT_bit
    5.18 -  where
    5.19 -    "NOT 0 = (1::bit)"
    5.20 -  | "NOT 1 = (0::bit)"
    5.21 -
    5.22 -primrec bitAND_bit
    5.23 -  where
    5.24 -    "0 AND y = (0::bit)"
    5.25 -  | "1 AND y = (y::bit)"
    5.26 -
    5.27 -primrec bitOR_bit
    5.28 -  where
    5.29 -    "0 OR y = (y::bit)"
    5.30 -  | "1 OR y = (1::bit)"
    5.31 -
    5.32 -primrec bitXOR_bit
    5.33 -  where
    5.34 -    "0 XOR y = (y::bit)"
    5.35 -  | "1 XOR y = (NOT y :: bit)"
    5.36 -
    5.37 -instance  ..
    5.38 -
    5.39 -end
    5.40 -
    5.41 -lemmas bit_simps =
    5.42 -  bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
    5.43 -
    5.44 -lemma bit_extra_simps [simp]:
    5.45 -  "x AND 0 = 0"
    5.46 -  "x AND 1 = x"
    5.47 -  "x OR 1 = 1"
    5.48 -  "x OR 0 = x"
    5.49 -  "x XOR 1 = NOT x"
    5.50 -  "x XOR 0 = x"
    5.51 -  for x :: bit
    5.52 -  by (cases x; auto)+
    5.53 -
    5.54 -lemma bit_ops_comm:
    5.55 -  "x AND y = y AND x"
    5.56 -  "x OR y = y OR x"
    5.57 -  "x XOR y = y XOR x"
    5.58 -  for x :: bit
    5.59 -  by (cases y; auto)+
    5.60 -
    5.61 -lemma bit_ops_same [simp]:
    5.62 -  "x AND x = x"
    5.63 -  "x OR x = x"
    5.64 -  "x XOR x = 0"
    5.65 -  for x :: bit
    5.66 -  by (cases x; auto)+
    5.67 -
    5.68 -lemma bit_not_not [simp]: "NOT (NOT x) = x"
    5.69 -  for x :: bit
    5.70 -  by (cases x) auto
    5.71 -
    5.72 -lemma bit_or_def: "b OR c = NOT (NOT b AND NOT c)"
    5.73 -  for b c :: bit
    5.74 -  by (induct b) simp_all
    5.75 -
    5.76 -lemma bit_xor_def: "b XOR c = (b AND NOT c) OR (NOT b AND c)"
    5.77 -  for b c :: bit
    5.78 -  by (induct b) simp_all
    5.79 -
    5.80 -lemma bit_NOT_eq_1_iff [simp]: "NOT b = 1 \<longleftrightarrow> b = 0"
    5.81 -  for b :: bit
    5.82 -  by (induct b) simp_all
    5.83 -
    5.84 -lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
    5.85 -  for a b :: bit
    5.86 -  by (induct a) simp_all
    5.87 -
    5.88 -lemma bit_nand_same [simp]: "x AND NOT x = 0"
    5.89 -  for x :: bit
    5.90 -  by (cases x) simp_all
    5.91 -
    5.92 -end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Word/Bits_Z2.thy	Fri Jun 14 08:34:27 2019 +0000
     6.3 @@ -0,0 +1,89 @@
     6.4 +(*  Title:      HOL/Word/Bits_Z2.thy
     6.5 +    Author:     Author: Brian Huffman, PSU and Gerwin Klein, NICTA
     6.6 +*)
     6.7 +
     6.8 +section \<open>Bit operations in $\cal Z_2$\<close>
     6.9 +
    6.10 +theory Bits_Z2
    6.11 +  imports Bits "HOL-Library.Z2"
    6.12 +begin
    6.13 +
    6.14 +instantiation bit :: bit_operations
    6.15 +begin
    6.16 +
    6.17 +primrec bitNOT_bit
    6.18 +  where
    6.19 +    "NOT 0 = (1::bit)"
    6.20 +  | "NOT 1 = (0::bit)"
    6.21 +
    6.22 +primrec bitAND_bit
    6.23 +  where
    6.24 +    "0 AND y = (0::bit)"
    6.25 +  | "1 AND y = (y::bit)"
    6.26 +
    6.27 +primrec bitOR_bit
    6.28 +  where
    6.29 +    "0 OR y = (y::bit)"
    6.30 +  | "1 OR y = (1::bit)"
    6.31 +
    6.32 +primrec bitXOR_bit
    6.33 +  where
    6.34 +    "0 XOR y = (y::bit)"
    6.35 +  | "1 XOR y = (NOT y :: bit)"
    6.36 +
    6.37 +instance  ..
    6.38 +
    6.39 +end
    6.40 +
    6.41 +lemmas bit_simps =
    6.42 +  bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
    6.43 +
    6.44 +lemma bit_extra_simps [simp]:
    6.45 +  "x AND 0 = 0"
    6.46 +  "x AND 1 = x"
    6.47 +  "x OR 1 = 1"
    6.48 +  "x OR 0 = x"
    6.49 +  "x XOR 1 = NOT x"
    6.50 +  "x XOR 0 = x"
    6.51 +  for x :: bit
    6.52 +  by (cases x; auto)+
    6.53 +
    6.54 +lemma bit_ops_comm:
    6.55 +  "x AND y = y AND x"
    6.56 +  "x OR y = y OR x"
    6.57 +  "x XOR y = y XOR x"
    6.58 +  for x :: bit
    6.59 +  by (cases y; auto)+
    6.60 +
    6.61 +lemma bit_ops_same [simp]:
    6.62 +  "x AND x = x"
    6.63 +  "x OR x = x"
    6.64 +  "x XOR x = 0"
    6.65 +  for x :: bit
    6.66 +  by (cases x; auto)+
    6.67 +
    6.68 +lemma bit_not_not [simp]: "NOT (NOT x) = x"
    6.69 +  for x :: bit
    6.70 +  by (cases x) auto
    6.71 +
    6.72 +lemma bit_or_def: "b OR c = NOT (NOT b AND NOT c)"
    6.73 +  for b c :: bit
    6.74 +  by (induct b) simp_all
    6.75 +
    6.76 +lemma bit_xor_def: "b XOR c = (b AND NOT c) OR (NOT b AND c)"
    6.77 +  for b c :: bit
    6.78 +  by (induct b) simp_all
    6.79 +
    6.80 +lemma bit_NOT_eq_1_iff [simp]: "NOT b = 1 \<longleftrightarrow> b = 0"
    6.81 +  for b :: bit
    6.82 +  by (induct b) simp_all
    6.83 +
    6.84 +lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
    6.85 +  for a b :: bit
    6.86 +  by (induct a) simp_all
    6.87 +
    6.88 +lemma bit_nand_same [simp]: "x AND NOT x = 0"
    6.89 +  for x :: bit
    6.90 +  by (cases x) simp_all
    6.91 +
    6.92 +end
     7.1 --- a/src/HOL/Word/Misc_Arithmetic.thy	Fri Jun 14 08:34:27 2019 +0000
     7.2 +++ b/src/HOL/Word/Misc_Arithmetic.thy	Fri Jun 14 08:34:27 2019 +0000
     7.3 @@ -3,7 +3,7 @@
     7.4  section \<open>Miscellaneous lemmas, mostly for arithmetic\<close>
     7.5  
     7.6  theory Misc_Arithmetic
     7.7 -  imports Misc_Auxiliary "HOL-Library.Bit"
     7.8 +  imports Misc_Auxiliary "HOL-Library.Z2"
     7.9  begin
    7.10  
    7.11  lemma one_mod_exp_eq_one [simp]:
     8.1 --- a/src/HOL/Word/Word.thy	Fri Jun 14 08:34:27 2019 +0000
     8.2 +++ b/src/HOL/Word/Word.thy	Fri Jun 14 08:34:27 2019 +0000
     8.3 @@ -9,7 +9,7 @@
     8.4    "HOL-Library.Type_Length"
     8.5    "HOL-Library.Boolean_Algebra"
     8.6    Bits_Int
     8.7 -  Bits_Bit
     8.8 +  Bits_Z2
     8.9    Bit_Comprehension
    8.10    Misc_Typedef
    8.11    Misc_Arithmetic