src/HOL/String.thy
author haftmann
Wed Apr 25 09:04:25 2018 +0000 (13 months ago)
changeset 68033 ad4b8b6892c3
parent 68028 1f9f973eed2a
child 68224 1f7308050349
permissions -rw-r--r--
uniform tagging for printable and non-printable literals
haftmann@31051
     1
(* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
haftmann@31051
     2
wenzelm@60758
     3
section \<open>Character and string types\<close>
haftmann@31051
     4
haftmann@31051
     5
theory String
blanchet@55969
     6
imports Enum
haftmann@31051
     7
begin
haftmann@31051
     8
haftmann@68028
     9
subsection \<open>Strings as list of bytes\<close>
haftmann@68028
    10
haftmann@68028
    11
text \<open>
haftmann@68028
    12
  When modelling strings, we follow the approach given
haftmann@68028
    13
  in @{url "http://utf8everywhere.org/"}:
haftmann@68028
    14
haftmann@68028
    15
  \<^item> Strings are a list of bytes (8 bit).
haftmann@68028
    16
haftmann@68028
    17
  \<^item> Byte values from 0 to 127 are US-ASCII.
haftmann@31051
    18
haftmann@68028
    19
  \<^item> Byte values from 128 to 255 are uninterpreted blobs.
haftmann@68028
    20
\<close>
haftmann@68028
    21
haftmann@68028
    22
subsubsection \<open>Bytes as datatype\<close>
haftmann@68028
    23
haftmann@68028
    24
datatype char =
haftmann@68028
    25
  Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool)
haftmann@68028
    26
       (digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool)
haftmann@68028
    27
haftmann@68028
    28
context comm_semiring_1
haftmann@68028
    29
begin
haftmann@62364
    30
haftmann@68028
    31
definition of_char :: "char \<Rightarrow> 'a"
haftmann@68028
    32
  where "of_char c = ((((((of_bool (digit7 c) * 2
haftmann@68028
    33
    + of_bool (digit6 c)) * 2
haftmann@68028
    34
    + of_bool (digit5 c)) * 2
haftmann@68028
    35
    + of_bool (digit4 c)) * 2
haftmann@68028
    36
    + of_bool (digit3 c)) * 2
haftmann@68028
    37
    + of_bool (digit2 c)) * 2
haftmann@68028
    38
    + of_bool (digit1 c)) * 2
haftmann@68028
    39
    + of_bool (digit0 c)"
haftmann@68028
    40
haftmann@68028
    41
lemma of_char_Char [simp]:
haftmann@68028
    42
  "of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
haftmann@68028
    43
    foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0"
haftmann@68028
    44
  by (simp add: of_char_def ac_simps)
haftmann@68028
    45
haftmann@68028
    46
end
haftmann@68028
    47
haftmann@68028
    48
context semiring_parity
haftmann@68028
    49
begin
haftmann@68028
    50
haftmann@68028
    51
definition char_of :: "'a \<Rightarrow> char"
haftmann@68028
    52
  where "char_of n = Char (odd n) (odd (drop_bit 1 n))
haftmann@68028
    53
    (odd (drop_bit 2 n)) (odd (drop_bit 3 n))
haftmann@68028
    54
    (odd (drop_bit 4 n)) (odd (drop_bit 5 n))
haftmann@68028
    55
    (odd (drop_bit 6 n)) (odd (drop_bit 7 n))"
haftmann@68028
    56
haftmann@68028
    57
lemma char_of_char [simp]:
haftmann@68028
    58
  "char_of (of_char c) = c"
haftmann@68028
    59
proof (cases c)
haftmann@68028
    60
  have **: "drop_bit n (q * 2 + of_bool d) = drop_bit (n - 1) q + drop_bit n (of_bool d)"
haftmann@68028
    61
    if "n > 0" for q :: 'a and n :: nat and d :: bool
haftmann@68028
    62
    using that by (cases n) simp_all
haftmann@68028
    63
  case (Char d0 d1 d2 d3 d4 d5 d6 d7)
haftmann@68028
    64
  then show ?thesis
haftmann@68028
    65
    by (simp only: of_char_def char_of_def char.simps char.sel drop_bit_of_bool **) simp
haftmann@62364
    66
qed
haftmann@62364
    67
haftmann@68028
    68
lemma char_of_comp_of_char [simp]:
haftmann@68028
    69
  "char_of \<circ> of_char = id"
haftmann@68028
    70
  by (simp add: fun_eq_iff)
haftmann@62364
    71
haftmann@68028
    72
lemma inj_of_char:
haftmann@68028
    73
  "inj of_char"
haftmann@62364
    74
proof (rule injI)
haftmann@62364
    75
  fix c d
haftmann@68028
    76
  assume "of_char c = of_char d"
haftmann@68028
    77
  then have "char_of (of_char c) = char_of (of_char d)"
haftmann@62364
    78
    by simp
haftmann@62364
    79
  then show "c = d"
haftmann@62364
    80
    by simp
haftmann@62364
    81
qed
haftmann@62364
    82
  
haftmann@68028
    83
lemma of_char_eq_iff [simp]:
haftmann@68028
    84
  "of_char c = of_char d \<longleftrightarrow> c = d"
haftmann@68028
    85
  by (simp add: inj_eq inj_of_char)
haftmann@62364
    86
haftmann@68028
    87
lemma of_char_of [simp]:
haftmann@68028
    88
  "of_char (char_of a) = a mod 256"
haftmann@68028
    89
proof -
haftmann@68028
    90
  have *: "{0::nat..<8} = {0, 1, 2, 3, 4, 5, 6, 7}"
haftmann@68028
    91
    by auto
haftmann@68028
    92
  have "of_char (char_of (take_bit 8 a)) =
haftmann@68028
    93
    (\<Sum>k\<in>{0, 1, 2, 3, 4, 5, 6, 7}. push_bit k (of_bool (odd (drop_bit k a))))"
haftmann@68028
    94
    by (simp add: of_char_def char_of_def push_bit_of_1 drop_bit_take_bit)
haftmann@68028
    95
  also have "\<dots> = take_bit 8 a"
haftmann@68028
    96
    using * take_bit_sum [of 8 a] by simp
haftmann@68028
    97
  also have "char_of(take_bit 8 a) = char_of a"
haftmann@68028
    98
    by (simp add: char_of_def drop_bit_take_bit)
haftmann@68028
    99
  finally show ?thesis
haftmann@68028
   100
    by (simp add: take_bit_eq_mod)
haftmann@68028
   101
qed
haftmann@62364
   102
haftmann@68028
   103
lemma char_of_mod_256 [simp]:
haftmann@68028
   104
  "char_of (n mod 256) = char_of n"
haftmann@68028
   105
  by (metis char_of_char of_char_of)
haftmann@68028
   106
haftmann@68028
   107
lemma of_char_mod_256 [simp]:
haftmann@68028
   108
  "of_char c mod 256 = of_char c"
haftmann@68028
   109
  by (metis char_of_char of_char_of)
haftmann@62364
   110
haftmann@68028
   111
lemma char_of_quasi_inj [simp]:
haftmann@68028
   112
  "char_of m = char_of n \<longleftrightarrow> m mod 256 = n mod 256"
haftmann@68028
   113
  by (metis char_of_mod_256 of_char_of)
haftmann@68028
   114
haftmann@68028
   115
lemma char_of_nat_eq_iff:
haftmann@68028
   116
  "char_of n = c \<longleftrightarrow> take_bit 8 n = of_char c"
haftmann@68028
   117
  by (simp add: take_bit_eq_mod) (use of_char_eq_iff in fastforce)
haftmann@68028
   118
haftmann@68028
   119
lemma char_of_nat [simp]:
haftmann@68028
   120
  "char_of (of_nat n) = char_of n"
haftmann@68028
   121
  by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
haftmann@68033
   122
haftmann@68028
   123
end
haftmann@62364
   124
haftmann@62364
   125
lemma inj_on_char_of_nat [simp]:
haftmann@68028
   126
  "inj_on char_of {0::nat..<256}"
haftmann@62364
   127
  by (rule inj_onI) simp
haftmann@62364
   128
haftmann@62364
   129
lemma nat_of_char_less_256 [simp]:
haftmann@68028
   130
  "of_char c < (256 :: nat)"
haftmann@62364
   131
proof -
haftmann@68028
   132
  have "of_char c mod (256 :: nat) < 256"
haftmann@62364
   133
    by arith
haftmann@62364
   134
  then show ?thesis by simp
haftmann@62364
   135
qed
haftmann@62364
   136
haftmann@68028
   137
lemma range_nat_of_char:
haftmann@68028
   138
  "range of_char = {0::nat..<256}"
haftmann@68028
   139
proof (rule; rule)
haftmann@68028
   140
  fix n :: nat
haftmann@68028
   141
  assume "n \<in> range of_char"
haftmann@68028
   142
  then show "n \<in> {0..<256}"
haftmann@68028
   143
    by auto
haftmann@68028
   144
next
haftmann@68028
   145
  fix n :: nat
haftmann@68028
   146
  assume "n \<in> {0..<256}"
haftmann@68028
   147
  then have "n = of_char (char_of n)"
haftmann@68028
   148
    by simp
haftmann@68028
   149
  then show "n \<in> range of_char"
haftmann@68028
   150
    by (rule range_eqI)
haftmann@68028
   151
qed
haftmann@68028
   152
haftmann@62364
   153
lemma UNIV_char_of_nat:
haftmann@68028
   154
  "UNIV = char_of ` {0::nat..<256}"
haftmann@62364
   155
proof -
haftmann@68028
   156
  have "range (of_char :: char \<Rightarrow> nat) = of_char ` char_of ` {0::nat..<256}"
haftmann@68028
   157
    by (auto simp add: range_nat_of_char intro!: image_eqI)
haftmann@68028
   158
  with inj_of_char [where ?'a = nat] show ?thesis 
haftmann@68028
   159
    by (simp add: inj_image_eq_iff)
haftmann@62364
   160
qed
haftmann@62364
   161
haftmann@62597
   162
lemma card_UNIV_char:
haftmann@62597
   163
  "card (UNIV :: char set) = 256"
haftmann@62597
   164
  by (auto simp add: UNIV_char_of_nat card_image)
haftmann@31051
   165
haftmann@68028
   166
context
haftmann@68028
   167
  includes lifting_syntax integer.lifting natural.lifting
haftmann@49972
   168
begin
haftmann@49972
   169
haftmann@68028
   170
lemma [transfer_rule]:
haftmann@68028
   171
  "(pcr_integer ===> (=)) (char_of :: int \<Rightarrow> char) (char_of :: integer \<Rightarrow> char)"
haftmann@68028
   172
  by (unfold char_of_def [abs_def]) transfer_prover
haftmann@68028
   173
haftmann@68028
   174
lemma [transfer_rule]:
haftmann@68028
   175
  "((=) ===> pcr_integer) (of_char :: char \<Rightarrow> int) (of_char :: char \<Rightarrow> integer)"
haftmann@68028
   176
  by (unfold of_char_def [abs_def]) transfer_prover
haftmann@49972
   177
haftmann@68028
   178
lemma [transfer_rule]:
haftmann@68028
   179
  "(pcr_natural ===> (=)) (char_of :: nat \<Rightarrow> char) (char_of :: natural \<Rightarrow> char)"
haftmann@68028
   180
  by (unfold char_of_def [abs_def]) transfer_prover
haftmann@68028
   181
haftmann@68028
   182
lemma [transfer_rule]:
haftmann@68028
   183
  "((=) ===> pcr_natural) (of_char :: char \<Rightarrow> nat) (of_char :: char \<Rightarrow> natural)"
haftmann@68028
   184
  by (unfold of_char_def [abs_def]) transfer_prover
haftmann@49972
   185
haftmann@49972
   186
end
haftmann@49972
   187
haftmann@68028
   188
lifting_update integer.lifting
haftmann@68028
   189
lifting_forget integer.lifting
haftmann@64630
   190
haftmann@68028
   191
lifting_update natural.lifting
haftmann@68028
   192
lifting_forget natural.lifting
haftmann@62364
   193
haftmann@31051
   194
syntax
haftmann@62597
   195
  "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
haftmann@62678
   196
  "_Char_ord" :: "num_const \<Rightarrow> char"   ("CHR _")
haftmann@31051
   197
bulwahn@42163
   198
type_synonym string = "char list"
haftmann@31051
   199
haftmann@31051
   200
syntax
haftmann@68028
   201
  "_String" :: "str_position \<Rightarrow> string"    ("_")
haftmann@31051
   202
wenzelm@48891
   203
ML_file "Tools/string_syntax.ML"
haftmann@31051
   204
haftmann@49972
   205
instantiation char :: enum
haftmann@49972
   206
begin
haftmann@49972
   207
haftmann@49972
   208
definition
haftmann@68028
   209
  "Enum.enum = [
haftmann@68028
   210
    CHR 0x00, CHR 0x01, CHR 0x02, CHR 0x03,
haftmann@62678
   211
    CHR 0x04, CHR 0x05, CHR 0x06, CHR 0x07,
haftmann@62678
   212
    CHR 0x08, CHR 0x09, CHR ''\<newline>'', CHR 0x0B,
haftmann@62678
   213
    CHR 0x0C, CHR 0x0D, CHR 0x0E, CHR 0x0F,
haftmann@62678
   214
    CHR 0x10, CHR 0x11, CHR 0x12, CHR 0x13,
haftmann@62678
   215
    CHR 0x14, CHR 0x15, CHR 0x16, CHR 0x17,
haftmann@62678
   216
    CHR 0x18, CHR 0x19, CHR 0x1A, CHR 0x1B,
haftmann@62678
   217
    CHR 0x1C, CHR 0x1D, CHR 0x1E, CHR 0x1F,
haftmann@62678
   218
    CHR '' '', CHR ''!'', CHR 0x22, CHR ''#'',
haftmann@62678
   219
    CHR ''$'', CHR ''%'', CHR ''&'', CHR 0x27,
haftmann@62597
   220
    CHR ''('', CHR '')'', CHR ''*'', CHR ''+'',
haftmann@62597
   221
    CHR '','', CHR ''-'', CHR ''.'', CHR ''/'',
haftmann@62597
   222
    CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
haftmann@62597
   223
    CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'',
haftmann@62597
   224
    CHR ''8'', CHR ''9'', CHR '':'', CHR '';'',
haftmann@62597
   225
    CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'',
haftmann@62597
   226
    CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'',
haftmann@62597
   227
    CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'',
haftmann@62597
   228
    CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'',
haftmann@62597
   229
    CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
haftmann@62597
   230
    CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'',
haftmann@62597
   231
    CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'',
haftmann@62597
   232
    CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['',
haftmann@62678
   233
    CHR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
haftmann@62678
   234
    CHR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
haftmann@62597
   235
    CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'',
haftmann@62597
   236
    CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'',
haftmann@62597
   237
    CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'',
haftmann@62597
   238
    CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'',
haftmann@62597
   239
    CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
haftmann@62597
   240
    CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'',
haftmann@62678
   241
    CHR ''|'', CHR ''}'', CHR ''~'', CHR 0x7F,
haftmann@62678
   242
    CHR 0x80, CHR 0x81, CHR 0x82, CHR 0x83,
haftmann@62678
   243
    CHR 0x84, CHR 0x85, CHR 0x86, CHR 0x87,
haftmann@62678
   244
    CHR 0x88, CHR 0x89, CHR 0x8A, CHR 0x8B,
haftmann@62678
   245
    CHR 0x8C, CHR 0x8D, CHR 0x8E, CHR 0x8F,
haftmann@62678
   246
    CHR 0x90, CHR 0x91, CHR 0x92, CHR 0x93,
haftmann@62678
   247
    CHR 0x94, CHR 0x95, CHR 0x96, CHR 0x97,
haftmann@62678
   248
    CHR 0x98, CHR 0x99, CHR 0x9A, CHR 0x9B,
haftmann@62678
   249
    CHR 0x9C, CHR 0x9D, CHR 0x9E, CHR 0x9F,
haftmann@62678
   250
    CHR 0xA0, CHR 0xA1, CHR 0xA2, CHR 0xA3,
haftmann@62678
   251
    CHR 0xA4, CHR 0xA5, CHR 0xA6, CHR 0xA7,
haftmann@62678
   252
    CHR 0xA8, CHR 0xA9, CHR 0xAA, CHR 0xAB,
haftmann@62678
   253
    CHR 0xAC, CHR 0xAD, CHR 0xAE, CHR 0xAF,
haftmann@62678
   254
    CHR 0xB0, CHR 0xB1, CHR 0xB2, CHR 0xB3,
haftmann@62678
   255
    CHR 0xB4, CHR 0xB5, CHR 0xB6, CHR 0xB7,
haftmann@62678
   256
    CHR 0xB8, CHR 0xB9, CHR 0xBA, CHR 0xBB,
haftmann@62678
   257
    CHR 0xBC, CHR 0xBD, CHR 0xBE, CHR 0xBF,
haftmann@62678
   258
    CHR 0xC0, CHR 0xC1, CHR 0xC2, CHR 0xC3,
haftmann@62678
   259
    CHR 0xC4, CHR 0xC5, CHR 0xC6, CHR 0xC7,
haftmann@62678
   260
    CHR 0xC8, CHR 0xC9, CHR 0xCA, CHR 0xCB,
haftmann@62678
   261
    CHR 0xCC, CHR 0xCD, CHR 0xCE, CHR 0xCF,
haftmann@62678
   262
    CHR 0xD0, CHR 0xD1, CHR 0xD2, CHR 0xD3,
haftmann@62678
   263
    CHR 0xD4, CHR 0xD5, CHR 0xD6, CHR 0xD7,
haftmann@62678
   264
    CHR 0xD8, CHR 0xD9, CHR 0xDA, CHR 0xDB,
haftmann@62678
   265
    CHR 0xDC, CHR 0xDD, CHR 0xDE, CHR 0xDF,
haftmann@62678
   266
    CHR 0xE0, CHR 0xE1, CHR 0xE2, CHR 0xE3,
haftmann@62678
   267
    CHR 0xE4, CHR 0xE5, CHR 0xE6, CHR 0xE7,
haftmann@62678
   268
    CHR 0xE8, CHR 0xE9, CHR 0xEA, CHR 0xEB,
haftmann@62678
   269
    CHR 0xEC, CHR 0xED, CHR 0xEE, CHR 0xEF,
haftmann@62678
   270
    CHR 0xF0, CHR 0xF1, CHR 0xF2, CHR 0xF3,
haftmann@62678
   271
    CHR 0xF4, CHR 0xF5, CHR 0xF6, CHR 0xF7,
haftmann@62678
   272
    CHR 0xF8, CHR 0xF9, CHR 0xFA, CHR 0xFB,
haftmann@62678
   273
    CHR 0xFC, CHR 0xFD, CHR 0xFE, CHR 0xFF]"
haftmann@31484
   274
haftmann@49972
   275
definition
haftmann@49972
   276
  "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
haftmann@49972
   277
haftmann@49972
   278
definition
haftmann@49972
   279
  "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
haftmann@49972
   280
haftmann@62597
   281
lemma enum_char_unfold:
haftmann@68028
   282
  "Enum.enum = map char_of [0..<256]"
haftmann@62597
   283
proof -
haftmann@68028
   284
  have "map (of_char :: char \<Rightarrow> nat) Enum.enum = [0..<256]"
haftmann@68028
   285
    by (simp add: enum_char_def of_char_def upt_conv_Cons_Cons numeral_2_eq_2 [symmetric])
haftmann@68028
   286
  then have "map char_of (map (of_char :: char \<Rightarrow> nat) Enum.enum) =
haftmann@68028
   287
    map char_of [0..<256]"
haftmann@68028
   288
    by simp
haftmann@68028
   289
  then show ?thesis
haftmann@68028
   290
    by simp
haftmann@62597
   291
qed
haftmann@51160
   292
haftmann@49972
   293
instance proof
haftmann@49972
   294
  show UNIV: "UNIV = set (Enum.enum :: char list)"
haftmann@62597
   295
    by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan)
haftmann@49972
   296
  show "distinct (Enum.enum :: char list)"
haftmann@62597
   297
    by (auto simp add: enum_char_unfold distinct_map intro: inj_onI)
haftmann@49972
   298
  show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
haftmann@49972
   299
    by (simp add: UNIV enum_all_char_def list_all_iff)
haftmann@49972
   300
  show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
haftmann@49972
   301
    by (simp add: UNIV enum_ex_char_def list_ex_iff)
haftmann@49972
   302
qed
haftmann@49972
   303
haftmann@49972
   304
end
haftmann@49972
   305
haftmann@68028
   306
lemma linorder_char:
haftmann@68028
   307
  "class.linorder (\<lambda>c d. of_char c \<le> (of_char d :: nat)) (\<lambda>c d. of_char c < (of_char d :: nat))"
haftmann@68028
   308
  by standard auto
haftmann@68028
   309
haftmann@68028
   310
text \<open>Optimized version for execution\<close>
haftmann@68028
   311
haftmann@68028
   312
definition char_of_integer :: "integer \<Rightarrow> char"
haftmann@68028
   313
  where [code_abbrev]: "char_of_integer = char_of"
haftmann@68028
   314
haftmann@68028
   315
definition integer_of_char :: "char \<Rightarrow> integer"
haftmann@68028
   316
  where [code_abbrev]: "integer_of_char = of_char"
haftmann@68028
   317
haftmann@62597
   318
lemma char_of_integer_code [code]:
haftmann@68028
   319
  "char_of_integer k = (let
haftmann@68028
   320
     (q0, b0) = bit_cut_integer k;
haftmann@68028
   321
     (q1, b1) = bit_cut_integer q0;
haftmann@68028
   322
     (q2, b2) = bit_cut_integer q1;
haftmann@68028
   323
     (q3, b3) = bit_cut_integer q2;
haftmann@68028
   324
     (q4, b4) = bit_cut_integer q3;
haftmann@68028
   325
     (q5, b5) = bit_cut_integer q4;
haftmann@68028
   326
     (q6, b6) = bit_cut_integer q5;
haftmann@68028
   327
     (_, b7) = bit_cut_integer q6
haftmann@68028
   328
    in Char b0 b1 b2 b3 b4 b5 b6 b7)"
haftmann@68028
   329
  by (simp add: bit_cut_integer_def char_of_integer_def char_of_def div_mult2_numeral_eq odd_iff_mod_2_eq_one drop_bit_eq_div)
haftmann@49948
   330
haftmann@68028
   331
lemma integer_of_char_code [code]:
haftmann@68028
   332
  "integer_of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
haftmann@68028
   333
    ((((((of_bool b7 * 2 + of_bool b6) * 2 +
haftmann@68028
   334
      of_bool b5) * 2 + of_bool b4) * 2 +
haftmann@68028
   335
        of_bool b3) * 2 + of_bool b2) * 2 +
haftmann@68028
   336
          of_bool b1) * 2 + of_bool b0"
haftmann@68028
   337
  by (simp only: integer_of_char_def of_char_def char.sel)
haftmann@66331
   338
haftmann@31051
   339
haftmann@68028
   340
subsection \<open>Strings as dedicated type for target language code generation\<close>
haftmann@68028
   341
haftmann@68028
   342
subsubsection \<open>Logical specification\<close>
haftmann@68028
   343
haftmann@68028
   344
context
haftmann@68028
   345
begin
haftmann@68028
   346
haftmann@68028
   347
qualified definition ascii_of :: "char \<Rightarrow> char"
haftmann@68028
   348
  where "ascii_of c = Char (digit0 c) (digit1 c) (digit2 c) (digit3 c) (digit4 c) (digit5 c) (digit6 c) False"
bulwahn@39250
   349
haftmann@68028
   350
qualified lemma ascii_of_Char [simp]:
haftmann@68028
   351
  "ascii_of (Char b0 b1 b2 b3 b4 b5 b6 b7) = Char b0 b1 b2 b3 b4 b5 b6 False"
haftmann@68028
   352
  by (simp add: ascii_of_def)
haftmann@68028
   353
haftmann@68028
   354
qualified lemma not_digit7_ascii_of [simp]:
haftmann@68028
   355
  "\<not> digit7 (ascii_of c)"
haftmann@68028
   356
  by (simp add: ascii_of_def)
haftmann@68028
   357
haftmann@68028
   358
qualified lemma ascii_of_idem:
haftmann@68028
   359
  "ascii_of c = c" if "\<not> digit7 c"
haftmann@68028
   360
  using that by (cases c) simp
bulwahn@39250
   361
haftmann@68028
   362
qualified lemma char_of_ascii_of [simp]:
haftmann@68028
   363
  "of_char (ascii_of c) = take_bit 7 (of_char c :: nat)"
haftmann@68028
   364
  by (cases c)
haftmann@68028
   365
    (simp add: numeral_3_eq_3 [symmetric] numeral_2_eq_2 [symmetric])
haftmann@68028
   366
haftmann@68028
   367
qualified typedef literal = "{cs. \<forall>c\<in>set cs. \<not> digit7 c}"
haftmann@68028
   368
  morphisms explode Abs_literal
haftmann@68028
   369
proof
haftmann@68028
   370
  show "[] \<in> {cs. \<forall>c\<in>set cs. \<not> digit7 c}"
haftmann@68028
   371
    by simp
haftmann@68028
   372
qed
haftmann@68028
   373
haftmann@68028
   374
qualified setup_lifting type_definition_literal
haftmann@59484
   375
haftmann@68028
   376
qualified lift_definition implode :: "string \<Rightarrow> literal"
haftmann@68028
   377
  is "map ascii_of"
haftmann@68028
   378
  by auto
haftmann@68028
   379
haftmann@68028
   380
qualified lemma implode_explode_eq [simp]:
haftmann@68028
   381
  "String.implode (String.explode s) = s"
haftmann@68028
   382
proof transfer
haftmann@68028
   383
  fix cs
haftmann@68028
   384
  show "map ascii_of cs = cs" if "\<forall>c\<in>set cs. \<not> digit7 c"
haftmann@68028
   385
    using that
haftmann@68028
   386
      by (induction cs) (simp_all add: ascii_of_idem)
haftmann@68028
   387
qed
haftmann@68028
   388
haftmann@68028
   389
qualified lemma explode_implode_eq [simp]:
haftmann@68028
   390
  "String.explode (String.implode cs) = map ascii_of cs"
haftmann@59484
   391
  by transfer rule
Andreas@54594
   392
haftmann@68028
   393
end
haftmann@68028
   394
haftmann@68028
   395
haftmann@68028
   396
subsubsection \<open>Syntactic representation\<close>
haftmann@68028
   397
haftmann@68028
   398
text \<open>
haftmann@68028
   399
  Logical ground representations for literals are:
haftmann@68028
   400
haftmann@68028
   401
  \<^enum> @{text 0} for the empty literal;
haftmann@66251
   402
haftmann@68028
   403
  \<^enum> @{text "Literal b0 \<dots> b6 s"} for a literal starting with one
haftmann@68028
   404
    character and continued by another literal.
haftmann@68028
   405
haftmann@68028
   406
  Syntactic representations for literals are:
haftmann@68028
   407
haftmann@68028
   408
  \<^enum> Printable text as string prefixed with @{text STR};
haftmann@68028
   409
haftmann@68033
   410
  \<^enum> A single ascii value as numerical hexadecimal value prefixed with @{text STR}.
haftmann@68028
   411
\<close>
haftmann@68028
   412
haftmann@68028
   413
instantiation String.literal :: zero
bulwahn@39250
   414
begin
haftmann@31051
   415
haftmann@68028
   416
context
haftmann@68028
   417
begin
haftmann@68028
   418
haftmann@68028
   419
qualified lift_definition zero_literal :: String.literal
haftmann@68028
   420
  is Nil
haftmann@68028
   421
  by simp
haftmann@31051
   422
bulwahn@39250
   423
instance ..
bulwahn@39250
   424
bulwahn@39250
   425
end
bulwahn@39250
   426
haftmann@68028
   427
end
haftmann@68028
   428
haftmann@68028
   429
context
bulwahn@39250
   430
begin
haftmann@31051
   431
haftmann@68028
   432
qualified abbreviation (output) empty_literal :: String.literal
haftmann@68028
   433
  where "empty_literal \<equiv> 0"
haftmann@68028
   434
haftmann@68028
   435
qualified lift_definition Literal :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal"
haftmann@68028
   436
  is "\<lambda>b0 b1 b2 b3 b4 b5 b6 cs. Char b0 b1 b2 b3 b4 b5 b6 False # cs"
haftmann@68028
   437
  by auto
haftmann@31051
   438
haftmann@68028
   439
qualified lemma Literal_eq_iff [simp]:
haftmann@68028
   440
  "Literal b0 b1 b2 b3 b4 b5 b6 s = Literal c0 c1 c2 c3 c4 c5 c6 t
haftmann@68028
   441
     \<longleftrightarrow> (b0 \<longleftrightarrow> c0) \<and> (b1 \<longleftrightarrow> c1) \<and> (b2 \<longleftrightarrow> c2) \<and> (b3 \<longleftrightarrow> c3)
haftmann@68028
   442
         \<and> (b4 \<longleftrightarrow> c4) \<and> (b5 \<longleftrightarrow> c5) \<and> (b6 \<longleftrightarrow> c6) \<and> s = t"
haftmann@68028
   443
  by transfer simp
haftmann@68028
   444
haftmann@68028
   445
qualified lemma empty_neq_Literal [simp]:
haftmann@68028
   446
  "empty_literal \<noteq> Literal b0 b1 b2 b3 b4 b5 b6 s"
haftmann@68028
   447
  by transfer simp
haftmann@68028
   448
haftmann@68028
   449
qualified lemma Literal_neq_empty [simp]:
haftmann@68028
   450
  "Literal b0 b1 b2 b3 b4 b5 b6 s \<noteq> empty_literal"
haftmann@68028
   451
  by transfer simp
bulwahn@39250
   452
bulwahn@39250
   453
end
haftmann@31051
   454
haftmann@68028
   455
code_datatype "0 :: String.literal" String.Literal
haftmann@68028
   456
haftmann@68028
   457
syntax
haftmann@68028
   458
  "_Literal" :: "str_position \<Rightarrow> String.literal"   ("STR _")
haftmann@68033
   459
  "_Ascii" :: "num_const \<Rightarrow> String.literal"        ("STR _")
Andreas@54594
   460
haftmann@68028
   461
ML_file "Tools/literal.ML"
haftmann@68028
   462
haftmann@52365
   463
haftmann@68028
   464
subsubsection \<open>Operations\<close>
haftmann@68028
   465
haftmann@68028
   466
instantiation String.literal :: plus
haftmann@67730
   467
begin
haftmann@67730
   468
haftmann@68028
   469
context
haftmann@68028
   470
begin
haftmann@68028
   471
haftmann@68028
   472
qualified lift_definition plus_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal"
haftmann@68028
   473
  is "(@)"
haftmann@68028
   474
  by auto
haftmann@67730
   475
haftmann@67730
   476
instance ..
haftmann@67730
   477
haftmann@67730
   478
end
haftmann@67730
   479
haftmann@68028
   480
end
haftmann@67730
   481
haftmann@68028
   482
instance String.literal :: monoid_add
haftmann@68028
   483
  by (standard; transfer) simp_all
haftmann@68028
   484
haftmann@68028
   485
instantiation String.literal :: size
haftmann@67729
   486
begin
haftmann@67729
   487
haftmann@68028
   488
context
haftmann@68028
   489
  includes literal.lifting
haftmann@68028
   490
begin
haftmann@68028
   491
haftmann@68028
   492
lift_definition size_literal :: "String.literal \<Rightarrow> nat"
haftmann@68028
   493
  is length .
haftmann@68028
   494
haftmann@68028
   495
end
haftmann@67729
   496
haftmann@67729
   497
instance ..
haftmann@67729
   498
haftmann@67729
   499
end
haftmann@67729
   500
haftmann@68028
   501
instantiation String.literal :: equal
haftmann@68028
   502
begin
haftmann@68028
   503
haftmann@68028
   504
context
haftmann@68028
   505
begin
haftmann@68028
   506
haftmann@68028
   507
qualified lift_definition equal_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
haftmann@68028
   508
  is HOL.equal .
haftmann@68028
   509
haftmann@68028
   510
instance
haftmann@68028
   511
  by (standard; transfer) (simp add: equal)
haftmann@68028
   512
haftmann@68028
   513
end
haftmann@68028
   514
haftmann@68028
   515
end
haftmann@68028
   516
haftmann@68028
   517
instantiation String.literal :: linorder
haftmann@68028
   518
begin
haftmann@67729
   519
haftmann@68028
   520
context
haftmann@68028
   521
begin
haftmann@68028
   522
haftmann@68028
   523
qualified lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
haftmann@68028
   524
  is "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
haftmann@68028
   525
  .
haftmann@68028
   526
haftmann@68028
   527
qualified lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
haftmann@68028
   528
  is "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat))"
haftmann@68028
   529
  .
haftmann@68028
   530
haftmann@68028
   531
instance proof -
haftmann@68028
   532
  from linorder_char interpret linorder "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
haftmann@68028
   533
    "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat)) :: string \<Rightarrow> string \<Rightarrow> bool"
haftmann@68028
   534
    by (rule linorder.lexordp_linorder)
haftmann@68028
   535
  show "PROP ?thesis"
haftmann@68028
   536
    by (standard; transfer) (simp_all add: less_le_not_le linear)
haftmann@68028
   537
qed
haftmann@68028
   538
haftmann@68028
   539
end
haftmann@68028
   540
haftmann@68028
   541
end
haftmann@67730
   542
haftmann@68028
   543
lemma infinite_literal:
haftmann@68028
   544
  "infinite (UNIV :: String.literal set)"
haftmann@68028
   545
proof -
haftmann@68028
   546
  define S where "S = range (\<lambda>n. replicate n CHR ''A'')"
haftmann@68028
   547
  have "inj_on String.implode S"
haftmann@68028
   548
  proof (rule inj_onI)
haftmann@68028
   549
    fix cs ds
haftmann@68028
   550
    assume "String.implode cs = String.implode ds"
haftmann@68028
   551
    then have "String.explode (String.implode cs) = String.explode (String.implode ds)"
haftmann@68028
   552
      by simp
haftmann@68028
   553
    moreover assume "cs \<in> S" and "ds \<in> S"
haftmann@68028
   554
    ultimately show "cs = ds"
haftmann@68028
   555
      by (auto simp add: S_def)
haftmann@68028
   556
  qed
haftmann@68028
   557
  moreover have "infinite S"
haftmann@68028
   558
    by (auto simp add: S_def dest: finite_range_imageI [of _ length])
haftmann@68028
   559
  ultimately have "infinite (String.implode ` S)"
haftmann@68028
   560
    by (simp add: finite_image_iff)
haftmann@68028
   561
  then show ?thesis
haftmann@68028
   562
    by (auto intro: finite_subset)
haftmann@68028
   563
qed
haftmann@68028
   564
haftmann@68028
   565
haftmann@68028
   566
subsubsection \<open>Executable conversions\<close>
haftmann@68028
   567
haftmann@68028
   568
context
haftmann@68028
   569
begin
haftmann@68028
   570
haftmann@68028
   571
qualified lift_definition asciis_of_literal :: "String.literal \<Rightarrow> integer list"
haftmann@68028
   572
  is "map of_char"
haftmann@68028
   573
  .
haftmann@68028
   574
haftmann@68028
   575
qualified lift_definition literal_of_asciis :: "integer list \<Rightarrow> String.literal"
haftmann@68028
   576
  is "map (String.ascii_of \<circ> char_of)"
haftmann@68028
   577
  by auto
Andreas@55426
   578
haftmann@68028
   579
qualified lemma literal_of_asciis_of_literal [simp]:
haftmann@68028
   580
  "literal_of_asciis (asciis_of_literal s) = s"
haftmann@68028
   581
proof transfer
haftmann@68028
   582
  fix cs
haftmann@68028
   583
  assume "\<forall>c\<in>set cs. \<not> digit7 c"
haftmann@68028
   584
  then show "map (String.ascii_of \<circ> char_of) (map of_char cs) = cs"
haftmann@68028
   585
    by (induction cs) (simp_all add: String.ascii_of_idem) 
haftmann@68028
   586
qed
haftmann@68028
   587
haftmann@68028
   588
qualified lemma explode_code [code]:
haftmann@68028
   589
  "String.explode s = map char_of (asciis_of_literal s)"
haftmann@68028
   590
  by transfer simp
haftmann@68028
   591
haftmann@68028
   592
qualified lemma implode_code [code]:
haftmann@68028
   593
  "String.implode cs = literal_of_asciis (map of_char cs)"
haftmann@68028
   594
  by transfer simp
haftmann@64994
   595
haftmann@68028
   596
end
haftmann@68028
   597
haftmann@68028
   598
declare [[code drop: String.literal_of_asciis String.asciis_of_literal]]
haftmann@68028
   599
haftmann@68028
   600
haftmann@68028
   601
subsubsection \<open>Technical code generation setup\<close>
haftmann@68028
   602
haftmann@68028
   603
text \<open>Alternative constructor for generated computations\<close>
haftmann@68028
   604
haftmann@68028
   605
context
haftmann@68028
   606
begin  
haftmann@68028
   607
haftmann@68028
   608
qualified definition Literal' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal"
haftmann@68028
   609
  where [simp]: "Literal' = String.Literal"
haftmann@68028
   610
haftmann@68028
   611
lemma [code]:
haftmann@68028
   612
  "Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis
haftmann@68028
   613
    [foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0] + s" 
haftmann@68028
   614
  unfolding Literal'_def by transfer (simp add: char_of_def)
haftmann@64994
   615
haftmann@64994
   616
lemma [code_computation_unfold]:
haftmann@68028
   617
  "String.Literal = Literal'"
haftmann@68028
   618
  by simp
haftmann@64994
   619
haftmann@68028
   620
end
haftmann@31051
   621
haftmann@68028
   622
code_reserved SML string Char
haftmann@68028
   623
code_reserved OCaml string String Char List
haftmann@68028
   624
code_reserved Haskell Prelude
haftmann@34886
   625
code_reserved Scala string
haftmann@33237
   626
haftmann@52435
   627
code_printing
haftmann@68028
   628
  type_constructor String.literal \<rightharpoonup>
haftmann@52435
   629
    (SML) "string"
haftmann@52435
   630
    and (OCaml) "string"
haftmann@52435
   631
    and (Haskell) "String"
haftmann@52435
   632
    and (Scala) "String"
haftmann@68028
   633
| constant "STR ''''" \<rightharpoonup>
haftmann@68028
   634
    (SML) "\"\""
haftmann@68028
   635
    and (OCaml) "\"\""
haftmann@68028
   636
    and (Haskell) "\"\""
haftmann@68028
   637
    and (Scala) "\"\""
haftmann@31051
   638
wenzelm@60758
   639
setup \<open>
haftmann@68028
   640
  fold Literal.add_code ["SML", "OCaml", "Haskell", "Scala"]
wenzelm@60758
   641
\<close>
haftmann@31051
   642
haftmann@52435
   643
code_printing
haftmann@68028
   644
  constant "(+) :: String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal" \<rightharpoonup>
haftmann@68028
   645
    (SML) infixl 18 "^"
haftmann@68028
   646
    and (OCaml) infixr 6 "^"
haftmann@68028
   647
    and (Haskell) infixr 5 "++"
haftmann@68028
   648
    and (Scala) infixl 7 "+"
haftmann@68028
   649
| constant String.literal_of_asciis \<rightharpoonup>
haftmann@68028
   650
    (SML) "!(String.implode/ o map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))"
haftmann@68028
   651
    and (OCaml) "!(let ks = _ in let res = Bytes.create (List.length ks) in let rec imp i = function | [] -> res | k :: ks ->
haftmann@68028
   652
      let l = Big'_int.int'_of'_big'_int k in if 0 <= l && l < 128 then Bytes.set res i (Char.chr l) else failwith \"Non-ASCII character in literal\"; imp (i + 1) ks in imp 0 ks)"
haftmann@68028
   653
    and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
haftmann@68028
   654
    and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))"
haftmann@68028
   655
| constant String.asciis_of_literal \<rightharpoonup>
haftmann@68028
   656
    (SML) "!(map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)"
haftmann@68028
   657
    and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (Bytes.get s i) in
haftmann@68028
   658
      if k < 128 then Big'_int.big'_int'_of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (Bytes.length s - 1) [])"
haftmann@68028
   659
    and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"
haftmann@68028
   660
    and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))"
haftmann@68028
   661
| class_instance String.literal :: equal \<rightharpoonup>
haftmann@52435
   662
    (Haskell) -
haftmann@68028
   663
| constant "HOL.equal :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
   664
    (SML) "!((_ : string) = _)"
haftmann@52435
   665
    and (OCaml) "!((_ : string) = _)"
haftmann@52435
   666
    and (Haskell) infix 4 "=="
haftmann@52435
   667
    and (Scala) infixl 5 "=="
haftmann@68028
   668
| constant "(\<le>) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
haftmann@68028
   669
    (SML) "!((_ : string) <= _)"
haftmann@68028
   670
    and (OCaml) "!((_ : string) <= _)"
haftmann@68028
   671
    \<comment> \<open>Order operations for @{typ String.literal} work in Haskell only
haftmann@68028
   672
          if no type class instance needs to be generated, because String = [Char] in Haskell
haftmann@68028
   673
          and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
haftmann@68028
   674
    and (Haskell) infix 4 "<="
haftmann@68028
   675
    and (Scala) infixl 4 "<="
haftmann@68028
   676
    and (Eval) infixl 6 "<="
haftmann@68028
   677
| constant "(<) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
haftmann@68028
   678
    (SML) "!((_ : string) < _)"
haftmann@68028
   679
    and (OCaml) "!((_ : string) < _)"
haftmann@68028
   680
    and (Haskell) infix 4 "<"
haftmann@68028
   681
    and (Scala) infixl 4 "<"
haftmann@68028
   682
    and (Eval) infixl 6 "<"
haftmann@68028
   683
haftmann@68028
   684
haftmann@68028
   685
subsubsection \<open>Code generation utility\<close>
haftmann@31051
   686
wenzelm@60758
   687
setup \<open>Sign.map_naming (Name_Space.mandatory_path "Code")\<close>
Andreas@52910
   688
haftmann@68028
   689
definition abort :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
haftmann@68028
   690
  where [simp]: "abort _ f = f ()"
Andreas@52910
   691
haftmann@68028
   692
declare [[code drop: Code.abort]]
haftmann@68028
   693
haftmann@68028
   694
lemma abort_cong:
haftmann@68028
   695
  "msg = msg' \<Longrightarrow> Code.abort msg f = Code.abort msg' f"
haftmann@68028
   696
  by simp
Andreas@54317
   697
wenzelm@60758
   698
setup \<open>Sign.map_naming Name_Space.parent_path\<close>
Andreas@52910
   699
wenzelm@60758
   700
setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong})\<close>
Andreas@54317
   701
haftmann@68028
   702
code_printing
haftmann@68028
   703
  constant Code.abort \<rightharpoonup>
Andreas@52910
   704
    (SML) "!(raise/ Fail/ _)"
Andreas@52910
   705
    and (OCaml) "failwith"
haftmann@59483
   706
    and (Haskell) "!(error/ ::/ forall a./ String -> (() -> a) -> a)"
haftmann@68028
   707
    and (Scala) "!{/ sys.error((_));/ ((_)).apply(())/ }"
haftmann@68028
   708
Andreas@52910
   709
haftmann@68028
   710
subsubsection \<open>Finally\<close>
haftmann@31205
   711
haftmann@68028
   712
lifting_update literal.lifting
haftmann@68028
   713
lifting_forget literal.lifting
haftmann@57437
   714
bulwahn@39250
   715
end