1 (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
3 header {* Character and string types *}
9 subsection {* Characters and strings *}
12 Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
13 | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
16 "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
17 Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
18 proof (rule UNIV_eq_I)
19 fix x show "x \<in> ?A" by (cases x) simp_all
22 lemma size_nibble [code, simp]:
23 "size (x::nibble) = 0" by (cases x) simp_all
25 lemma nibble_size [code, simp]:
26 "nibble_size (x::nibble) = 0" by (cases x) simp_all
28 instantiation nibble :: enum
32 "Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
33 Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
36 "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
37 \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
40 "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
41 \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
44 qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
48 lemma card_UNIV_nibble:
49 "card (UNIV :: nibble set) = 16"
50 by (simp add: card_UNIV_length_enum enum_nibble_def)
52 primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
54 "nat_of_nibble Nibble0 = 0"
55 | "nat_of_nibble Nibble1 = 1"
56 | "nat_of_nibble Nibble2 = 2"
57 | "nat_of_nibble Nibble3 = 3"
58 | "nat_of_nibble Nibble4 = 4"
59 | "nat_of_nibble Nibble5 = 5"
60 | "nat_of_nibble Nibble6 = 6"
61 | "nat_of_nibble Nibble7 = 7"
62 | "nat_of_nibble Nibble8 = 8"
63 | "nat_of_nibble Nibble9 = 9"
64 | "nat_of_nibble NibbleA = 10"
65 | "nat_of_nibble NibbleB = 11"
66 | "nat_of_nibble NibbleC = 12"
67 | "nat_of_nibble NibbleD = 13"
68 | "nat_of_nibble NibbleE = 14"
69 | "nat_of_nibble NibbleF = 15"
71 definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
72 "nibble_of_nat n = Enum.enum ! (n mod 16)"
74 lemma nibble_of_nat_simps [simp]:
75 "nibble_of_nat 0 = Nibble0"
76 "nibble_of_nat 1 = Nibble1"
77 "nibble_of_nat 2 = Nibble2"
78 "nibble_of_nat 3 = Nibble3"
79 "nibble_of_nat 4 = Nibble4"
80 "nibble_of_nat 5 = Nibble5"
81 "nibble_of_nat 6 = Nibble6"
82 "nibble_of_nat 7 = Nibble7"
83 "nibble_of_nat 8 = Nibble8"
84 "nibble_of_nat 9 = Nibble9"
85 "nibble_of_nat 10 = NibbleA"
86 "nibble_of_nat 11 = NibbleB"
87 "nibble_of_nat 12 = NibbleC"
88 "nibble_of_nat 13 = NibbleD"
89 "nibble_of_nat 14 = NibbleE"
90 "nibble_of_nat 15 = NibbleF"
91 unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
93 lemma nibble_of_nat_of_nibble [simp]:
94 "nibble_of_nat (nat_of_nibble x) = x"
95 by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
97 lemma nat_of_nibble_of_nat [simp]:
98 "nat_of_nibble (nibble_of_nat n) = n mod 16"
99 by (cases "nibble_of_nat n")
100 (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
102 lemma inj_nat_of_nibble:
104 by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
106 lemma nat_of_nibble_eq_iff:
107 "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
108 by (rule inj_eq) (rule inj_nat_of_nibble)
110 lemma nat_of_nibble_less_16:
111 "nat_of_nibble x < 16"
114 lemma nibble_of_nat_mod_16:
115 "nibble_of_nat (n mod 16) = nibble_of_nat n"
116 by (simp add: nibble_of_nat_def)
118 datatype char = Char nibble nibble
119 -- "Note: canonical order of character encoding coincides with standard term ordering"
122 "_Char" :: "str_position => char" ("CHR _")
124 type_synonym string = "char list"
127 "_String" :: "str_position => string" ("_")
129 ML_file "Tools/string_syntax.ML"
130 setup String_Syntax.setup
133 "UNIV = image (split Char) (UNIV \<times> UNIV)"
134 proof (rule UNIV_eq_I)
135 fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
138 lemma size_char [code, simp]:
139 "size (c::char) = 0" by (cases c) simp
141 lemma char_size [code, simp]:
142 "char_size (c::char) = 0" by (cases c) simp
144 instantiation char :: enum
148 "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
149 Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
150 Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
151 Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
152 Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
153 Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
154 Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
155 Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
156 Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
157 Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
158 Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
159 Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
160 Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
161 CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
162 CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
163 CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
164 CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
165 CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
166 CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
167 CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
168 CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
169 CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
170 CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
171 CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
172 CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
173 Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
174 Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
175 Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
176 Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
177 Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
178 Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
179 Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
180 Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
181 Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
182 Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
183 Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
184 Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
185 Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
186 Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
187 Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
188 Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
189 Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
190 Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
191 Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
192 Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
193 Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
194 Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
195 Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
196 Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
197 Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
198 Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
199 Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
200 Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
201 Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
202 Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
203 Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
204 Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
205 Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
206 Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
207 Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
208 Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
209 Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
210 Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
211 Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
212 Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
213 Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
214 Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
215 Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
218 "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
221 "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
223 lemma enum_char_product_enum_nibble:
224 "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
225 by (simp add: enum_char_def enum_nibble_def)
228 show UNIV: "UNIV = set (Enum.enum :: char list)"
229 by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV)
230 show "distinct (Enum.enum :: char list)"
231 by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
232 show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
233 by (simp add: UNIV enum_all_char_def list_all_iff)
234 show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
235 by (simp add: UNIV enum_ex_char_def list_ex_iff)
240 lemma card_UNIV_char:
241 "card (UNIV :: char set) = 256"
242 by (simp add: card_UNIV_length_enum enum_char_def)
244 definition nat_of_char :: "char \<Rightarrow> nat"
246 "nat_of_char c = (case c of Char x y \<Rightarrow> nat_of_nibble x * 16 + nat_of_nibble y)"
248 lemma nat_of_char_Char:
249 "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y"
250 by (simp add: nat_of_char_def)
254 val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
256 put_simpset HOL_ss @{context}
257 addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
258 fun mk_code_eqn x y =
259 Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
261 val code_eqns = map_product mk_code_eqn nibbles nibbles;
263 Global_Theory.note_thmss ""
264 [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
269 declare nat_of_char_simps [code]
271 lemma nibble_of_nat_of_char_div_16:
272 "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
274 (simp add: nat_of_char_def add_commute nat_of_nibble_less_16)
276 lemma nibble_of_nat_nat_of_char:
277 "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
280 then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
281 by (simp add: nibble_of_nat_mod_16)
282 then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
283 by (simp only: nibble_of_nat_mod_16)
284 with Char show ?thesis by (simp add: nat_of_char_def add_commute)
287 code_datatype Char -- {* drop case certificate for char *}
289 lemma char_case_code [code]:
290 "char_case f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
292 (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.cases)
295 "char_rec = char_case"
296 by (simp add: fun_eq_iff split: char.split)
298 definition char_of_nat :: "nat \<Rightarrow> char" where
299 "char_of_nat n = Enum.enum ! (n mod 256)"
301 lemma char_of_nat_Char_nibbles:
302 "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
304 from mod_mult2_eq [of n 16 16]
305 have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
307 by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble
308 card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add_commute)
311 lemma char_of_nat_of_char [simp]:
312 "char_of_nat (nat_of_char c) = c"
314 (simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char)
316 lemma nat_of_char_of_nat [simp]:
317 "nat_of_char (char_of_nat n) = n mod 256"
319 have "n mod 256 = n mod (16 * 16)" by simp
320 then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq)
322 by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
325 lemma inj_nat_of_char:
327 by (rule inj_on_inverseI) (rule char_of_nat_of_char)
329 lemma nat_of_char_eq_iff:
330 "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
331 by (rule inj_eq) (rule inj_nat_of_char)
333 lemma nat_of_char_less_256:
334 "nat_of_char c < 256"
337 with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
338 show ?thesis by (simp add: nat_of_char_def)
341 lemma char_of_nat_mod_256:
342 "char_of_nat (n mod 256) = char_of_nat n"
344 from nibble_of_nat_mod_16 [of "n mod 256"]
345 have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp
346 with nibble_of_nat_mod_16 [of n]
347 have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel)
348 have "n mod 256 = n mod (16 * 16)" by simp
349 then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq)
351 by (simp add: char_of_nat_Char_nibbles *)
352 (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **)
356 subsection {* Strings as dedicated type *}
358 typedef literal = "UNIV :: string set"
359 morphisms explode STR ..
361 instantiation literal :: size
364 definition size_literal :: "literal \<Rightarrow> nat"
366 [code]: "size_literal (s\<Colon>literal) = 0"
372 instantiation literal :: equal
375 definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
377 "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
381 qed (auto simp add: equal_literal_def explode_inject)
386 fixes s :: "String.literal"
387 shows "HOL.equal s s \<longleftrightarrow> True"
390 lemma STR_inject' [simp]:
391 "STR xs = STR ys \<longleftrightarrow> xs = ys"
392 by (simp add: STR_inject)
395 subsection {* Code generator *}
397 ML_file "Tools/string_code.ML"
399 code_reserved SML string
400 code_reserved OCaml string
401 code_reserved Scala string
404 type_constructor literal \<rightharpoonup>
407 and (Haskell) "String"
411 fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
415 class_instance literal :: equal \<rightharpoonup>
417 | constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
418 (SML) "!((_ : string) = _)"
419 and (OCaml) "!((_ : string) = _)"
420 and (Haskell) infix 4 "=="
421 and (Scala) infixl 5 "=="
423 setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *}
425 definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
426 where [simp, code del]: "abort _ f = f ()"
428 setup {* Sign.map_naming Name_Space.parent_path *}
430 code_printing constant Code.abort \<rightharpoonup>
431 (SML) "!(raise/ Fail/ _)"
432 and (OCaml) "failwith"
433 and (Haskell) "error"
434 and (Scala) "!{/ sys.error((_));/ ((_)).apply(())/ }"
436 hide_type (open) literal