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