src/HOL/String.thy
author haftmann
Sun Jul 02 20:13:38 2017 +0200 (22 months ago)
changeset 66251 cd935b7cb3fb
parent 66190 a41435469559
child 66331 f773691617c0
permissions -rw-r--r--
proper concept of code declaration wrt. atomicity and Isar declarations
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
wenzelm@60758
     9
subsection \<open>Characters and strings\<close>
haftmann@31051
    10
haftmann@62364
    11
subsubsection \<open>Characters as finite algebraic type\<close>
haftmann@62364
    12
haftmann@62364
    13
typedef char = "{n::nat. n < 256}"
haftmann@62364
    14
  morphisms nat_of_char Abs_char
haftmann@62364
    15
proof
haftmann@62364
    16
  show "Suc 0 \<in> {n. n < 256}" by simp
haftmann@62364
    17
qed
haftmann@62364
    18
haftmann@62364
    19
definition char_of_nat :: "nat \<Rightarrow> char"
haftmann@62364
    20
where
haftmann@62364
    21
  "char_of_nat n = Abs_char (n mod 256)"
haftmann@62364
    22
haftmann@62364
    23
lemma char_cases [case_names char_of_nat, cases type: char]:
haftmann@62364
    24
  "(\<And>n. c = char_of_nat n \<Longrightarrow> n < 256 \<Longrightarrow> P) \<Longrightarrow> P"
haftmann@62364
    25
  by (cases c) (simp add: char_of_nat_def)
haftmann@62364
    26
haftmann@62364
    27
lemma char_of_nat_of_char [simp]:
haftmann@62364
    28
  "char_of_nat (nat_of_char c) = c"
haftmann@62364
    29
  by (cases c) (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse)
haftmann@62364
    30
haftmann@62364
    31
lemma inj_nat_of_char:
haftmann@62364
    32
  "inj nat_of_char"
haftmann@62364
    33
proof (rule injI)
haftmann@62364
    34
  fix c d
haftmann@62364
    35
  assume "nat_of_char c = nat_of_char d"
haftmann@62364
    36
  then have "char_of_nat (nat_of_char c) = char_of_nat (nat_of_char d)"
haftmann@62364
    37
    by simp
haftmann@62364
    38
  then show "c = d"
haftmann@62364
    39
    by simp
haftmann@62364
    40
qed
haftmann@62364
    41
  
haftmann@62364
    42
lemma nat_of_char_eq_iff [simp]:
haftmann@62364
    43
  "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
haftmann@62364
    44
  by (fact nat_of_char_inject)
haftmann@62364
    45
haftmann@62364
    46
lemma nat_of_char_of_nat [simp]:
haftmann@62364
    47
  "nat_of_char (char_of_nat n) = n mod 256"
haftmann@62364
    48
  by (cases "char_of_nat n") (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse)
haftmann@62364
    49
haftmann@62364
    50
lemma char_of_nat_mod_256 [simp]:
haftmann@62364
    51
  "char_of_nat (n mod 256) = char_of_nat n"
haftmann@62364
    52
  by (cases "char_of_nat (n mod 256)") (simp add: char_of_nat_def)
haftmann@62364
    53
haftmann@62364
    54
lemma char_of_nat_quasi_inj [simp]:
haftmann@62364
    55
  "char_of_nat m = char_of_nat n \<longleftrightarrow> m mod 256 = n mod 256"
haftmann@62364
    56
  by (simp add: char_of_nat_def Abs_char_inject)
haftmann@62364
    57
haftmann@62364
    58
lemma inj_on_char_of_nat [simp]:
haftmann@62597
    59
  "inj_on char_of_nat {..<256}"
haftmann@62364
    60
  by (rule inj_onI) simp
haftmann@62364
    61
haftmann@62364
    62
lemma nat_of_char_mod_256 [simp]:
haftmann@62364
    63
  "nat_of_char c mod 256 = nat_of_char c"
haftmann@62364
    64
  by (cases c) simp
haftmann@62364
    65
haftmann@62364
    66
lemma nat_of_char_less_256 [simp]:
haftmann@62364
    67
  "nat_of_char c < 256"
haftmann@62364
    68
proof -
haftmann@62364
    69
  have "nat_of_char c mod 256 < 256"
haftmann@62364
    70
    by arith
haftmann@62364
    71
  then show ?thesis by simp
haftmann@62364
    72
qed
haftmann@62364
    73
haftmann@62364
    74
lemma UNIV_char_of_nat:
haftmann@62597
    75
  "UNIV = char_of_nat ` {..<256}"
haftmann@62364
    76
proof -
haftmann@62364
    77
  { fix c
haftmann@62597
    78
    have "c \<in> char_of_nat ` {..<256}"
haftmann@62364
    79
      by (cases c) auto
haftmann@62364
    80
  } then show ?thesis by auto
haftmann@62364
    81
qed
haftmann@62364
    82
haftmann@62597
    83
lemma card_UNIV_char:
haftmann@62597
    84
  "card (UNIV :: char set) = 256"
haftmann@62597
    85
  by (auto simp add: UNIV_char_of_nat card_image)
haftmann@31051
    86
haftmann@62597
    87
lemma range_nat_of_char:
haftmann@62597
    88
  "range nat_of_char = {..<256}"
haftmann@62597
    89
  by (auto simp add: UNIV_char_of_nat image_image image_def)
haftmann@31051
    90
haftmann@49972
    91
haftmann@62597
    92
subsubsection \<open>Character literals as variant of numerals\<close>
haftmann@62597
    93
haftmann@62597
    94
instantiation char :: zero
haftmann@49972
    95
begin
haftmann@49972
    96
haftmann@62597
    97
definition zero_char :: char
haftmann@62597
    98
  where "0 = char_of_nat 0"
haftmann@49972
    99
haftmann@62597
   100
instance ..
haftmann@49972
   101
haftmann@49972
   102
end
haftmann@49972
   103
haftmann@62597
   104
definition Char :: "num \<Rightarrow> char"
haftmann@62597
   105
  where "Char k = char_of_nat (numeral k)"
haftmann@62597
   106
haftmann@62597
   107
code_datatype "0 :: char" Char
haftmann@62597
   108
haftmann@62597
   109
lemma nat_of_char_zero [simp]:
haftmann@62597
   110
  "nat_of_char 0 = 0"
haftmann@62597
   111
  by (simp add: zero_char_def)
haftmann@62597
   112
haftmann@62597
   113
lemma nat_of_char_Char [simp]:
haftmann@62597
   114
  "nat_of_char (Char k) = numeral k mod 256"
haftmann@62597
   115
  by (simp add: Char_def)
haftmann@31051
   116
haftmann@64630
   117
lemma Char_eq_Char_iff:
haftmann@62597
   118
  "Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
haftmann@62597
   119
proof -
haftmann@62597
   120
  have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
haftmann@62597
   121
    by (rule sym, rule inj_eq) (fact inj_nat_of_char)
haftmann@62597
   122
  also have "nat_of_char (Char k) = nat_of_char (Char l) \<longleftrightarrow> ?Q"
haftmann@62597
   123
    by (simp only: Char_def nat_of_char_of_nat)
haftmann@62597
   124
  finally show ?thesis .
haftmann@62597
   125
qed
haftmann@62597
   126
haftmann@64630
   127
lemma zero_eq_Char_iff:
haftmann@62597
   128
  "0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
haftmann@62597
   129
  by (auto simp add: zero_char_def Char_def)
haftmann@62597
   130
haftmann@64630
   131
lemma Char_eq_zero_iff:
haftmann@62597
   132
  "Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
haftmann@62597
   133
  by (auto simp add: zero_char_def Char_def) 
haftmann@62597
   134
haftmann@64630
   135
simproc_setup char_eq
haftmann@64630
   136
  ("Char m = Char n" | "Char m = 0" | "0 = Char n") = \<open>
haftmann@64630
   137
  let
haftmann@64630
   138
    val ss = put_simpset HOL_ss @{context}
haftmann@64630
   139
      |> fold Simplifier.add_simp @{thms Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff cong_exp_iff_simps}
haftmann@64630
   140
      |> simpset_of 
haftmann@64630
   141
  in
haftmann@64630
   142
    fn _ => fn ctxt => SOME o Simplifier.rewrite (put_simpset ss ctxt)
haftmann@64630
   143
  end
haftmann@64630
   144
\<close>
haftmann@64630
   145
haftmann@62597
   146
definition integer_of_char :: "char \<Rightarrow> integer"
haftmann@51160
   147
where
haftmann@62597
   148
  "integer_of_char = integer_of_nat \<circ> nat_of_char"
haftmann@51160
   149
haftmann@62597
   150
definition char_of_integer :: "integer \<Rightarrow> char"
haftmann@62597
   151
where
haftmann@62597
   152
  "char_of_integer = char_of_nat \<circ> nat_of_integer"
haftmann@62597
   153
haftmann@62597
   154
lemma integer_of_char_zero [simp, code]:
haftmann@62597
   155
  "integer_of_char 0 = 0"
haftmann@62597
   156
  by (simp add: integer_of_char_def integer_of_nat_def)
haftmann@51160
   157
haftmann@62597
   158
lemma integer_of_char_Char [simp]:
haftmann@62597
   159
  "integer_of_char (Char k) = numeral k mod 256"
haftmann@62597
   160
  by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
haftmann@63950
   161
    id_apply zmod_int modulo_integer.abs_eq [symmetric]) simp
haftmann@51160
   162
haftmann@66190
   163
lemma integer_of_char_Char_code [code]:
haftmann@66190
   164
  "integer_of_char (Char k) = integer_of_num k mod 256"
haftmann@66190
   165
  by simp
haftmann@66190
   166
  
haftmann@62597
   167
lemma nat_of_char_code [code]:
haftmann@62597
   168
  "nat_of_char = nat_of_integer \<circ> integer_of_char"
haftmann@62597
   169
  by (simp add: integer_of_char_def fun_eq_iff)
haftmann@51160
   170
haftmann@62597
   171
lemma char_of_nat_code [code]:
haftmann@62597
   172
  "char_of_nat = char_of_integer \<circ> integer_of_nat"
haftmann@62597
   173
  by (simp add: char_of_integer_def fun_eq_iff)
haftmann@51160
   174
haftmann@62597
   175
instantiation char :: equal
haftmann@62364
   176
begin
haftmann@62364
   177
haftmann@62597
   178
definition equal_char
haftmann@62597
   179
  where "equal_char (c :: char) d \<longleftrightarrow> c = d"
haftmann@62364
   180
haftmann@62597
   181
instance
haftmann@62597
   182
  by standard (simp add: equal_char_def)
haftmann@31051
   183
haftmann@62364
   184
end
haftmann@62364
   185
haftmann@62597
   186
lemma equal_char_simps [code]:
haftmann@62597
   187
  "HOL.equal (0::char) 0 \<longleftrightarrow> True"
haftmann@62597
   188
  "HOL.equal (Char k) (Char l) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) (numeral l mod 256)"
haftmann@62597
   189
  "HOL.equal 0 (Char k) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
haftmann@62597
   190
  "HOL.equal (Char k) 0 \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
haftmann@62597
   191
  by (simp_all only: equal refl Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff)
haftmann@62364
   192
haftmann@31051
   193
syntax
haftmann@62597
   194
  "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
haftmann@62678
   195
  "_Char_ord" :: "num_const \<Rightarrow> char"   ("CHR _")
haftmann@31051
   196
bulwahn@42163
   197
type_synonym string = "char list"
haftmann@31051
   198
haftmann@31051
   199
syntax
wenzelm@46483
   200
  "_String" :: "str_position => string"    ("_")
haftmann@31051
   201
wenzelm@48891
   202
ML_file "Tools/string_syntax.ML"
haftmann@31051
   203
haftmann@49972
   204
instantiation char :: enum
haftmann@49972
   205
begin
haftmann@49972
   206
haftmann@49972
   207
definition
haftmann@62678
   208
  "Enum.enum = [0, CHR 0x01, CHR 0x02, CHR 0x03,
haftmann@62678
   209
    CHR 0x04, CHR 0x05, CHR 0x06, CHR 0x07,
haftmann@62678
   210
    CHR 0x08, CHR 0x09, CHR ''\<newline>'', CHR 0x0B,
haftmann@62678
   211
    CHR 0x0C, CHR 0x0D, CHR 0x0E, CHR 0x0F,
haftmann@62678
   212
    CHR 0x10, CHR 0x11, CHR 0x12, CHR 0x13,
haftmann@62678
   213
    CHR 0x14, CHR 0x15, CHR 0x16, CHR 0x17,
haftmann@62678
   214
    CHR 0x18, CHR 0x19, CHR 0x1A, CHR 0x1B,
haftmann@62678
   215
    CHR 0x1C, CHR 0x1D, CHR 0x1E, CHR 0x1F,
haftmann@62678
   216
    CHR '' '', CHR ''!'', CHR 0x22, CHR ''#'',
haftmann@62678
   217
    CHR ''$'', CHR ''%'', CHR ''&'', CHR 0x27,
haftmann@62597
   218
    CHR ''('', CHR '')'', CHR ''*'', CHR ''+'',
haftmann@62597
   219
    CHR '','', CHR ''-'', CHR ''.'', CHR ''/'',
haftmann@62597
   220
    CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
haftmann@62597
   221
    CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'',
haftmann@62597
   222
    CHR ''8'', CHR ''9'', CHR '':'', CHR '';'',
haftmann@62597
   223
    CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'',
haftmann@62597
   224
    CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'',
haftmann@62597
   225
    CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'',
haftmann@62597
   226
    CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'',
haftmann@62597
   227
    CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
haftmann@62597
   228
    CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'',
haftmann@62597
   229
    CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'',
haftmann@62597
   230
    CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['',
haftmann@62678
   231
    CHR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
haftmann@62678
   232
    CHR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
haftmann@62597
   233
    CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'',
haftmann@62597
   234
    CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'',
haftmann@62597
   235
    CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'',
haftmann@62597
   236
    CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'',
haftmann@62597
   237
    CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
haftmann@62597
   238
    CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'',
haftmann@62678
   239
    CHR ''|'', CHR ''}'', CHR ''~'', CHR 0x7F,
haftmann@62678
   240
    CHR 0x80, CHR 0x81, CHR 0x82, CHR 0x83,
haftmann@62678
   241
    CHR 0x84, CHR 0x85, CHR 0x86, CHR 0x87,
haftmann@62678
   242
    CHR 0x88, CHR 0x89, CHR 0x8A, CHR 0x8B,
haftmann@62678
   243
    CHR 0x8C, CHR 0x8D, CHR 0x8E, CHR 0x8F,
haftmann@62678
   244
    CHR 0x90, CHR 0x91, CHR 0x92, CHR 0x93,
haftmann@62678
   245
    CHR 0x94, CHR 0x95, CHR 0x96, CHR 0x97,
haftmann@62678
   246
    CHR 0x98, CHR 0x99, CHR 0x9A, CHR 0x9B,
haftmann@62678
   247
    CHR 0x9C, CHR 0x9D, CHR 0x9E, CHR 0x9F,
haftmann@62678
   248
    CHR 0xA0, CHR 0xA1, CHR 0xA2, CHR 0xA3,
haftmann@62678
   249
    CHR 0xA4, CHR 0xA5, CHR 0xA6, CHR 0xA7,
haftmann@62678
   250
    CHR 0xA8, CHR 0xA9, CHR 0xAA, CHR 0xAB,
haftmann@62678
   251
    CHR 0xAC, CHR 0xAD, CHR 0xAE, CHR 0xAF,
haftmann@62678
   252
    CHR 0xB0, CHR 0xB1, CHR 0xB2, CHR 0xB3,
haftmann@62678
   253
    CHR 0xB4, CHR 0xB5, CHR 0xB6, CHR 0xB7,
haftmann@62678
   254
    CHR 0xB8, CHR 0xB9, CHR 0xBA, CHR 0xBB,
haftmann@62678
   255
    CHR 0xBC, CHR 0xBD, CHR 0xBE, CHR 0xBF,
haftmann@62678
   256
    CHR 0xC0, CHR 0xC1, CHR 0xC2, CHR 0xC3,
haftmann@62678
   257
    CHR 0xC4, CHR 0xC5, CHR 0xC6, CHR 0xC7,
haftmann@62678
   258
    CHR 0xC8, CHR 0xC9, CHR 0xCA, CHR 0xCB,
haftmann@62678
   259
    CHR 0xCC, CHR 0xCD, CHR 0xCE, CHR 0xCF,
haftmann@62678
   260
    CHR 0xD0, CHR 0xD1, CHR 0xD2, CHR 0xD3,
haftmann@62678
   261
    CHR 0xD4, CHR 0xD5, CHR 0xD6, CHR 0xD7,
haftmann@62678
   262
    CHR 0xD8, CHR 0xD9, CHR 0xDA, CHR 0xDB,
haftmann@62678
   263
    CHR 0xDC, CHR 0xDD, CHR 0xDE, CHR 0xDF,
haftmann@62678
   264
    CHR 0xE0, CHR 0xE1, CHR 0xE2, CHR 0xE3,
haftmann@62678
   265
    CHR 0xE4, CHR 0xE5, CHR 0xE6, CHR 0xE7,
haftmann@62678
   266
    CHR 0xE8, CHR 0xE9, CHR 0xEA, CHR 0xEB,
haftmann@62678
   267
    CHR 0xEC, CHR 0xED, CHR 0xEE, CHR 0xEF,
haftmann@62678
   268
    CHR 0xF0, CHR 0xF1, CHR 0xF2, CHR 0xF3,
haftmann@62678
   269
    CHR 0xF4, CHR 0xF5, CHR 0xF6, CHR 0xF7,
haftmann@62678
   270
    CHR 0xF8, CHR 0xF9, CHR 0xFA, CHR 0xFB,
haftmann@62678
   271
    CHR 0xFC, CHR 0xFD, CHR 0xFE, CHR 0xFF]"
haftmann@31484
   272
haftmann@49972
   273
definition
haftmann@49972
   274
  "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
haftmann@49972
   275
haftmann@49972
   276
definition
haftmann@49972
   277
  "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
haftmann@49972
   278
haftmann@62597
   279
lemma enum_char_unfold:
haftmann@62597
   280
  "Enum.enum = map char_of_nat [0..<256]"
haftmann@62597
   281
proof -
haftmann@62597
   282
  have *: "Suc (Suc 0) = 2" by simp
haftmann@62597
   283
  have "map nat_of_char Enum.enum = [0..<256]"
haftmann@62597
   284
    by (simp add: enum_char_def upt_conv_Cons_Cons *)
haftmann@62597
   285
  then have "map char_of_nat (map nat_of_char Enum.enum) =
haftmann@62597
   286
    map char_of_nat [0..<256]" by simp
haftmann@62597
   287
  then show ?thesis by (simp add: comp_def)
haftmann@62597
   288
qed
haftmann@51160
   289
haftmann@49972
   290
instance proof
haftmann@49972
   291
  show UNIV: "UNIV = set (Enum.enum :: char list)"
haftmann@62597
   292
    by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan)
haftmann@49972
   293
  show "distinct (Enum.enum :: char list)"
haftmann@62597
   294
    by (auto simp add: enum_char_unfold distinct_map intro: inj_onI)
haftmann@49972
   295
  show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
haftmann@49972
   296
    by (simp add: UNIV enum_all_char_def list_all_iff)
haftmann@49972
   297
  show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
haftmann@49972
   298
    by (simp add: UNIV enum_ex_char_def list_ex_iff)
haftmann@49972
   299
qed
haftmann@49972
   300
haftmann@49972
   301
end
haftmann@49972
   302
haftmann@62597
   303
lemma char_of_integer_code [code]:
haftmann@62597
   304
  "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
haftmann@62597
   305
  by (simp add: char_of_integer_def enum_char_unfold)
haftmann@49948
   306
haftmann@31051
   307
wenzelm@60758
   308
subsection \<open>Strings as dedicated type\<close>
bulwahn@39250
   309
wenzelm@49834
   310
typedef literal = "UNIV :: string set"
bulwahn@39250
   311
  morphisms explode STR ..
bulwahn@39250
   312
haftmann@59484
   313
setup_lifting type_definition_literal
haftmann@59484
   314
haftmann@59484
   315
lemma STR_inject' [simp]:
haftmann@59484
   316
  "STR s = STR t \<longleftrightarrow> s = t"
haftmann@59484
   317
  by transfer rule
Andreas@54594
   318
haftmann@57437
   319
definition implode :: "string \<Rightarrow> String.literal"
haftmann@57437
   320
where
haftmann@59484
   321
  [code del]: "implode = STR"
haftmann@66251
   322
bulwahn@39250
   323
instantiation literal :: size
bulwahn@39250
   324
begin
haftmann@31051
   325
bulwahn@39250
   326
definition size_literal :: "literal \<Rightarrow> nat"
bulwahn@39250
   327
where
wenzelm@61076
   328
  [code]: "size_literal (s::literal) = 0"
haftmann@31051
   329
bulwahn@39250
   330
instance ..
bulwahn@39250
   331
bulwahn@39250
   332
end
bulwahn@39250
   333
bulwahn@39250
   334
instantiation literal :: equal
bulwahn@39250
   335
begin
haftmann@31051
   336
Andreas@54594
   337
lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "op =" .
haftmann@31051
   338
Andreas@54594
   339
instance by intro_classes (transfer, simp)
bulwahn@39250
   340
bulwahn@39250
   341
end
haftmann@31051
   342
Andreas@54594
   343
declare equal_literal.rep_eq[code]
Andreas@54594
   344
haftmann@52365
   345
lemma [code nbe]:
haftmann@52365
   346
  fixes s :: "String.literal"
haftmann@52365
   347
  shows "HOL.equal s s \<longleftrightarrow> True"
haftmann@52365
   348
  by (simp add: equal)
haftmann@52365
   349
Andreas@55426
   350
lifting_update literal.lifting
Andreas@55426
   351
lifting_forget literal.lifting
Andreas@55426
   352
haftmann@64994
   353
  
haftmann@64994
   354
subsection \<open>Dedicated conversion for generated computations\<close>
haftmann@64994
   355
haftmann@64994
   356
definition char_of_num :: "num \<Rightarrow> char"
haftmann@64994
   357
  where "char_of_num = char_of_nat o nat_of_num"
haftmann@64994
   358
haftmann@64994
   359
lemma [code_computation_unfold]:
haftmann@64994
   360
  "Char = char_of_num"
haftmann@64994
   361
  by (simp add: fun_eq_iff char_of_num_def nat_of_num_numeral Char_def)
haftmann@64994
   362
haftmann@64994
   363
wenzelm@60758
   364
subsection \<open>Code generator\<close>
haftmann@31051
   365
wenzelm@48891
   366
ML_file "Tools/string_code.ML"
haftmann@31051
   367
haftmann@33237
   368
code_reserved SML string
haftmann@33237
   369
code_reserved OCaml string
haftmann@34886
   370
code_reserved Scala string
haftmann@33237
   371
haftmann@52435
   372
code_printing
haftmann@52435
   373
  type_constructor literal \<rightharpoonup>
haftmann@52435
   374
    (SML) "string"
haftmann@52435
   375
    and (OCaml) "string"
haftmann@52435
   376
    and (Haskell) "String"
haftmann@52435
   377
    and (Scala) "String"
haftmann@31051
   378
wenzelm@60758
   379
setup \<open>
haftmann@34886
   380
  fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
wenzelm@60758
   381
\<close>
haftmann@31051
   382
haftmann@52435
   383
code_printing
haftmann@52435
   384
  class_instance literal :: equal \<rightharpoonup>
haftmann@52435
   385
    (Haskell) -
haftmann@52435
   386
| constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
   387
    (SML) "!((_ : string) = _)"
haftmann@52435
   388
    and (OCaml) "!((_ : string) = _)"
haftmann@52435
   389
    and (Haskell) infix 4 "=="
haftmann@52435
   390
    and (Scala) infixl 5 "=="
haftmann@31051
   391
wenzelm@60758
   392
setup \<open>Sign.map_naming (Name_Space.mandatory_path "Code")\<close>
Andreas@52910
   393
Andreas@52910
   394
definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
Andreas@52910
   395
where [simp, code del]: "abort _ f = f ()"
Andreas@52910
   396
Andreas@54317
   397
lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
Andreas@54317
   398
by simp
Andreas@54317
   399
wenzelm@60758
   400
setup \<open>Sign.map_naming Name_Space.parent_path\<close>
Andreas@52910
   401
wenzelm@60758
   402
setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong})\<close>
Andreas@54317
   403
Andreas@52910
   404
code_printing constant Code.abort \<rightharpoonup>
Andreas@52910
   405
    (SML) "!(raise/ Fail/ _)"
Andreas@52910
   406
    and (OCaml) "failwith"
haftmann@59483
   407
    and (Haskell) "!(error/ ::/ forall a./ String -> (() -> a) -> a)"
Andreas@52910
   408
    and (Scala) "!{/ sys.error((_));/  ((_)).apply(())/ }"
Andreas@52910
   409
wenzelm@36176
   410
hide_type (open) literal
haftmann@31205
   411
haftmann@57437
   412
hide_const (open) implode explode
haftmann@57437
   413
bulwahn@39250
   414
end