src/HOL/Library/Z2.thy
changeset 70342 e4d626692640
parent 69593 3dda49e08b9d
child 70351 32b4e1aec5ca
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Z2.thy	Fri Jun 14 08:34:27 2019 +0000
     1.3 @@ -0,0 +1,180 @@
     1.4 +(*  Title:      HOL/Library/Z2.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +section \<open>The Field of Integers mod 2\<close>
     1.9 +
    1.10 +theory Z2
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +text \<open>
    1.15 +  Note that in most cases \<^typ>\<open>bool\<close> is appropriate hen a binary type is needed; the
    1.16 +  type provided here, for historical reasons named \<guillemotright>bit\<guillemotleft>, is only needed if proper
    1.17 +  field operations are required.
    1.18 +\<close>
    1.19 +
    1.20 +subsection \<open>Bits as a datatype\<close>
    1.21 +
    1.22 +typedef bit = "UNIV :: bool set"
    1.23 +  morphisms set Bit ..
    1.24 +
    1.25 +instantiation bit :: "{zero, one}"
    1.26 +begin
    1.27 +
    1.28 +definition zero_bit_def: "0 = Bit False"
    1.29 +
    1.30 +definition one_bit_def: "1 = Bit True"
    1.31 +
    1.32 +instance ..
    1.33 +
    1.34 +end
    1.35 +
    1.36 +old_rep_datatype "0::bit" "1::bit"
    1.37 +proof -
    1.38 +  fix P :: "bit \<Rightarrow> bool"
    1.39 +  fix x :: bit
    1.40 +  assume "P 0" and "P 1"
    1.41 +  then have "\<forall>b. P (Bit b)"
    1.42 +    unfolding zero_bit_def one_bit_def
    1.43 +    by (simp add: all_bool_eq)
    1.44 +  then show "P x"
    1.45 +    by (induct x) simp
    1.46 +next
    1.47 +  show "(0::bit) \<noteq> (1::bit)"
    1.48 +    unfolding zero_bit_def one_bit_def
    1.49 +    by (simp add: Bit_inject)
    1.50 +qed
    1.51 +
    1.52 +lemma Bit_set_eq [simp]: "Bit (set b) = b"
    1.53 +  by (fact set_inverse)
    1.54 +
    1.55 +lemma set_Bit_eq [simp]: "set (Bit P) = P"
    1.56 +  by (rule Bit_inverse) rule
    1.57 +
    1.58 +lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
    1.59 +  by (auto simp add: set_inject)
    1.60 +
    1.61 +lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
    1.62 +  by (auto simp add: Bit_inject)
    1.63 +
    1.64 +lemma set [iff]:
    1.65 +  "\<not> set 0"
    1.66 +  "set 1"
    1.67 +  by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
    1.68 +
    1.69 +lemma [code]:
    1.70 +  "set 0 \<longleftrightarrow> False"
    1.71 +  "set 1 \<longleftrightarrow> True"
    1.72 +  by simp_all
    1.73 +
    1.74 +lemma set_iff: "set b \<longleftrightarrow> b = 1"
    1.75 +  by (cases b) simp_all
    1.76 +
    1.77 +lemma bit_eq_iff_set:
    1.78 +  "b = 0 \<longleftrightarrow> \<not> set b"
    1.79 +  "b = 1 \<longleftrightarrow> set b"
    1.80 +  by (simp_all add: bit_eq_iff)
    1.81 +
    1.82 +lemma Bit [simp, code]:
    1.83 +  "Bit False = 0"
    1.84 +  "Bit True = 1"
    1.85 +  by (simp_all add: zero_bit_def one_bit_def)
    1.86 +
    1.87 +lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit
    1.88 +  by (simp add: bit_eq_iff)
    1.89 +
    1.90 +lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit
    1.91 +  by (simp add: bit_eq_iff)
    1.92 +
    1.93 +lemma [code]:
    1.94 +  "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
    1.95 +  "HOL.equal 1 b \<longleftrightarrow> set b"
    1.96 +  by (simp_all add: equal set_iff)
    1.97 +
    1.98 +
    1.99 +subsection \<open>Type \<^typ>\<open>bit\<close> forms a field\<close>
   1.100 +
   1.101 +instantiation bit :: field
   1.102 +begin
   1.103 +
   1.104 +definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x"
   1.105 +
   1.106 +definition times_bit_def: "x * y = case_bit 0 y x"
   1.107 +
   1.108 +definition uminus_bit_def [simp]: "- x = x" for x :: bit
   1.109 +
   1.110 +definition minus_bit_def [simp]: "x - y = x + y" for x y :: bit
   1.111 +
   1.112 +definition inverse_bit_def [simp]: "inverse x = x" for x :: bit
   1.113 +
   1.114 +definition divide_bit_def [simp]: "x div y = x * y" for x y :: bit
   1.115 +
   1.116 +lemmas field_bit_defs =
   1.117 +  plus_bit_def times_bit_def minus_bit_def uminus_bit_def
   1.118 +  divide_bit_def inverse_bit_def
   1.119 +
   1.120 +instance
   1.121 +  by standard (auto simp: field_bit_defs split: bit.split)
   1.122 +
   1.123 +end
   1.124 +
   1.125 +lemma bit_add_self: "x + x = 0" for x :: bit
   1.126 +  unfolding plus_bit_def by (simp split: bit.split)
   1.127 +
   1.128 +lemma bit_mult_eq_1_iff [simp]: "x * y = 1 \<longleftrightarrow> x = 1 \<and> y = 1" for x y :: bit
   1.129 +  unfolding times_bit_def by (simp split: bit.split)
   1.130 +
   1.131 +text \<open>Not sure whether the next two should be simp rules.\<close>
   1.132 +
   1.133 +lemma bit_add_eq_0_iff: "x + y = 0 \<longleftrightarrow> x = y" for x y :: bit
   1.134 +  unfolding plus_bit_def by (simp split: bit.split)
   1.135 +
   1.136 +lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit
   1.137 +  unfolding plus_bit_def by (simp split: bit.split)
   1.138 +
   1.139 +
   1.140 +subsection \<open>Numerals at type \<^typ>\<open>bit\<close>\<close>
   1.141 +
   1.142 +text \<open>All numerals reduce to either 0 or 1.\<close>
   1.143 +
   1.144 +lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
   1.145 +  by (simp only: uminus_bit_def)
   1.146 +
   1.147 +lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
   1.148 +  by (simp only: uminus_bit_def)
   1.149 +
   1.150 +lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   1.151 +  by (simp only: numeral_Bit0 bit_add_self)
   1.152 +
   1.153 +lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
   1.154 +  by (simp only: numeral_Bit1 bit_add_self add_0_left)
   1.155 +
   1.156 +
   1.157 +subsection \<open>Conversion from \<^typ>\<open>bit\<close>\<close>
   1.158 +
   1.159 +context zero_neq_one
   1.160 +begin
   1.161 +
   1.162 +definition of_bit :: "bit \<Rightarrow> 'a"
   1.163 +  where "of_bit b = case_bit 0 1 b"
   1.164 +
   1.165 +lemma of_bit_eq [simp, code]:
   1.166 +  "of_bit 0 = 0"
   1.167 +  "of_bit 1 = 1"
   1.168 +  by (simp_all add: of_bit_def)
   1.169 +
   1.170 +lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y"
   1.171 +  by (cases x) (cases y; simp)+
   1.172 +
   1.173 +end
   1.174 +
   1.175 +lemma (in semiring_1) of_nat_of_bit_eq: "of_nat (of_bit b) = of_bit b"
   1.176 +  by (cases b) simp_all
   1.177 +
   1.178 +lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b"
   1.179 +  by (cases b) simp_all
   1.180 +
   1.181 +hide_const (open) set
   1.182 +
   1.183 +end