clear separation of types for bits (False / True) and Z2 (0 / 1)
authorhaftmann
Fri, 14 Jun 2019 08:34:27 +0000
changeset 70527 e4d626692640
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
--- a/NEWS	Fri Jun 14 08:34:27 2019 +0000
+++ b/NEWS	Fri Jun 14 08:34:27 2019 +0000
@@ -14,6 +14,9 @@
 * ASCII membership syntax concerning big operators for infimum
 and supremum is gone.  INCOMPATIBILITY.
 
+* Clear distinction between types for bits (False / True) and
+Z2 (0 / 1): theory HOL/Library/Bit.thy has been renamed accordingly.
+INCOMPATIBILITY.
 
 
 New in Isabelle2019 (June 2019)
--- a/src/HOL/Library/Bit.thy	Fri Jun 14 08:34:27 2019 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,174 +0,0 @@
-(*  Title:      HOL/Library/Bit.thy
-    Author:     Brian Huffman
-*)
-
-section \<open>The Field of Integers mod 2\<close>
-
-theory Bit
-imports Main
-begin
-
-subsection \<open>Bits as a datatype\<close>
-
-typedef bit = "UNIV :: bool set"
-  morphisms set Bit ..
-
-instantiation bit :: "{zero, one}"
-begin
-
-definition zero_bit_def: "0 = Bit False"
-
-definition one_bit_def: "1 = Bit True"
-
-instance ..
-
-end
-
-old_rep_datatype "0::bit" "1::bit"
-proof -
-  fix P :: "bit \<Rightarrow> bool"
-  fix x :: bit
-  assume "P 0" and "P 1"
-  then have "\<forall>b. P (Bit b)"
-    unfolding zero_bit_def one_bit_def
-    by (simp add: all_bool_eq)
-  then show "P x"
-    by (induct x) simp
-next
-  show "(0::bit) \<noteq> (1::bit)"
-    unfolding zero_bit_def one_bit_def
-    by (simp add: Bit_inject)
-qed
-
-lemma Bit_set_eq [simp]: "Bit (set b) = b"
-  by (fact set_inverse)
-
-lemma set_Bit_eq [simp]: "set (Bit P) = P"
-  by (rule Bit_inverse) rule
-
-lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
-  by (auto simp add: set_inject)
-
-lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
-  by (auto simp add: Bit_inject)
-
-lemma set [iff]:
-  "\<not> set 0"
-  "set 1"
-  by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
-
-lemma [code]:
-  "set 0 \<longleftrightarrow> False"
-  "set 1 \<longleftrightarrow> True"
-  by simp_all
-
-lemma set_iff: "set b \<longleftrightarrow> b = 1"
-  by (cases b) simp_all
-
-lemma bit_eq_iff_set:
-  "b = 0 \<longleftrightarrow> \<not> set b"
-  "b = 1 \<longleftrightarrow> set b"
-  by (simp_all add: bit_eq_iff)
-
-lemma Bit [simp, code]:
-  "Bit False = 0"
-  "Bit True = 1"
-  by (simp_all add: zero_bit_def one_bit_def)
-
-lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit
-  by (simp add: bit_eq_iff)
-
-lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit
-  by (simp add: bit_eq_iff)
-
-lemma [code]:
-  "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
-  "HOL.equal 1 b \<longleftrightarrow> set b"
-  by (simp_all add: equal set_iff)
-
-
-subsection \<open>Type \<^typ>\<open>bit\<close> forms a field\<close>
-
-instantiation bit :: field
-begin
-
-definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x"
-
-definition times_bit_def: "x * y = case_bit 0 y x"
-
-definition uminus_bit_def [simp]: "- x = x" for x :: bit
-
-definition minus_bit_def [simp]: "x - y = x + y" for x y :: bit
-
-definition inverse_bit_def [simp]: "inverse x = x" for x :: bit
-
-definition divide_bit_def [simp]: "x div y = x * y" for x y :: bit
-
-lemmas field_bit_defs =
-  plus_bit_def times_bit_def minus_bit_def uminus_bit_def
-  divide_bit_def inverse_bit_def
-
-instance
-  by standard (auto simp: field_bit_defs split: bit.split)
-
-end
-
-lemma bit_add_self: "x + x = 0" for x :: bit
-  unfolding plus_bit_def by (simp split: bit.split)
-
-lemma bit_mult_eq_1_iff [simp]: "x * y = 1 \<longleftrightarrow> x = 1 \<and> y = 1" for x y :: bit
-  unfolding times_bit_def by (simp split: bit.split)
-
-text \<open>Not sure whether the next two should be simp rules.\<close>
-
-lemma bit_add_eq_0_iff: "x + y = 0 \<longleftrightarrow> x = y" for x y :: bit
-  unfolding plus_bit_def by (simp split: bit.split)
-
-lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit
-  unfolding plus_bit_def by (simp split: bit.split)
-
-
-subsection \<open>Numerals at type \<^typ>\<open>bit\<close>\<close>
-
-text \<open>All numerals reduce to either 0 or 1.\<close>
-
-lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
-  by (simp only: uminus_bit_def)
-
-lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
-  by (simp only: uminus_bit_def)
-
-lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
-  by (simp only: numeral_Bit0 bit_add_self)
-
-lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
-  by (simp only: numeral_Bit1 bit_add_self add_0_left)
-
-
-subsection \<open>Conversion from \<^typ>\<open>bit\<close>\<close>
-
-context zero_neq_one
-begin
-
-definition of_bit :: "bit \<Rightarrow> 'a"
-  where "of_bit b = case_bit 0 1 b"
-
-lemma of_bit_eq [simp, code]:
-  "of_bit 0 = 0"
-  "of_bit 1 = 1"
-  by (simp_all add: of_bit_def)
-
-lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y"
-  by (cases x) (cases y; simp)+
-
-end
-
-lemma (in semiring_1) of_nat_of_bit_eq: "of_nat (of_bit b) = of_bit b"
-  by (cases b) simp_all
-
-lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b"
-  by (cases b) simp_all
-
-hide_const (open) set
-
-end
--- a/src/HOL/Library/Library.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Library/Library.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -4,7 +4,6 @@
   AList
   Adhoc_Overloading
   BigO
-  Bit
   BNF_Axiomatization
   BNF_Corec
   Boolean_Algebra
@@ -94,6 +93,7 @@
   Type_Length
   Uprod
   While_Combinator
+  Z2
 begin
 end
 (*>*)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Z2.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -0,0 +1,180 @@
+(*  Title:      HOL/Library/Z2.thy
+    Author:     Brian Huffman
+*)
+
+section \<open>The Field of Integers mod 2\<close>
+
+theory Z2
+imports Main
+begin
+
+text \<open>
+  Note that in most cases \<^typ>\<open>bool\<close> is appropriate hen a binary type is needed; the
+  type provided here, for historical reasons named \<guillemotright>bit\<guillemotleft>, is only needed if proper
+  field operations are required.
+\<close>
+
+subsection \<open>Bits as a datatype\<close>
+
+typedef bit = "UNIV :: bool set"
+  morphisms set Bit ..
+
+instantiation bit :: "{zero, one}"
+begin
+
+definition zero_bit_def: "0 = Bit False"
+
+definition one_bit_def: "1 = Bit True"
+
+instance ..
+
+end
+
+old_rep_datatype "0::bit" "1::bit"
+proof -
+  fix P :: "bit \<Rightarrow> bool"
+  fix x :: bit
+  assume "P 0" and "P 1"
+  then have "\<forall>b. P (Bit b)"
+    unfolding zero_bit_def one_bit_def
+    by (simp add: all_bool_eq)
+  then show "P x"
+    by (induct x) simp
+next
+  show "(0::bit) \<noteq> (1::bit)"
+    unfolding zero_bit_def one_bit_def
+    by (simp add: Bit_inject)
+qed
+
+lemma Bit_set_eq [simp]: "Bit (set b) = b"
+  by (fact set_inverse)
+
+lemma set_Bit_eq [simp]: "set (Bit P) = P"
+  by (rule Bit_inverse) rule
+
+lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
+  by (auto simp add: set_inject)
+
+lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
+  by (auto simp add: Bit_inject)
+
+lemma set [iff]:
+  "\<not> set 0"
+  "set 1"
+  by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
+
+lemma [code]:
+  "set 0 \<longleftrightarrow> False"
+  "set 1 \<longleftrightarrow> True"
+  by simp_all
+
+lemma set_iff: "set b \<longleftrightarrow> b = 1"
+  by (cases b) simp_all
+
+lemma bit_eq_iff_set:
+  "b = 0 \<longleftrightarrow> \<not> set b"
+  "b = 1 \<longleftrightarrow> set b"
+  by (simp_all add: bit_eq_iff)
+
+lemma Bit [simp, code]:
+  "Bit False = 0"
+  "Bit True = 1"
+  by (simp_all add: zero_bit_def one_bit_def)
+
+lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit
+  by (simp add: bit_eq_iff)
+
+lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit
+  by (simp add: bit_eq_iff)
+
+lemma [code]:
+  "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
+  "HOL.equal 1 b \<longleftrightarrow> set b"
+  by (simp_all add: equal set_iff)
+
+
+subsection \<open>Type \<^typ>\<open>bit\<close> forms a field\<close>
+
+instantiation bit :: field
+begin
+
+definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x"
+
+definition times_bit_def: "x * y = case_bit 0 y x"
+
+definition uminus_bit_def [simp]: "- x = x" for x :: bit
+
+definition minus_bit_def [simp]: "x - y = x + y" for x y :: bit
+
+definition inverse_bit_def [simp]: "inverse x = x" for x :: bit
+
+definition divide_bit_def [simp]: "x div y = x * y" for x y :: bit
+
+lemmas field_bit_defs =
+  plus_bit_def times_bit_def minus_bit_def uminus_bit_def
+  divide_bit_def inverse_bit_def
+
+instance
+  by standard (auto simp: field_bit_defs split: bit.split)
+
+end
+
+lemma bit_add_self: "x + x = 0" for x :: bit
+  unfolding plus_bit_def by (simp split: bit.split)
+
+lemma bit_mult_eq_1_iff [simp]: "x * y = 1 \<longleftrightarrow> x = 1 \<and> y = 1" for x y :: bit
+  unfolding times_bit_def by (simp split: bit.split)
+
+text \<open>Not sure whether the next two should be simp rules.\<close>
+
+lemma bit_add_eq_0_iff: "x + y = 0 \<longleftrightarrow> x = y" for x y :: bit
+  unfolding plus_bit_def by (simp split: bit.split)
+
+lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit
+  unfolding plus_bit_def by (simp split: bit.split)
+
+
+subsection \<open>Numerals at type \<^typ>\<open>bit\<close>\<close>
+
+text \<open>All numerals reduce to either 0 or 1.\<close>
+
+lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
+  by (simp only: uminus_bit_def)
+
+lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
+  by (simp only: uminus_bit_def)
+
+lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
+  by (simp only: numeral_Bit0 bit_add_self)
+
+lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
+  by (simp only: numeral_Bit1 bit_add_self add_0_left)
+
+
+subsection \<open>Conversion from \<^typ>\<open>bit\<close>\<close>
+
+context zero_neq_one
+begin
+
+definition of_bit :: "bit \<Rightarrow> 'a"
+  where "of_bit b = case_bit 0 1 b"
+
+lemma of_bit_eq [simp, code]:
+  "of_bit 0 = 0"
+  "of_bit 1 = 1"
+  by (simp_all add: of_bit_def)
+
+lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y"
+  by (cases x) (cases y; simp)+
+
+end
+
+lemma (in semiring_1) of_nat_of_bit_eq: "of_nat (of_bit b) = of_bit b"
+  by (cases b) simp_all
+
+lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b"
+  by (cases b) simp_all
+
+hide_const (open) set
+
+end
--- a/src/HOL/Word/Bits_Bit.thy	Fri Jun 14 08:34:27 2019 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,89 +0,0 @@
-(*  Title:      HOL/Word/Bits_Bit.thy
-    Author:     Author: Brian Huffman, PSU and Gerwin Klein, NICTA
-*)
-
-section \<open>Bit operations in $\cal Z_2$\<close>
-
-theory Bits_Bit
-  imports Bits "HOL-Library.Bit"
-begin
-
-instantiation bit :: bit_operations
-begin
-
-primrec bitNOT_bit
-  where
-    "NOT 0 = (1::bit)"
-  | "NOT 1 = (0::bit)"
-
-primrec bitAND_bit
-  where
-    "0 AND y = (0::bit)"
-  | "1 AND y = (y::bit)"
-
-primrec bitOR_bit
-  where
-    "0 OR y = (y::bit)"
-  | "1 OR y = (1::bit)"
-
-primrec bitXOR_bit
-  where
-    "0 XOR y = (y::bit)"
-  | "1 XOR y = (NOT y :: bit)"
-
-instance  ..
-
-end
-
-lemmas bit_simps =
-  bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
-
-lemma bit_extra_simps [simp]:
-  "x AND 0 = 0"
-  "x AND 1 = x"
-  "x OR 1 = 1"
-  "x OR 0 = x"
-  "x XOR 1 = NOT x"
-  "x XOR 0 = x"
-  for x :: bit
-  by (cases x; auto)+
-
-lemma bit_ops_comm:
-  "x AND y = y AND x"
-  "x OR y = y OR x"
-  "x XOR y = y XOR x"
-  for x :: bit
-  by (cases y; auto)+
-
-lemma bit_ops_same [simp]:
-  "x AND x = x"
-  "x OR x = x"
-  "x XOR x = 0"
-  for x :: bit
-  by (cases x; auto)+
-
-lemma bit_not_not [simp]: "NOT (NOT x) = x"
-  for x :: bit
-  by (cases x) auto
-
-lemma bit_or_def: "b OR c = NOT (NOT b AND NOT c)"
-  for b c :: bit
-  by (induct b) simp_all
-
-lemma bit_xor_def: "b XOR c = (b AND NOT c) OR (NOT b AND c)"
-  for b c :: bit
-  by (induct b) simp_all
-
-lemma bit_NOT_eq_1_iff [simp]: "NOT b = 1 \<longleftrightarrow> b = 0"
-  for b :: bit
-  by (induct b) simp_all
-
-lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
-  for a b :: bit
-  by (induct a) simp_all
-
-lemma bit_nand_same [simp]: "x AND NOT x = 0"
-  for x :: bit
-  by (cases x) simp_all
-
-end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Bits_Z2.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -0,0 +1,89 @@
+(*  Title:      HOL/Word/Bits_Z2.thy
+    Author:     Author: Brian Huffman, PSU and Gerwin Klein, NICTA
+*)
+
+section \<open>Bit operations in $\cal Z_2$\<close>
+
+theory Bits_Z2
+  imports Bits "HOL-Library.Z2"
+begin
+
+instantiation bit :: bit_operations
+begin
+
+primrec bitNOT_bit
+  where
+    "NOT 0 = (1::bit)"
+  | "NOT 1 = (0::bit)"
+
+primrec bitAND_bit
+  where
+    "0 AND y = (0::bit)"
+  | "1 AND y = (y::bit)"
+
+primrec bitOR_bit
+  where
+    "0 OR y = (y::bit)"
+  | "1 OR y = (1::bit)"
+
+primrec bitXOR_bit
+  where
+    "0 XOR y = (y::bit)"
+  | "1 XOR y = (NOT y :: bit)"
+
+instance  ..
+
+end
+
+lemmas bit_simps =
+  bitNOT_bit.simps bitAND_bit.simps bitOR_bit.simps bitXOR_bit.simps
+
+lemma bit_extra_simps [simp]:
+  "x AND 0 = 0"
+  "x AND 1 = x"
+  "x OR 1 = 1"
+  "x OR 0 = x"
+  "x XOR 1 = NOT x"
+  "x XOR 0 = x"
+  for x :: bit
+  by (cases x; auto)+
+
+lemma bit_ops_comm:
+  "x AND y = y AND x"
+  "x OR y = y OR x"
+  "x XOR y = y XOR x"
+  for x :: bit
+  by (cases y; auto)+
+
+lemma bit_ops_same [simp]:
+  "x AND x = x"
+  "x OR x = x"
+  "x XOR x = 0"
+  for x :: bit
+  by (cases x; auto)+
+
+lemma bit_not_not [simp]: "NOT (NOT x) = x"
+  for x :: bit
+  by (cases x) auto
+
+lemma bit_or_def: "b OR c = NOT (NOT b AND NOT c)"
+  for b c :: bit
+  by (induct b) simp_all
+
+lemma bit_xor_def: "b XOR c = (b AND NOT c) OR (NOT b AND c)"
+  for b c :: bit
+  by (induct b) simp_all
+
+lemma bit_NOT_eq_1_iff [simp]: "NOT b = 1 \<longleftrightarrow> b = 0"
+  for b :: bit
+  by (induct b) simp_all
+
+lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
+  for a b :: bit
+  by (induct a) simp_all
+
+lemma bit_nand_same [simp]: "x AND NOT x = 0"
+  for x :: bit
+  by (cases x) simp_all
+
+end
--- a/src/HOL/Word/Misc_Arithmetic.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Word/Misc_Arithmetic.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -3,7 +3,7 @@
 section \<open>Miscellaneous lemmas, mostly for arithmetic\<close>
 
 theory Misc_Arithmetic
-  imports Misc_Auxiliary "HOL-Library.Bit"
+  imports Misc_Auxiliary "HOL-Library.Z2"
 begin
 
 lemma one_mod_exp_eq_one [simp]:
--- a/src/HOL/Word/Word.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Word/Word.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -9,7 +9,7 @@
   "HOL-Library.Type_Length"
   "HOL-Library.Boolean_Algebra"
   Bits_Int
-  Bits_Bit
+  Bits_Z2
   Bit_Comprehension
   Misc_Typedef
   Misc_Arithmetic