src/HOL/Library/Bit.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 41959 b460124855b8
child 45701 615da8b8d758
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
     1 (*  Title:      HOL/Library/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_inverse_zero
    53 begin
    54 
    55 definition plus_bit_def:
    56   "x + y = bit_case y (bit_case 1 0 y) x"
    57 
    58 definition times_bit_def:
    59   "x * y = bit_case 0 y x"
    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_add_self: "x + x = (0 :: bit)"
    83   unfolding plus_bit_def by (simp split: bit.split)
    84 
    85 lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
    86   unfolding times_bit_def by (simp split: bit.split)
    87 
    88 text {* Not sure whether the next two should be simp rules. *}
    89 
    90 lemma bit_add_eq_0_iff: "x + y = (0 :: bit) \<longleftrightarrow> x = y"
    91   unfolding plus_bit_def by (simp split: bit.split)
    92 
    93 lemma bit_add_eq_1_iff: "x + y = (1 :: bit) \<longleftrightarrow> x \<noteq> y"
    94   unfolding plus_bit_def by (simp split: bit.split)
    95 
    96 
    97 subsection {* Numerals at type @{typ bit} *}
    98 
    99 instantiation bit :: number_ring
   100 begin
   101 
   102 definition number_of_bit_def:
   103   "(number_of w :: bit) = of_int w"
   104 
   105 instance proof
   106 qed (rule number_of_bit_def)
   107 
   108 end
   109 
   110 text {* All numerals reduce to either 0 or 1. *}
   111 
   112 lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
   113   by (simp only: number_of_Min uminus_bit_def)
   114 
   115 lemma bit_number_of_even [simp]: "number_of (Int.Bit0 w) = (0 :: bit)"
   116   by (simp only: number_of_Bit0 add_0_left bit_add_self)
   117 
   118 lemma bit_number_of_odd [simp]: "number_of (Int.Bit1 w) = (1 :: bit)"
   119   by (simp only: number_of_Bit1 add_assoc bit_add_self
   120                  monoid_add_class.add_0_right)
   121 
   122 end