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 datatype char = Char nibble nibble
53 -- "Note: canonical order of character encoding coincides with standard term ordering"
56 "_Char" :: "str_position => char" ("CHR _")
58 type_synonym string = "char list"
61 "_String" :: "str_position => string" ("_")
63 ML_file "Tools/string_syntax.ML"
64 setup String_Syntax.setup
67 "UNIV = image (split Char) (UNIV \<times> UNIV)"
68 proof (rule UNIV_eq_I)
69 fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
72 lemma size_char [code, simp]:
73 "size (c::char) = 0" by (cases c) simp
75 lemma char_size [code, simp]:
76 "char_size (c::char) = 0" by (cases c) simp
78 instantiation char :: enum
82 "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
83 Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
84 Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
85 Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
86 Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
87 Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
88 Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
89 Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
90 Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
91 Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
92 Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
93 Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
94 Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
95 CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
96 CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
97 CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
98 CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
99 CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
100 CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
101 CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
102 CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
103 CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
104 CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
105 CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
106 CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
107 Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
108 Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
109 Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
110 Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
111 Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
112 Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
113 Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
114 Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
115 Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
116 Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
117 Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
118 Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
119 Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
120 Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
121 Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
122 Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
123 Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
124 Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
125 Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
126 Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
127 Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
128 Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
129 Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
130 Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
131 Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
132 Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
133 Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
134 Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
135 Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
136 Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
137 Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
138 Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
139 Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
140 Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
141 Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
142 Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
143 Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
144 Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
145 Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
146 Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
147 Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
148 Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
149 Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
152 "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
155 "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
158 have enum: "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
159 by (simp add: enum_char_def enum_nibble_def)
160 show UNIV: "UNIV = set (Enum.enum :: char list)"
161 by (simp add: enum UNIV_char product_list_set enum_UNIV)
162 show "distinct (Enum.enum :: char list)"
163 by (auto intro: inj_onI simp add: enum distinct_map distinct_product enum_distinct)
164 show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
165 by (simp add: UNIV enum_all_char_def list_all_iff)
166 show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
167 by (simp add: UNIV enum_ex_char_def list_ex_iff)
172 lemma card_UNIV_char:
173 "card (UNIV :: char set) = 256"
174 by (simp add: card_UNIV_length_enum enum_char_def)
176 primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
177 "nibble_pair_of_char (Char n m) = (n, m)"
181 val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
182 val thms = map_product
183 (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
186 Global_Theory.note_thmss ""
187 [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
188 #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
192 lemma char_case_nibble_pair [code, code_unfold]:
193 "char_case f = split f o nibble_pair_of_char"
194 by (simp add: fun_eq_iff split: char.split)
196 lemma char_rec_nibble_pair [code, code_unfold]:
197 "char_rec f = split f o nibble_pair_of_char"
198 unfolding char_case_nibble_pair [symmetric]
199 by (simp add: fun_eq_iff split: char.split)
202 subsection {* Strings as dedicated type *}
204 typedef literal = "UNIV :: string set"
205 morphisms explode STR ..
207 instantiation literal :: size
210 definition size_literal :: "literal \<Rightarrow> nat"
212 [code]: "size_literal (s\<Colon>literal) = 0"
218 instantiation literal :: equal
221 definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
223 "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
227 qed (auto simp add: equal_literal_def explode_inject)
231 lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
232 by(simp add: STR_inject)
235 subsection {* Code generator *}
237 ML_file "Tools/string_code.ML"
239 code_reserved SML string
240 code_reserved OCaml string
241 code_reserved Scala string
250 fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
253 code_instance literal :: equal
256 code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
257 (SML "!((_ : string) = _)")
258 (OCaml "!((_ : string) = _)")
259 (Haskell infix 4 "==")
260 (Scala infixl 5 "==")
262 hide_type (open) literal