src/HOL/Library/Bit.thy
 changeset 29994 6ca6b6bd6e15 child 29995 62efbd0ef132
equal inserted replaced
29993:84b2c432b94a 29994:6ca6b6bd6e15
`       `
`     1 (* Title:      Bit.thy`
`       `
`     2    Author:     Brian Huffman`
`       `
`     3 *)`
`       `
`     4 `
`       `
`     5 header {* The Field of Integers mod 2 *}`
`       `
`     6 `
`       `
`     7 theory Bit`
`       `
`     8 imports Main`
`       `
`     9 begin`
`       `
`    10 `
`       `
`    11 subsection {* Bits as a datatype *}`
`       `
`    12 `
`       `
`    13 typedef (open) bit = "UNIV :: bool set" ..`
`       `
`    14 `
`       `
`    15 instantiation bit :: "{zero, one}"`
`       `
`    16 begin`
`       `
`    17 `
`       `
`    18 definition zero_bit_def:`
`       `
`    19   "0 = Abs_bit False"`
`       `
`    20 `
`       `
`    21 definition one_bit_def:`
`       `
`    22   "1 = Abs_bit True"`
`       `
`    23 `
`       `
`    24 instance ..`
`       `
`    25 `
`       `
`    26 end`
`       `
`    27 `
`       `
`    28 rep_datatype (bit) "0::bit" "1::bit"`
`       `
`    29 proof -`
`       `
`    30   fix P and x :: bit`
`       `
`    31   assume "P (0::bit)" and "P (1::bit)"`
`       `
`    32   then have "\<forall>b. P (Abs_bit b)"`
`       `
`    33     unfolding zero_bit_def one_bit_def`
`       `
`    34     by (simp add: all_bool_eq)`
`       `
`    35   then show "P x"`
`       `
`    36     by (induct x) simp`
`       `
`    37 next`
`       `
`    38   show "(0::bit) \<noteq> (1::bit)"`
`       `
`    39     unfolding zero_bit_def one_bit_def`
`       `
`    40     by (simp add: Abs_bit_inject)`
`       `
`    41 qed`
`       `
`    42 `
`       `
`    43 lemma bit_not_0_iff [iff]: "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"`
`       `
`    44   by (induct x) simp_all`
`       `
`    45 `
`       `
`    46 lemma bit_not_1_iff [iff]: "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"`
`       `
`    47   by (induct x) simp_all`
`       `
`    48 `
`       `
`    49 `
`       `
`    50 subsection {* Type @{typ bit} forms a field *}`
`       `
`    51 `
`       `
`    52 instantiation bit :: "{field, division_by_zero}"`
`       `
`    53 begin`
`       `
`    54 `
`       `
`    55 definition plus_bit_def:`
`       `
`    56   "x + y = (case x of 0 \<Rightarrow> y | 1 \<Rightarrow> (case y of 0 \<Rightarrow> 1 | 1 \<Rightarrow> 0))"`
`       `
`    57 `
`       `
`    58 definition times_bit_def:`
`       `
`    59   "x * y = (case x of 0 \<Rightarrow> 0 | 1 \<Rightarrow> y)"`
`       `
`    60 `
`       `
`    61 definition uminus_bit_def [simp]:`
`       `
`    62   "- x = (x :: bit)"`
`       `
`    63 `
`       `
`    64 definition minus_bit_def [simp]:`
`       `
`    65   "x - y = (x + y :: bit)"`
`       `
`    66 `
`       `
`    67 definition inverse_bit_def [simp]:`
`       `
`    68   "inverse x = (x :: bit)"`
`       `
`    69 `
`       `
`    70 definition divide_bit_def [simp]:`
`       `
`    71   "x / y = (x * y :: bit)"`
`       `
`    72 `
`       `
`    73 lemmas field_bit_defs =`
`       `
`    74   plus_bit_def times_bit_def minus_bit_def uminus_bit_def`
`       `
`    75   divide_bit_def inverse_bit_def`
`       `
`    76 `
`       `
`    77 instance proof`
`       `
`    78 qed (unfold field_bit_defs, auto split: bit.split)`
`       `
`    79 `
`       `
`    80 end`
`       `
`    81 `
`       `
`    82 lemma bit_1_plus_1 [simp]: "1 + 1 = (0 :: bit)"`
`       `
`    83   unfolding plus_bit_def by simp`
`       `
`    84 `
`       `
`    85 lemma bit_add_self [simp]: "x + x = (0 :: bit)"`
`       `
`    86   by (cases x) simp_all`
`       `
`    87 `
`       `
`    88 lemma bit_add_self_left [simp]: "x + (x + y) = (y :: bit)"`
`       `
`    89   by simp`
`       `
`    90 `
`       `
`    91 lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"`
`       `
`    92   unfolding times_bit_def by (simp split: bit.split)`
`       `
`    93 `
`       `
`    94 text {* Not sure whether the next two should be simp rules. *}`
`       `
`    95 `
`       `
`    96 lemma bit_add_eq_0_iff: "x + y = (0 :: bit) \<longleftrightarrow> x = y"`
`       `
`    97   unfolding plus_bit_def by (simp split: bit.split)`
`       `
`    98 `
`       `
`    99 lemma bit_add_eq_1_iff: "x + y = (1 :: bit) \<longleftrightarrow> x \<noteq> y"`
`       `
`   100   unfolding plus_bit_def by (simp split: bit.split)`
`       `
`   101 `
`       `
`   102 `
`       `
`   103 subsection {* Numerals at type @{typ bit} *}`
`       `
`   104 `
`       `
`   105 instantiation bit :: number_ring`
`       `
`   106 begin`
`       `
`   107 `
`       `
`   108 definition number_of_bit_def:`
`       `
`   109   "(number_of w :: bit) = of_int w"`
`       `
`   110 `
`       `
`   111 instance proof`
`       `
`   112 qed (rule number_of_bit_def)`
`       `
`   113 `
`       `
`   114 end`
`       `
`   115 `
`       `
`   116 text {* All numerals reduce to either 0 or 1. *}`
`       `
`   117 `
`       `
`   118 lemma bit_number_of_even [simp]: "number_of (Int.Bit0 w) = (0 :: bit)"`
`       `
`   119   by (simp only: number_of_Bit0 add_0_left bit_add_self)`
`       `
`   120 `
`       `
`   121 lemma bit_number_of_odd [simp]: "number_of (Int.Bit1 w) = (1 :: bit)"`
`       `
`   122   by (simp only: number_of_Bit1 add_assoc bit_add_self`
`       `
`   123                  monoid_add_class.add_0_right)`
`       `
`   124 `
`       `
`   125 end`