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