src/HOL/Library/Bit.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 63462 c1fe30f2bc32
child 69593 3dda49e08b9d
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Library/Bit.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 section \<open>The Field of Integers mod 2\<close>
     6 
     7 theory Bit
     8 imports Main
     9 begin
    10 
    11 subsection \<open>Bits as a datatype\<close>
    12 
    13 typedef bit = "UNIV :: bool set"
    14   morphisms set Bit ..
    15 
    16 instantiation bit :: "{zero, one}"
    17 begin
    18 
    19 definition zero_bit_def: "0 = Bit False"
    20 
    21 definition one_bit_def: "1 = Bit True"
    22 
    23 instance ..
    24 
    25 end
    26 
    27 old_rep_datatype "0::bit" "1::bit"
    28 proof -
    29   fix P :: "bit \<Rightarrow> bool"
    30   fix x :: bit
    31   assume "P 0" and "P 1"
    32   then have "\<forall>b. P (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: Bit_inject)
    41 qed
    42 
    43 lemma Bit_set_eq [simp]: "Bit (set b) = b"
    44   by (fact set_inverse)
    45 
    46 lemma set_Bit_eq [simp]: "set (Bit P) = P"
    47   by (rule Bit_inverse) rule
    48 
    49 lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
    50   by (auto simp add: set_inject)
    51 
    52 lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
    53   by (auto simp add: Bit_inject)
    54 
    55 lemma set [iff]:
    56   "\<not> set 0"
    57   "set 1"
    58   by (simp_all add: zero_bit_def one_bit_def Bit_inverse)
    59 
    60 lemma [code]:
    61   "set 0 \<longleftrightarrow> False"
    62   "set 1 \<longleftrightarrow> True"
    63   by simp_all
    64 
    65 lemma set_iff: "set b \<longleftrightarrow> b = 1"
    66   by (cases b) simp_all
    67 
    68 lemma bit_eq_iff_set:
    69   "b = 0 \<longleftrightarrow> \<not> set b"
    70   "b = 1 \<longleftrightarrow> set b"
    71   by (simp_all add: bit_eq_iff)
    72 
    73 lemma Bit [simp, code]:
    74   "Bit False = 0"
    75   "Bit True = 1"
    76   by (simp_all add: zero_bit_def one_bit_def)
    77 
    78 lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit
    79   by (simp add: bit_eq_iff)
    80 
    81 lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit
    82   by (simp add: bit_eq_iff)
    83 
    84 lemma [code]:
    85   "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
    86   "HOL.equal 1 b \<longleftrightarrow> set b"
    87   by (simp_all add: equal set_iff)
    88 
    89 
    90 subsection \<open>Type @{typ bit} forms a field\<close>
    91 
    92 instantiation bit :: field
    93 begin
    94 
    95 definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x"
    96 
    97 definition times_bit_def: "x * y = case_bit 0 y x"
    98 
    99 definition uminus_bit_def [simp]: "- x = x" for x :: bit
   100 
   101 definition minus_bit_def [simp]: "x - y = x + y" for x y :: bit
   102 
   103 definition inverse_bit_def [simp]: "inverse x = x" for x :: bit
   104 
   105 definition divide_bit_def [simp]: "x div y = x * y" for x y :: bit
   106 
   107 lemmas field_bit_defs =
   108   plus_bit_def times_bit_def minus_bit_def uminus_bit_def
   109   divide_bit_def inverse_bit_def
   110 
   111 instance
   112   by standard (auto simp: field_bit_defs split: bit.split)
   113 
   114 end
   115 
   116 lemma bit_add_self: "x + x = 0" for x :: bit
   117   unfolding plus_bit_def by (simp split: bit.split)
   118 
   119 lemma bit_mult_eq_1_iff [simp]: "x * y = 1 \<longleftrightarrow> x = 1 \<and> y = 1" for x y :: bit
   120   unfolding times_bit_def by (simp split: bit.split)
   121 
   122 text \<open>Not sure whether the next two should be simp rules.\<close>
   123 
   124 lemma bit_add_eq_0_iff: "x + y = 0 \<longleftrightarrow> x = y" for x y :: bit
   125   unfolding plus_bit_def by (simp split: bit.split)
   126 
   127 lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit
   128   unfolding plus_bit_def by (simp split: bit.split)
   129 
   130 
   131 subsection \<open>Numerals at type @{typ bit}\<close>
   132 
   133 text \<open>All numerals reduce to either 0 or 1.\<close>
   134 
   135 lemma bit_minus1 [simp]: "- 1 = (1 :: bit)"
   136   by (simp only: uminus_bit_def)
   137 
   138 lemma bit_neg_numeral [simp]: "(- numeral w :: bit) = numeral w"
   139   by (simp only: uminus_bit_def)
   140 
   141 lemma bit_numeral_even [simp]: "numeral (Num.Bit0 w) = (0 :: bit)"
   142   by (simp only: numeral_Bit0 bit_add_self)
   143 
   144 lemma bit_numeral_odd [simp]: "numeral (Num.Bit1 w) = (1 :: bit)"
   145   by (simp only: numeral_Bit1 bit_add_self add_0_left)
   146 
   147 
   148 subsection \<open>Conversion from @{typ bit}\<close>
   149 
   150 context zero_neq_one
   151 begin
   152 
   153 definition of_bit :: "bit \<Rightarrow> 'a"
   154   where "of_bit b = case_bit 0 1 b"
   155 
   156 lemma of_bit_eq [simp, code]:
   157   "of_bit 0 = 0"
   158   "of_bit 1 = 1"
   159   by (simp_all add: of_bit_def)
   160 
   161 lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y"
   162   by (cases x) (cases y; simp)+
   163 
   164 end
   165 
   166 lemma (in semiring_1) of_nat_of_bit_eq: "of_nat (of_bit b) = of_bit b"
   167   by (cases b) simp_all
   168 
   169 lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b"
   170   by (cases b) simp_all
   171 
   172 hide_const (open) set
   173 
   174 end