src/HOL/String.thy
changeset 51160 599ff65b85e2
parent 49972 f11f8905d9fd
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/String.thy	Fri Feb 15 15:22:16 2013 +0100
     1.2 +++ b/src/HOL/String.thy	Fri Feb 15 11:47:33 2013 +0100
     1.3 @@ -49,6 +49,72 @@
     1.4    "card (UNIV :: nibble set) = 16"
     1.5    by (simp add: card_UNIV_length_enum enum_nibble_def)
     1.6  
     1.7 +primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
     1.8 +where
     1.9 +  "nat_of_nibble Nibble0 = 0"
    1.10 +| "nat_of_nibble Nibble1 = 1"
    1.11 +| "nat_of_nibble Nibble2 = 2"
    1.12 +| "nat_of_nibble Nibble3 = 3"
    1.13 +| "nat_of_nibble Nibble4 = 4"
    1.14 +| "nat_of_nibble Nibble5 = 5"
    1.15 +| "nat_of_nibble Nibble6 = 6"
    1.16 +| "nat_of_nibble Nibble7 = 7"
    1.17 +| "nat_of_nibble Nibble8 = 8"
    1.18 +| "nat_of_nibble Nibble9 = 9"
    1.19 +| "nat_of_nibble NibbleA = 10"
    1.20 +| "nat_of_nibble NibbleB = 11"
    1.21 +| "nat_of_nibble NibbleC = 12"
    1.22 +| "nat_of_nibble NibbleD = 13"
    1.23 +| "nat_of_nibble NibbleE = 14"
    1.24 +| "nat_of_nibble NibbleF = 15"
    1.25 +
    1.26 +definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
    1.27 +  "nibble_of_nat n = Enum.enum ! (n mod 16)"
    1.28 +
    1.29 +lemma nibble_of_nat_simps [simp]:
    1.30 +  "nibble_of_nat  0 = Nibble0"
    1.31 +  "nibble_of_nat  1 = Nibble1"
    1.32 +  "nibble_of_nat  2 = Nibble2"
    1.33 +  "nibble_of_nat  3 = Nibble3"
    1.34 +  "nibble_of_nat  4 = Nibble4"
    1.35 +  "nibble_of_nat  5 = Nibble5"
    1.36 +  "nibble_of_nat  6 = Nibble6"
    1.37 +  "nibble_of_nat  7 = Nibble7"
    1.38 +  "nibble_of_nat  8 = Nibble8"
    1.39 +  "nibble_of_nat  9 = Nibble9"
    1.40 +  "nibble_of_nat 10 = NibbleA"
    1.41 +  "nibble_of_nat 11 = NibbleB"
    1.42 +  "nibble_of_nat 12 = NibbleC"
    1.43 +  "nibble_of_nat 13 = NibbleD"
    1.44 +  "nibble_of_nat 14 = NibbleE"
    1.45 +  "nibble_of_nat 15 = NibbleF"
    1.46 +  unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
    1.47 +
    1.48 +lemma nibble_of_nat_of_nibble [simp]:
    1.49 +  "nibble_of_nat (nat_of_nibble x) = x"
    1.50 +  by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
    1.51 +
    1.52 +lemma nat_of_nibble_of_nat [simp]:
    1.53 +  "nat_of_nibble (nibble_of_nat n) = n mod 16"
    1.54 +  by (cases "nibble_of_nat n")
    1.55 +     (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
    1.56 +
    1.57 +lemma inj_nat_of_nibble:
    1.58 +  "inj nat_of_nibble"
    1.59 +  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
    1.60 +
    1.61 +lemma nat_of_nibble_eq_iff:
    1.62 +  "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
    1.63 +  by (rule inj_eq) (rule inj_nat_of_nibble)
    1.64 +
    1.65 +lemma nat_of_nibble_less_16:
    1.66 +  "nat_of_nibble x < 16"
    1.67 +  by (cases x) auto
    1.68 +
    1.69 +lemma nibble_of_nat_mod_16:
    1.70 +  "nibble_of_nat (n mod 16) = nibble_of_nat n"
    1.71 +  by (simp add: nibble_of_nat_def)
    1.72 +
    1.73  datatype char = Char nibble nibble
    1.74    -- "Note: canonical order of character encoding coincides with standard term ordering"
    1.75  
    1.76 @@ -154,13 +220,15 @@
    1.77  definition
    1.78    "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
    1.79  
    1.80 +lemma enum_char_product_enum_nibble:
    1.81 +  "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
    1.82 +  by (simp add: enum_char_def enum_nibble_def)
    1.83 +
    1.84  instance proof
    1.85 -  have enum: "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
    1.86 -    by (simp add: enum_char_def enum_nibble_def)
    1.87    show UNIV: "UNIV = set (Enum.enum :: char list)"
    1.88 -    by (simp add: enum UNIV_char product_list_set enum_UNIV)
    1.89 +    by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV)
    1.90    show "distinct (Enum.enum :: char list)"
    1.91 -    by (auto intro: inj_onI simp add: enum distinct_map distinct_product enum_distinct)
    1.92 +    by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
    1.93    show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
    1.94      by (simp add: UNIV enum_all_char_def list_all_iff)
    1.95    show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
    1.96 @@ -173,30 +241,115 @@
    1.97    "card (UNIV :: char set) = 256"
    1.98    by (simp add: card_UNIV_length_enum enum_char_def)
    1.99  
   1.100 -primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
   1.101 -  "nibble_pair_of_char (Char n m) = (n, m)"
   1.102 +definition nat_of_char :: "char \<Rightarrow> nat"
   1.103 +where
   1.104 +  "nat_of_char c = (case c of Char x y \<Rightarrow> nat_of_nibble x * 16 + nat_of_nibble y)"
   1.105 +
   1.106 +lemma nat_of_char_Char:
   1.107 +  "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y"
   1.108 +  by (simp add: nat_of_char_def)
   1.109  
   1.110  setup {*
   1.111  let
   1.112    val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
   1.113 -  val thms = map_product
   1.114 -   (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
   1.115 -      nibbles nibbles;
   1.116 +  val simpset = HOL_ss addsimps
   1.117 +    @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
   1.118 +  fun mk_code_eqn x y =
   1.119 +    Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
   1.120 +    |> simplify simpset;
   1.121 +  val code_eqns = map_product mk_code_eqn nibbles nibbles;
   1.122  in
   1.123    Global_Theory.note_thmss ""
   1.124 -    [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
   1.125 -  #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
   1.126 +    [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
   1.127 +  #> snd
   1.128  end
   1.129  *}
   1.130  
   1.131 -lemma char_case_nibble_pair [code, code_unfold]:
   1.132 -  "char_case f = split f o nibble_pair_of_char"
   1.133 +declare nat_of_char_simps [code]
   1.134 +
   1.135 +lemma nibble_of_nat_of_char_div_16:
   1.136 +  "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
   1.137 +  by (cases c)
   1.138 +    (simp add: nat_of_char_def add_commute nat_of_nibble_less_16)
   1.139 +
   1.140 +lemma nibble_of_nat_nat_of_char:
   1.141 +  "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
   1.142 +proof (cases c)
   1.143 +  case (Char x y)
   1.144 +  then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
   1.145 +    by (simp add: nibble_of_nat_mod_16)
   1.146 +  then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
   1.147 +    by (simp only: nibble_of_nat_mod_16)
   1.148 +  with Char show ?thesis by (simp add: nat_of_char_def add_commute)
   1.149 +qed
   1.150 +
   1.151 +code_datatype Char -- {* drop case certificate for char *}
   1.152 +
   1.153 +lemma char_case_code [code]:
   1.154 +  "char_case f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
   1.155 +  by (cases c)
   1.156 +    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
   1.157 +
   1.158 +lemma [code]:
   1.159 +  "char_rec = char_case"
   1.160    by (simp add: fun_eq_iff split: char.split)
   1.161  
   1.162 -lemma char_rec_nibble_pair [code, code_unfold]:
   1.163 -  "char_rec f = split f o nibble_pair_of_char"
   1.164 -  unfolding char_case_nibble_pair [symmetric]
   1.165 -  by (simp add: fun_eq_iff split: char.split)
   1.166 +definition char_of_nat :: "nat \<Rightarrow> char" where
   1.167 +  "char_of_nat n = Enum.enum ! (n mod 256)"
   1.168 +
   1.169 +lemma char_of_nat_Char_nibbles:
   1.170 +  "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
   1.171 +proof -
   1.172 +  from mod_mult2_eq [of n 16 16]
   1.173 +  have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
   1.174 +  then show ?thesis
   1.175 +    by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble
   1.176 +      card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add_commute)
   1.177 +qed
   1.178 +
   1.179 +lemma char_of_nat_of_char [simp]:
   1.180 +  "char_of_nat (nat_of_char c) = c"
   1.181 +  by (cases c)
   1.182 +    (simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char)
   1.183 +
   1.184 +lemma nat_of_char_of_nat [simp]:
   1.185 +  "nat_of_char (char_of_nat n) = n mod 256"
   1.186 +proof -
   1.187 +  have "n mod 256 = n mod (16 * 16)" by simp
   1.188 +  then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq)
   1.189 +  then show ?thesis
   1.190 +    by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
   1.191 +qed
   1.192 +
   1.193 +lemma inj_nat_of_char:
   1.194 +  "inj nat_of_char"
   1.195 +  by (rule inj_on_inverseI) (rule char_of_nat_of_char)
   1.196 +
   1.197 +lemma nat_of_char_eq_iff:
   1.198 +  "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
   1.199 +  by (rule inj_eq) (rule inj_nat_of_char)
   1.200 +
   1.201 +lemma nat_of_char_less_256:
   1.202 +  "nat_of_char c < 256"
   1.203 +proof (cases c)
   1.204 +  case (Char x y)
   1.205 +  with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
   1.206 +  show ?thesis by (simp add: nat_of_char_def)
   1.207 +qed
   1.208 +
   1.209 +lemma char_of_nat_mod_256:
   1.210 +  "char_of_nat (n mod 256) = char_of_nat n"
   1.211 +proof -
   1.212 +  from nibble_of_nat_mod_16 [of "n mod 256"]
   1.213 +  have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp
   1.214 +  with nibble_of_nat_mod_16 [of n]
   1.215 +  have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel)
   1.216 +  have "n mod 256 = n mod (16 * 16)" by simp
   1.217 +  then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq)
   1.218 +  show ?thesis
   1.219 +    by (simp add: char_of_nat_Char_nibbles *)
   1.220 +     (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **)
   1.221 +qed
   1.222  
   1.223  
   1.224  subsection {* Strings as dedicated type *}
   1.225 @@ -228,8 +381,9 @@
   1.226  
   1.227  end
   1.228  
   1.229 -lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
   1.230 -by(simp add: STR_inject)
   1.231 +lemma STR_inject' [simp]:
   1.232 +  "STR xs = STR ys \<longleftrightarrow> xs = ys"
   1.233 +  by (simp add: STR_inject)
   1.234  
   1.235  
   1.236  subsection {* Code generator *}