src/HOL/Library/Bit.thy
changeset 29994 6ca6b6bd6e15
child 29995 62efbd0ef132
equal deleted 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