src/HOL/Word/WordArith.thy
author haftmann
Tue, 04 May 2010 08:55:43 +0200
changeset 36635 080b755377c0
parent 32149 ef59550a55d3
child 37117 59cee8807c29
permissions -rw-r--r--
locale predicates of classes carry a mandatory "class" prefix
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     1
(* 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     2
    Author:     Jeremy Dawson and Gerwin Klein, NICTA
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     3
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     4
  contains arithmetic theorems for word, instantiations to
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     5
  arithmetic type classes and tactics for reducing word arithmetic
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     6
  to linear arithmetic on int or nat
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     7
*) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     8
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
     9
header {* Word Arithmetic *}
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
    10
26560
haftmann
parents: 26514
diff changeset
    11
theory WordArith
haftmann
parents: 26514
diff changeset
    12
imports WordDefinition
haftmann
parents: 26514
diff changeset
    13
begin
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    14
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    15
lemma word_less_alt: "(a < b) = (uint a < uint b)"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    16
  unfolding word_less_def word_le_def
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    17
  by (auto simp del: word_uint.Rep_inject 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    18
           simp: word_uint.Rep_inject [symmetric])
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    19
36635
080b755377c0 locale predicates of classes carry a mandatory "class" prefix
haftmann
parents: 32149
diff changeset
    20
lemma signed_linorder: "class.linorder word_sle word_sless"
28823
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28059
diff changeset
    21
proof
dcbef866c9e2 tuned unfold_locales invocation
haftmann
parents: 28059
diff changeset
    22
qed (unfold word_sle_def word_sless_def, auto)
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    23
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30686
diff changeset
    24
interpretation signed: linorder "word_sle" "word_sless"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    25
  by (rule signed_linorder)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    26
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25350
diff changeset
    27
lemmas word_arith_wis = 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    28
  word_add_def word_mult_def word_minus_def 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    29
  word_succ_def word_pred_def word_0_wi word_1_wi
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    30
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    31
lemma udvdI: 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    32
  "0 \<le> n ==> uint b = n * uint a ==> a udvd b"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    33
  by (auto simp: udvd_def)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    34
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    35
lemmas word_div_no [simp] = 
25350
a5fcf6d12a53 eliminated illegal schematic variables in where/of;
wenzelm
parents: 25134
diff changeset
    36
  word_div_def [of "number_of a" "number_of b", standard]
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    37
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    38
lemmas word_mod_no [simp] = 
25350
a5fcf6d12a53 eliminated illegal schematic variables in where/of;
wenzelm
parents: 25134
diff changeset
    39
  word_mod_def [of "number_of a" "number_of b", standard]
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    40
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    41
lemmas word_less_no [simp] = 
25350
a5fcf6d12a53 eliminated illegal schematic variables in where/of;
wenzelm
parents: 25134
diff changeset
    42
  word_less_def [of "number_of a" "number_of b", standard]
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    43
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    44
lemmas word_le_no [simp] = 
25350
a5fcf6d12a53 eliminated illegal schematic variables in where/of;
wenzelm
parents: 25134
diff changeset
    45
  word_le_def [of "number_of a" "number_of b", standard]
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    46
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    47
lemmas word_sless_no [simp] = 
25350
a5fcf6d12a53 eliminated illegal schematic variables in where/of;
wenzelm
parents: 25134
diff changeset
    48
  word_sless_def [of "number_of a" "number_of b", standard]
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    49
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    50
lemmas word_sle_no [simp] = 
25350
a5fcf6d12a53 eliminated illegal schematic variables in where/of;
wenzelm
parents: 25134
diff changeset
    51
  word_sle_def [of "number_of a" "number_of b", standard]
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    52
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    53
(* following two are available in class number_ring, 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    54
  but convenient to have them here here;
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    55
  note - the number_ring versions, numeral_0_eq_0 and numeral_1_eq_1
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    56
  are in the default simpset, so to use the automatic simplifications for
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    57
  (eg) sint (number_of bin) on sint 1, must do
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    58
  (simp add: word_1_no del: numeral_1_eq_1) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    59
  *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    60
lemmas word_0_wi_Pls = word_0_wi [folded Pls_def]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    61
lemmas word_0_no = word_0_wi_Pls [folded word_no_wi]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    62
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
    63
lemma int_one_bin: "(1 :: int) == (Int.Pls BIT bit.B1)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    64
  unfolding Pls_def Bit_def by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    65
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    66
lemma word_1_no: 
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
    67
  "(1 :: 'a :: len0 word) == number_of (Int.Pls BIT bit.B1)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    68
  unfolding word_1_wi word_number_of_def int_one_bin by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    69
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    70
lemma word_m1_wi: "-1 == word_of_int -1" 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    71
  by (rule word_number_of_alt)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    72
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
    73
lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    74
  by (simp add: word_m1_wi number_of_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    75
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    76
lemma word_0_bl: "of_bl [] = 0" 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    77
  unfolding word_0_wi of_bl_def by (simp add : Pls_def)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    78
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    79
lemma word_1_bl: "of_bl [True] = 1" 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    80
  unfolding word_1_wi of_bl_def
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    81
  by (simp add : bl_to_bin_def Bit_def Pls_def)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    82
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    83
lemma uint_0 [simp] : "(uint 0 = 0)" 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    84
  unfolding word_0_wi
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    85
  by (simp add: word_ubin.eq_norm Pls_def [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    86
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    87
lemma of_bl_0 [simp] : "of_bl (replicate n False) = 0"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    88
  by (simp add : word_0_wi of_bl_def bl_to_bin_rep_False Pls_def)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    89
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    90
lemma to_bl_0: 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    91
  "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    92
  unfolding uint_bl
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    93
  by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric])
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
    94
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    95
lemma uint_0_iff: "(uint x = 0) = (x = 0)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    96
  by (auto intro!: word_uint.Rep_eqD)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    97
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    98
lemma unat_0_iff: "(unat x = 0) = (x = 0)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    99
  unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   100
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   101
lemma unat_0 [simp]: "unat 0 = 0"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   102
  unfolding unat_def by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   103
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   104
lemma size_0_same': "size w = 0 ==> w = (v :: 'a :: len0 word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   105
  apply (unfold word_size)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   106
  apply (rule box_equals)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   107
    defer
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   108
    apply (rule word_uint.Rep_inverse)+
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   109
  apply (rule word_ubin.norm_eq_iff [THEN iffD1])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   110
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   111
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   112
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   113
lemmas size_0_same = size_0_same' [folded word_size]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   114
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   115
lemmas unat_eq_0 = unat_0_iff
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   116
lemmas unat_eq_zero = unat_0_iff
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   117
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   118
lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   119
by (auto simp: unat_0_iff [symmetric])
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   120
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   121
lemma ucast_0 [simp] : "ucast 0 = 0"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   122
unfolding ucast_def
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   123
by simp (simp add: word_0_wi)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   124
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   125
lemma sint_0 [simp] : "sint 0 = 0"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   126
unfolding sint_uint
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   127
by (simp add: Pls_def [symmetric])
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   128
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   129
lemma scast_0 [simp] : "scast 0 = 0"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   130
apply (unfold scast_def)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   131
apply simp
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   132
apply (simp add: word_0_wi)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   133
done
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   134
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   135
lemma sint_n1 [simp] : "sint -1 = -1"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   136
apply (unfold word_m1_wi_Min)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   137
apply (simp add: word_sbin.eq_norm)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   138
apply (unfold Min_def number_of_eq)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   139
apply simp
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
   140
done
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   141
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   142
lemma scast_n1 [simp] : "scast -1 = -1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   143
  apply (unfold scast_def sint_n1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   144
  apply (unfold word_number_of_alt)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   145
  apply (rule refl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   146
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   147
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   148
lemma uint_1 [simp] : "uint (1 :: 'a :: len word) = 1"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   149
  unfolding word_1_wi
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   150
  by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   151
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   152
lemma unat_1 [simp] : "unat (1 :: 'a :: len word) = 1"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   153
  by (unfold unat_def uint_1) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   154
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   155
lemma ucast_1 [simp] : "ucast (1 :: 'a :: len word) = 1"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   156
  unfolding ucast_def word_1_wi
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   157
  by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   158
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   159
(* abstraction preserves the operations
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   160
  (the definitions tell this for bins in range uint) *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   161
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   162
lemmas arths = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   163
  bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1],
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   164
                folded word_ubin.eq_norm, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   165
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   166
lemma wi_homs: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   167
  shows
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   168
  wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   169
  wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   170
  wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   171
  wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Int.succ a)" and
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   172
  wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   173
  by (auto simp: word_arith_wis arths)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   174
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   175
lemmas wi_hom_syms = wi_homs [symmetric]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   176
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   177
lemma word_sub_def: "a - b == a + - (b :: 'a :: len0 word)"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   178
  unfolding word_sub_wi diff_def
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   179
  by (simp only : word_uint.Rep_inverse wi_hom_syms)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   180
    
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   181
lemmas word_diff_minus = word_sub_def [THEN meta_eq_to_obj_eq, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   182
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   183
lemma word_of_int_sub_hom:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   184
  "(word_of_int a) - word_of_int b = word_of_int (a - b)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   185
  unfolding word_sub_def diff_def by (simp only : wi_homs)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   186
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   187
lemmas new_word_of_int_homs = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   188
  word_of_int_sub_hom wi_homs word_0_wi word_1_wi 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   189
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   190
lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   191
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   192
lemmas word_of_int_hom_syms =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   193
  new_word_of_int_hom_syms [unfolded succ_def pred_def]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   194
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   195
lemmas word_of_int_homs =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   196
  new_word_of_int_homs [unfolded succ_def pred_def]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   197
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   198
lemmas word_of_int_add_hom = word_of_int_homs (2)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   199
lemmas word_of_int_mult_hom = word_of_int_homs (3)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   200
lemmas word_of_int_minus_hom = word_of_int_homs (4)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   201
lemmas word_of_int_succ_hom = word_of_int_homs (5)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   202
lemmas word_of_int_pred_hom = word_of_int_homs (6)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   203
lemmas word_of_int_0_hom = word_of_int_homs (7)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   204
lemmas word_of_int_1_hom = word_of_int_homs (8)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   205
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   206
(* now, to get the weaker results analogous to word_div/mod_def *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   207
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   208
lemmas word_arith_alts = 
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25350
diff changeset
   209
  word_sub_wi [unfolded succ_def pred_def, standard]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   210
  word_arith_wis [unfolded succ_def pred_def, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   211
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   212
lemmas word_sub_alt = word_arith_alts (1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   213
lemmas word_add_alt = word_arith_alts (2)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   214
lemmas word_mult_alt = word_arith_alts (3)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   215
lemmas word_minus_alt = word_arith_alts (4)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   216
lemmas word_succ_alt = word_arith_alts (5)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   217
lemmas word_pred_alt = word_arith_alts (6)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   218
lemmas word_0_alt = word_arith_alts (7)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   219
lemmas word_1_alt = word_arith_alts (8)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   220
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
   221
subsection  "Transferring goals from words to ints"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   222
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   223
lemma word_ths:  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   224
  shows
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   225
  word_succ_p1:   "word_succ a = a + 1" and
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   226
  word_pred_m1:   "word_pred a = a - 1" and
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   227
  word_pred_succ: "word_pred (word_succ a) = a" and
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   228
  word_succ_pred: "word_succ (word_pred a) = a" and
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   229
  word_mult_succ: "word_succ a * b = b + a * b"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   230
  by (rule word_uint.Abs_cases [of b],
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   231
      rule word_uint.Abs_cases [of a],
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   232
      simp add: pred_def succ_def add_commute mult_commute 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   233
                ring_distribs new_word_of_int_homs)+
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   234
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   235
lemmas uint_cong = arg_cong [where f = uint]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   236
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   237
lemmas uint_word_ariths = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   238
  word_arith_alts [THEN trans [OF uint_cong int_word_uint], standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   239
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   240
lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   241
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   242
(* similar expressions for sint (arith operations) *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   243
lemmas sint_word_ariths = uint_word_arith_bintrs
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   244
  [THEN uint_sint [symmetric, THEN trans],
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   245
  unfolded uint_sint bintr_arith1s bintr_ariths 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   246
    len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep, standard]
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   247
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   248
lemmas uint_div_alt = word_div_def
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25350
diff changeset
   249
  [THEN trans [OF uint_cong int_word_uint], standard]
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   250
lemmas uint_mod_alt = word_mod_def
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25350
diff changeset
   251
  [THEN trans [OF uint_cong int_word_uint], standard]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   252
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   253
lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   254
  unfolding word_pred_def number_of_eq
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   255
  by (simp add : pred_def word_no_wi)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   256
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   257
lemma word_pred_0_Min: "word_pred 0 = word_of_int Int.Min"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   258
  by (simp add: word_pred_0_n1 number_of_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   259
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   260
lemma word_m1_Min: "- 1 = word_of_int Int.Min"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   261
  unfolding Min_def by (simp only: word_of_int_hom_syms)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   262
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   263
lemma succ_pred_no [simp]:
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   264
  "word_succ (number_of bin) = number_of (Int.succ bin) & 
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   265
    word_pred (number_of bin) = number_of (Int.pred bin)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   266
  unfolding word_number_of_def by (simp add : new_word_of_int_homs)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   267
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   268
lemma word_sp_01 [simp] : 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   269
  "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   270
  by (unfold word_0_no word_1_no) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   271
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   272
(* alternative approach to lifting arithmetic equalities *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   273
lemma word_of_int_Ex:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   274
  "\<exists>y. x = word_of_int y"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   275
  by (rule_tac x="uint x" in exI) simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   276
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   277
lemma word_arith_eqs:
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   278
  fixes a :: "'a::len0 word"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   279
  fixes b :: "'a::len0 word"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   280
  shows
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   281
  word_add_0: "0 + a = a" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   282
  word_add_0_right: "a + 0 = a" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   283
  word_mult_1: "1 * a = a" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   284
  word_mult_1_right: "a * 1 = a" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   285
  word_add_commute: "a + b = b + a" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   286
  word_add_assoc: "a + b + c = a + (b + c)" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   287
  word_add_left_commute: "a + (b + c) = b + (a + c)" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   288
  word_mult_commute: "a * b = b * a" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   289
  word_mult_assoc: "a * b * c = a * (b * c)" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   290
  word_mult_left_commute: "a * (b * c) = b * (a * c)" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   291
  word_left_distrib: "(a + b) * c = a * c + b * c" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   292
  word_right_distrib: "a * (b + c) = a * b + a * c" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   293
  word_left_minus: "- a + a = 0" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   294
  word_diff_0_right: "a - 0 = a" and
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   295
  word_diff_self: "a - a = 0"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   296
  using word_of_int_Ex [of a] 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   297
        word_of_int_Ex [of b] 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   298
        word_of_int_Ex [of c]
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   299
  by (auto simp: word_of_int_hom_syms [symmetric]
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   300
                 zadd_0_right add_commute add_assoc add_left_commute
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   301
                 mult_commute mult_assoc mult_left_commute
28059
295a8fc92684 fixed names of class assumptions
haftmann
parents: 27682
diff changeset
   302
                 left_distrib right_distrib)
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   303
  
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   304
lemmas word_add_ac = word_add_commute word_add_assoc word_add_left_commute
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   305
lemmas word_mult_ac = word_mult_commute word_mult_assoc word_mult_left_commute
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   306
  
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   307
lemmas word_plus_ac0 = word_add_0 word_add_0_right word_add_ac
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   308
lemmas word_times_ac1 = word_mult_1 word_mult_1_right word_mult_ac
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   309
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   310
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
   311
subsection "Order on fixed-length words"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   312
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   313
lemma word_order_trans: "x <= y ==> y <= z ==> x <= (z :: 'a :: len0 word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   314
  unfolding word_le_def by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   315
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   316
lemma word_order_refl: "z <= (z :: 'a :: len0 word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   317
  unfolding word_le_def by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   318
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   319
lemma word_order_antisym: "x <= y ==> y <= x ==> x = (y :: 'a :: len0 word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   320
  unfolding word_le_def by (auto intro!: word_uint.Rep_eqD)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   321
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   322
lemma word_order_linear:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   323
  "y <= x | x <= (y :: 'a :: len0 word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   324
  unfolding word_le_def by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   325
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   326
lemma word_zero_le [simp] :
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   327
  "0 <= (y :: 'a :: len0 word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   328
  unfolding word_le_def by auto
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   329
  
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   330
instance word :: (len0) semigroup_add
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   331
  by intro_classes (simp add: word_add_assoc)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   332
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   333
instance word :: (len0) linorder
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   334
  by intro_classes (auto simp: word_less_def word_le_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   335
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   336
instance word :: (len0) ring
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   337
  by intro_classes
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   338
     (auto simp: word_arith_eqs word_diff_minus 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   339
                 word_diff_self [unfolded word_diff_minus])
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   340
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   341
lemma word_m1_ge [simp] : "word_pred 0 >= y"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   342
  unfolding word_le_def
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   343
  by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   344
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   345
lemmas word_n1_ge [simp]  = word_m1_ge [simplified word_sp_01]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   346
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   347
lemmas word_not_simps [simp] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   348
  word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   349
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   350
lemma word_gt_0: "0 < y = (0 ~= (y :: 'a :: len0 word))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   351
  unfolding word_less_def by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   352
25350
a5fcf6d12a53 eliminated illegal schematic variables in where/of;
wenzelm
parents: 25134
diff changeset
   353
lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of y", standard]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   354
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   355
lemma word_sless_alt: "(a <s b) == (sint a < sint b)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   356
  unfolding word_sle_def word_sless_def
27682
25aceefd4786 added class preorder
haftmann
parents: 26560
diff changeset
   357
  by (auto simp add: less_le)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   358
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   359
lemma word_le_nat_alt: "(a <= b) = (unat a <= unat b)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   360
  unfolding unat_def word_le_def
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   361
  by (rule nat_le_eq_zle [symmetric]) simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   362
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   363
lemma word_less_nat_alt: "(a < b) = (unat a < unat b)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   364
  unfolding unat_def word_less_alt
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   365
  by (rule nat_less_eq_zless [symmetric]) simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   366
  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   367
lemma wi_less: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   368
  "(word_of_int n < (word_of_int m :: 'a :: len0 word)) = 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   369
    (n mod 2 ^ len_of TYPE('a) < m mod 2 ^ len_of TYPE('a))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   370
  unfolding word_less_alt by (simp add: word_uint.eq_norm)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   371
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   372
lemma wi_le: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   373
  "(word_of_int n <= (word_of_int m :: 'a :: len0 word)) = 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   374
    (n mod 2 ^ len_of TYPE('a) <= m mod 2 ^ len_of TYPE('a))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   375
  unfolding word_le_def by (simp add: word_uint.eq_norm)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   376
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   377
lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   378
  apply (unfold udvd_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   379
  apply safe
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   380
   apply (simp add: unat_def nat_mult_distrib)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   381
  apply (simp add: uint_nat int_mult)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   382
  apply (rule exI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   383
  apply safe
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   384
   prefer 2
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   385
   apply (erule notE)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   386
   apply (rule refl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   387
  apply force
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   388
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   389
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   390
lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   391
  unfolding dvd_def udvd_nat_alt by force
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   392
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   393
lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
24378
af83eeb4a702 move udvd, div and mod stuff from WordDefinition to WordArith
huffman
parents: 24377
diff changeset
   394
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   395
lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) ==> (0 :: 'a word) ~= 1";
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   396
  unfolding word_arith_wis
28959
9d35303719b5 fixed proofs due to changes in Int.thy
huffman
parents: 28823
diff changeset
   397
  by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   398
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   399
lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   400
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   401
lemma no_no [simp] : "number_of (number_of b) = number_of b"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   402
  by (simp add: number_of_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   403
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   404
lemma unat_minus_one: "x ~= 0 ==> unat (x - 1) = unat x - 1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   405
  apply (unfold unat_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   406
  apply (simp only: int_word_uint word_arith_alts rdmods)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   407
  apply (subgoal_tac "uint x >= 1")
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   408
   prefer 2
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   409
   apply (drule contrapos_nn)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   410
    apply (erule word_uint.Rep_inverse' [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   411
   apply (insert uint_ge_0 [of x])[1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   412
   apply arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   413
  apply (rule box_equals)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   414
    apply (rule nat_diff_distrib)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   415
     prefer 2
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   416
     apply assumption
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   417
    apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   418
   apply (subst mod_pos_pos_trivial)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   419
     apply arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   420
    apply (insert uint_lt2p [of x])[1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   421
    apply arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   422
   apply (rule refl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   423
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   424
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   425
    
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   426
lemma measure_unat: "p ~= 0 ==> unat (p - 1) < unat p"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   427
  by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   428
  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   429
lemmas uint_add_ge0 [simp] =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   430
  add_nonneg_nonneg [OF uint_ge_0 uint_ge_0, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   431
lemmas uint_mult_ge0 [simp] =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   432
  mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   433
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   434
lemma uint_sub_lt2p [simp]: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   435
  "uint (x :: 'a :: len0 word) - uint (y :: 'b :: len0 word) < 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   436
    2 ^ len_of TYPE('a)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   437
  using uint_ge_0 [of y] uint_lt2p [of x] by arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   438
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   439
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
   440
subsection "Conditions for the addition (etc) of two words to overflow"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   441
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   442
lemma uint_add_lem: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   443
  "(uint x + uint y < 2 ^ len_of TYPE('a)) = 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   444
    (uint (x + y :: 'a :: len0 word) = uint x + uint y)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   445
  by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   446
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   447
lemma uint_mult_lem: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   448
  "(uint x * uint y < 2 ^ len_of TYPE('a)) = 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   449
    (uint (x * y :: 'a :: len0 word) = uint x * uint y)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   450
  by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   451
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   452
lemma uint_sub_lem: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   453
  "(uint x >= uint y) = (uint (x - y) = uint x - uint y)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   454
  by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   455
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   456
lemma uint_add_le: "uint (x + y) <= uint x + uint y"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   457
  unfolding uint_word_ariths by (auto simp: mod_add_if_z)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   458
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   459
lemma uint_sub_ge: "uint (x - y) >= uint x - uint y"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   460
  unfolding uint_word_ariths by (auto simp: mod_sub_if_z)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   461
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   462
lemmas uint_sub_if' =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   463
  trans [OF uint_word_ariths(1) mod_sub_if_z, simplified, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   464
lemmas uint_plus_if' =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   465
  trans [OF uint_word_ariths(2) mod_add_if_z, simplified, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   466
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   467
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
   468
subsection {* Definition of uint\_arith *}
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   469
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   470
lemma word_of_int_inverse:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   471
  "word_of_int r = a ==> 0 <= r ==> r < 2 ^ len_of TYPE('a) ==> 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   472
   uint (a::'a::len0 word) = r"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   473
  apply (erule word_uint.Abs_inverse' [rotated])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   474
  apply (simp add: uints_num)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   475
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   476
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   477
lemma uint_split:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   478
  fixes x::"'a::len0 word"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   479
  shows "P (uint x) = 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   480
         (ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) --> P i)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   481
  apply (fold word_int_case_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   482
  apply (auto dest!: word_of_int_inverse simp: int_word_uint int_mod_eq'
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   483
              split: word_int_split)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   484
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   485
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   486
lemma uint_split_asm:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   487
  fixes x::"'a::len0 word"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   488
  shows "P (uint x) = 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   489
         (~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   490
  by (auto dest!: word_of_int_inverse 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   491
           simp: int_word_uint int_mod_eq'
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   492
           split: uint_split)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   493
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   494
lemmas uint_splits = uint_split uint_split_asm
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   495
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   496
lemmas uint_arith_simps = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   497
  word_le_def word_less_alt
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   498
  word_uint.Rep_inject [symmetric] 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   499
  uint_sub_if' uint_plus_if'
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   500
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   501
(* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   502
lemma power_False_cong: "False ==> a ^ b = c ^ d" 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   503
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   504
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   505
(* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   506
ML {*
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   507
fun uint_arith_ss_of ss = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   508
  ss addsimps @{thms uint_arith_simps}
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   509
     delsimps @{thms word_uint.Rep_inject}
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   510
     addsplits @{thms split_if_asm} 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   511
     addcongs @{thms power_False_cong}
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   512
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   513
fun uint_arith_tacs ctxt = 
30607
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 30549
diff changeset
   514
  let
30686
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30649
diff changeset
   515
    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 31072
diff changeset
   516
    val cs = claset_of ctxt;
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 31072
diff changeset
   517
    val ss = simpset_of ctxt;
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   518
  in 
30607
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 30549
diff changeset
   519
    [ clarify_tac cs 1,
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 30549
diff changeset
   520
      full_simp_tac (uint_arith_ss_of ss) 1,
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   521
      ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms uint_splits} 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   522
                                      addcongs @{thms power_False_cong})),
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   523
      rewrite_goals_tac @{thms word_size}, 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   524
      ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   525
                         REPEAT (etac conjE n) THEN
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   526
                         REPEAT (dtac @{thm word_of_int_inverse} n 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   527
                                 THEN atac n 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   528
                                 THEN atac n)),
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   529
      TRYALL arith_tac' ]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   530
  end
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   531
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   532
fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt))
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   533
*}
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   534
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   535
method_setup uint_arith = 
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30509
diff changeset
   536
  {* Scan.succeed (SIMPLE_METHOD' o uint_arith_tac) *}
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   537
  "solving word arithmetic via integers and arith"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   538
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   539
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
   540
subsection "More on overflows and monotonicity"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   541
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   542
lemma no_plus_overflow_uint_size: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   543
  "((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   544
  unfolding word_size by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   545
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   546
lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   547
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   548
lemma no_ulen_sub: "((x :: 'a :: len0 word) >= x - y) = (uint y <= uint x)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   549
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   550
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   551
lemma no_olen_add':
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   552
  fixes x :: "'a::len0 word"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   553
  shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   554
  by (simp add: word_add_ac add_ac no_olen_add)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   555
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   556
lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric], standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   557
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   558
lemmas uint_plus_simple_iff = trans [OF no_olen_add uint_add_lem, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   559
lemmas uint_plus_simple = uint_plus_simple_iff [THEN iffD1, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   560
lemmas uint_minus_simple_iff = trans [OF no_ulen_sub uint_sub_lem, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   561
lemmas uint_minus_simple_alt = uint_sub_lem [folded word_le_def]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   562
lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   563
lemmas word_sub_le = word_sub_le_iff [THEN iffD2, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   564
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   565
lemma word_less_sub1: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   566
  "(x :: 'a :: len word) ~= 0 ==> (1 < x) = (0 < x - 1)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   567
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   568
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   569
lemma word_le_sub1: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   570
  "(x :: 'a :: len word) ~= 0 ==> (1 <= x) = (0 <= x - 1)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   571
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   572
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   573
lemma sub_wrap_lt: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   574
  "((x :: 'a :: len0 word) < x - z) = (x < z)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   575
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   576
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   577
lemma sub_wrap: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   578
  "((x :: 'a :: len0 word) <= x - z) = (z = 0 | x < z)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   579
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   580
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   581
lemma plus_minus_not_NULL_ab: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   582
  "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> c ~= 0 ==> x + c ~= 0"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   583
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   584
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   585
lemma plus_minus_no_overflow_ab: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   586
  "(x :: 'a :: len0 word) <= ab - c ==> c <= ab ==> x <= x + c" 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   587
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   588
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   589
lemma le_minus': 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   590
  "(a :: 'a :: len0 word) + c <= b ==> a <= a + c ==> c <= b - a"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   591
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   592
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   593
lemma le_plus': 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   594
  "(a :: 'a :: len0 word) <= b ==> c <= b - a ==> a + c <= b"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   595
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   596
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   597
lemmas le_plus = le_plus' [rotated]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   598
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   599
lemmas le_minus = leD [THEN thin_rl, THEN le_minus', standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   600
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   601
lemma word_plus_mono_right: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   602
  "(y :: 'a :: len0 word) <= z ==> x <= x + z ==> x + y <= x + z"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   603
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   604
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   605
lemma word_less_minus_cancel: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   606
  "y - x < z - x ==> x <= z ==> (y :: 'a :: len0 word) < z"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   607
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   608
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   609
lemma word_less_minus_mono_left: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   610
  "(y :: 'a :: len0 word) < z ==> x <= y ==> y - x < z - x"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   611
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   612
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   613
lemma word_less_minus_mono:  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   614
  "a < c ==> d < b ==> a - b < a ==> c - d < c 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   615
  ==> a - b < c - (d::'a::len word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   616
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   617
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   618
lemma word_le_minus_cancel: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   619
  "y - x <= z - x ==> x <= z ==> (y :: 'a :: len0 word) <= z"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   620
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   621
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   622
lemma word_le_minus_mono_left: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   623
  "(y :: 'a :: len0 word) <= z ==> x <= y ==> y - x <= z - x"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   624
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   625
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   626
lemma word_le_minus_mono:  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   627
  "a <= c ==> d <= b ==> a - b <= a ==> c - d <= c 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   628
  ==> a - b <= c - (d::'a::len word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   629
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   630
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   631
lemma plus_le_left_cancel_wrap: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   632
  "(x :: 'a :: len0 word) + y' < x ==> x + y < x ==> (x + y' < x + y) = (y' < y)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   633
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   634
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   635
lemma plus_le_left_cancel_nowrap: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   636
  "(x :: 'a :: len0 word) <= x + y' ==> x <= x + y ==> 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   637
    (x + y' < x + y) = (y' < y)" 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   638
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   639
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   640
lemma word_plus_mono_right2: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   641
  "(a :: 'a :: len0 word) <= a + b ==> c <= b ==> a <= a + c"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   642
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   643
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   644
lemma word_less_add_right: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   645
  "(x :: 'a :: len0 word) < y - z ==> z <= y ==> x + z < y"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   646
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   647
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   648
lemma word_less_sub_right: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   649
  "(x :: 'a :: len0 word) < y + z ==> y <= x ==> x - y < z"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   650
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   651
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   652
lemma word_le_plus_either: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   653
  "(x :: 'a :: len0 word) <= y | x <= z ==> y <= y + z ==> x <= y + z"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   654
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   655
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   656
lemma word_less_nowrapI: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   657
  "(x :: 'a :: len0 word) < z - k ==> k <= z ==> 0 < k ==> x < x + k"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   658
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   659
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   660
lemma inc_le: "(i :: 'a :: len word) < m ==> i + 1 <= m"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   661
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   662
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   663
lemma inc_i: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   664
  "(1 :: 'a :: len word) <= i ==> i < m ==> 1 <= (i + 1) & i + 1 <= m"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   665
  by uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   666
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   667
lemma udvd_incr_lem:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   668
  "up < uq ==> up = ua + n * uint K ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   669
    uq = ua + n' * uint K ==> up + uint K <= uq"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   670
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   671
  apply (drule less_le_mult)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   672
  apply safe
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   673
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   674
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   675
lemma udvd_incr': 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   676
  "p < q ==> uint p = ua + n * uint K ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   677
    uint q = ua + n' * uint K ==> p + K <= q" 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   678
  apply (unfold word_less_alt word_le_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   679
  apply (drule (2) udvd_incr_lem)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   680
  apply (erule uint_add_le [THEN order_trans])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   681
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   682
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   683
lemma udvd_decr': 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   684
  "p < q ==> uint p = ua + n * uint K ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   685
    uint q = ua + n' * uint K ==> p <= q - K"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   686
  apply (unfold word_less_alt word_le_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   687
  apply (drule (2) udvd_incr_lem)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   688
  apply (drule le_diff_eq [THEN iffD2])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   689
  apply (erule order_trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   690
  apply (rule uint_sub_ge)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   691
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   692
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   693
lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, simplified]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   694
lemmas udvd_incr0 = udvd_incr' [where ua=0, simplified]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   695
lemmas udvd_decr0 = udvd_decr' [where ua=0, simplified]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   696
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   697
lemma udvd_minus_le': 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   698
  "xy < k ==> z udvd xy ==> z udvd k ==> xy <= k - z"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   699
  apply (unfold udvd_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   700
  apply clarify
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   701
  apply (erule (2) udvd_decr0)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   702
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   703
31072
796d3d42c873 proper structure name
haftmann
parents: 31021
diff changeset
   704
ML {* Delsimprocs Numeral_Simprocs.cancel_factors *}
796d3d42c873 proper structure name
haftmann
parents: 31021
diff changeset
   705
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   706
lemma udvd_incr2_K: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   707
  "p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   708
    0 < K ==> p <= p + K & p + K <= a + s"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   709
  apply (unfold udvd_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   710
  apply clarify
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   711
  apply (simp add: uint_arith_simps split: split_if_asm)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   712
   prefer 2 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   713
   apply (insert uint_range' [of s])[1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   714
   apply arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   715
  apply (drule add_commute [THEN xtr1])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   716
  apply (simp add: diff_less_eq [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   717
  apply (drule less_le_mult)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   718
   apply arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   719
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   720
  done
31072
796d3d42c873 proper structure name
haftmann
parents: 31021
diff changeset
   721
796d3d42c873 proper structure name
haftmann
parents: 31021
diff changeset
   722
ML {* Addsimprocs Numeral_Simprocs.cancel_factors *}
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   723
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   724
(* links with rbl operations *)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   725
lemma word_succ_rbl:
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   726
  "to_bl w = bl ==> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   727
  apply (unfold word_succ_def)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   728
  apply clarify
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   729
  apply (simp add: to_bl_of_bin)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   730
  apply (simp add: to_bl_def rbl_succ)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   731
  done
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   732
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   733
lemma word_pred_rbl:
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   734
  "to_bl w = bl ==> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   735
  apply (unfold word_pred_def)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   736
  apply clarify
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   737
  apply (simp add: to_bl_of_bin)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   738
  apply (simp add: to_bl_def rbl_pred)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   739
  done
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   740
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   741
lemma word_add_rbl:
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   742
  "to_bl v = vbl ==> to_bl w = wbl ==> 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   743
    to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   744
  apply (unfold word_add_def)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   745
  apply clarify
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   746
  apply (simp add: to_bl_of_bin)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   747
  apply (simp add: to_bl_def rbl_add)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   748
  done
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   749
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   750
lemma word_mult_rbl:
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   751
  "to_bl v = vbl ==> to_bl w = wbl ==> 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   752
    to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   753
  apply (unfold word_mult_def)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   754
  apply clarify
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   755
  apply (simp add: to_bl_of_bin)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   756
  apply (simp add: to_bl_def rbl_mult)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   757
  done
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   758
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   759
lemma rtb_rbl_ariths:
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   760
  "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   761
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   762
  "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   763
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   764
  "[| rev (to_bl v) = ys; rev (to_bl w) = xs |] 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   765
  ==> rev (to_bl (v * w)) = rbl_mult ys xs"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   766
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   767
  "[| rev (to_bl v) = ys; rev (to_bl w) = xs |] 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   768
  ==> rev (to_bl (v + w)) = rbl_add ys xs"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   769
  by (auto simp: rev_swap [symmetric] word_succ_rbl 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   770
                 word_pred_rbl word_mult_rbl word_add_rbl)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   771
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   772
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
   773
subsection "Arithmetic type class instantiations"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   774
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   775
instance word :: (len0) comm_monoid_add ..
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   776
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   777
instance word :: (len0) comm_monoid_mult
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   778
  apply (intro_classes)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   779
   apply (simp add: word_mult_commute)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   780
  apply (simp add: word_mult_1)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   781
  done
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   782
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   783
instance word :: (len0) comm_semiring 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   784
  by (intro_classes) (simp add : word_left_distrib)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   785
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   786
instance word :: (len0) ab_group_add ..
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   787
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   788
instance word :: (len0) comm_ring ..
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   789
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   790
instance word :: (len) comm_semiring_1 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   791
  by (intro_classes) (simp add: lenw1_zero_neq_one)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   792
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   793
instance word :: (len) comm_ring_1 ..
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   794
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   795
instance word :: (len0) comm_semiring_0 ..
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   796
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   797
instance word :: (len0) order ..
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   798
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   799
(* note that iszero_def is only for class comm_semiring_1_cancel,
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   800
   which requires word length >= 1, ie 'a :: len word *) 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   801
lemma zero_bintrunc:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   802
  "iszero (number_of x :: 'a :: len word) = 
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25762
diff changeset
   803
    (bintrunc (len_of TYPE('a)) x = Int.Pls)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   804
  apply (unfold iszero_def word_0_wi word_no_wi)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   805
  apply (rule word_ubin.norm_eq_iff [symmetric, THEN trans])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   806
  apply (simp add : Pls_def [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   807
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   808
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   809
lemmas word_le_0_iff [simp] =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   810
  word_zero_le [THEN leD, THEN linorder_antisym_conv1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   811
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   812
lemma word_of_nat: "of_nat n = word_of_int (int n)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   813
  by (induct n) (auto simp add : word_of_int_hom_syms)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   814
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   815
lemma word_of_int: "of_int = word_of_int"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   816
  apply (rule ext)
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   817
  apply (unfold of_int_def)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   818
  apply (rule contentsI)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   819
  apply safe
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   820
  apply (simp_all add: word_of_nat word_of_int_homs)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   821
   defer
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   822
   apply (rule Rep_Integ_ne [THEN nonemptyE])
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   823
   apply (rule bexI)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   824
    prefer 2
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   825
    apply assumption
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   826
   apply (auto simp add: RI_eq_diff)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   827
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   828
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   829
lemma word_of_int_nat: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   830
  "0 <= x ==> word_of_int x = of_nat (nat x)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   831
  by (simp add: of_nat_nat word_of_int)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   832
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   833
lemma word_number_of_eq: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   834
  "number_of w = (of_int w :: 'a :: len word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   835
  unfolding word_number_of_def word_of_int by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   836
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   837
instance word :: (len) number_ring
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   838
  by (intro_classes) (simp add : word_number_of_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   839
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   840
lemma iszero_word_no [simp] : 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   841
  "iszero (number_of bin :: 'a :: len word) = 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   842
    iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)"
24368
4c2e80f30aeb remove redundant lemma int_number_of
huffman
parents: 24350
diff changeset
   843
  apply (simp add: zero_bintrunc number_of_is_id)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   844
  apply (unfold iszero_def Pls_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   845
  apply (rule refl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   846
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   847
    
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   848
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
   849
subsection "Word and nat"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   850
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   851
lemma td_ext_unat':
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   852
  "n = len_of TYPE ('a :: len) ==> 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   853
    td_ext (unat :: 'a word => nat) of_nat 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   854
    (unats n) (%i. i mod 2 ^ n)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   855
  apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   856
  apply (auto intro!: imageI simp add : word_of_int_hom_syms)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   857
  apply (erule word_uint.Abs_inverse [THEN arg_cong])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   858
  apply (simp add: int_word_uint nat_mod_distrib nat_power_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   859
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   860
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   861
lemmas td_ext_unat = refl [THEN td_ext_unat']
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   862
lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   863
30729
461ee3e49ad3 interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents: 30686
diff changeset
   864
interpretation word_unat:
29235
2d62b637fa80 More porting to new locales.
ballarin
parents: 28959
diff changeset
   865
  td_ext "unat::'a::len word => nat" 
2d62b637fa80 More porting to new locales.
ballarin
parents: 28959
diff changeset
   866
         of_nat 
2d62b637fa80 More porting to new locales.
ballarin
parents: 28959
diff changeset
   867
         "unats (len_of TYPE('a::len))"
2d62b637fa80 More porting to new locales.
ballarin
parents: 28959
diff changeset
   868
         "%i. i mod 2 ^ len_of TYPE('a::len)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   869
  by (rule td_ext_unat)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   870
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   871
lemmas td_unat = word_unat.td_thm
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   872
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   873
lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   874
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   875
lemma unat_le: "y <= unat (z :: 'a :: len word) ==> y : unats (len_of TYPE ('a))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   876
  apply (unfold unats_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   877
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   878
  apply (rule xtrans, rule unat_lt2p, assumption) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   879
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   880
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   881
lemma word_nchotomy:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   882
  "ALL w. EX n. (w :: 'a :: len word) = of_nat n & n < 2 ^ len_of TYPE ('a)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   883
  apply (rule allI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   884
  apply (rule word_unat.Abs_cases)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   885
  apply (unfold unats_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   886
  apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   887
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   888
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   889
lemma of_nat_eq:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   890
  fixes w :: "'a::len word"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   891
  shows "(of_nat n = w) = (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   892
  apply (rule trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   893
   apply (rule word_unat.inverse_norm)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   894
  apply (rule iffI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   895
   apply (rule mod_eqD)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   896
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   897
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   898
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   899
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   900
lemma of_nat_eq_size: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   901
  "(of_nat n = w) = (EX q. n = unat w + q * 2 ^ size w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   902
  unfolding word_size by (rule of_nat_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   903
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   904
lemma of_nat_0:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   905
  "(of_nat m = (0::'a::len word)) = (\<exists>q. m = q * 2 ^ len_of TYPE('a))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   906
  by (simp add: of_nat_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   907
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   908
lemmas of_nat_2p = mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   909
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   910
lemma of_nat_gt_0: "of_nat k ~= 0 ==> 0 < k"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   911
  by (cases k) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   912
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   913
lemma of_nat_neq_0: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   914
  "0 < k ==> k < 2 ^ len_of TYPE ('a :: len) ==> of_nat k ~= (0 :: 'a word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   915
  by (clarsimp simp add : of_nat_0)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   916
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   917
lemma Abs_fnat_hom_add:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   918
  "of_nat a + of_nat b = of_nat (a + b)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   919
  by simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   920
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   921
lemma Abs_fnat_hom_mult:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   922
  "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   923
  by (simp add: word_of_nat word_of_int_mult_hom zmult_int)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   924
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   925
lemma Abs_fnat_hom_Suc:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   926
  "word_succ (of_nat a) = of_nat (Suc a)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   927
  by (simp add: word_of_nat word_of_int_succ_hom add_ac)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   928
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   929
lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   930
  by (simp add: word_of_nat word_0_wi)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   931
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   932
lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   933
  by (simp add: word_of_nat word_1_wi)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   934
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   935
lemmas Abs_fnat_homs = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   936
  Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   937
  Abs_fnat_hom_0 Abs_fnat_hom_1
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   938
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   939
lemma word_arith_nat_add:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   940
  "a + b = of_nat (unat a + unat b)" 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   941
  by simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   942
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   943
lemma word_arith_nat_mult:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   944
  "a * b = of_nat (unat a * unat b)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   945
  by (simp add: Abs_fnat_hom_mult [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   946
    
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   947
lemma word_arith_nat_Suc:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   948
  "word_succ a = of_nat (Suc (unat a))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   949
  by (subst Abs_fnat_hom_Suc [symmetric]) simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   950
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   951
lemma word_arith_nat_div:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   952
  "a div b = of_nat (unat a div unat b)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   953
  by (simp add: word_div_def word_of_nat zdiv_int uint_nat)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   954
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   955
lemma word_arith_nat_mod:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   956
  "a mod b = of_nat (unat a mod unat b)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   957
  by (simp add: word_mod_def word_of_nat zmod_int uint_nat)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   958
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   959
lemmas word_arith_nat_defs =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   960
  word_arith_nat_add word_arith_nat_mult
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   961
  word_arith_nat_Suc Abs_fnat_hom_0
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   962
  Abs_fnat_hom_1 word_arith_nat_div
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   963
  word_arith_nat_mod 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   964
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   965
lemmas unat_cong = arg_cong [where f = "unat"]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   966
  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   967
lemmas unat_word_ariths = word_arith_nat_defs
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   968
  [THEN trans [OF unat_cong unat_of_nat], standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   969
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   970
lemmas word_sub_less_iff = word_sub_le_iff
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   971
  [simplified linorder_not_less [symmetric], simplified]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   972
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   973
lemma unat_add_lem: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   974
  "(unat x + unat y < 2 ^ len_of TYPE('a)) = 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   975
    (unat (x + y :: 'a :: len word) = unat x + unat y)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   976
  unfolding unat_word_ariths
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   977
  by (auto intro!: trans [OF _ nat_mod_lem])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   978
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   979
lemma unat_mult_lem: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   980
  "(unat x * unat y < 2 ^ len_of TYPE('a)) = 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   981
    (unat (x * y :: 'a :: len word) = unat x * unat y)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   982
  unfolding unat_word_ariths
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   983
  by (auto intro!: trans [OF _ nat_mod_lem])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   984
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   985
lemmas unat_plus_if' = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   986
  trans [OF unat_word_ariths(1) mod_nat_add, simplified, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   987
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   988
lemma le_no_overflow: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
   989
  "x <= b ==> a <= a + b ==> x <= a + (b :: 'a :: len0 word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   990
  apply (erule order_trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   991
  apply (erule olen_add_eqv [THEN iffD1])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   992
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   993
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   994
lemmas un_ui_le = trans 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   995
  [OF word_le_nat_alt [symmetric] 
25762
c03e9d04b3e4 splitted class uminus from class minus
haftmann
parents: 25350
diff changeset
   996
      word_le_def, 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   997
   standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   998
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   999
lemma unat_sub_if_size:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1000
  "unat (x - y) = (if unat y <= unat x 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1001
   then unat x - unat y 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1002
   else unat x + 2 ^ size x - unat y)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1003
  apply (unfold word_size)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1004
  apply (simp add: un_ui_le)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1005
  apply (auto simp add: unat_def uint_sub_if')
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1006
   apply (rule nat_diff_distrib)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1007
    prefer 3
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 29509
diff changeset
  1008
    apply (simp add: algebra_simps)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1009
    apply (rule nat_diff_distrib [THEN trans])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1010
      prefer 3
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1011
      apply (subst nat_add_distrib)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1012
        prefer 3
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1013
        apply (simp add: nat_power_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1014
       apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1015
  apply uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1016
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1017
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1018
lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1019
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1020
lemma unat_div: "unat ((x :: 'a :: len word) div y) = unat x div unat y"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1021
  apply (simp add : unat_word_ariths)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1022
  apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1023
  apply (rule div_le_dividend)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1024
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1025
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1026
lemma unat_mod: "unat ((x :: 'a :: len word) mod y) = unat x mod unat y"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1027
  apply (clarsimp simp add : unat_word_ariths)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1028
  apply (cases "unat y")
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1029
   prefer 2
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1030
   apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1031
   apply (rule mod_le_divisor)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1032
   apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1033
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1034
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1035
lemma uint_div: "uint ((x :: 'a :: len word) div y) = uint x div uint y"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1036
  unfolding uint_nat by (simp add : unat_div zdiv_int)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1037
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1038
lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1039
  unfolding uint_nat by (simp add : unat_mod zmod_int)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1040
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1041
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
  1042
subsection {* Definition of unat\_arith tactic *}
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1043
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1044
lemma unat_split:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1045
  fixes x::"'a::len word"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1046
  shows "P (unat x) = 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1047
         (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1048
  by (auto simp: unat_of_nat)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1049
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1050
lemma unat_split_asm:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1051
  fixes x::"'a::len word"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1052
  shows "P (unat x) = 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1053
         (~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1054
  by (auto simp: unat_of_nat)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1055
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1056
lemmas of_nat_inverse = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1057
  word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1058
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1059
lemmas unat_splits = unat_split unat_split_asm
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1060
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1061
lemmas unat_arith_simps =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1062
  word_le_nat_alt word_less_nat_alt
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1063
  word_unat.Rep_inject [symmetric]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1064
  unat_sub_if' unat_plus_if' unat_div unat_mod
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1065
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1066
(* unat_arith_tac: tactic to reduce word arithmetic to nat, 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1067
   try to solve via arith *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1068
ML {*
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1069
fun unat_arith_ss_of ss = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1070
  ss addsimps @{thms unat_arith_simps}
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1071
     delsimps @{thms word_unat.Rep_inject}
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1072
     addsplits @{thms split_if_asm}
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1073
     addcongs @{thms power_False_cong}
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1074
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1075
fun unat_arith_tacs ctxt =   
30607
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 30549
diff changeset
  1076
  let
30686
47a32dd1b86e moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
haftmann
parents: 30649
diff changeset
  1077
    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
32149
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 31072
diff changeset
  1078
    val cs = claset_of ctxt;
ef59550a55d3 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents: 31072
diff changeset
  1079
    val ss = simpset_of ctxt;
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1080
  in 
30607
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 30549
diff changeset
  1081
    [ clarify_tac cs 1,
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 30549
diff changeset
  1082
      full_simp_tac (unat_arith_ss_of ss) 1,
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1083
      ALLGOALS (full_simp_tac (HOL_ss addsplits @{thms unat_splits} 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1084
                                       addcongs @{thms power_False_cong})),
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1085
      rewrite_goals_tac @{thms word_size}, 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1086
      ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1087
                         REPEAT (etac conjE n) THEN
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1088
                         REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1089
      TRYALL arith_tac' ] 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1090
  end
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1091
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1092
fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1093
*}
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1094
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1095
method_setup unat_arith = 
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30509
diff changeset
  1096
  {* Scan.succeed (SIMPLE_METHOD' o unat_arith_tac) *}
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1097
  "solving word arithmetic via natural numbers and arith"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1098
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1099
lemma no_plus_overflow_unat_size: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1100
  "((x :: 'a :: len word) <= x + y) = (unat x + unat y < 2 ^ size x)" 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1101
  unfolding word_size by unat_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1102
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1103
lemma unat_sub: "b <= a ==> unat (a - b) = unat a - unat (b :: 'a :: len word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1104
  by unat_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1105
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1106
lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1107
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1108
lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1109
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1110
lemma word_div_mult: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1111
  "(0 :: 'a :: len word) < y ==> unat x * unat y < 2 ^ len_of TYPE('a) ==> 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1112
    x * y div y = x"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1113
  apply unat_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1114
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1115
  apply (subst unat_mult_lem [THEN iffD1])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1116
  apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1117
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1118
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1119
lemma div_lt': "(i :: 'a :: len word) <= k div x ==> 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1120
    unat i * unat x < 2 ^ len_of TYPE('a)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1121
  apply unat_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1122
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1123
  apply (drule mult_le_mono1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1124
  apply (erule order_le_less_trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1125
  apply (rule xtr7 [OF unat_lt2p div_mult_le])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1126
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1127
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1128
lemmas div_lt'' = order_less_imp_le [THEN div_lt']
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1129
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1130
lemma div_lt_mult: "(i :: 'a :: len word) < k div x ==> 0 < x ==> i * x < k"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1131
  apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1132
  apply (simp add: unat_arith_simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1133
  apply (drule (1) mult_less_mono1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1134
  apply (erule order_less_le_trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1135
  apply (rule div_mult_le)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1136
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1137
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1138
lemma div_le_mult: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1139
  "(i :: 'a :: len word) <= k div x ==> 0 < x ==> i * x <= k"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1140
  apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1141
  apply (simp add: unat_arith_simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1142
  apply (drule mult_le_mono1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1143
  apply (erule order_trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1144
  apply (rule div_mult_le)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1145
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1146
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1147
lemma div_lt_uint': 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1148
  "(i :: 'a :: len word) <= k div x ==> uint i * uint x < 2 ^ len_of TYPE('a)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1149
  apply (unfold uint_nat)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1150
  apply (drule div_lt')
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1151
  apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1152
                   nat_power_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1153
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1154
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1155
lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1156
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1157
lemma word_le_exists': 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1158
  "(x :: 'a :: len0 word) <= y ==> 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1159
    (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1160
  apply (rule exI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1161
  apply (rule conjI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1162
  apply (rule zadd_diff_inverse)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1163
  apply uint_arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1164
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1165
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1166
lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1167
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1168
lemmas plus_minus_no_overflow =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1169
  order_less_imp_le [THEN plus_minus_no_overflow_ab]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1170
  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1171
lemmas mcs = word_less_minus_cancel word_less_minus_mono_left
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1172
  word_le_minus_cancel word_le_minus_mono_left
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1173
25350
a5fcf6d12a53 eliminated illegal schematic variables in where/of;
wenzelm
parents: 25134
diff changeset
  1174
lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel, standard]
a5fcf6d12a53 eliminated illegal schematic variables in where/of;
wenzelm
parents: 25134
diff changeset
  1175
lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel, standard]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1176
lemmas word_plus_mcs = word_diff_ls 
25350
a5fcf6d12a53 eliminated illegal schematic variables in where/of;
wenzelm
parents: 25134
diff changeset
  1177
  [where y = "v + x", unfolded add_diff_cancel, standard]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1178
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1179
lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1180
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1181
lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1182
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1183
lemma thd1:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1184
  "a div b * b \<le> (a::nat)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1185
  using gt_or_eq_0 [of b]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1186
  apply (rule disjE)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1187
   apply (erule xtr4 [OF thd mult_commute])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1188
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1189
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1190
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1191
lemmas uno_simps [THEN le_unat_uoi, standard] =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1192
  mod_le_divisor div_le_dividend thd1 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1193
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1194
lemma word_mod_div_equality:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1195
  "(n div b) * b + (n mod b) = (n :: 'a :: len word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1196
  apply (unfold word_less_nat_alt word_arith_nat_defs)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1197
  apply (cut_tac y="unat b" in gt_or_eq_0)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1198
  apply (erule disjE)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1199
   apply (simp add: mod_div_equality uno_simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1200
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1201
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1202
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1203
lemma word_div_mult_le: "a div b * b <= (a::'a::len word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1204
  apply (unfold word_le_nat_alt word_arith_nat_defs)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1205
  apply (cut_tac y="unat b" in gt_or_eq_0)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1206
  apply (erule disjE)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1207
   apply (simp add: div_mult_le uno_simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1208
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1209
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1210
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1211
lemma word_mod_less_divisor: "0 < n ==> m mod n < (n :: 'a :: len word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1212
  apply (simp only: word_less_nat_alt word_arith_nat_defs)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1213
  apply (clarsimp simp add : uno_simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1214
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1215
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1216
lemma word_of_int_power_hom: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1217
  "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1218
  by (induct n) (simp_all add : word_of_int_hom_syms power_Suc)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1219
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1220
lemma word_arith_power_alt: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1221
  "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1222
  by (simp add : word_of_int_power_hom [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1223
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1224
lemma of_bl_length_less: 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1225
  "length x = k ==> k < len_of TYPE('a) ==> (of_bl x :: 'a :: len word) < 2 ^ k"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1226
  apply (unfold of_bl_no [unfolded word_number_of_def]
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1227
                word_less_alt word_number_of_alt)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1228
  apply safe
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1229
  apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1230
                       del: word_of_int_bin)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1231
  apply (simp add: mod_pos_pos_trivial)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1232
  apply (subst mod_pos_pos_trivial)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1233
    apply (rule bl_to_bin_ge0)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1234
   apply (rule order_less_trans)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1235
    apply (rule bl_to_bin_lt2p)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1236
   apply simp
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1237
  apply (rule bl_to_bin_lt2p)    
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1238
  done
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1239
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1240
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
  1241
subsection "Cardinality, finiteness of set of words"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1242
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1243
lemmas card_lessThan' = card_lessThan [unfolded lessThan_def]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1244
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1245
lemmas card_eq = word_unat.Abs_inj_on [THEN card_image,
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1246
  unfolded word_unat.image, unfolded unats_def, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1247
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1248
lemmas card_word = trans [OF card_eq card_lessThan', standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1249
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1250
lemma finite_word_UNIV: "finite (UNIV :: 'a :: len word set)"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
  1251
apply (rule contrapos_np)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
  1252
 prefer 2
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
  1253
 apply (erule card_infinite)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
  1254
apply (simp add: card_word)
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
  1255
done
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1256
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1257
lemma card_word_size: 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24415
diff changeset
  1258
  "card (UNIV :: 'a :: len word set) = (2 ^ size (x :: 'a word))"
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
  1259
unfolding word_size by (rule card_word)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1260
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1261
end