src/HOL/String.thy

 lemma char_of_nat_quasi_inj [simp]:
   "char_of_nat m = char_of_nat n \<longleftrightarrow> m mod 256 = n mod 256"
   by (simp add: char_of_nat_def Abs_char_inject)
 
 lemma inj_on_char_of_nat [simp]:
-  "inj_on char_of_nat {0..<256}"
+  "inj_on char_of_nat {..<256}"
   by (rule inj_onI) simp
 
 lemma nat_of_char_mod_256 [simp]:
   "nat_of_char c mod 256 = nat_of_char c"
   by (cases c) simp

     by arith
   then show ?thesis by simp
 qed
 
 lemma UNIV_char_of_nat:
-  "UNIV = char_of_nat ` {0..<256}"
+  "UNIV = char_of_nat ` {..<256}"
 proof -
   { fix c
-    have "c \<in> char_of_nat ` {0..<256}"
+    have "c \<in> char_of_nat ` {..<256}"
       by (cases c) auto
   } then show ?thesis by auto
 qed
 
-
-subsubsection \<open>Traditional concrete representation of characters\<close>
-
-datatype (plugins del: transfer) nibble =
-    Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
-  | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
-
-lemma UNIV_nibble:
-  "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
-    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
-proof (rule UNIV_eq_I)
-  fix x show "x \<in> ?A" by (cases x) simp_all
-qed
-
-lemma size_nibble [code, simp]:
-  "size_nibble (x::nibble) = 0"
-  "size (x::nibble) = 0"
-  by (cases x, simp_all)+
-
-instantiation nibble :: enum
-begin
-
-definition
-  "Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
-    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
-
-definition
-  "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
-     \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
-
-definition
-  "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
-     \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
-
-instance proof
-qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
-
-end
-
-lemma card_UNIV_nibble:
-  "card (UNIV :: nibble set) = 16"
-  by (simp add: card_UNIV_length_enum enum_nibble_def)
-
-primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
+lemma card_UNIV_char:
+  "card (UNIV :: char set) = 256"
+  by (auto simp add: UNIV_char_of_nat card_image)
+
+lemma range_nat_of_char:
+  "range nat_of_char = {..<256}"
+  by (auto simp add: UNIV_char_of_nat image_image image_def)
+
+
+subsubsection \<open>Character literals as variant of numerals\<close>
+
+instantiation char :: zero
+begin
+
+definition zero_char :: char
+  where "0 = char_of_nat 0"
+
+instance ..
+
+end
+
+definition Char :: "num \<Rightarrow> char"
+  where "Char k = char_of_nat (numeral k)"
+
+code_datatype "0 :: char" Char
+
+lemma nat_of_char_zero [simp]:
+  "nat_of_char 0 = 0"
+  by (simp add: zero_char_def)
+
+lemma nat_of_char_Char [simp]:
+  "nat_of_char (Char k) = numeral k mod 256"
+  by (simp add: Char_def)
+
+lemma Char_eq_Char_iff [simp]:
+  "Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
+proof -
+  have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
+    by (rule sym, rule inj_eq) (fact inj_nat_of_char)
+  also have "nat_of_char (Char k) = nat_of_char (Char l) \<longleftrightarrow> ?Q"
+    by (simp only: Char_def nat_of_char_of_nat)
+  finally show ?thesis .
+qed
+
+lemma zero_eq_Char_iff [simp]:
+  "0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
+  by (auto simp add: zero_char_def Char_def)
+
+lemma Char_eq_zero_iff [simp]:
+  "Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
+  by (auto simp add: zero_char_def Char_def) 
+
+definition integer_of_char :: "char \<Rightarrow> integer"
 where
-  "nat_of_nibble Nibble0 = 0"
-| "nat_of_nibble Nibble1 = 1"
-| "nat_of_nibble Nibble2 = 2"
-| "nat_of_nibble Nibble3 = 3"
-| "nat_of_nibble Nibble4 = 4"
-| "nat_of_nibble Nibble5 = 5"
-| "nat_of_nibble Nibble6 = 6"
-| "nat_of_nibble Nibble7 = 7"
-| "nat_of_nibble Nibble8 = 8"
-| "nat_of_nibble Nibble9 = 9"
-| "nat_of_nibble NibbleA = 10"
-| "nat_of_nibble NibbleB = 11"
-| "nat_of_nibble NibbleC = 12"
-| "nat_of_nibble NibbleD = 13"
-| "nat_of_nibble NibbleE = 14"
-| "nat_of_nibble NibbleF = 15"
-
-definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
-  "nibble_of_nat n = Enum.enum ! (n mod 16)"
-
-lemma nibble_of_nat_simps [simp]:
-  "nibble_of_nat  0 = Nibble0"
-  "nibble_of_nat  1 = Nibble1"
-  "nibble_of_nat  2 = Nibble2"
-  "nibble_of_nat  3 = Nibble3"
-  "nibble_of_nat  4 = Nibble4"
-  "nibble_of_nat  5 = Nibble5"
-  "nibble_of_nat  6 = Nibble6"
-  "nibble_of_nat  7 = Nibble7"
-  "nibble_of_nat  8 = Nibble8"
-  "nibble_of_nat  9 = Nibble9"
-  "nibble_of_nat 10 = NibbleA"
-  "nibble_of_nat 11 = NibbleB"
-  "nibble_of_nat 12 = NibbleC"
-  "nibble_of_nat 13 = NibbleD"
-  "nibble_of_nat 14 = NibbleE"
-  "nibble_of_nat 15 = NibbleF"
-  unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
-
-lemma nibble_of_nat_of_nibble [simp]:
-  "nibble_of_nat (nat_of_nibble x) = x"
-  by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
-
-lemma nat_of_nibble_of_nat [simp]:
-  "nat_of_nibble (nibble_of_nat n) = n mod 16"
-  by (cases "nibble_of_nat n")
-     (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
-
-lemma inj_nat_of_nibble:
-  "inj nat_of_nibble"
-  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
-
-lemma nat_of_nibble_eq_iff:
-  "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
-  by (rule inj_eq) (rule inj_nat_of_nibble)
-
-lemma nat_of_nibble_less_16:
-  "nat_of_nibble x < 16"
-  by (cases x) auto
-
-lemma nibble_of_nat_mod_16:
-  "nibble_of_nat (n mod 16) = nibble_of_nat n"
-  by (simp add: nibble_of_nat_def)
-
-context
-begin
-
-local_setup \<open>Local_Theory.map_background_naming (Name_Space.add_path "char")\<close>
-
-definition Char :: "nibble \<Rightarrow> nibble \<Rightarrow> char"
+  "integer_of_char = integer_of_nat \<circ> nat_of_char"
+
+definition char_of_integer :: "integer \<Rightarrow> char"
 where
-  "Char x y = char_of_nat (nat_of_nibble x * 16 + nat_of_nibble y)"
-  \<comment> "Note: canonical order of character encoding coincides with standard term ordering"
-
-end
-
-lemma nat_of_char_Char:
-  "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y" (is "_ = ?rhs")
+  "char_of_integer = char_of_nat \<circ> nat_of_integer"
+
+lemma integer_of_char_zero [simp, code]:
+  "integer_of_char 0 = 0"
+  by (simp add: integer_of_char_def integer_of_nat_def)
+
+lemma integer_of_char_Char [simp]:
+  "integer_of_char (Char k) = numeral k mod 256"
+  by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
+    id_apply zmod_int mod_integer.abs_eq [symmetric]) simp
+
+lemma less_256_integer_of_char_Char:
+  assumes "numeral k < (256 :: integer)"
+  shows "integer_of_char (Char k) = numeral k"
 proof -
-  have "?rhs < 256"
-    using nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
-    by arith
-  then show ?thesis by (simp add: Char_def)
-qed
-
-lemma char_of_nat_Char_nibbles:
-  "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
-proof -
-  from mod_mult2_eq [of n 16 16]
-  have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
-  then show ?thesis
-    by (simp add: Char_def)
-qed
-
-lemma char_of_nat_nibble_pair [simp]:
-  "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
-  by (simp add: nat_of_char_Char [symmetric])
-
-free_constructors char for Char
-proof -
-  fix P c
-  assume hyp: "\<And>x y. c = Char x y \<Longrightarrow> P"
-  have "nat_of_char c \<le> 255"
-    using nat_of_char_less_256 [of c] by arith
-  then have "nat_of_char c div 16 \<le> 255 div 16"
-    by (auto intro: div_le_mono2)
-  then have "nat_of_char c div 16 < 16"
-    by auto
-  then have "nat_of_char c div 16 mod 16 = nat_of_char c div 16"
-    by simp
-  then have "c = Char (nibble_of_nat (nat_of_char c div 16))
-    (nibble_of_nat (nat_of_char c mod 16))"
-    by (simp add: Char_def)
-  then show P by (rule hyp)
-next
-  fix x y z w
-  have "Char x y = Char z w
-    \<longleftrightarrow> nat_of_char (Char x y) = nat_of_char (Char z w)"
-    by auto
-  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")
-  proof
-    assume "?Q \<and> ?R"
-    then show ?P by (simp add: nat_of_char_Char)
-  next
-    assume ?P
-    then have ?Q
-      using nat_of_nibble_less_16 [of y] nat_of_nibble_less_16 [of w]
-      by (simp add: nat_of_char_Char)
-    moreover with \<open>?P\<close> have ?R by (simp add: nat_of_char_Char)
-    ultimately show "?Q \<and> ?R" ..
-  qed
-  also have "\<dots> \<longleftrightarrow> x = z \<and> y = w"
-    by (simp add: nat_of_nibble_eq_iff)
-  finally show "Char x y = Char z w \<longleftrightarrow> x = z \<and> y = w" .
-qed
+  have "numeral k mod 256 = (numeral k :: integer)"
+    by (rule semiring_numeral_div_class.mod_less) (insert assms, simp_all)
+  then show ?thesis using integer_of_char_Char [of k]
+    by (simp only:)
+qed
+
+setup \<open>
+let
+  val chars = map_range (Thm.cterm_of @{context} o HOLogic.mk_numeral o curry (op +) 1) 255;
+  val simpset =
+    put_simpset HOL_ss @{context}
+      addsimps @{thms numeral_less_iff less_num_simps};
+  fun mk_code_eqn ct =
+    Thm.instantiate' [] [SOME ct] @{thm less_256_integer_of_char_Char}
+    |> full_simplify simpset;
+  val code_eqns = map mk_code_eqn chars;
+in
+  Global_Theory.note_thmss ""
+    [((@{binding integer_of_char_simps}, []), [(code_eqns, [])])]
+  #> snd
+end
+\<close>
+
+declare integer_of_char_simps [code]
+
+lemma nat_of_char_code [code]:
+  "nat_of_char = nat_of_integer \<circ> integer_of_char"
+  by (simp add: integer_of_char_def fun_eq_iff)
+
+lemma char_of_nat_code [code]:
+  "char_of_nat = char_of_integer \<circ> integer_of_nat"
+  by (simp add: char_of_integer_def fun_eq_iff)
+
+instantiation char :: equal
+begin
+
+definition equal_char
+  where "equal_char (c :: char) d \<longleftrightarrow> c = d"
+
+instance
+  by standard (simp add: equal_char_def)
+
+end
+
+lemma equal_char_simps [code]:
+  "HOL.equal (0::char) 0 \<longleftrightarrow> True"
+  "HOL.equal (Char k) (Char l) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) (numeral l mod 256)"
+  "HOL.equal 0 (Char k) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
+  "HOL.equal (Char k) 0 \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
+  by (simp_all only: equal refl Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff)
 
 syntax
-  "_Char" :: "str_position => char"    ("CHR _")
+  "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
+
+syntax
+  "_Char_ord" :: "num_const \<Rightarrow> char"     ("CHAR _")
 
 type_synonym string = "char list"
 
 syntax
   "_String" :: "str_position => string"    ("_")
 
 ML_file "Tools/string_syntax.ML"
 
-lemma UNIV_char:
-  "UNIV = image (case_prod Char) (UNIV \<times> UNIV)"
-proof (rule UNIV_eq_I)
-  fix x show "x \<in> image (case_prod Char) (UNIV \<times> UNIV)" by (cases x) auto
-qed
-
 instantiation char :: enum
 begin
 
 definition
-  "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
-  Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
-  Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
-  Char Nibble0 Nibble9, CHR ''\<newline>'', Char Nibble0 NibbleB,
-  Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
-  Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
-  Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
-  Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
-  Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
-  Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
-  Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
-  Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
-  Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
-  CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
-  CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
-  CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
-  CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
-  CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
-  CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
-  CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
-  CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
-  CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
-  CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
-  CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
-  CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
-  Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
-  Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
-  Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
-  Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
-  Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
-  Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
-  Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
-  Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
-  Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
-  Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
-  Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
-  Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
-  Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
-  Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
-  Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
-  Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
-  Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
-  Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
-  Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
-  Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
-  Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
-  Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
-  Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
-  Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
-  Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
-  Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
-  Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
-  Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
-  Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
-  Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
-  Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
-  Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
-  Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
-  Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
-  Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
-  Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
-  Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
-  Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
-  Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
-  Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
-  Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
-  Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
-  Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
+  "Enum.enum = [0, CHAR 0x01, CHAR 0x02, CHAR 0x03,
+    CHAR 0x04, CHAR 0x05, CHAR 0x06, CHAR 0x07,
+    CHAR 0x08, CHAR 0x09, CHR ''\<newline>'', CHAR 0x0B,
+    CHAR 0x0C, CHAR 0x0D, CHAR 0x0E, CHAR 0x0F,
+    CHAR 0x10, CHAR 0x11, CHAR 0x12, CHAR 0x13,
+    CHAR 0x14, CHAR 0x15, CHAR 0x16, CHAR 0x17,
+    CHAR 0x18, CHAR 0x19, CHAR 0x1A, CHAR 0x1B,
+    CHAR 0x1C, CHAR 0x1D, CHAR 0x1E, CHAR 0x1F,
+    CHR '' '', CHR ''!'', CHAR 0x22, CHR ''#'',
+    CHR ''$'', CHR ''%'', CHR ''&'', CHAR 0x27,
+    CHR ''('', CHR '')'', CHR ''*'', CHR ''+'',
+    CHR '','', CHR ''-'', CHR ''.'', CHR ''/'',
+    CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
+    CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'',
+    CHR ''8'', CHR ''9'', CHR '':'', CHR '';'',
+    CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'',
+    CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'',
+    CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'',
+    CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'',
+    CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
+    CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'',
+    CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'',
+    CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['',
+    CHAR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
+    CHAR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
+    CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'',
+    CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'',
+    CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'',
+    CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'',
+    CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
+    CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'',
+    CHR ''|'', CHR ''}'', CHR ''~'', CHAR 0x7F,
+    CHAR 0x80, CHAR 0x81, CHAR 0x82, CHAR 0x83,
+    CHAR 0x84, CHAR 0x85, CHAR 0x86, CHAR 0x87,
+    CHAR 0x88, CHAR 0x89, CHAR 0x8A, CHAR 0x8B,
+    CHAR 0x8C, CHAR 0x8D, CHAR 0x8E, CHAR 0x8F,
+    CHAR 0x90, CHAR 0x91, CHAR 0x92, CHAR 0x93,
+    CHAR 0x94, CHAR 0x95, CHAR 0x96, CHAR 0x97,
+    CHAR 0x98, CHAR 0x99, CHAR 0x9A, CHAR 0x9B,
+    CHAR 0x9C, CHAR 0x9D, CHAR 0x9E, CHAR 0x9F,
+    CHAR 0xA0, CHAR 0xA1, CHAR 0xA2, CHAR 0xA3,
+    CHAR 0xA4, CHAR 0xA5, CHAR 0xA6, CHAR 0xA7,
+    CHAR 0xA8, CHAR 0xA9, CHAR 0xAA, CHAR 0xAB,
+    CHAR 0xAC, CHAR 0xAD, CHAR 0xAE, CHAR 0xAF,
+    CHAR 0xB0, CHAR 0xB1, CHAR 0xB2, CHAR 0xB3,
+    CHAR 0xB4, CHAR 0xB5, CHAR 0xB6, CHAR 0xB7,
+    CHAR 0xB8, CHAR 0xB9, CHAR 0xBA, CHAR 0xBB,
+    CHAR 0xBC, CHAR 0xBD, CHAR 0xBE, CHAR 0xBF,
+    CHAR 0xC0, CHAR 0xC1, CHAR 0xC2, CHAR 0xC3,
+    CHAR 0xC4, CHAR 0xC5, CHAR 0xC6, CHAR 0xC7,
+    CHAR 0xC8, CHAR 0xC9, CHAR 0xCA, CHAR 0xCB,
+    CHAR 0xCC, CHAR 0xCD, CHAR 0xCE, CHAR 0xCF,
+    CHAR 0xD0, CHAR 0xD1, CHAR 0xD2, CHAR 0xD3,
+    CHAR 0xD4, CHAR 0xD5, CHAR 0xD6, CHAR 0xD7,
+    CHAR 0xD8, CHAR 0xD9, CHAR 0xDA, CHAR 0xDB,
+    CHAR 0xDC, CHAR 0xDD, CHAR 0xDE, CHAR 0xDF,
+    CHAR 0xE0, CHAR 0xE1, CHAR 0xE2, CHAR 0xE3,
+    CHAR 0xE4, CHAR 0xE5, CHAR 0xE6, CHAR 0xE7,
+    CHAR 0xE8, CHAR 0xE9, CHAR 0xEA, CHAR 0xEB,
+    CHAR 0xEC, CHAR 0xED, CHAR 0xEE, CHAR 0xEF,
+    CHAR 0xF0, CHAR 0xF1, CHAR 0xF2, CHAR 0xF3,
+    CHAR 0xF4, CHAR 0xF5, CHAR 0xF6, CHAR 0xF7,
+    CHAR 0xF8, CHAR 0xF9, CHAR 0xFA, CHAR 0xFB,
+    CHAR 0xFC, CHAR 0xFD, CHAR 0xFE, CHAR 0xFF]"
 
 definition
   "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
 
 definition
   "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
-
-lemma enum_char_product_enum_nibble:
-  "(Enum.enum :: char list) = map (case_prod Char) (List.product Enum.enum Enum.enum)"
-  by (simp add: enum_char_def enum_nibble_def)
-
-instance proof
-  show UNIV: "UNIV = set (Enum.enum :: char list)"
-    by (simp add: enum_char_product_enum_nibble UNIV_char enum_UNIV)
-  show "distinct (Enum.enum :: char list)"
-    by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
-  show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
-    by (simp add: UNIV enum_all_char_def list_all_iff)
-  show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
-    by (simp add: UNIV enum_ex_char_def list_ex_iff)
-qed
-
-end
-
-lemma card_UNIV_char:
-  "card (UNIV :: char set) = 256"
-  by (simp add: card_UNIV_length_enum enum_char_def)
 
 lemma enum_char_unfold:
   "Enum.enum = map char_of_nat [0..<256]"
 proof -
   have *: "Suc (Suc 0) = 2" by simp
   have "map nat_of_char Enum.enum = [0..<256]"
-    by (simp add: enum_char_def nat_of_char_Char upt_conv_Cons_Cons *)
+    by (simp add: enum_char_def upt_conv_Cons_Cons *)
   then have "map char_of_nat (map nat_of_char Enum.enum) =
     map char_of_nat [0..<256]" by simp
   then show ?thesis by (simp add: comp_def)
 qed
 
-setup \<open>
-let
-  val nibbles = map_range (Thm.cterm_of @{context} o HOLogic.mk_nibble) 16;
-  val simpset =
-    put_simpset HOL_ss @{context}
-      addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
-  fun mk_code_eqn x y =
-    Thm.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
-    |> simplify simpset;
-  val code_eqns = map_product mk_code_eqn nibbles nibbles;
-in
-  Global_Theory.note_thmss ""
-    [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
-  #> snd
-end
-\<close>
-
-declare nat_of_char_simps [code]
-
-lemma nibble_of_nat_of_char_div_16:
-  "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
-  by (cases c)
-    (simp add: nat_of_char_Char add.commute nat_of_nibble_less_16)
-
-lemma nibble_of_nat_nat_of_char:
-  "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
-proof (cases c)
-  case (Char x y)
-  then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
-    by (simp add: nibble_of_nat_mod_16)
-  then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
-    by (simp only: nibble_of_nat_mod_16)
-  with Char show ?thesis by (simp add: nat_of_char_Char add.commute)
-qed
-
-code_datatype Char \<comment> \<open>drop case certificate for char\<close>
-
-lemma case_char_code [code]:
-  "char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
-  by (cases c)
-    (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
-
-lemma char_of_nat_enum [code]:
-  "char_of_nat n = Enum.enum ! (n mod 256)"
-  by (simp add: enum_char_unfold)
+instance proof
+  show UNIV: "UNIV = set (Enum.enum :: char list)"
+    by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan)
+  show "distinct (Enum.enum :: char list)"
+    by (auto simp add: enum_char_unfold distinct_map intro: inj_onI)
+  show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
+    by (simp add: UNIV enum_all_char_def list_all_iff)
+  show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
+    by (simp add: UNIV enum_ex_char_def list_ex_iff)
+qed
+
+end
+
+lemma char_of_integer_code [code]:
+  "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
+  by (simp add: char_of_integer_def enum_char_unfold)
 
 
 subsection \<open>Strings as dedicated type\<close>
 
 typedef literal = "UNIV :: string set"