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