# HG changeset patch # User haftmann # Date 1560501267 0 # Node ID e4d626692640452c2ff3314b8f66d81b141ef04e # Parent 972c0c744e7ca19ca2a6c7bc4b8056814e23ecb6 clear separation of types for bits (False / True) and Z2 (0 / 1) diff -r 972c0c744e7c -r e4d626692640 NEWS --- 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) diff -r 972c0c744e7c -r e4d626692640 src/HOL/Library/Bit.thy --- 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 \The Field of Integers mod 2\ - -theory Bit -imports Main -begin - -subsection \Bits as a datatype\ - -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 \ bool" - fix x :: bit - assume "P 0" and "P 1" - then have "\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) \ (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 \ (set x \ set y)" - by (auto simp add: set_inject) - -lemma Bit_inject [simp]: "Bit P = Bit Q \ (P \ Q)" - by (auto simp add: Bit_inject) - -lemma set [iff]: - "\ set 0" - "set 1" - by (simp_all add: zero_bit_def one_bit_def Bit_inverse) - -lemma [code]: - "set 0 \ False" - "set 1 \ True" - by simp_all - -lemma set_iff: "set b \ b = 1" - by (cases b) simp_all - -lemma bit_eq_iff_set: - "b = 0 \ \ set b" - "b = 1 \ 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 \ 0 \ x = 1" for x :: bit - by (simp add: bit_eq_iff) - -lemma bit_not_1_iff [iff]: "x \ 1 \ x = 0" for x :: bit - by (simp add: bit_eq_iff) - -lemma [code]: - "HOL.equal 0 b \ \ set b" - "HOL.equal 1 b \ set b" - by (simp_all add: equal set_iff) - - -subsection \Type \<^typ>\bit\ forms a field\ - -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 \ x = 1 \ y = 1" for x y :: bit - unfolding times_bit_def by (simp split: bit.split) - -text \Not sure whether the next two should be simp rules.\ - -lemma bit_add_eq_0_iff: "x + y = 0 \ x = y" for x y :: bit - unfolding plus_bit_def by (simp split: bit.split) - -lemma bit_add_eq_1_iff: "x + y = 1 \ x \ y" for x y :: bit - unfolding plus_bit_def by (simp split: bit.split) - - -subsection \Numerals at type \<^typ>\bit\\ - -text \All numerals reduce to either 0 or 1.\ - -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 \Conversion from \<^typ>\bit\\ - -context zero_neq_one -begin - -definition of_bit :: "bit \ '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 \ 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 diff -r 972c0c744e7c -r e4d626692640 src/HOL/Library/Library.thy --- 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 (*>*) diff -r 972c0c744e7c -r e4d626692640 src/HOL/Library/Z2.thy --- /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 \The Field of Integers mod 2\ + +theory Z2 +imports Main +begin + +text \ + Note that in most cases \<^typ>\bool\ is appropriate hen a binary type is needed; the + type provided here, for historical reasons named \bit\, is only needed if proper + field operations are required. +\ + +subsection \Bits as a datatype\ + +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 \ bool" + fix x :: bit + assume "P 0" and "P 1" + then have "\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) \ (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 \ (set x \ set y)" + by (auto simp add: set_inject) + +lemma Bit_inject [simp]: "Bit P = Bit Q \ (P \ Q)" + by (auto simp add: Bit_inject) + +lemma set [iff]: + "\ set 0" + "set 1" + by (simp_all add: zero_bit_def one_bit_def Bit_inverse) + +lemma [code]: + "set 0 \ False" + "set 1 \ True" + by simp_all + +lemma set_iff: "set b \ b = 1" + by (cases b) simp_all + +lemma bit_eq_iff_set: + "b = 0 \ \ set b" + "b = 1 \ 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 \ 0 \ x = 1" for x :: bit + by (simp add: bit_eq_iff) + +lemma bit_not_1_iff [iff]: "x \ 1 \ x = 0" for x :: bit + by (simp add: bit_eq_iff) + +lemma [code]: + "HOL.equal 0 b \ \ set b" + "HOL.equal 1 b \ set b" + by (simp_all add: equal set_iff) + + +subsection \Type \<^typ>\bit\ forms a field\ + +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 \ x = 1 \ y = 1" for x y :: bit + unfolding times_bit_def by (simp split: bit.split) + +text \Not sure whether the next two should be simp rules.\ + +lemma bit_add_eq_0_iff: "x + y = 0 \ x = y" for x y :: bit + unfolding plus_bit_def by (simp split: bit.split) + +lemma bit_add_eq_1_iff: "x + y = 1 \ x \ y" for x y :: bit + unfolding plus_bit_def by (simp split: bit.split) + + +subsection \Numerals at type \<^typ>\bit\\ + +text \All numerals reduce to either 0 or 1.\ + +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 \Conversion from \<^typ>\bit\\ + +context zero_neq_one +begin + +definition of_bit :: "bit \ '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 \ 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 diff -r 972c0c744e7c -r e4d626692640 src/HOL/Word/Bits_Bit.thy --- 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 \Bit operations in $\cal Z_2$\ - -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 \ b = 0" - for b :: bit - by (induct b) simp_all - -lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \ a = 1 \ 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 diff -r 972c0c744e7c -r e4d626692640 src/HOL/Word/Bits_Z2.thy --- /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 \Bit operations in $\cal Z_2$\ + +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 \ b = 0" + for b :: bit + by (induct b) simp_all + +lemma bit_AND_eq_1_iff [simp]: "a AND b = 1 \ a = 1 \ 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 diff -r 972c0c744e7c -r e4d626692640 src/HOL/Word/Misc_Arithmetic.thy --- 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 \Miscellaneous lemmas, mostly for arithmetic\ theory Misc_Arithmetic - imports Misc_Auxiliary "HOL-Library.Bit" + imports Misc_Auxiliary "HOL-Library.Z2" begin lemma one_mod_exp_eq_one [simp]: diff -r 972c0c744e7c -r e4d626692640 src/HOL/Word/Word.thy --- 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