src/HOL/ex/Word.thy
author haftmann
Tue, 04 Aug 2020 09:33:05 +0000
changeset 72082 41393ecb57ac
parent 72079 8c355e2dd7db
permissions -rw-r--r--
uniform mask operation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
     1
(*  Author:  Florian Haftmann, TUM
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
     2
*)
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
     3
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
     4
section \<open>Proof of concept for algebraically founded bit word types\<close>
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
     5
71042
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
     6
theory Word
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
     7
  imports
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
     8
    Main
66453
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents: 64593
diff changeset
     9
    "HOL-Library.Type_Length"
71956
a4bffc0de967 bit operations as distinctive library theory
haftmann
parents: 71954
diff changeset
    10
    "HOL-Library.Bit_Operations"
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    11
begin
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    12
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    13
subsection \<open>Bit strings as quotient type\<close>
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    14
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    15
subsubsection \<open>Basic properties\<close>
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    16
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
    17
quotient_type (overloaded) 'a word = int / "\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l"
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    18
  by (auto intro!: equivpI reflpI sympI transpI)
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    19
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
    20
instantiation word :: (len) "{semiring_numeral, comm_semiring_0, comm_ring}"
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    21
begin
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    22
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    23
lift_definition zero_word :: "'a word"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    24
  is 0
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    25
  .
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    26
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    27
lift_definition one_word :: "'a word"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    28
  is 1
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    29
  .
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    30
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    31
lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    32
  is plus
67961
9c31678d2139 even more on bit operations
haftmann
parents: 67907
diff changeset
    33
  by (subst take_bit_add [symmetric]) (simp add: take_bit_add)
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    34
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    35
lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    36
  is uminus
71424
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
    37
  by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus)
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    38
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    39
lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    40
  is minus
71424
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
    41
  by (subst take_bit_diff [symmetric]) (simp add: take_bit_diff)
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    42
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    43
lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    44
  is times
67907
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
    45
  by (auto simp add: take_bit_eq_mod intro: mod_mult_cong)
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    46
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    47
instance
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    48
  by standard (transfer; simp add: algebra_simps)+
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    49
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    50
end
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    51
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    52
instance word :: (len) comm_ring_1
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    53
  by standard (transfer; simp)+
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    54
70903
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
    55
quickcheck_generator word
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
    56
  constructors:
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
    57
    "zero_class.zero :: ('a::len) word",
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
    58
    "numeral :: num \<Rightarrow> ('a::len) word",
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
    59
    "uminus :: ('a::len) word \<Rightarrow> ('a::len) word"
70903
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
    60
70973
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
    61
context
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
    62
  includes lifting_syntax
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
    63
  notes power_transfer [transfer_rule]
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
    64
begin
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
    65
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
    66
lemma power_transfer_word [transfer_rule]:
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
    67
  \<open>(pcr_word ===> (=) ===> pcr_word) (^) (^)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
    68
  by transfer_prover
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
    69
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
    70
end
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
    71
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    72
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    73
subsubsection \<open>Conversions\<close>
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    74
70927
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    75
context
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    76
  includes lifting_syntax
71182
410935efbf5c characterization of singleton bit operation
haftmann
parents: 71181
diff changeset
    77
  notes 
410935efbf5c characterization of singleton bit operation
haftmann
parents: 71181
diff changeset
    78
    transfer_rule_of_bool [transfer_rule]
410935efbf5c characterization of singleton bit operation
haftmann
parents: 71181
diff changeset
    79
    transfer_rule_numeral [transfer_rule]
70927
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    80
    transfer_rule_of_nat [transfer_rule]
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    81
    transfer_rule_of_int [transfer_rule]
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    82
begin
70348
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
    83
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
    84
lemma [transfer_rule]:
71182
410935efbf5c characterization of singleton bit operation
haftmann
parents: 71181
diff changeset
    85
  "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) of_bool of_bool"
410935efbf5c characterization of singleton bit operation
haftmann
parents: 71181
diff changeset
    86
  by transfer_prover
410935efbf5c characterization of singleton bit operation
haftmann
parents: 71181
diff changeset
    87
410935efbf5c characterization of singleton bit operation
haftmann
parents: 71181
diff changeset
    88
lemma [transfer_rule]:
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
    89
  "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral"
70927
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    90
  by transfer_prover
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    91
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    92
lemma [transfer_rule]:
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    93
  "((=) ===> pcr_word) int of_nat"
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    94
  by transfer_prover
71042
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
    95
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    96
lemma [transfer_rule]:
70927
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    97
  "((=) ===> pcr_word) (\<lambda>k. k) of_int"
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
    98
proof -
70927
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
    99
  have "((=) ===> pcr_word) of_int of_int"
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   100
    by transfer_prover
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   101
  then show ?thesis by (simp add: id_def)
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   102
qed
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   103
70927
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
   104
end
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
   105
70973
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   106
lemma abs_word_eq:
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   107
  "abs_word = of_int"
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   108
  by (rule ext) (transfer, rule)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   109
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   110
context semiring_1
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   111
begin
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   112
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
   113
lift_definition unsigned :: "'b::len word \<Rightarrow> 'a"
67907
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
   114
  is "of_nat \<circ> nat \<circ> take_bit LENGTH('b)"
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   115
  by simp
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   116
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   117
lemma unsigned_0 [simp]:
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   118
  "unsigned 0 = 0"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   119
  by transfer simp
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   120
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   121
end
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   122
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   123
context semiring_char_0
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   124
begin
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   125
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   126
lemma word_eq_iff_unsigned:
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   127
  "a = b \<longleftrightarrow> unsigned a = unsigned b"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   128
  by safe (transfer; simp add: eq_nat_nat_iff)
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   129
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   130
end
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   131
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
   132
instantiation word :: (len) equal
70903
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   133
begin
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   134
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   135
definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   136
  where "equal_word a b \<longleftrightarrow> (unsigned a :: int) = unsigned b"
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   137
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   138
instance proof
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   139
  fix a b :: "'a word"
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   140
  show "HOL.equal a b \<longleftrightarrow> a = b"
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   141
    using word_eq_iff_unsigned [of a b] by (auto simp add: equal_word_def)
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   142
qed
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   143
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   144
end
c550368a4e29 added quickcheck setup
haftmann
parents: 70348
diff changeset
   145
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   146
context ring_1
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   147
begin
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   148
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   149
lift_definition signed :: "'b::len word \<Rightarrow> 'a"
67907
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
   150
  is "of_int \<circ> signed_take_bit (LENGTH('b) - 1)"
72010
a851ce626b78 signed_take_bit
haftmann
parents: 71991
diff changeset
   151
  by (cases \<open>LENGTH('b)\<close>)
a851ce626b78 signed_take_bit
haftmann
parents: 71991
diff changeset
   152
    (simp_all add: signed_take_bit_eq_iff_take_bit_eq [symmetric])
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   153
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   154
lemma signed_0 [simp]:
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   155
  "signed 0 = 0"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   156
  by transfer simp
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   157
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   158
end
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   159
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   160
lemma unsigned_of_nat [simp]:
67907
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
   161
  "unsigned (of_nat n :: 'a word) = take_bit LENGTH('a::len) n"
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
   162
  by transfer (simp add: nat_eq_iff take_bit_eq_mod zmod_int)
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   163
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   164
lemma of_nat_unsigned [simp]:
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   165
  "of_nat (unsigned a) = a"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   166
  by transfer simp
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   167
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   168
lemma of_int_unsigned [simp]:
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   169
  "of_int (unsigned a) = a"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   170
  by transfer simp
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   171
70973
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   172
lemma unsigned_nat_less:
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
   173
  \<open>unsigned a < (2 ^ LENGTH('a) :: nat)\<close> for a :: \<open>'a::len word\<close>
70973
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   174
  by transfer (simp add: take_bit_eq_mod)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   175
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   176
lemma unsigned_int_less:
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
   177
  \<open>unsigned a < (2 ^ LENGTH('a) :: int)\<close> for a :: \<open>'a::len word\<close>
70973
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   178
  by transfer (simp add: take_bit_eq_mod)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   179
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   180
context ring_char_0
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   181
begin
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   182
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   183
lemma word_eq_iff_signed:
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   184
  "a = b \<longleftrightarrow> signed a = signed b"
67907
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
   185
  by safe (transfer; auto simp add: signed_take_bit_eq_iff_take_bit_eq)
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   186
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   187
end
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   188
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   189
lemma signed_of_int [simp]:
67907
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
   190
  "signed (of_int k :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) k"
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   191
  by transfer simp
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   192
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   193
lemma of_int_signed [simp]:
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   194
  "of_int (signed a) = a"
72079
8c355e2dd7db more consequent transferability
haftmann
parents: 72010
diff changeset
   195
  by transfer (simp_all add: take_bit_signed_take_bit)
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   196
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   197
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   198
subsubsection \<open>Properties\<close>
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   199
71196
29e7c6d11cf1 more rules
haftmann
parents: 71195
diff changeset
   200
lemma exp_eq_zero_iff:
29e7c6d11cf1 more rules
haftmann
parents: 71195
diff changeset
   201
  \<open>(2 :: 'a::len word) ^ n = 0 \<longleftrightarrow> LENGTH('a) \<le> n\<close>
29e7c6d11cf1 more rules
haftmann
parents: 71195
diff changeset
   202
  by transfer simp
29e7c6d11cf1 more rules
haftmann
parents: 71195
diff changeset
   203
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   204
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   205
subsubsection \<open>Division\<close>
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   206
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
   207
instantiation word :: (len) modulo
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   208
begin
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   209
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   210
lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
67907
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
   211
  is "\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b"
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   212
  by simp
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   213
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   214
lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
67907
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
   215
  is "\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b"
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   216
  by simp
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   217
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   218
instance ..
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   219
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   220
end
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   221
70973
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   222
lemma zero_word_div_eq [simp]:
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
   223
  \<open>0 div a = 0\<close> for a :: \<open>'a::len word\<close>
70973
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   224
  by transfer simp
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   225
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   226
lemma div_zero_word_eq [simp]:
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
   227
  \<open>a div 0 = 0\<close> for a :: \<open>'a::len word\<close>
70973
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   228
  by transfer simp
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   229
70927
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
   230
context
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
   231
  includes lifting_syntax
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
   232
begin
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
   233
70348
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   234
lemma [transfer_rule]:
70927
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
   235
  "(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)"
70348
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   236
proof -
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   237
  have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q")
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   238
    for k :: int
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   239
  proof
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   240
    assume ?P
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   241
    then show ?Q
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   242
      by auto
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   243
  next
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   244
    assume ?Q
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   245
    then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" ..
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   246
    then have "even (take_bit LENGTH('a) k)"
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   247
      by simp
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   248
    then show ?P
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   249
      by simp
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   250
  qed
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   251
  show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def])
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   252
    transfer_prover
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   253
qed
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   254
70927
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
   255
end
cc204e10385c tuned syntax
haftmann
parents: 70925
diff changeset
   256
70348
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   257
instance word :: (len) semiring_modulo
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   258
proof
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   259
  show "a div b * b + a mod b = a" for a b :: "'a word"
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   260
  proof transfer
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   261
    fix k l :: int
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   262
    define r :: int where "r = 2 ^ LENGTH('a)"
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   263
    then have r: "take_bit LENGTH('a) k = k mod r" for k
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   264
      by (simp add: take_bit_eq_mod)
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   265
    have "k mod r = ((k mod r) div (l mod r) * (l mod r)
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   266
      + (k mod r) mod (l mod r)) mod r"
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   267
      by (simp add: div_mult_mod_eq)
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   268
    also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   269
      + (k mod r) mod (l mod r)) mod r"
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   270
      by (simp add: mod_add_left_eq)
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   271
    also have "... = (((k mod r) div (l mod r) * l) mod r
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   272
      + (k mod r) mod (l mod r)) mod r"
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   273
      by (simp add: mod_mult_right_eq)
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   274
    finally have "k mod r = ((k mod r) div (l mod r) * l
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   275
      + (k mod r) mod (l mod r)) mod r"
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   276
      by (simp add: mod_simps)
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   277
    with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   278
      + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k"
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   279
      by simp
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   280
  qed
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   281
qed
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   282
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   283
instance word :: (len) semiring_parity
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   284
proof
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   285
  show "\<not> 2 dvd (1::'a word)"
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   286
    by transfer simp
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   287
  show even_iff_mod_2_eq_0: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   288
    for a :: "'a word"
71535
b612edee9b0c more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents: 71443
diff changeset
   289
    by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
70348
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   290
  show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   291
    for a :: "'a word"
71535
b612edee9b0c more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents: 71443
diff changeset
   292
    by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
70348
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   293
qed
bde161c740ca more theorems for proof of concept for word type
haftmann
parents: 70171
diff changeset
   294
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   295
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   296
subsubsection \<open>Orderings\<close>
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   297
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
   298
instantiation word :: (len) linorder
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   299
begin
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   300
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   301
lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
67907
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
   302
  is "\<lambda>a b. take_bit LENGTH('a) a \<le> take_bit LENGTH('a) b"
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   303
  by simp
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   304
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   305
lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
67907
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
   306
  is "\<lambda>a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b"
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   307
  by simp
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   308
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   309
instance
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   310
  by standard (transfer; auto)+
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   311
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   312
end
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   313
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   314
context linordered_semidom
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   315
begin
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   316
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   317
lemma word_less_eq_iff_unsigned:
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   318
  "a \<le> b \<longleftrightarrow> unsigned a \<le> unsigned b"
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   319
  by (transfer fixing: less_eq) (simp add: nat_le_eq_zle)
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   320
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   321
lemma word_less_iff_unsigned:
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   322
  "a < b \<longleftrightarrow> unsigned a < unsigned b"
67907
02a14c1cb917 prefer convention to place operation name before type name
haftmann
parents: 67816
diff changeset
   323
  by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative])
64015
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   324
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   325
end
c9f3a94cb825 proof of concept for algebraically founded word types
haftmann
parents:
diff changeset
   326
70973
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   327
lemma word_greater_zero_iff:
71954
13bb3f5cdc5b pragmatically ruled out word types of length zero: a bit string with no bits is not bit string at all
haftmann
parents: 71921
diff changeset
   328
  \<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len word\<close>
70973
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   329
  by transfer (simp add: less_le)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   330
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   331
lemma of_nat_word_eq_iff:
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   332
  \<open>of_nat m = (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   333
  by transfer (simp add: take_bit_of_nat)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   334
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   335
lemma of_nat_word_less_eq_iff:
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   336
  \<open>of_nat m \<le> (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   337
  by transfer (simp add: take_bit_of_nat)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   338
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   339
lemma of_nat_word_less_iff:
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   340
  \<open>of_nat m < (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m < take_bit LENGTH('a) n\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   341
  by transfer (simp add: take_bit_of_nat)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   342
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   343
lemma of_nat_word_eq_0_iff:
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   344
  \<open>of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   345
  using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   346
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   347
lemma of_int_word_eq_iff:
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   348
  \<open>of_int k = (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   349
  by transfer rule
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   350
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   351
lemma of_int_word_less_eq_iff:
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   352
  \<open>of_int k \<le> (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   353
  by transfer rule
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   354
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   355
lemma of_int_word_less_iff:
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   356
  \<open>of_int k < (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   357
  by transfer rule
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   358
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   359
lemma of_int_word_eq_0_iff:
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   360
  \<open>of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   361
  using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   362
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   363
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   364
subsection \<open>Bit structure on \<^typ>\<open>'a word\<close>\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   365
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   366
lemma word_bit_induct [case_names zero even odd]:
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   367
  \<open>P a\<close> if word_zero: \<open>P 0\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   368
    and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (2 * a)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   369
    and word_odd: \<open>\<And>a. P a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (1 + 2 * a)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   370
  for P and a :: \<open>'a::len word\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   371
proof -
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   372
  define m :: nat where \<open>m = LENGTH('a) - 1\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   373
  then have l: \<open>LENGTH('a) = Suc m\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   374
    by simp
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   375
  define n :: nat where \<open>n = unsigned a\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   376
  then have \<open>n < 2 ^ LENGTH('a)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   377
    by (simp add: unsigned_nat_less)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   378
  then have \<open>n < 2 * 2 ^ m\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   379
    by (simp add: l)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   380
  then have \<open>P (of_nat n)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   381
  proof (induction n rule: nat_bit_induct)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   382
    case zero
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   383
    show ?case
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   384
      by simp (rule word_zero)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   385
  next
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   386
    case (even n)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   387
    then have \<open>n < 2 ^ m\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   388
      by simp
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   389
    with even.IH have \<open>P (of_nat n)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   390
      by simp
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   391
    moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   392
      by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   393
    moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   394
      using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   395
      by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   396
    ultimately have \<open>P (2 * of_nat n)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   397
      by (rule word_even)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   398
    then show ?case
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   399
      by simp
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   400
  next
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   401
    case (odd n)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   402
    then have \<open>Suc n \<le> 2 ^ m\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   403
      by simp
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   404
    with odd.IH have \<open>P (of_nat n)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   405
      by simp
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   406
    moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   407
      using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   408
      by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   409
    ultimately have \<open>P (1 + 2 * of_nat n)\<close>
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   410
      by (rule word_odd)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   411
    then show ?case
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   412
      by simp
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   413
  qed
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   414
  then show ?thesis
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   415
    by (simp add: n_def)
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   416
qed
a7a52ba0717d more lemmas
haftmann
parents: 70927
diff changeset
   417
71042
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   418
lemma bit_word_half_eq:
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   419
  \<open>(of_bool b + a * 2) div 2 = a\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   420
    if \<open>a < 2 ^ (LENGTH('a) - Suc 0)\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   421
    for a :: \<open>'a::len word\<close>
71195
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   422
proof (cases \<open>2 \<le> LENGTH('a::len)\<close>)
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   423
  case False
71042
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   424
  have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   425
    by auto
71195
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   426
  with False that show ?thesis
71535
b612edee9b0c more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents: 71443
diff changeset
   427
    by transfer (simp add: eq_iff)
71042
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   428
next
71195
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   429
  case True
71042
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   430
  obtain n where length: \<open>LENGTH('a) = Suc n\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   431
    by (cases \<open>LENGTH('a)\<close>) simp_all
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   432
  show ?thesis proof (cases b)
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   433
    case False
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   434
    moreover have \<open>a * 2 div 2 = a\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   435
    using that proof transfer
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   436
      fix k :: int
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   437
      from length have \<open>k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   438
        by simp
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   439
      moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   440
      with \<open>LENGTH('a) = Suc n\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   441
      have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   442
        by (simp add: take_bit_eq_mod divmod_digit_0)
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   443
      ultimately have \<open>take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   444
        by (simp add: take_bit_eq_mod)
71195
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   445
      with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2)
71042
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   446
        = take_bit LENGTH('a) k\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   447
        by simp
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   448
    qed
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   449
    ultimately show ?thesis
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   450
      by simp
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   451
  next
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   452
    case True
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   453
    moreover have \<open>(1 + a * 2) div 2 = a\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   454
    using that proof transfer
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   455
      fix k :: int
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   456
      from length have \<open>(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   457
        using pos_zmod_mult_2 [of \<open>2 ^ n\<close> k] by (simp add: ac_simps)
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   458
      moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   459
      with \<open>LENGTH('a) = Suc n\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   460
      have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   461
        by (simp add: take_bit_eq_mod divmod_digit_0)
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   462
      ultimately have \<open>take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\<close>
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   463
        by (simp add: take_bit_eq_mod)
71195
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   464
      with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2)
71042
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   465
        = take_bit LENGTH('a) k\<close>
71535
b612edee9b0c more frugal simp rules for bit operations; more pervasive use of bit selector
haftmann
parents: 71443
diff changeset
   466
        by (auto simp add: take_bit_Suc)
71042
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   467
    qed
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   468
    ultimately show ?thesis
400e9512f1d3 proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents: 70973
diff changeset
   469
      by simp
70925
525853e4ec80 bit operations for word type
haftmann
parents: 70903
diff changeset
   470
  qed
525853e4ec80 bit operations for word type
haftmann
parents: 70903
diff changeset
   471
qed
525853e4ec80 bit operations for word type
haftmann
parents: 70903
diff changeset
   472
71409
0bb0cb558bf9 sketches of ideas still to come
haftmann
parents: 71196
diff changeset
   473
lemma even_mult_exp_div_word_iff:
0bb0cb558bf9 sketches of ideas still to come
haftmann
parents: 71196
diff changeset
   474
  \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> \<not> (
0bb0cb558bf9 sketches of ideas still to come
haftmann
parents: 71196
diff changeset
   475
    m \<le> n \<and>
0bb0cb558bf9 sketches of ideas still to come
haftmann
parents: 71196
diff changeset
   476
    n < LENGTH('a) \<and> odd (a div 2 ^ (n - m)))\<close> for a :: \<open>'a::len word\<close>
0bb0cb558bf9 sketches of ideas still to come
haftmann
parents: 71196
diff changeset
   477
  by transfer
0bb0cb558bf9 sketches of ideas still to come
haftmann
parents: 71196
diff changeset
   478
    (auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff,
71412
96d126844adc more theorems
haftmann
parents: 71409
diff changeset
   479
      simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int)
71409
0bb0cb558bf9 sketches of ideas still to come
haftmann
parents: 71196
diff changeset
   480
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   481
instantiation word :: (len) semiring_bits
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   482
begin
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   483
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   484
lift_definition bit_word :: \<open>'a word \<Rightarrow> nat \<Rightarrow> bool\<close>
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   485
  is \<open>\<lambda>k n. n < LENGTH('a) \<and> bit k n\<close>
71094
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   486
proof
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   487
  fix k l :: int and n :: nat
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   488
  assume *: \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   489
  show \<open>n < LENGTH('a) \<and> bit k n \<longleftrightarrow> n < LENGTH('a) \<and> bit l n\<close>
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   490
  proof (cases \<open>n < LENGTH('a)\<close>)
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   491
    case True
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   492
    from * have \<open>bit (take_bit LENGTH('a) k) n \<longleftrightarrow> bit (take_bit LENGTH('a) l) n\<close>
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   493
      by simp
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   494
    then show ?thesis
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   495
      by (simp add: bit_take_bit_iff)
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   496
  next
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   497
    case False
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   498
    then show ?thesis
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   499
      by simp
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   500
  qed
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   501
qed
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   502
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   503
instance proof
71094
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   504
  show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   505
    and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   506
  for P and a :: \<open>'a word\<close>
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   507
  proof (induction a rule: word_bit_induct)
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   508
    case zero
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   509
    from stable [of 0] show ?case
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   510
      by simp
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   511
  next
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   512
    case (even a)
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   513
    with rec [of a False] show ?case
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   514
      using bit_word_half_eq [of a False] by (simp add: ac_simps)
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   515
  next
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   516
    case (odd a)
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   517
    with rec [of a True] show ?case
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   518
      using bit_word_half_eq [of a True] by (simp add: ac_simps)
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   519
  qed
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   520
  show \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close> for a :: \<open>'a word\<close> and n
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   521
    by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit bit_iff_odd_drop_bit)
71138
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   522
  show \<open>0 div a = 0\<close>
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   523
    for a :: \<open>'a word\<close>
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   524
    by transfer simp
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   525
  show \<open>a div 1 = a\<close>
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   526
    for a :: \<open>'a word\<close>
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   527
    by transfer simp
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   528
  show \<open>a mod b div b = 0\<close>
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   529
    for a b :: \<open>'a word\<close>
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   530
    apply transfer
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   531
    apply (simp add: take_bit_eq_mod)
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   532
    apply (subst (3) mod_pos_pos_trivial [of _ \<open>2 ^ LENGTH('a)\<close>])
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   533
      apply simp_all
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   534
     apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power)
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   535
    using pos_mod_bound [of \<open>2 ^ LENGTH('a)\<close>] apply simp
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   536
  proof -
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   537
    fix aa :: int and ba :: int
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   538
    have f1: "\<And>i n. (i::int) mod 2 ^ n = 0 \<or> 0 < i mod 2 ^ n"
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   539
      by (metis le_less take_bit_eq_mod take_bit_nonnegative)
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   540
    have "(0::int) < 2 ^ len_of (TYPE('a)::'a itself) \<and> ba mod 2 ^ len_of (TYPE('a)::'a itself) \<noteq> 0 \<or> aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)"
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   541
      by (metis (no_types) mod_by_0 unique_euclidean_semiring_numeral_class.pos_mod_bound zero_less_numeral zero_less_power)
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   542
    then show "aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)"
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   543
      using f1 by (meson le_less less_le_trans unique_euclidean_semiring_numeral_class.pos_mod_bound)
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   544
  qed
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   545
  show \<open>(1 + a) div 2 = a div 2\<close>
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   546
    if \<open>even a\<close>
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   547
    for a :: \<open>'a word\<close>
71822
67cc2319104f prefer _ mod 2 over of_bool (odd _)
haftmann
parents: 71760
diff changeset
   548
    using that by transfer
67cc2319104f prefer _ mod 2 over of_bool (odd _)
haftmann
parents: 71760
diff changeset
   549
      (auto dest: le_Suc_ex simp add: mod_2_eq_odd take_bit_Suc elim!: evenE)
71182
410935efbf5c characterization of singleton bit operation
haftmann
parents: 71181
diff changeset
   550
  show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
410935efbf5c characterization of singleton bit operation
haftmann
parents: 71181
diff changeset
   551
    for m n :: nat
410935efbf5c characterization of singleton bit operation
haftmann
parents: 71181
diff changeset
   552
    by transfer (simp, simp add: exp_div_exp_eq)
71138
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   553
  show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)"
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   554
    for a :: "'a word" and m n :: nat
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   555
    apply transfer
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   556
    apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div)
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   557
    apply (simp add: drop_bit_take_bit)
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   558
    done
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   559
  show "a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n"
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   560
    for a :: "'a word" and m n :: nat
71195
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   561
    by transfer (auto simp flip: take_bit_eq_mod simp add: ac_simps)
71138
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   562
  show \<open>a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m\<close>
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   563
    if \<open>m \<le> n\<close> for a :: "'a word" and m n :: nat
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   564
    using that apply transfer
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   565
    apply (auto simp flip: take_bit_eq_mod)
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   566
           apply (auto simp flip: push_bit_eq_mult simp add: push_bit_take_bit split: split_min_lin)
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   567
    done
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   568
  show \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
9de7f1067520 strengthened type class for bit operations
haftmann
parents: 71095
diff changeset
   569
    for a :: "'a word" and m n :: nat
71195
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   570
    by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin)
71413
65ffe9e910d4 more specific class assumptions
haftmann
parents: 71412
diff changeset
   571
  show \<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a word) \<or> m \<le> n\<close>
65ffe9e910d4 more specific class assumptions
haftmann
parents: 71412
diff changeset
   572
    for m n :: nat
65ffe9e910d4 more specific class assumptions
haftmann
parents: 71412
diff changeset
   573
    by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)
71424
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
   574
  show \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::'a word) ^ n = 0 \<or> m \<le> n \<and> even (a div 2 ^ (n - m))\<close>
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
   575
    for a :: \<open>'a word\<close> and m n :: nat
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
   576
  proof transfer
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
   577
    show \<open>even (take_bit LENGTH('a) (k * 2 ^ m) div take_bit LENGTH('a) (2 ^ n)) \<longleftrightarrow>
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
   578
      n < m
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
   579
      \<or> take_bit LENGTH('a) ((2::int) ^ n) = take_bit LENGTH('a) 0
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
   580
      \<or> (m \<le> n \<and> even (take_bit LENGTH('a) k div take_bit LENGTH('a) (2 ^ (n - m))))\<close>
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
   581
    for m n :: nat and k l :: int
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
   582
      by (auto simp flip: take_bit_eq_mod drop_bit_eq_div push_bit_eq_mult
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
   583
        simp add: div_push_bit_of_1_eq_drop_bit drop_bit_take_bit drop_bit_push_bit_int [of n m])
e83fe2c31088 rule concerning bit (push_bit ...)
haftmann
parents: 71418
diff changeset
   584
  qed
71094
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   585
qed
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   586
71183
eda1ef0090ef transfer rule for bit operation
haftmann
parents: 71182
diff changeset
   587
end
eda1ef0090ef transfer rule for bit operation
haftmann
parents: 71182
diff changeset
   588
71094
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   589
instantiation word :: (len) semiring_bit_shifts
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   590
begin
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   591
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   592
lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   593
  is push_bit
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   594
proof -
71195
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   595
  show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close>
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   596
    if \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> for k l :: int and n :: nat
71094
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   597
  proof -
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   598
    from that
71195
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   599
    have \<open>take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k)
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   600
      = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\<close>
71094
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   601
      by simp
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   602
    moreover have \<open>min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\<close>
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   603
      by simp
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   604
    ultimately show ?thesis
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   605
      by (simp add: take_bit_push_bit)
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   606
  qed
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   607
qed
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   608
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   609
lift_definition drop_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   610
  is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close>
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   611
  by (simp add: take_bit_eq_mod)
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   612
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   613
lift_definition take_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   614
  is \<open>\<lambda>n. take_bit (min LENGTH('a) n)\<close>
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   615
  by (simp add: ac_simps) (simp only: flip: take_bit_take_bit)
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   616
71094
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   617
instance proof
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   618
  show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: "'a word"
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   619
    by transfer (simp add: push_bit_eq_mult)
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   620
  show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: "'a word"
71195
d50a718ccf35 tuned material
haftmann
parents: 71186
diff changeset
   621
    by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   622
  show \<open>take_bit n a = a mod 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   623
    by transfer (auto simp flip: take_bit_eq_mod)
71094
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   624
qed
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   625
70925
525853e4ec80 bit operations for word type
haftmann
parents: 70903
diff changeset
   626
end
71094
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   627
71095
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   628
instantiation word :: (len) ring_bit_operations
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   629
begin
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   630
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   631
lift_definition not_word :: "'a word \<Rightarrow> 'a word"
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   632
  is not
71418
bd9d27ccb3a3 more theorems
haftmann
parents: 71413
diff changeset
   633
  by (simp add: take_bit_not_iff)
71095
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   634
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   635
lift_definition and_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
71409
0bb0cb558bf9 sketches of ideas still to come
haftmann
parents: 71196
diff changeset
   636
  is \<open>and\<close>
71095
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   637
  by simp
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   638
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   639
lift_definition or_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   640
  is or
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   641
  by simp
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   642
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   643
lift_definition xor_word ::  "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   644
  is xor
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   645
  by simp
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   646
72082
41393ecb57ac uniform mask operation
haftmann
parents: 72079
diff changeset
   647
lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
41393ecb57ac uniform mask operation
haftmann
parents: 72079
diff changeset
   648
  is mask .
41393ecb57ac uniform mask operation
haftmann
parents: 72079
diff changeset
   649
41393ecb57ac uniform mask operation
haftmann
parents: 72079
diff changeset
   650
instance by (standard; transfer)
41393ecb57ac uniform mask operation
haftmann
parents: 72079
diff changeset
   651
  (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
41393ecb57ac uniform mask operation
haftmann
parents: 72079
diff changeset
   652
    bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)
71095
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   653
71094
a197532693a5 bit shifts as class operations
haftmann
parents: 71093
diff changeset
   654
end
71095
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   655
71854
6a51e64ba13d slightly more specific implementations
haftmann
parents: 71822
diff changeset
   656
definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close>
6a51e64ba13d slightly more specific implementations
haftmann
parents: 71822
diff changeset
   657
  where [code_abbrev]: \<open>even_word = even\<close>
6a51e64ba13d slightly more specific implementations
haftmann
parents: 71822
diff changeset
   658
6a51e64ba13d slightly more specific implementations
haftmann
parents: 71822
diff changeset
   659
lemma even_word_iff [code]:
6a51e64ba13d slightly more specific implementations
haftmann
parents: 71822
diff changeset
   660
  \<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
71921
a238074c5a9d avoid overaggressive default simp rules
haftmann
parents: 71854
diff changeset
   661
  by (simp add: even_word_def and_one_eq even_iff_mod_2_eq_zero)
71854
6a51e64ba13d slightly more specific implementations
haftmann
parents: 71822
diff changeset
   662
71965
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   663
lemma bit_word_iff_drop_bit_and [code]:
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   664
  \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
d45f5d4c41bd more class operations for the sake of efficient generated code
haftmann
parents: 71956
diff changeset
   665
  by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq)
71854
6a51e64ba13d slightly more specific implementations
haftmann
parents: 71822
diff changeset
   666
71443
ff6394cfc05c canonical approach towards lifting
haftmann
parents: 71424
diff changeset
   667
lifting_update word.lifting
ff6394cfc05c canonical approach towards lifting
haftmann
parents: 71424
diff changeset
   668
lifting_forget word.lifting
ff6394cfc05c canonical approach towards lifting
haftmann
parents: 71424
diff changeset
   669
71095
038727567817 tuned order between theories
haftmann
parents: 71094
diff changeset
   670
end