src/HOL/Library/Char_nat.thy
author hoelzl
Tue Jul 19 14:37:49 2011 +0200 (2011-07-19)
changeset 43922 c6f35921056e
parent 40077 c8a9eaaa2f59
child 46730 e3b99d0231bc
permissions -rw-r--r--
add nat => enat coercion
haftmann@22799
     1
(*  Title:      HOL/Library/Char_nat.thy
haftmann@22799
     2
    Author:     Norbert Voelker, Florian Haftmann
haftmann@22799
     3
*)
haftmann@22799
     4
haftmann@22799
     5
header {* Mapping between characters and natural numbers *}
haftmann@22799
     6
haftmann@22799
     7
theory Char_nat
haftmann@30663
     8
imports List Main
haftmann@22799
     9
begin
haftmann@22799
    10
haftmann@22799
    11
text {* Conversions between nibbles and natural numbers in [0..15]. *}
haftmann@22799
    12
haftmann@26152
    13
primrec
haftmann@22799
    14
  nat_of_nibble :: "nibble \<Rightarrow> nat" where
wenzelm@23394
    15
    "nat_of_nibble Nibble0 = 0"
haftmann@22799
    16
  | "nat_of_nibble Nibble1 = 1"
haftmann@22799
    17
  | "nat_of_nibble Nibble2 = 2"
haftmann@22799
    18
  | "nat_of_nibble Nibble3 = 3"
haftmann@22799
    19
  | "nat_of_nibble Nibble4 = 4"
haftmann@22799
    20
  | "nat_of_nibble Nibble5 = 5"
haftmann@22799
    21
  | "nat_of_nibble Nibble6 = 6"
haftmann@22799
    22
  | "nat_of_nibble Nibble7 = 7"
haftmann@22799
    23
  | "nat_of_nibble Nibble8 = 8"
haftmann@22799
    24
  | "nat_of_nibble Nibble9 = 9"
haftmann@22799
    25
  | "nat_of_nibble NibbleA = 10"
haftmann@22799
    26
  | "nat_of_nibble NibbleB = 11"
haftmann@22799
    27
  | "nat_of_nibble NibbleC = 12"
haftmann@22799
    28
  | "nat_of_nibble NibbleD = 13"
haftmann@22799
    29
  | "nat_of_nibble NibbleE = 14"
haftmann@22799
    30
  | "nat_of_nibble NibbleF = 15"
haftmann@22799
    31
haftmann@22799
    32
definition
haftmann@22799
    33
  nibble_of_nat :: "nat \<Rightarrow> nibble" where
haftmann@22799
    34
  "nibble_of_nat x = (let y = x mod 16 in
haftmann@22799
    35
    if y = 0 then Nibble0 else
haftmann@22799
    36
    if y = 1 then Nibble1 else
haftmann@22799
    37
    if y = 2 then Nibble2 else
haftmann@22799
    38
    if y = 3 then Nibble3 else
haftmann@22799
    39
    if y = 4 then Nibble4 else
haftmann@22799
    40
    if y = 5 then Nibble5 else
haftmann@22799
    41
    if y = 6 then Nibble6 else
haftmann@22799
    42
    if y = 7 then Nibble7 else
haftmann@22799
    43
    if y = 8 then Nibble8 else
haftmann@22799
    44
    if y = 9 then Nibble9 else
haftmann@22799
    45
    if y = 10 then NibbleA else
haftmann@22799
    46
    if y = 11 then NibbleB else
haftmann@22799
    47
    if y = 12 then NibbleC else
haftmann@22799
    48
    if y = 13 then NibbleD else
haftmann@22799
    49
    if y = 14 then NibbleE else
haftmann@22799
    50
    NibbleF)"
haftmann@22799
    51
haftmann@22799
    52
lemma nibble_of_nat_norm:
haftmann@22799
    53
  "nibble_of_nat (n mod 16) = nibble_of_nat n"
huffman@36843
    54
  unfolding nibble_of_nat_def mod_mod_trivial ..
haftmann@22799
    55
haftmann@22799
    56
lemma nibble_of_nat_simps [simp]:
haftmann@22799
    57
  "nibble_of_nat  0 = Nibble0"
haftmann@22799
    58
  "nibble_of_nat  1 = Nibble1"
haftmann@22799
    59
  "nibble_of_nat  2 = Nibble2"
haftmann@22799
    60
  "nibble_of_nat  3 = Nibble3"
haftmann@22799
    61
  "nibble_of_nat  4 = Nibble4"
haftmann@22799
    62
  "nibble_of_nat  5 = Nibble5"
haftmann@22799
    63
  "nibble_of_nat  6 = Nibble6"
haftmann@22799
    64
  "nibble_of_nat  7 = Nibble7"
haftmann@22799
    65
  "nibble_of_nat  8 = Nibble8"
haftmann@22799
    66
  "nibble_of_nat  9 = Nibble9"
haftmann@22799
    67
  "nibble_of_nat 10 = NibbleA"
haftmann@22799
    68
  "nibble_of_nat 11 = NibbleB"
haftmann@22799
    69
  "nibble_of_nat 12 = NibbleC"
haftmann@22799
    70
  "nibble_of_nat 13 = NibbleD"
haftmann@22799
    71
  "nibble_of_nat 14 = NibbleE"
haftmann@22799
    72
  "nibble_of_nat 15 = NibbleF"
huffman@36843
    73
  unfolding nibble_of_nat_def by auto
haftmann@22799
    74
haftmann@22799
    75
lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
haftmann@22799
    76
  by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
haftmann@22799
    77
haftmann@22799
    78
lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16"
haftmann@22799
    79
proof -
wenzelm@23394
    80
  have nibble_nat_enum:
huffman@36843
    81
    "n mod 16 \<in> {15, 14, 13, 12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0}"
haftmann@22799
    82
  proof -
haftmann@22799
    83
    have set_unfold: "\<And>n. {0..Suc n} = insert (Suc n) {0..n}" by auto
haftmann@22799
    84
    have "(n\<Colon>nat) mod 16 \<in> {0..Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
haftmann@22799
    85
      (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))}" by simp
haftmann@22799
    86
    from this [simplified set_unfold atLeastAtMost_singleton]
huffman@36843
    87
    show ?thesis by (simp add: numeral_2_eq_2 [symmetric])
haftmann@22799
    88
  qed
huffman@36843
    89
  then show ?thesis unfolding nibble_of_nat_def
haftmann@22799
    90
  by auto
haftmann@22799
    91
qed
haftmann@22799
    92
haftmann@22799
    93
lemma inj_nat_of_nibble: "inj nat_of_nibble"
haftmann@22799
    94
  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
haftmann@22799
    95
haftmann@22799
    96
lemma nat_of_nibble_eq: "nat_of_nibble n = nat_of_nibble m \<longleftrightarrow> n = m"
haftmann@22799
    97
  by (rule inj_eq) (rule inj_nat_of_nibble)
haftmann@22799
    98
haftmann@22799
    99
lemma nat_of_nibble_less_16: "nat_of_nibble n < 16"
haftmann@22799
   100
  by (cases n) auto
haftmann@22799
   101
haftmann@22799
   102
lemma nat_of_nibble_div_16: "nat_of_nibble n div 16 = 0"
haftmann@22799
   103
  by (cases n) auto
haftmann@22799
   104
haftmann@22799
   105
haftmann@22799
   106
text {* Conversion between chars and nats. *}
haftmann@22799
   107
haftmann@22799
   108
definition
wenzelm@23394
   109
  nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble" where
haftmann@22799
   110
  "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
haftmann@22799
   111
haftmann@28562
   112
lemma nibble_of_pair [code]:
haftmann@22799
   113
  "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
haftmann@22799
   114
  unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
haftmann@22799
   115
haftmann@26152
   116
primrec
haftmann@22799
   117
  nat_of_char :: "char \<Rightarrow> nat" where
haftmann@22799
   118
  "nat_of_char (Char n m) = nat_of_nibble n * 16 + nat_of_nibble m"
haftmann@22799
   119
haftmann@22799
   120
lemmas [simp del] = nat_of_char.simps
haftmann@22799
   121
haftmann@22799
   122
definition
haftmann@22799
   123
  char_of_nat :: "nat \<Rightarrow> char" where
haftmann@22799
   124
  char_of_nat_def: "char_of_nat n = split Char (nibble_pair_of_nat n)"
haftmann@22799
   125
haftmann@22799
   126
lemma Char_char_of_nat:
haftmann@22799
   127
  "Char n m = char_of_nat (nat_of_nibble n * 16 + nat_of_nibble m)"
haftmann@22799
   128
  unfolding char_of_nat_def Let_def nibble_pair_of_nat_def
nipkow@30224
   129
  by (auto simp add: div_add1_eq mod_add_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
haftmann@22799
   130
haftmann@22799
   131
lemma char_of_nat_of_char:
haftmann@22799
   132
  "char_of_nat (nat_of_char c) = c"
haftmann@22799
   133
  by (cases c) (simp add: nat_of_char.simps, simp add: Char_char_of_nat)
haftmann@22799
   134
haftmann@22799
   135
lemma nat_of_char_of_nat:
haftmann@22799
   136
  "nat_of_char (char_of_nat n) = n mod 256"
haftmann@22799
   137
proof -
haftmann@22799
   138
  from mod_div_equality [of n, symmetric, of 16]
haftmann@22799
   139
  have mod_mult_self3: "\<And>m k n \<Colon> nat. (k * n + m) mod n = m mod n"
haftmann@22799
   140
  proof -
haftmann@22799
   141
    fix m k n :: nat
haftmann@22799
   142
    show "(k * n + m) mod n = m mod n"
wenzelm@23394
   143
      by (simp only: mod_mult_self1 [symmetric, of m n k] add_commute)
haftmann@22799
   144
  qed
haftmann@22799
   145
  from mod_div_decomp [of n 256] obtain k l where n: "n = k * 256 + l"
haftmann@22799
   146
    and k: "k = n div 256" and l: "l = n mod 256" by blast
haftmann@22799
   147
  have 16: "(0::nat) < 16" by auto
haftmann@22799
   148
  have 256: "(256 :: nat) = 16 * 16" by auto
haftmann@22799
   149
  have l_256: "l mod 256 = l" using l by auto
haftmann@22799
   150
  have l_div_256: "l div 16 * 16 mod 256 = l div 16 * 16"
haftmann@22799
   151
    using l by auto
haftmann@22799
   152
  have aux2: "(k * 256 mod 16 + l mod 16) div 16 = 0"
haftmann@27651
   153
    unfolding 256 mult_assoc [symmetric] mod_mult_self2_is_0 by simp
haftmann@22799
   154
  have aux3: "(k * 256 + l) div 16 = k * 16 + l div 16"
haftmann@22799
   155
    unfolding div_add1_eq [of "k * 256" l 16] aux2 256
haftmann@22799
   156
      mult_assoc [symmetric] div_mult_self_is_m [OF 16] by simp
haftmann@22799
   157
  have aux4: "(k * 256 + l) mod 16 = l mod 16"
haftmann@22799
   158
    unfolding 256 mult_assoc [symmetric] mod_mult_self3 ..
haftmann@22799
   159
  show ?thesis
wenzelm@23394
   160
    by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair
wenzelm@23394
   161
      nat_of_nibble_of_nat mod_mult_distrib
nipkow@30224
   162
      n aux3 mod_mult_self3 l_256 aux4 mod_add_eq [of "256 * k"] l_div_256)
haftmann@22799
   163
qed
haftmann@22799
   164
haftmann@22799
   165
lemma nibble_pair_of_nat_char:
haftmann@22799
   166
  "nibble_pair_of_nat (nat_of_char (Char n m)) = (n, m)"
haftmann@22799
   167
proof -
haftmann@22799
   168
  have nat_of_nibble_256:
wenzelm@23394
   169
    "\<And>n m. (nat_of_nibble n * 16 + nat_of_nibble m) mod 256 =
wenzelm@23394
   170
      nat_of_nibble n * 16 + nat_of_nibble m"
haftmann@22799
   171
  proof -
haftmann@22799
   172
    fix n m
haftmann@22799
   173
    have nat_of_nibble_less_eq_15: "\<And>n. nat_of_nibble n \<le> 15"
nipkow@40077
   174
      using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: eval_nat_numeral)
wenzelm@23394
   175
    have less_eq_240: "nat_of_nibble n * 16 \<le> 240"
wenzelm@23394
   176
      using nat_of_nibble_less_eq_15 by auto
haftmann@22799
   177
    have "nat_of_nibble n * 16 + nat_of_nibble m \<le> 240 + 15"
wenzelm@23394
   178
      by (rule add_le_mono [of _ 240 _ 15]) (auto intro: nat_of_nibble_less_eq_15 less_eq_240)
haftmann@22799
   179
    then have "nat_of_nibble n * 16 + nat_of_nibble m < 256" (is "?rhs < _") by auto
haftmann@22799
   180
    then show "?rhs mod 256 = ?rhs" by auto
haftmann@22799
   181
  qed
haftmann@22799
   182
  show ?thesis
wenzelm@23394
   183
    unfolding nibble_pair_of_nat_def Char_char_of_nat nat_of_char_of_nat nat_of_nibble_256
wenzelm@23394
   184
    by (simp add: add_commute nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
haftmann@22799
   185
qed
haftmann@22799
   186
haftmann@22799
   187
haftmann@22799
   188
text {* Code generator setup *}
haftmann@22799
   189
haftmann@22799
   190
code_modulename SML
haftmann@37221
   191
  Char_nat String
haftmann@22799
   192
haftmann@22799
   193
code_modulename OCaml
haftmann@37221
   194
  Char_nat String
haftmann@22799
   195
haftmann@22799
   196
code_modulename Haskell
haftmann@37221
   197
  Char_nat String
haftmann@22799
   198
haftmann@22799
   199
end