src/HOL/Library/Bit.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 53063 8f7ac535892f
child 54489 03ff4d1e6784
permissions -rw-r--r--
more simplification rules on unary and binary minus
     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 bit = "UNIV :: bool set"
    14   morphisms set Bit
    15   ..
    16 
    17 instantiation bit :: "{zero, one}"
    18 begin
    19 
    20 definition zero_bit_def:
    21   "0 = Bit False"
    22 
    23 definition one_bit_def:
    24   "1 = Bit True"
    25 
    26 instance ..
    27 
    28 end
    29 
    30 rep_datatype "0::bit" "1::bit"
    31 proof -
    32   fix P and x :: bit
    33   assume "P (0::bit)" and "P (1::bit)"
    34   then have "\<forall>b. P (Bit b)"
    35     unfolding zero_bit_def one_bit_def
    36     by (simp add: all_bool_eq)
    37   then show "P x"
    38     by (induct x) simp
    39 next
    40   show "(0::bit) \<noteq> (1::bit)"
    41     unfolding zero_bit_def one_bit_def
    42     by (simp add: Bit_inject)
    43 qed
    44 
    45 lemma Bit_set_eq [simp]:
    46   "Bit (set b) = b"
    47   by (fact set_inverse)
    48   
    49 lemma set_Bit_eq [simp]:
    50   "set (Bit P) = P"
    51   by (rule Bit_inverse) rule
    52 
    53 lemma bit_eq_iff:
    54   "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
    55   by (auto simp add: set_inject)
    56 
    57 lemma Bit_inject [simp]:
    58   "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
    59   by (auto simp add: Bit_inject)  
    60 
    61 lemma set [iff]:
    62   "\<not> set 0"
    63   "set 1"
    64   by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
    65 
    66 lemma [code]:
    67   "set 0 \<longleftrightarrow> False"
    68   "set 1 \<longleftrightarrow> True"
    69   by simp_all
    70 
    71 lemma set_iff:
    72   "set b \<longleftrightarrow> b = 1"
    73   by (cases b) simp_all
    74 
    75 lemma bit_eq_iff_set:
    76   "b = 0 \<longleftrightarrow> \<not> set b"
    77   "b = 1 \<longleftrightarrow> set b"
    78   by (simp_all add: bit_eq_iff)
    79 
    80 lemma Bit [simp, code]:
    81   "Bit False = 0"
    82   "Bit True = 1"
    83   by (simp_all add: zero_bit_def one_bit_def)
    84 
    85 lemma bit_not_0_iff [iff]:
    86   "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
    87   by (simp add: bit_eq_iff)
    88 
    89 lemma bit_not_1_iff [iff]:
    90   "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
    91   by (simp add: bit_eq_iff)
    92 
    93 lemma [code]:
    94   "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
    95   "HOL.equal 1 b \<longleftrightarrow> set b"
    96   by (simp_all add: equal set_iff)  
    97 
    98   
    99 subsection {* Type @{typ bit} forms a field *}
   100 
   101 instantiation bit :: field_inverse_zero
   102 begin
   103 
   104 definition plus_bit_def:
   105   "x + y = bit_case y (bit_case 1 0 y) x"
   106 
   107 definition times_bit_def:
   108   "x * y = bit_case 0 y x"
   109 
   110 definition uminus_bit_def [simp]:
   111   "- x = (x :: bit)"
   112 
   113 definition minus_bit_def [simp]:
   114   "x - y = (x + y :: bit)"
   115 
   116 definition inverse_bit_def [simp]:
   117   "inverse x = (x :: bit)"
   118 
   119 definition divide_bit_def [simp]:
   120   "x / y = (x * y :: bit)"
   121 
   122 lemmas field_bit_defs =
   123   plus_bit_def times_bit_def minus_bit_def uminus_bit_def
   124   divide_bit_def inverse_bit_def
   125 
   126 instance proof
   127 qed (unfold field_bit_defs, auto split: bit.split)
   128 
   129 end
   130 
   131 lemma bit_add_self: "x + x = (0 :: bit)"
   132   unfolding plus_bit_def by (simp split: bit.split)
   133 
   134 lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
   135   unfolding times_bit_def by (simp split: bit.split)
   136 
   137 text {* Not sure whether the next two should be simp rules. *}
   138 
   139 lemma bit_add_eq_0_iff: "x + y = (0 :: bit) \<longleftrightarrow> x = y"
   140   unfolding plus_bit_def by (simp split: bit.split)
   141 
   142 lemma bit_add_eq_1_iff: "x + y = (1 :: bit) \<longleftrightarrow> x \<noteq> y"
   143   unfolding plus_bit_def by (simp split: bit.split)
   144 
   145 
   146 subsection {* Numerals at type @{typ bit} *}
   147 
   148 text {* All numerals reduce to either 0 or 1. *}
   149 
   150 lemma bit_minus1 [simp]: "-1 = (1 :: bit)"
   151   by (simp only: minus_one [symmetric] uminus_bit_def)
   152 
   153 lemma bit_neg_numeral [simp]: "(neg_numeral w :: bit) = numeral w"
   154   by (simp only: neg_numeral_def uminus_bit_def)
   155 
   156 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   157   by (simp only: numeral_Bit0 bit_add_self)
   158 
   159 lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
   160   by (simp only: numeral_Bit1 bit_add_self add_0_left)
   161 
   162 
   163 subsection {* Conversion from @{typ bit} *}
   164 
   165 context zero_neq_one
   166 begin
   167 
   168 definition of_bit :: "bit \<Rightarrow> 'a"
   169 where
   170   "of_bit b = bit_case 0 1 b" 
   171 
   172 lemma of_bit_eq [simp, code]:
   173   "of_bit 0 = 0"
   174   "of_bit 1 = 1"
   175   by (simp_all add: of_bit_def)
   176 
   177 lemma of_bit_eq_iff:
   178   "of_bit x = of_bit y \<longleftrightarrow> x = y"
   179   by (cases x) (cases y, simp_all)+
   180 
   181 end  
   182 
   183 context semiring_1
   184 begin
   185 
   186 lemma of_nat_of_bit_eq:
   187   "of_nat (of_bit b) = of_bit b"
   188   by (cases b) simp_all
   189 
   190 end
   191 
   192 context ring_1
   193 begin
   194 
   195 lemma of_int_of_bit_eq:
   196   "of_int (of_bit b) = of_bit b"
   197   by (cases b) simp_all
   198 
   199 end
   200 
   201 hide_const (open) set
   202 
   203 end
   204