src/HOL/String.thy
changeset 62597 b3f2b8c906a6
parent 62580 7011429f44f9
child 62678 843ff6f1de38
     1.1 --- a/src/HOL/String.thy	Fri Mar 11 17:20:14 2016 +0100
     1.2 +++ b/src/HOL/String.thy	Sat Mar 12 22:04:52 2016 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4    by (simp add: char_of_nat_def Abs_char_inject)
     1.5  
     1.6  lemma inj_on_char_of_nat [simp]:
     1.7 -  "inj_on char_of_nat {0..<256}"
     1.8 +  "inj_on char_of_nat {..<256}"
     1.9    by (rule inj_onI) simp
    1.10  
    1.11  lemma nat_of_char_mod_256 [simp]:
    1.12 @@ -72,197 +72,143 @@
    1.13  qed
    1.14  
    1.15  lemma UNIV_char_of_nat:
    1.16 -  "UNIV = char_of_nat ` {0..<256}"
    1.17 +  "UNIV = char_of_nat ` {..<256}"
    1.18  proof -
    1.19    { fix c
    1.20 -    have "c \<in> char_of_nat ` {0..<256}"
    1.21 +    have "c \<in> char_of_nat ` {..<256}"
    1.22        by (cases c) auto
    1.23    } then show ?thesis by auto
    1.24  qed
    1.25  
    1.26 -
    1.27 -subsubsection \<open>Traditional concrete representation of characters\<close>
    1.28 -
    1.29 -datatype (plugins del: transfer) nibble =
    1.30 -    Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    1.31 -  | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    1.32 +lemma card_UNIV_char:
    1.33 +  "card (UNIV :: char set) = 256"
    1.34 +  by (auto simp add: UNIV_char_of_nat card_image)
    1.35  
    1.36 -lemma UNIV_nibble:
    1.37 -  "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
    1.38 -    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
    1.39 -proof (rule UNIV_eq_I)
    1.40 -  fix x show "x \<in> ?A" by (cases x) simp_all
    1.41 -qed
    1.42 +lemma range_nat_of_char:
    1.43 +  "range nat_of_char = {..<256}"
    1.44 +  by (auto simp add: UNIV_char_of_nat image_image image_def)
    1.45  
    1.46 -lemma size_nibble [code, simp]:
    1.47 -  "size_nibble (x::nibble) = 0"
    1.48 -  "size (x::nibble) = 0"
    1.49 -  by (cases x, simp_all)+
    1.50  
    1.51 -instantiation nibble :: enum
    1.52 +subsubsection \<open>Character literals as variant of numerals\<close>
    1.53 +
    1.54 +instantiation char :: zero
    1.55  begin
    1.56  
    1.57 -definition
    1.58 -  "Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
    1.59 -    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
    1.60 +definition zero_char :: char
    1.61 +  where "0 = char_of_nat 0"
    1.62  
    1.63 -definition
    1.64 -  "Enum.enum_all P \<longleftrightarrow> P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7
    1.65 -     \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
    1.66 -
    1.67 -definition
    1.68 -  "Enum.enum_ex P \<longleftrightarrow> P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7
    1.69 -     \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
    1.70 -
    1.71 -instance proof
    1.72 -qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
    1.73 +instance ..
    1.74  
    1.75  end
    1.76  
    1.77 -lemma card_UNIV_nibble:
    1.78 -  "card (UNIV :: nibble set) = 16"
    1.79 -  by (simp add: card_UNIV_length_enum enum_nibble_def)
    1.80 +definition Char :: "num \<Rightarrow> char"
    1.81 +  where "Char k = char_of_nat (numeral k)"
    1.82 +
    1.83 +code_datatype "0 :: char" Char
    1.84 +
    1.85 +lemma nat_of_char_zero [simp]:
    1.86 +  "nat_of_char 0 = 0"
    1.87 +  by (simp add: zero_char_def)
    1.88 +
    1.89 +lemma nat_of_char_Char [simp]:
    1.90 +  "nat_of_char (Char k) = numeral k mod 256"
    1.91 +  by (simp add: Char_def)
    1.92  
    1.93 -primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
    1.94 +lemma Char_eq_Char_iff [simp]:
    1.95 +  "Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
    1.96 +proof -
    1.97 +  have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
    1.98 +    by (rule sym, rule inj_eq) (fact inj_nat_of_char)
    1.99 +  also have "nat_of_char (Char k) = nat_of_char (Char l) \<longleftrightarrow> ?Q"
   1.100 +    by (simp only: Char_def nat_of_char_of_nat)
   1.101 +  finally show ?thesis .
   1.102 +qed
   1.103 +
   1.104 +lemma zero_eq_Char_iff [simp]:
   1.105 +  "0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
   1.106 +  by (auto simp add: zero_char_def Char_def)
   1.107 +
   1.108 +lemma Char_eq_zero_iff [simp]:
   1.109 +  "Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
   1.110 +  by (auto simp add: zero_char_def Char_def) 
   1.111 +
   1.112 +definition integer_of_char :: "char \<Rightarrow> integer"
   1.113  where
   1.114 -  "nat_of_nibble Nibble0 = 0"
   1.115 -| "nat_of_nibble Nibble1 = 1"
   1.116 -| "nat_of_nibble Nibble2 = 2"
   1.117 -| "nat_of_nibble Nibble3 = 3"
   1.118 -| "nat_of_nibble Nibble4 = 4"
   1.119 -| "nat_of_nibble Nibble5 = 5"
   1.120 -| "nat_of_nibble Nibble6 = 6"
   1.121 -| "nat_of_nibble Nibble7 = 7"
   1.122 -| "nat_of_nibble Nibble8 = 8"
   1.123 -| "nat_of_nibble Nibble9 = 9"
   1.124 -| "nat_of_nibble NibbleA = 10"
   1.125 -| "nat_of_nibble NibbleB = 11"
   1.126 -| "nat_of_nibble NibbleC = 12"
   1.127 -| "nat_of_nibble NibbleD = 13"
   1.128 -| "nat_of_nibble NibbleE = 14"
   1.129 -| "nat_of_nibble NibbleF = 15"
   1.130 +  "integer_of_char = integer_of_nat \<circ> nat_of_char"
   1.131  
   1.132 -definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
   1.133 -  "nibble_of_nat n = Enum.enum ! (n mod 16)"
   1.134 +definition char_of_integer :: "integer \<Rightarrow> char"
   1.135 +where
   1.136 +  "char_of_integer = char_of_nat \<circ> nat_of_integer"
   1.137 +
   1.138 +lemma integer_of_char_zero [simp, code]:
   1.139 +  "integer_of_char 0 = 0"
   1.140 +  by (simp add: integer_of_char_def integer_of_nat_def)
   1.141  
   1.142 -lemma nibble_of_nat_simps [simp]:
   1.143 -  "nibble_of_nat  0 = Nibble0"
   1.144 -  "nibble_of_nat  1 = Nibble1"
   1.145 -  "nibble_of_nat  2 = Nibble2"
   1.146 -  "nibble_of_nat  3 = Nibble3"
   1.147 -  "nibble_of_nat  4 = Nibble4"
   1.148 -  "nibble_of_nat  5 = Nibble5"
   1.149 -  "nibble_of_nat  6 = Nibble6"
   1.150 -  "nibble_of_nat  7 = Nibble7"
   1.151 -  "nibble_of_nat  8 = Nibble8"
   1.152 -  "nibble_of_nat  9 = Nibble9"
   1.153 -  "nibble_of_nat 10 = NibbleA"
   1.154 -  "nibble_of_nat 11 = NibbleB"
   1.155 -  "nibble_of_nat 12 = NibbleC"
   1.156 -  "nibble_of_nat 13 = NibbleD"
   1.157 -  "nibble_of_nat 14 = NibbleE"
   1.158 -  "nibble_of_nat 15 = NibbleF"
   1.159 -  unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
   1.160 +lemma integer_of_char_Char [simp]:
   1.161 +  "integer_of_char (Char k) = numeral k mod 256"
   1.162 +  by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
   1.163 +    id_apply zmod_int mod_integer.abs_eq [symmetric]) simp
   1.164  
   1.165 -lemma nibble_of_nat_of_nibble [simp]:
   1.166 -  "nibble_of_nat (nat_of_nibble x) = x"
   1.167 -  by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
   1.168 +lemma less_256_integer_of_char_Char:
   1.169 +  assumes "numeral k < (256 :: integer)"
   1.170 +  shows "integer_of_char (Char k) = numeral k"
   1.171 +proof -
   1.172 +  have "numeral k mod 256 = (numeral k :: integer)"
   1.173 +    by (rule semiring_numeral_div_class.mod_less) (insert assms, simp_all)
   1.174 +  then show ?thesis using integer_of_char_Char [of k]
   1.175 +    by (simp only:)
   1.176 +qed
   1.177  
   1.178 -lemma nat_of_nibble_of_nat [simp]:
   1.179 -  "nat_of_nibble (nibble_of_nat n) = n mod 16"
   1.180 -  by (cases "nibble_of_nat n")
   1.181 -     (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
   1.182 -
   1.183 -lemma inj_nat_of_nibble:
   1.184 -  "inj nat_of_nibble"
   1.185 -  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
   1.186 +setup \<open>
   1.187 +let
   1.188 +  val chars = map_range (Thm.cterm_of @{context} o HOLogic.mk_numeral o curry (op +) 1) 255;
   1.189 +  val simpset =
   1.190 +    put_simpset HOL_ss @{context}
   1.191 +      addsimps @{thms numeral_less_iff less_num_simps};
   1.192 +  fun mk_code_eqn ct =
   1.193 +    Thm.instantiate' [] [SOME ct] @{thm less_256_integer_of_char_Char}
   1.194 +    |> full_simplify simpset;
   1.195 +  val code_eqns = map mk_code_eqn chars;
   1.196 +in
   1.197 +  Global_Theory.note_thmss ""
   1.198 +    [((@{binding integer_of_char_simps}, []), [(code_eqns, [])])]
   1.199 +  #> snd
   1.200 +end
   1.201 +\<close>
   1.202  
   1.203 -lemma nat_of_nibble_eq_iff:
   1.204 -  "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
   1.205 -  by (rule inj_eq) (rule inj_nat_of_nibble)
   1.206 +declare integer_of_char_simps [code]
   1.207 +
   1.208 +lemma nat_of_char_code [code]:
   1.209 +  "nat_of_char = nat_of_integer \<circ> integer_of_char"
   1.210 +  by (simp add: integer_of_char_def fun_eq_iff)
   1.211  
   1.212 -lemma nat_of_nibble_less_16:
   1.213 -  "nat_of_nibble x < 16"
   1.214 -  by (cases x) auto
   1.215 +lemma char_of_nat_code [code]:
   1.216 +  "char_of_nat = char_of_integer \<circ> integer_of_nat"
   1.217 +  by (simp add: char_of_integer_def fun_eq_iff)
   1.218  
   1.219 -lemma nibble_of_nat_mod_16:
   1.220 -  "nibble_of_nat (n mod 16) = nibble_of_nat n"
   1.221 -  by (simp add: nibble_of_nat_def)
   1.222 -
   1.223 -context
   1.224 +instantiation char :: equal
   1.225  begin
   1.226  
   1.227 -local_setup \<open>Local_Theory.map_background_naming (Name_Space.add_path "char")\<close>
   1.228 +definition equal_char
   1.229 +  where "equal_char (c :: char) d \<longleftrightarrow> c = d"
   1.230  
   1.231 -definition Char :: "nibble \<Rightarrow> nibble \<Rightarrow> char"
   1.232 -where
   1.233 -  "Char x y = char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y)"
   1.234 -  \<comment> "Note: canonical order of character encoding coincides with standard term ordering"
   1.235 +instance
   1.236 +  by standard (simp add: equal_char_def)
   1.237  
   1.238  end
   1.239  
   1.240 -lemma nat_of_char_Char:
   1.241 -  "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y" (is "_ = ?rhs")
   1.242 -proof -
   1.243 -  have "?rhs < 256"
   1.244 -    using nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
   1.245 -    by arith
   1.246 -  then show ?thesis by (simp add: Char_def)
   1.247 -qed
   1.248 -
   1.249 -lemma char_of_nat_Char_nibbles:
   1.250 -  "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
   1.251 -proof -
   1.252 -  from mod_mult2_eq [of n 16 16]
   1.253 -  have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
   1.254 -  then show ?thesis
   1.255 -    by (simp add: Char_def)
   1.256 -qed
   1.257 -
   1.258 -lemma char_of_nat_nibble_pair [simp]:
   1.259 -  "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
   1.260 -  by (simp add: nat_of_char_Char [symmetric])
   1.261 -
   1.262 -free_constructors char for Char
   1.263 -proof -
   1.264 -  fix P c
   1.265 -  assume hyp: "\<And>x y. c = Char x y \<Longrightarrow> P"
   1.266 -  have "nat_of_char c \<le> 255"
   1.267 -    using nat_of_char_less_256 [of c] by arith
   1.268 -  then have "nat_of_char c div 16 \<le> 255 div 16"
   1.269 -    by (auto intro: div_le_mono2)
   1.270 -  then have "nat_of_char c div 16 < 16"
   1.271 -    by auto
   1.272 -  then have "nat_of_char c div 16 mod 16 = nat_of_char c div 16"
   1.273 -    by simp
   1.274 -  then have "c = Char (nibble_of_nat (nat_of_char c div 16))
   1.275 -    (nibble_of_nat (nat_of_char c mod 16))"
   1.276 -    by (simp add: Char_def)
   1.277 -  then show P by (rule hyp)
   1.278 -next
   1.279 -  fix x y z w
   1.280 -  have "Char x y = Char z w
   1.281 -    \<longleftrightarrow> nat_of_char (Char x y) = nat_of_char (Char z w)"
   1.282 -    by auto
   1.283 -  also have "\<dots> \<longleftrightarrow> nat_of_nibble x = nat_of_nibble z \<and> nat_of_nibble y = nat_of_nibble w" (is "?P \<longleftrightarrow> ?Q \<and> ?R")
   1.284 -  proof
   1.285 -    assume "?Q \<and> ?R"
   1.286 -    then show ?P by (simp add: nat_of_char_Char)
   1.287 -  next
   1.288 -    assume ?P
   1.289 -    then have ?Q
   1.290 -      using nat_of_nibble_less_16 [of y] nat_of_nibble_less_16 [of w]
   1.291 -      by (simp add: nat_of_char_Char)
   1.292 -    moreover with \<open>?P\<close> have ?R by (simp add: nat_of_char_Char)
   1.293 -    ultimately show "?Q \<and> ?R" ..
   1.294 -  qed
   1.295 -  also have "\<dots> \<longleftrightarrow> x = z \<and> y = w"
   1.296 -    by (simp add: nat_of_nibble_eq_iff)
   1.297 -  finally show "Char x y = Char z w \<longleftrightarrow> x = z \<and> y = w" .
   1.298 -qed
   1.299 +lemma equal_char_simps [code]:
   1.300 +  "HOL.equal (0::char) 0 \<longleftrightarrow> True"
   1.301 +  "HOL.equal (Char k) (Char l) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) (numeral l mod 256)"
   1.302 +  "HOL.equal 0 (Char k) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
   1.303 +  "HOL.equal (Char k) 0 \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
   1.304 +  by (simp_all only: equal refl Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff)
   1.305  
   1.306  syntax
   1.307 -  "_Char" :: "str_position => char"    ("CHR _")
   1.308 +  "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
   1.309 +
   1.310 +syntax
   1.311 +  "_Char_ord" :: "num_const \<Rightarrow> char"     ("CHAR _")
   1.312  
   1.313  type_synonym string = "char list"
   1.314  
   1.315 @@ -271,84 +217,74 @@
   1.316  
   1.317  ML_file "Tools/string_syntax.ML"
   1.318  
   1.319 -lemma UNIV_char:
   1.320 -  "UNIV = image (case_prod Char) (UNIV \<times> UNIV)"
   1.321 -proof (rule UNIV_eq_I)
   1.322 -  fix x show "x \<in> image (case_prod Char) (UNIV \<times> UNIV)" by (cases x) auto
   1.323 -qed
   1.324 -
   1.325  instantiation char :: enum
   1.326  begin
   1.327  
   1.328  definition
   1.329 -  "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
   1.330 -  Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
   1.331 -  Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
   1.332 -  Char Nibble0 Nibble9, CHR ''\<newline>'', Char Nibble0 NibbleB,
   1.333 -  Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
   1.334 -  Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
   1.335 -  Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
   1.336 -  Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
   1.337 -  Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
   1.338 -  Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
   1.339 -  Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
   1.340 -  Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
   1.341 -  Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
   1.342 -  CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
   1.343 -  CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
   1.344 -  CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
   1.345 -  CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
   1.346 -  CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
   1.347 -  CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
   1.348 -  CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
   1.349 -  CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
   1.350 -  CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
   1.351 -  CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
   1.352 -  CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
   1.353 -  CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
   1.354 -  Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
   1.355 -  Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
   1.356 -  Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
   1.357 -  Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
   1.358 -  Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
   1.359 -  Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
   1.360 -  Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
   1.361 -  Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
   1.362 -  Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
   1.363 -  Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
   1.364 -  Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
   1.365 -  Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
   1.366 -  Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
   1.367 -  Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
   1.368 -  Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
   1.369 -  Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
   1.370 -  Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
   1.371 -  Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
   1.372 -  Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
   1.373 -  Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
   1.374 -  Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
   1.375 -  Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
   1.376 -  Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
   1.377 -  Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
   1.378 -  Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
   1.379 -  Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
   1.380 -  Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
   1.381 -  Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
   1.382 -  Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
   1.383 -  Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
   1.384 -  Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
   1.385 -  Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
   1.386 -  Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
   1.387 -  Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
   1.388 -  Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
   1.389 -  Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
   1.390 -  Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
   1.391 -  Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
   1.392 -  Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
   1.393 -  Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
   1.394 -  Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
   1.395 -  Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
   1.396 -  Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
   1.397 +  "Enum.enum = [0, CHAR 0x01, CHAR 0x02, CHAR 0x03,
   1.398 +    CHAR 0x04, CHAR 0x05, CHAR 0x06, CHAR 0x07,
   1.399 +    CHAR 0x08, CHAR 0x09, CHR ''\<newline>'', CHAR 0x0B,
   1.400 +    CHAR 0x0C, CHAR 0x0D, CHAR 0x0E, CHAR 0x0F,
   1.401 +    CHAR 0x10, CHAR 0x11, CHAR 0x12, CHAR 0x13,
   1.402 +    CHAR 0x14, CHAR 0x15, CHAR 0x16, CHAR 0x17,
   1.403 +    CHAR 0x18, CHAR 0x19, CHAR 0x1A, CHAR 0x1B,
   1.404 +    CHAR 0x1C, CHAR 0x1D, CHAR 0x1E, CHAR 0x1F,
   1.405 +    CHR '' '', CHR ''!'', CHAR 0x22, CHR ''#'',
   1.406 +    CHR ''$'', CHR ''%'', CHR ''&'', CHAR 0x27,
   1.407 +    CHR ''('', CHR '')'', CHR ''*'', CHR ''+'',
   1.408 +    CHR '','', CHR ''-'', CHR ''.'', CHR ''/'',
   1.409 +    CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
   1.410 +    CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'',
   1.411 +    CHR ''8'', CHR ''9'', CHR '':'', CHR '';'',
   1.412 +    CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'',
   1.413 +    CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'',
   1.414 +    CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'',
   1.415 +    CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'',
   1.416 +    CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
   1.417 +    CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'',
   1.418 +    CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'',
   1.419 +    CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['',
   1.420 +    CHAR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
   1.421 +    CHAR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
   1.422 +    CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'',
   1.423 +    CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'',
   1.424 +    CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'',
   1.425 +    CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'',
   1.426 +    CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
   1.427 +    CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'',
   1.428 +    CHR ''|'', CHR ''}'', CHR ''~'', CHAR 0x7F,
   1.429 +    CHAR 0x80, CHAR 0x81, CHAR 0x82, CHAR 0x83,
   1.430 +    CHAR 0x84, CHAR 0x85, CHAR 0x86, CHAR 0x87,
   1.431 +    CHAR 0x88, CHAR 0x89, CHAR 0x8A, CHAR 0x8B,
   1.432 +    CHAR 0x8C, CHAR 0x8D, CHAR 0x8E, CHAR 0x8F,
   1.433 +    CHAR 0x90, CHAR 0x91, CHAR 0x92, CHAR 0x93,
   1.434 +    CHAR 0x94, CHAR 0x95, CHAR 0x96, CHAR 0x97,
   1.435 +    CHAR 0x98, CHAR 0x99, CHAR 0x9A, CHAR 0x9B,
   1.436 +    CHAR 0x9C, CHAR 0x9D, CHAR 0x9E, CHAR 0x9F,
   1.437 +    CHAR 0xA0, CHAR 0xA1, CHAR 0xA2, CHAR 0xA3,
   1.438 +    CHAR 0xA4, CHAR 0xA5, CHAR 0xA6, CHAR 0xA7,
   1.439 +    CHAR 0xA8, CHAR 0xA9, CHAR 0xAA, CHAR 0xAB,
   1.440 +    CHAR 0xAC, CHAR 0xAD, CHAR 0xAE, CHAR 0xAF,
   1.441 +    CHAR 0xB0, CHAR 0xB1, CHAR 0xB2, CHAR 0xB3,
   1.442 +    CHAR 0xB4, CHAR 0xB5, CHAR 0xB6, CHAR 0xB7,
   1.443 +    CHAR 0xB8, CHAR 0xB9, CHAR 0xBA, CHAR 0xBB,
   1.444 +    CHAR 0xBC, CHAR 0xBD, CHAR 0xBE, CHAR 0xBF,
   1.445 +    CHAR 0xC0, CHAR 0xC1, CHAR 0xC2, CHAR 0xC3,
   1.446 +    CHAR 0xC4, CHAR 0xC5, CHAR 0xC6, CHAR 0xC7,
   1.447 +    CHAR 0xC8, CHAR 0xC9, CHAR 0xCA, CHAR 0xCB,
   1.448 +    CHAR 0xCC, CHAR 0xCD, CHAR 0xCE, CHAR 0xCF,
   1.449 +    CHAR 0xD0, CHAR 0xD1, CHAR 0xD2, CHAR 0xD3,
   1.450 +    CHAR 0xD4, CHAR 0xD5, CHAR 0xD6, CHAR 0xD7,
   1.451 +    CHAR 0xD8, CHAR 0xD9, CHAR 0xDA, CHAR 0xDB,
   1.452 +    CHAR 0xDC, CHAR 0xDD, CHAR 0xDE, CHAR 0xDF,
   1.453 +    CHAR 0xE0, CHAR 0xE1, CHAR 0xE2, CHAR 0xE3,
   1.454 +    CHAR 0xE4, CHAR 0xE5, CHAR 0xE6, CHAR 0xE7,
   1.455 +    CHAR 0xE8, CHAR 0xE9, CHAR 0xEA, CHAR 0xEB,
   1.456 +    CHAR 0xEC, CHAR 0xED, CHAR 0xEE, CHAR 0xEF,
   1.457 +    CHAR 0xF0, CHAR 0xF1, CHAR 0xF2, CHAR 0xF3,
   1.458 +    CHAR 0xF4, CHAR 0xF5, CHAR 0xF6, CHAR 0xF7,
   1.459 +    CHAR 0xF8, CHAR 0xF9, CHAR 0xFA, CHAR 0xFB,
   1.460 +    CHAR 0xFC, CHAR 0xFD, CHAR 0xFE, CHAR 0xFF]"
   1.461  
   1.462  definition
   1.463    "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
   1.464 @@ -356,15 +292,22 @@
   1.465  definition
   1.466    "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
   1.467  
   1.468 -lemma enum_char_product_enum_nibble:
   1.469 -  "(Enum.enum :: char list) = map (case_prod Char) (List.product Enum.enum Enum.enum)"
   1.470 -  by (simp add: enum_char_def enum_nibble_def)
   1.471 +lemma enum_char_unfold:
   1.472 +  "Enum.enum = map char_of_nat [0..<256]"
   1.473 +proof -
   1.474 +  have *: "Suc (Suc 0) = 2" by simp
   1.475 +  have "map nat_of_char Enum.enum = [0..<256]"
   1.476 +    by (simp add: enum_char_def upt_conv_Cons_Cons *)
   1.477 +  then have "map char_of_nat (map nat_of_char Enum.enum) =
   1.478 +    map char_of_nat [0..<256]" by simp
   1.479 +  then show ?thesis by (simp add: comp_def)
   1.480 +qed
   1.481  
   1.482  instance proof
   1.483    show UNIV: "UNIV = set (Enum.enum :: char list)"
   1.484 -    by (simp add: enum_char_product_enum_nibble UNIV_char enum_UNIV)
   1.485 +    by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan)
   1.486    show "distinct (Enum.enum :: char list)"
   1.487 -    by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
   1.488 +    by (auto simp add: enum_char_unfold distinct_map intro: inj_onI)
   1.489    show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
   1.490      by (simp add: UNIV enum_all_char_def list_all_iff)
   1.491    show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
   1.492 @@ -373,66 +316,9 @@
   1.493  
   1.494  end
   1.495  
   1.496 -lemma card_UNIV_char:
   1.497 -  "card (UNIV :: char set) = 256"
   1.498 -  by (simp add: card_UNIV_length_enum enum_char_def)
   1.499 -
   1.500 -lemma enum_char_unfold:
   1.501 -  "Enum.enum = map char_of_nat [0..<256]"
   1.502 -proof -
   1.503 -  have *: "Suc (Suc 0) = 2" by simp
   1.504 -  have "map nat_of_char Enum.enum = [0..<256]"
   1.505 -    by (simp add: enum_char_def nat_of_char_Char upt_conv_Cons_Cons *)
   1.506 -  then have "map char_of_nat (map nat_of_char Enum.enum) =
   1.507 -    map char_of_nat [0..<256]" by simp
   1.508 -  then show ?thesis by (simp add: comp_def)
   1.509 -qed
   1.510 -
   1.511 -setup \<open>
   1.512 -let
   1.513 -  val nibbles = map_range (Thm.cterm_of @{context} o HOLogic.mk_nibble) 16;
   1.514 -  val simpset =
   1.515 -    put_simpset HOL_ss @{context}
   1.516 -      addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
   1.517 -  fun mk_code_eqn x y =
   1.518 -    Thm.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
   1.519 -    |> simplify simpset;
   1.520 -  val code_eqns = map_product mk_code_eqn nibbles nibbles;
   1.521 -in
   1.522 -  Global_Theory.note_thmss ""
   1.523 -    [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
   1.524 -  #> snd
   1.525 -end
   1.526 -\<close>
   1.527 -
   1.528 -declare nat_of_char_simps [code]
   1.529 -
   1.530 -lemma nibble_of_nat_of_char_div_16:
   1.531 -  "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
   1.532 -  by (cases c)
   1.533 -    (simp add: nat_of_char_Char add.commute nat_of_nibble_less_16)
   1.534 -
   1.535 -lemma nibble_of_nat_nat_of_char:
   1.536 -  "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
   1.537 -proof (cases c)
   1.538 -  case (Char x y)
   1.539 -  then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
   1.540 -    by (simp add: nibble_of_nat_mod_16)
   1.541 -  then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
   1.542 -    by (simp only: nibble_of_nat_mod_16)
   1.543 -  with Char show ?thesis by (simp add: nat_of_char_Char add.commute)
   1.544 -qed
   1.545 -
   1.546 -code_datatype Char \<comment> \<open>drop case certificate for char\<close>
   1.547 -
   1.548 -lemma case_char_code [code]:
   1.549 -  "char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
   1.550 -  by (cases c)
   1.551 -    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
   1.552 -
   1.553 -lemma char_of_nat_enum [code]:
   1.554 -  "char_of_nat n = Enum.enum ! (n mod 256)"
   1.555 -  by (simp add: enum_char_unfold)
   1.556 +lemma char_of_integer_code [code]:
   1.557 +  "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
   1.558 +  by (simp add: char_of_integer_def enum_char_unfold)
   1.559  
   1.560  
   1.561  subsection \<open>Strings as dedicated type\<close>