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