src/HOL/Word/Bit_Int.thy
author huffman
Sat, 12 Nov 2011 13:01:56 +0100
changeset 45475 b2b087c20e45
parent 44939 5930d35c976d
child 45529 0e1037d4e049
permissions -rw-r--r--
removed some old-style semicolons
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     1
(* 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     2
  Author: Jeremy Dawson and Gerwin Klein, NICTA
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     3
44939
5930d35c976d removed unused legacy lemma names, some comment cleanup.
kleing
parents: 37667
diff changeset
     4
  Definitions and basic theorems for bit-wise logical operations 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     5
  for integers expressed using Pls, Min, BIT,
44939
5930d35c976d removed unused legacy lemma names, some comment cleanup.
kleing
parents: 37667
diff changeset
     6
  and converting them to and from lists of bools.
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     7
*) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     8
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
     9
header {* Bitwise Operations on Binary Integers *}
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
    10
37658
df789294c77a more speaking names
haftmann
parents: 37657
diff changeset
    11
theory Bit_Int
df789294c77a more speaking names
haftmann
parents: 37657
diff changeset
    12
imports Bit_Representation Bit_Operations
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    13
begin
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    14
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    15
subsection {* Recursion combinators for bitstrings *}
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    16
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    17
function bin_rec :: "'a \<Rightarrow> 'a \<Rightarrow> (int \<Rightarrow> bit \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> int \<Rightarrow> 'a" where 
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    18
  "bin_rec f1 f2 f3 bin = (if bin = 0 then f1 
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    19
    else if bin = - 1 then f2
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    20
    else f3 (bin_rest bin) (bin_last bin) (bin_rec f1 f2 f3 (bin_rest bin)))"
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    21
  by pat_completeness auto
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    22
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    23
termination by (relation "measure (nat o abs o snd o snd o snd)")
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    24
  (simp_all add: bin_last_def bin_rest_def)
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    25
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    26
declare bin_rec.simps [simp del]
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    27
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    28
lemma bin_rec_PM:
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    29
  "f = bin_rec f1 f2 f3 ==> f Int.Pls = f1 & f Int.Min = f2"
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    30
  by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    31
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    32
lemma bin_rec_Pls: "bin_rec f1 f2 f3 Int.Pls = f1"
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    33
  by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    34
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    35
lemma bin_rec_Min: "bin_rec f1 f2 f3 Int.Min = f2"
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    36
  by (unfold Pls_def Min_def) (simp add: bin_rec.simps)
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    37
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    38
lemma bin_rec_Bit0:
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    39
  "f3 Int.Pls (0::bit) f1 = f1 \<Longrightarrow>
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    40
    bin_rec f1 f2 f3 (Int.Bit0 w) = f3 w (0::bit) (bin_rec f1 f2 f3 w)"
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    41
  by (unfold Pls_def Min_def Bit0_def Bit1_def) (simp add: bin_rec.simps bin_last_def bin_rest_def)
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    42
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    43
lemma bin_rec_Bit1:
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    44
  "f3 Int.Min (1::bit) f2 = f2 \<Longrightarrow>
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    45
    bin_rec f1 f2 f3 (Int.Bit1 w) = f3 w (1::bit) (bin_rec f1 f2 f3 w)"
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    46
  apply (cases "w = Int.Min")
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    47
  apply (simp add: bin_rec_Min)
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    48
  apply (cases "w = Int.Pls")
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    49
  apply (simp add: bin_rec_Pls number_of_is_id Pls_def [symmetric] bin_rec.simps)
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    50
  apply (subst bin_rec.simps)
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    51
  apply auto unfolding Pls_def Min_def Bit0_def Bit1_def number_of_is_id apply auto
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    52
  done
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    53
  
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    54
lemma bin_rec_Bit:
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    55
  "f = bin_rec f1 f2 f3  ==> f3 Int.Pls (0::bit) f1 = f1 ==> 
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    56
    f3 Int.Min (1::bit) f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    57
  by (cases b, simp add: bin_rec_Bit0, simp add: bin_rec_Bit1)
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    58
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    59
lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    60
  bin_rec_Bit0 bin_rec_Bit1
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    61
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    62
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
    63
subsection {* Logical operations *}
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
    64
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
    65
text "bit-wise logical operations on the int type"
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
    66
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    67
instantiation int :: bit
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    68
begin
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    69
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    70
definition
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    71
  int_not_def: "bitNOT = bin_rec (- 1) 0
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
    72
    (\<lambda>w b s. s BIT (NOT b))"
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    73
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    74
definition
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    75
  int_and_def: "bitAND = bin_rec (\<lambda>x. 0) (\<lambda>y. y) 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
    76
    (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    77
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    78
definition
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    79
  int_or_def: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. - 1) 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
    80
    (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    81
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    82
definition
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    83
  int_xor_def: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
    84
    (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    85
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    86
instance ..
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    87
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25112
diff changeset
    88
end
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
    89
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    90
lemma int_not_simps [simp]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
    91
  "NOT Int.Pls = Int.Min"
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
    92
  "NOT Int.Min = Int.Pls"
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
    93
  "NOT (Int.Bit0 w) = Int.Bit1 (NOT w)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
    94
  "NOT (Int.Bit1 w) = Int.Bit0 (NOT w)"
26558
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
    95
  "NOT (w BIT b) = (NOT w) BIT (NOT b)"
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    96
  unfolding int_not_def Pls_def [symmetric] Min_def [symmetric] by (simp_all add: bin_rec_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    97
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    98
lemma int_xor_Pls [simp]: 
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
    99
  "Int.Pls XOR x = x"
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   100
  unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   101
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   102
lemma int_xor_Min [simp]: 
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   103
  "Int.Min XOR x = NOT x"
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   104
  unfolding int_xor_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_PM)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   105
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   106
lemma int_xor_Bits [simp]: 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   107
  "(x BIT b) XOR (y BIT c) = (x XOR y) BIT (b XOR c)"
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   108
  apply (unfold int_xor_def Pls_def [symmetric] Min_def [symmetric])
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   109
  apply (rule bin_rec_simps (1) [THEN fun_cong, THEN trans])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   110
    apply (rule ext, simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   111
   prefer 2
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   112
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   113
  apply (rule ext)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   114
  apply (simp add: int_not_simps [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   115
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   116
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   117
lemma int_xor_Bits2 [simp]: 
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   118
  "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   119
  "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   120
  "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   121
  "(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   122
  unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   123
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   124
lemma int_xor_x_simps':
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   125
  "w XOR (Int.Pls BIT 0) = w"
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   126
  "w XOR (Int.Min BIT 1) = NOT w"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   127
  apply (induct w rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   128
       apply simp_all[4]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   129
   apply (unfold int_xor_Bits)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   130
   apply clarsimp+
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   131
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   132
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   133
lemma int_xor_extra_simps [simp]:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   134
  "w XOR Int.Pls = w"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   135
  "w XOR Int.Min = NOT w"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   136
  using int_xor_x_simps' by simp_all
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   137
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   138
lemma int_or_Pls [simp]: 
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   139
  "Int.Pls OR x = x"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24418
diff changeset
   140
  by (unfold int_or_def) (simp add: bin_rec_PM)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   141
  
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   142
lemma int_or_Min [simp]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   143
  "Int.Min OR x = Int.Min"
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   144
  by (unfold int_or_def Pls_def [symmetric] Min_def [symmetric]) (simp add: bin_rec_PM)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   145
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   146
lemma int_or_Bits [simp]: 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   147
  "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   148
  unfolding int_or_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   149
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   150
lemma int_or_Bits2 [simp]: 
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   151
  "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   152
  "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   153
  "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   154
  "(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   155
  unfolding BIT_simps [symmetric] int_or_Bits by simp_all
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   156
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   157
lemma int_or_x_simps': 
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   158
  "w OR (Int.Pls BIT 0) = w"
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   159
  "w OR (Int.Min BIT 1) = Int.Min"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   160
  apply (induct w rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   161
       apply simp_all[4]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   162
   apply (unfold int_or_Bits)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   163
   apply clarsimp+
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   164
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   165
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   166
lemma int_or_extra_simps [simp]:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   167
  "w OR Int.Pls = w"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   168
  "w OR Int.Min = Int.Min"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   169
  using int_or_x_simps' by simp_all
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   170
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   171
lemma int_and_Pls [simp]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   172
  "Int.Pls AND x = Int.Pls"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24418
diff changeset
   173
  unfolding int_and_def by (simp add: bin_rec_PM)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   174
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   175
lemma int_and_Min [simp]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   176
  "Int.Min AND x = x"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24418
diff changeset
   177
  unfolding int_and_def by (simp add: bin_rec_PM)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   178
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   179
lemma int_and_Bits [simp]: 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   180
  "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   181
  unfolding int_and_def Pls_def [symmetric] Min_def [symmetric] by (simp add: bin_rec_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   182
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   183
lemma int_and_Bits2 [simp]: 
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   184
  "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   185
  "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   186
  "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   187
  "(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   188
  unfolding BIT_simps [symmetric] int_and_Bits by simp_all
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   189
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   190
lemma int_and_x_simps': 
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   191
  "w AND (Int.Pls BIT 0) = Int.Pls"
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   192
  "w AND (Int.Min BIT 1) = w"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   193
  apply (induct w rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   194
       apply simp_all[4]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   195
   apply (unfold int_and_Bits)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   196
   apply clarsimp+
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   197
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   198
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   199
lemma int_and_extra_simps [simp]:
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   200
  "w AND Int.Pls = Int.Pls"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   201
  "w AND Int.Min = w"
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   202
  using int_and_x_simps' by simp_all
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   203
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   204
(* commutativity of the above *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   205
lemma bin_ops_comm:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   206
  shows
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   207
  int_and_comm: "!!y::int. x AND y = y AND x" and
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   208
  int_or_comm:  "!!y::int. x OR y = y OR x" and
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   209
  int_xor_comm: "!!y::int. x XOR y = y XOR x"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   210
  apply (induct x rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   211
          apply simp_all[6]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   212
    apply (case_tac y rule: bin_exhaust, simp add: bit_ops_comm)+
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   213
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   214
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   215
lemma bin_ops_same [simp]:
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   216
  "(x::int) AND x = x" 
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   217
  "(x::int) OR x = x" 
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   218
  "(x::int) XOR x = Int.Pls"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   219
  by (induct x rule: bin_induct) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   220
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   221
lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   222
  by (induct x rule: bin_induct) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   223
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   224
lemmas bin_log_esimps = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   225
  int_and_extra_simps  int_or_extra_simps  int_xor_extra_simps
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   226
  int_and_Pls int_and_Min  int_or_Pls int_or_Min  int_xor_Pls int_xor_Min
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   227
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   228
(* basic properties of logical (bit-wise) operations *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   229
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   230
lemma bbw_ao_absorb: 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   231
  "!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   232
  apply (induct x rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   233
    apply auto 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   234
   apply (case_tac [!] y rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   235
   apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   236
   apply (case_tac [!] bit)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   237
     apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   238
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   239
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   240
lemma bbw_ao_absorbs_other:
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   241
  "x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   242
  "(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   243
  "(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   244
  apply (auto simp: bbw_ao_absorb int_or_comm)  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   245
      apply (subst int_or_comm)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   246
    apply (simp add: bbw_ao_absorb)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   247
   apply (subst int_and_comm)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   248
   apply (subst int_or_comm)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   249
   apply (simp add: bbw_ao_absorb)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   250
  apply (subst int_and_comm)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   251
  apply (simp add: bbw_ao_absorb)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   252
  done
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   253
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   254
lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   255
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   256
lemma int_xor_not:
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   257
  "!!y::int. (NOT x) XOR y = NOT (x XOR y) & 
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   258
        x XOR (NOT y) = NOT (x XOR y)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   259
  apply (induct x rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   260
    apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   261
   apply (case_tac y rule: bin_exhaust, auto, 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   262
          case_tac b, auto)+
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   263
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   264
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   265
lemma bbw_assocs': 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   266
  "!!y z::int. (x AND y) AND z = x AND (y AND z) & 
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   267
          (x OR y) OR z = x OR (y OR z) & 
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   268
          (x XOR y) XOR z = x XOR (y XOR z)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   269
  apply (induct x rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   270
    apply (auto simp: int_xor_not)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   271
    apply (case_tac [!] y rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   272
    apply (case_tac [!] z rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   273
    apply (case_tac [!] bit)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   274
       apply (case_tac [!] b)
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   275
             apply (auto simp del: BIT_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   276
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   277
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   278
lemma int_and_assoc:
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   279
  "(x AND y) AND (z::int) = x AND (y AND z)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   280
  by (simp add: bbw_assocs')
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   281
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   282
lemma int_or_assoc:
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   283
  "(x OR y) OR (z::int) = x OR (y OR z)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   284
  by (simp add: bbw_assocs')
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   285
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   286
lemma int_xor_assoc:
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   287
  "(x XOR y) XOR (z::int) = x XOR (y XOR z)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   288
  by (simp add: bbw_assocs')
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   289
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   290
lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   291
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   292
lemma bbw_lcs [simp]: 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   293
  "(y::int) AND (x AND z) = x AND (y AND z)"
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   294
  "(y::int) OR (x OR z) = x OR (y OR z)"
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   295
  "(y::int) XOR (x XOR z) = x XOR (y XOR z)" 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   296
  apply (auto simp: bbw_assocs [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   297
  apply (auto simp: bin_ops_comm)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   298
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   299
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   300
lemma bbw_not_dist: 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   301
  "!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)" 
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   302
  "!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   303
  apply (induct x rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   304
       apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   305
   apply (case_tac [!] y rule: bin_exhaust)
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   306
   apply (case_tac [!] bit, auto simp del: BIT_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   307
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   308
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   309
lemma bbw_oa_dist: 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   310
  "!!y z::int. (x AND y) OR z = 
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   311
          (x OR z) AND (y OR z)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   312
  apply (induct x rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   313
    apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   314
  apply (case_tac y rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   315
  apply (case_tac z rule: bin_exhaust)
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   316
  apply (case_tac ba, auto simp del: BIT_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   317
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   318
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   319
lemma bbw_ao_dist: 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   320
  "!!y z::int. (x OR y) AND z = 
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   321
          (x AND z) OR (y AND z)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   322
   apply (induct x rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   323
    apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   324
  apply (case_tac y rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   325
  apply (case_tac z rule: bin_exhaust)
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   326
  apply (case_tac ba, auto simp del: BIT_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   327
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   328
24367
3e29eafabe16 AC rules for bitwise logical operators no longer declared simp
huffman
parents: 24366
diff changeset
   329
(*
3e29eafabe16 AC rules for bitwise logical operators no longer declared simp
huffman
parents: 24366
diff changeset
   330
Why were these declared simp???
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   331
declare bin_ops_comm [simp] bbw_assocs [simp] 
24367
3e29eafabe16 AC rules for bitwise logical operators no longer declared simp
huffman
parents: 24366
diff changeset
   332
*)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   334
lemma plus_and_or [rule_format]:
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   335
  "ALL y::int. (x AND y) + (x OR y) = x + y"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   336
  apply (induct x rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   337
    apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   338
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   339
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   340
  apply (case_tac y rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   341
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   342
  apply (unfold Bit_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   343
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   344
  apply (erule_tac x = "x" in allE)
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   345
  apply (simp add: bitval_def split: bit.split)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   346
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   347
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   348
lemma le_int_or:
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   349
  "bin_sign (y::int) = Int.Pls ==> x <= x OR y"
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   350
  apply (induct y arbitrary: x rule: bin_induct)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   351
    apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   352
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   353
  apply (case_tac x rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   354
  apply (case_tac b)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   355
   apply (case_tac [!] bit)
26514
eff55c0a6d34 tuned towards code generation
haftmann
parents: 26086
diff changeset
   356
     apply (auto simp: less_eq_int_code)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   357
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   358
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   359
lemmas int_and_le =
45475
b2b087c20e45 removed some old-style semicolons
huffman
parents: 44939
diff changeset
   360
  xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   361
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   362
lemma bin_nth_ops:
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   363
  "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)" 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   364
  "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   365
  "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)" 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   366
  "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   367
  apply (induct n)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   368
         apply safe
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   369
                         apply (case_tac [!] x rule: bin_exhaust)
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   370
                         apply (simp_all del: BIT_simps)
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   371
                      apply (case_tac [!] y rule: bin_exhaust)
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   372
                      apply (simp_all del: BIT_simps)
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   373
        apply (auto dest: not_B1_is_B0 intro: B1_ass_B0)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   374
  done
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   375
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   376
(* interaction between bit-wise and arithmetic *)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   377
(* good example of bin_induction *)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   378
lemma bin_add_not: "x + NOT x = Int.Min"
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   379
  apply (induct x rule: bin_induct)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   380
    apply clarsimp
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   381
   apply clarsimp
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   382
  apply (case_tac bit, auto)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   383
  done
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   384
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   385
(* truncating results of bit-wise operations *)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   386
lemma bin_trunc_ao: 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   387
  "!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)" 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   388
  "!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   389
  apply (induct n)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   390
      apply auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   391
      apply (case_tac [!] x rule: bin_exhaust)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   392
      apply (case_tac [!] y rule: bin_exhaust)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   393
      apply auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   394
  done
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   395
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   396
lemma bin_trunc_xor: 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   397
  "!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) = 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   398
          bintrunc n (x XOR y)"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   399
  apply (induct n)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   400
   apply auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   401
   apply (case_tac [!] x rule: bin_exhaust)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   402
   apply (case_tac [!] y rule: bin_exhaust)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   403
   apply auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   404
  done
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   405
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   406
lemma bin_trunc_not: 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   407
  "!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   408
  apply (induct n)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   409
   apply auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   410
   apply (case_tac [!] x rule: bin_exhaust)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   411
   apply auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   412
  done
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   413
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   414
(* want theorems of the form of bin_trunc_xor *)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   415
lemma bintr_bintr_i:
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   416
  "x = bintrunc n y ==> bintrunc n x = bintrunc n y"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   417
  by auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   418
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   419
lemmas bin_trunc_and = bin_trunc_ao(1) [THEN bintr_bintr_i]
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   420
lemmas bin_trunc_or = bin_trunc_ao(2) [THEN bintr_bintr_i]
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   421
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   422
subsection {* Setting and clearing bits *}
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   423
26558
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   424
primrec
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   425
  bin_sc :: "nat => bit => int => int"
26558
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   426
where
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   427
  Z: "bin_sc 0 b w = bin_rest w BIT b"
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   428
  | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w"
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   429
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   430
(** nth bit, set/clear **)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   431
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   432
lemma bin_nth_sc [simp]: 
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   433
  "!!w. bin_nth (bin_sc n b w) n = (b = 1)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   434
  by (induct n)  auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   435
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   436
lemma bin_sc_sc_same [simp]: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   437
  "!!w. bin_sc n c (bin_sc n b w) = bin_sc n c w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   438
  by (induct n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   439
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   440
lemma bin_sc_sc_diff:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   441
  "!!w m. m ~= n ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   442
    bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   443
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   444
   apply (case_tac [!] m)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   445
     apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   446
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   447
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   448
lemma bin_nth_sc_gen: 
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   449
  "!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = 1 else bin_nth w m)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   450
  by (induct n) (case_tac [!] m, auto)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   451
  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   452
lemma bin_sc_nth [simp]:
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   453
  "!!w. (bin_sc n (If (bin_nth w n) 1 0) w) = w"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24418
diff changeset
   454
  by (induct n) auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   455
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   456
lemma bin_sign_sc [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   457
  "!!w. bin_sign (bin_sc n b w) = bin_sign w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   458
  by (induct n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   459
  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   460
lemma bin_sc_bintr [simp]: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   461
  "!!w m. bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   462
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   463
   apply (case_tac [!] w rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   464
   apply (case_tac [!] m, auto)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   465
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   466
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   467
lemma bin_clr_le:
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   468
  "!!w. bin_sc n 0 w <= w"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   469
  apply (induct n) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   470
   apply (case_tac [!] w rule: bin_exhaust)
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   471
   apply (auto simp del: BIT_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   472
   apply (unfold Bit_def)
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   473
   apply (simp_all add: bitval_def split: bit.split)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   474
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   475
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   476
lemma bin_set_ge:
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   477
  "!!w. bin_sc n 1 w >= w"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   478
  apply (induct n) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   479
   apply (case_tac [!] w rule: bin_exhaust)
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   480
   apply (auto simp del: BIT_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   481
   apply (unfold Bit_def)
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   482
   apply (simp_all add: bitval_def split: bit.split)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   483
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   484
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   485
lemma bintr_bin_clr_le:
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   486
  "!!w m. bintrunc n (bin_sc m 0 w) <= bintrunc n w"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   487
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   488
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   489
  apply (case_tac w rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   490
  apply (case_tac m)
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   491
   apply (auto simp del: BIT_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   492
   apply (unfold Bit_def)
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   493
   apply (simp_all add: bitval_def split: bit.split)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   494
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   495
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   496
lemma bintr_bin_set_ge:
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   497
  "!!w m. bintrunc n (bin_sc m 1 w) >= bintrunc n w"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   498
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   499
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   500
  apply (case_tac w rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   501
  apply (case_tac m)
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25919
diff changeset
   502
   apply (auto simp del: BIT_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   503
   apply (unfold Bit_def)
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   504
   apply (simp_all add: bitval_def split: bit.split)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   505
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   506
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   507
lemma bin_sc_FP [simp]: "bin_sc n 0 Int.Pls = Int.Pls"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   508
  by (induct n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   509
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 30943
diff changeset
   510
lemma bin_sc_TM [simp]: "bin_sc n 1 Int.Min = Int.Min"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   511
  by (induct n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   512
  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   513
lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   514
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   515
lemma bin_sc_minus:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   516
  "0 < n ==> bin_sc (Suc (n - 1)) b w = bin_sc n b w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   517
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   518
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   519
lemmas bin_sc_Suc_minus = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   520
  trans [OF bin_sc_minus [symmetric] bin_sc.Suc, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   521
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   522
lemmas bin_sc_Suc_pred [simp] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   523
  bin_sc_Suc_minus [of "number_of bin", simplified nobm1, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   524
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24418
diff changeset
   525
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   526
subsection {* Splitting and concatenation *}
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   527
26558
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   528
definition bin_rcat :: "nat \<Rightarrow> int list \<Rightarrow> int" where
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   529
  "bin_rcat n = foldl (%u v. bin_cat u n v) Int.Pls"
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   530
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   531
lemma [code]:
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   532
  "bin_rcat n = foldl (\<lambda>u v. bin_cat u n v) 0"
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   533
  by (simp add: bin_rcat_def Pls_def)
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   534
28042
1471f2974eb1 more function -> fun
krauss
parents: 26558
diff changeset
   535
fun bin_rsplit_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
26558
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   536
  "bin_rsplit_aux n m c bs =
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   537
    (if m = 0 | n = 0 then bs else
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   538
      let (a, b) = bin_split n c 
26558
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   539
      in bin_rsplit_aux n (m - n) a (b # bs))"
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   540
26558
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   541
definition bin_rsplit :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   542
  "bin_rsplit n w = bin_rsplit_aux n (fst w) (snd w) []"
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   543
28042
1471f2974eb1 more function -> fun
krauss
parents: 26558
diff changeset
   544
fun bin_rsplitl_aux :: "nat \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int list \<Rightarrow> int list" where
26558
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   545
  "bin_rsplitl_aux n m c bs =
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   546
    (if m = 0 | n = 0 then bs else
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   547
      let (a, b) = bin_split (min m n) c 
26558
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   548
      in bin_rsplitl_aux n (m - n) a (b # bs))"
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   549
26558
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   550
definition bin_rsplitl :: "nat \<Rightarrow> nat \<times> int \<Rightarrow> int list" where
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   551
  "bin_rsplitl n w = bin_rsplitl_aux n (fst w) (snd w) []"
7fcc10088e72 renamed app2 to map2
haftmann
parents: 26514
diff changeset
   552
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   553
declare bin_rsplit_aux.simps [simp del]
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   554
declare bin_rsplitl_aux.simps [simp del]
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   555
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   556
lemma bin_sign_cat: 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   557
  "!!y. bin_sign (bin_cat x n y) = bin_sign x"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   558
  by (induct n) auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   559
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   560
lemma bin_cat_Suc_Bit:
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   561
  "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   562
  by auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   563
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   564
lemma bin_nth_cat: 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   565
  "!!n y. bin_nth (bin_cat x k y) n = 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   566
    (if n < k then bin_nth y n else bin_nth x (n - k))"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   567
  apply (induct k)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   568
   apply clarsimp
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   569
  apply (case_tac n, auto)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   570
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   571
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   572
lemma bin_nth_split:
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   573
  "!!b c. bin_split n c = (a, b) ==> 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   574
    (ALL k. bin_nth a k = bin_nth c (n + k)) & 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   575
    (ALL k. bin_nth b k = (k < n & bin_nth c k))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   576
  apply (induct n)
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   577
   apply clarsimp
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   578
  apply (clarsimp simp: Let_def split: ls_splits)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   579
  apply (case_tac k)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   580
  apply auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   581
  done
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   582
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   583
lemma bin_cat_assoc: 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   584
  "!!z. bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)" 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   585
  by (induct n) auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   586
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   587
lemma bin_cat_assoc_sym: "!!z m. 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   588
  bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   589
  apply (induct n, clarsimp)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   590
  apply (case_tac m, auto)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   591
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   592
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   593
lemma bin_cat_Pls [simp]: 
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   594
  "!!w. bin_cat Int.Pls n w = bintrunc n w"
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   595
  by (induct n) auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   596
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   597
lemma bintr_cat1: 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   598
  "!!b. bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   599
  by (induct n) auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   600
    
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   601
lemma bintr_cat: "bintrunc m (bin_cat a n b) = 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   602
    bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   603
  by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   604
    
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   605
lemma bintr_cat_same [simp]: 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   606
  "bintrunc n (bin_cat a n b) = bintrunc n b"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   607
  by (auto simp add : bintr_cat)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   608
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   609
lemma cat_bintr [simp]: 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   610
  "!!b. bin_cat a n (bintrunc n b) = bin_cat a n b"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   611
  by (induct n) auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   612
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   613
lemma split_bintrunc: 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   614
  "!!b c. bin_split n c = (a, b) ==> b = bintrunc n c"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   615
  by (induct n) (auto simp: Let_def split: ls_splits)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   616
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   617
lemma bin_cat_split:
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   618
  "!!v w. bin_split n w = (u, v) ==> w = bin_cat u n v"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   619
  by (induct n) (auto simp: Let_def split: ls_splits)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   620
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   621
lemma bin_split_cat:
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   622
  "!!w. bin_split n (bin_cat v n w) = (v, bintrunc n w)"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   623
  by (induct n) auto
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   624
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   625
lemma bin_split_Pls [simp]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   626
  "bin_split n Int.Pls = (Int.Pls, Int.Pls)"
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   627
  by (induct n) (auto simp: Let_def split: ls_splits)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   628
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   629
lemma bin_split_Min [simp]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   630
  "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)"
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   631
  by (induct n) (auto simp: Let_def split: ls_splits)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   632
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   633
lemma bin_split_trunc:
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   634
  "!!m b c. bin_split (min m n) c = (a, b) ==> 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   635
    bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   636
  apply (induct n, clarsimp)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   637
  apply (simp add: bin_rest_trunc Let_def split: ls_splits)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   638
  apply (case_tac m)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   639
   apply (auto simp: Let_def split: ls_splits)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   640
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   641
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   642
lemma bin_split_trunc1:
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   643
  "!!m b c. bin_split n c = (a, b) ==> 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   644
    bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   645
  apply (induct n, clarsimp)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   646
  apply (simp add: bin_rest_trunc Let_def split: ls_splits)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   647
  apply (case_tac m)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   648
   apply (auto simp: Let_def split: ls_splits)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   649
  done
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   650
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   651
lemma bin_cat_num:
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   652
  "!!b. bin_cat a n b = a * 2 ^ n + bintrunc n b"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   653
  apply (induct n, clarsimp)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   654
  apply (simp add: Bit_def cong: number_of_False_cong)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   655
  done
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   656
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   657
lemma bin_split_num:
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   658
  "!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)"
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   659
  apply (induct n, clarsimp)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   660
  apply (simp add: bin_rest_div zdiv_zmult2_eq)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   661
  apply (case_tac b rule: bin_exhaust)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   662
  apply simp
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
   663
  apply (simp add: Bit_def mod_mult_mult1 p1mod22k bitval_def
24364
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   664
              split: bit.split 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   665
              cong: number_of_False_cong)
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   666
  done 
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   667
31e359126ab6 reorganize into subsections
huffman
parents: 24353
diff changeset
   668
subsection {* Miscellaneous lemmas *}
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   669
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   670
lemma nth_2p_bin: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   671
  "!!m. bin_nth (2 ^ n) m = (m = n)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   672
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   673
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   674
   apply safe
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   675
     apply (case_tac m) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   676
      apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   677
   apply (case_tac m) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   678
    apply (auto simp: Bit_B0_2t [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   679
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   680
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   681
(* for use when simplifying with bin_nth_Bit *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   682
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   683
lemma ex_eq_or:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   684
  "(EX m. n = Suc m & (m = k | P m)) = (n = Suc k | (EX m. n = Suc m & P m))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   685
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   686
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   687
end
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   688