src/HOL/String.thy
author haftmann
Sat Mar 19 16:53:09 2016 +0100 (2016-03-19)
changeset 62678 843ff6f1de38
parent 62597 b3f2b8c906a6
child 63950 cdc1e59aa513
permissions -rw-r--r--
unified CHAR with CHR syntax
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@62597
   117
lemma Char_eq_Char_iff [simp]:
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@62597
   127
lemma zero_eq_Char_iff [simp]:
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@62597
   131
lemma Char_eq_zero_iff [simp]:
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@62597
   135
definition integer_of_char :: "char \<Rightarrow> integer"
haftmann@51160
   136
where
haftmann@62597
   137
  "integer_of_char = integer_of_nat \<circ> nat_of_char"
haftmann@51160
   138
haftmann@62597
   139
definition char_of_integer :: "integer \<Rightarrow> char"
haftmann@62597
   140
where
haftmann@62597
   141
  "char_of_integer = char_of_nat \<circ> nat_of_integer"
haftmann@62597
   142
haftmann@62597
   143
lemma integer_of_char_zero [simp, code]:
haftmann@62597
   144
  "integer_of_char 0 = 0"
haftmann@62597
   145
  by (simp add: integer_of_char_def integer_of_nat_def)
haftmann@51160
   146
haftmann@62597
   147
lemma integer_of_char_Char [simp]:
haftmann@62597
   148
  "integer_of_char (Char k) = numeral k mod 256"
haftmann@62597
   149
  by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
haftmann@62597
   150
    id_apply zmod_int mod_integer.abs_eq [symmetric]) simp
haftmann@51160
   151
haftmann@62597
   152
lemma less_256_integer_of_char_Char:
haftmann@62597
   153
  assumes "numeral k < (256 :: integer)"
haftmann@62597
   154
  shows "integer_of_char (Char k) = numeral k"
haftmann@62597
   155
proof -
haftmann@62597
   156
  have "numeral k mod 256 = (numeral k :: integer)"
haftmann@62597
   157
    by (rule semiring_numeral_div_class.mod_less) (insert assms, simp_all)
haftmann@62597
   158
  then show ?thesis using integer_of_char_Char [of k]
haftmann@62597
   159
    by (simp only:)
haftmann@62597
   160
qed
haftmann@51160
   161
haftmann@62597
   162
setup \<open>
haftmann@62597
   163
let
haftmann@62597
   164
  val chars = map_range (Thm.cterm_of @{context} o HOLogic.mk_numeral o curry (op +) 1) 255;
haftmann@62597
   165
  val simpset =
haftmann@62597
   166
    put_simpset HOL_ss @{context}
haftmann@62597
   167
      addsimps @{thms numeral_less_iff less_num_simps};
haftmann@62597
   168
  fun mk_code_eqn ct =
haftmann@62597
   169
    Thm.instantiate' [] [SOME ct] @{thm less_256_integer_of_char_Char}
haftmann@62597
   170
    |> full_simplify simpset;
haftmann@62597
   171
  val code_eqns = map mk_code_eqn chars;
haftmann@62597
   172
in
haftmann@62597
   173
  Global_Theory.note_thmss ""
haftmann@62597
   174
    [((@{binding integer_of_char_simps}, []), [(code_eqns, [])])]
haftmann@62597
   175
  #> snd
haftmann@62597
   176
end
haftmann@62597
   177
\<close>
haftmann@51160
   178
haftmann@62597
   179
declare integer_of_char_simps [code]
haftmann@62597
   180
haftmann@62597
   181
lemma nat_of_char_code [code]:
haftmann@62597
   182
  "nat_of_char = nat_of_integer \<circ> integer_of_char"
haftmann@62597
   183
  by (simp add: integer_of_char_def fun_eq_iff)
haftmann@51160
   184
haftmann@62597
   185
lemma char_of_nat_code [code]:
haftmann@62597
   186
  "char_of_nat = char_of_integer \<circ> integer_of_nat"
haftmann@62597
   187
  by (simp add: char_of_integer_def fun_eq_iff)
haftmann@51160
   188
haftmann@62597
   189
instantiation char :: equal
haftmann@62364
   190
begin
haftmann@62364
   191
haftmann@62597
   192
definition equal_char
haftmann@62597
   193
  where "equal_char (c :: char) d \<longleftrightarrow> c = d"
haftmann@62364
   194
haftmann@62597
   195
instance
haftmann@62597
   196
  by standard (simp add: equal_char_def)
haftmann@31051
   197
haftmann@62364
   198
end
haftmann@62364
   199
haftmann@62597
   200
lemma equal_char_simps [code]:
haftmann@62597
   201
  "HOL.equal (0::char) 0 \<longleftrightarrow> True"
haftmann@62597
   202
  "HOL.equal (Char k) (Char l) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) (numeral l mod 256)"
haftmann@62597
   203
  "HOL.equal 0 (Char k) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
haftmann@62597
   204
  "HOL.equal (Char k) 0 \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
haftmann@62597
   205
  by (simp_all only: equal refl Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff)
haftmann@62364
   206
haftmann@31051
   207
syntax
haftmann@62597
   208
  "_Char" :: "str_position \<Rightarrow> char"    ("CHR _")
haftmann@62678
   209
  "_Char_ord" :: "num_const \<Rightarrow> char"   ("CHR _")
haftmann@31051
   210
bulwahn@42163
   211
type_synonym string = "char list"
haftmann@31051
   212
haftmann@31051
   213
syntax
wenzelm@46483
   214
  "_String" :: "str_position => string"    ("_")
haftmann@31051
   215
wenzelm@48891
   216
ML_file "Tools/string_syntax.ML"
haftmann@31051
   217
haftmann@49972
   218
instantiation char :: enum
haftmann@49972
   219
begin
haftmann@49972
   220
haftmann@49972
   221
definition
haftmann@62678
   222
  "Enum.enum = [0, CHR 0x01, CHR 0x02, CHR 0x03,
haftmann@62678
   223
    CHR 0x04, CHR 0x05, CHR 0x06, CHR 0x07,
haftmann@62678
   224
    CHR 0x08, CHR 0x09, CHR ''\<newline>'', CHR 0x0B,
haftmann@62678
   225
    CHR 0x0C, CHR 0x0D, CHR 0x0E, CHR 0x0F,
haftmann@62678
   226
    CHR 0x10, CHR 0x11, CHR 0x12, CHR 0x13,
haftmann@62678
   227
    CHR 0x14, CHR 0x15, CHR 0x16, CHR 0x17,
haftmann@62678
   228
    CHR 0x18, CHR 0x19, CHR 0x1A, CHR 0x1B,
haftmann@62678
   229
    CHR 0x1C, CHR 0x1D, CHR 0x1E, CHR 0x1F,
haftmann@62678
   230
    CHR '' '', CHR ''!'', CHR 0x22, CHR ''#'',
haftmann@62678
   231
    CHR ''$'', CHR ''%'', CHR ''&'', CHR 0x27,
haftmann@62597
   232
    CHR ''('', CHR '')'', CHR ''*'', CHR ''+'',
haftmann@62597
   233
    CHR '','', CHR ''-'', CHR ''.'', CHR ''/'',
haftmann@62597
   234
    CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
haftmann@62597
   235
    CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'',
haftmann@62597
   236
    CHR ''8'', CHR ''9'', CHR '':'', CHR '';'',
haftmann@62597
   237
    CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'',
haftmann@62597
   238
    CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'',
haftmann@62597
   239
    CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'',
haftmann@62597
   240
    CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'',
haftmann@62597
   241
    CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
haftmann@62597
   242
    CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'',
haftmann@62597
   243
    CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'',
haftmann@62597
   244
    CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['',
haftmann@62678
   245
    CHR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
haftmann@62678
   246
    CHR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
haftmann@62597
   247
    CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'',
haftmann@62597
   248
    CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'',
haftmann@62597
   249
    CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'',
haftmann@62597
   250
    CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'',
haftmann@62597
   251
    CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
haftmann@62597
   252
    CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'',
haftmann@62678
   253
    CHR ''|'', CHR ''}'', CHR ''~'', CHR 0x7F,
haftmann@62678
   254
    CHR 0x80, CHR 0x81, CHR 0x82, CHR 0x83,
haftmann@62678
   255
    CHR 0x84, CHR 0x85, CHR 0x86, CHR 0x87,
haftmann@62678
   256
    CHR 0x88, CHR 0x89, CHR 0x8A, CHR 0x8B,
haftmann@62678
   257
    CHR 0x8C, CHR 0x8D, CHR 0x8E, CHR 0x8F,
haftmann@62678
   258
    CHR 0x90, CHR 0x91, CHR 0x92, CHR 0x93,
haftmann@62678
   259
    CHR 0x94, CHR 0x95, CHR 0x96, CHR 0x97,
haftmann@62678
   260
    CHR 0x98, CHR 0x99, CHR 0x9A, CHR 0x9B,
haftmann@62678
   261
    CHR 0x9C, CHR 0x9D, CHR 0x9E, CHR 0x9F,
haftmann@62678
   262
    CHR 0xA0, CHR 0xA1, CHR 0xA2, CHR 0xA3,
haftmann@62678
   263
    CHR 0xA4, CHR 0xA5, CHR 0xA6, CHR 0xA7,
haftmann@62678
   264
    CHR 0xA8, CHR 0xA9, CHR 0xAA, CHR 0xAB,
haftmann@62678
   265
    CHR 0xAC, CHR 0xAD, CHR 0xAE, CHR 0xAF,
haftmann@62678
   266
    CHR 0xB0, CHR 0xB1, CHR 0xB2, CHR 0xB3,
haftmann@62678
   267
    CHR 0xB4, CHR 0xB5, CHR 0xB6, CHR 0xB7,
haftmann@62678
   268
    CHR 0xB8, CHR 0xB9, CHR 0xBA, CHR 0xBB,
haftmann@62678
   269
    CHR 0xBC, CHR 0xBD, CHR 0xBE, CHR 0xBF,
haftmann@62678
   270
    CHR 0xC0, CHR 0xC1, CHR 0xC2, CHR 0xC3,
haftmann@62678
   271
    CHR 0xC4, CHR 0xC5, CHR 0xC6, CHR 0xC7,
haftmann@62678
   272
    CHR 0xC8, CHR 0xC9, CHR 0xCA, CHR 0xCB,
haftmann@62678
   273
    CHR 0xCC, CHR 0xCD, CHR 0xCE, CHR 0xCF,
haftmann@62678
   274
    CHR 0xD0, CHR 0xD1, CHR 0xD2, CHR 0xD3,
haftmann@62678
   275
    CHR 0xD4, CHR 0xD5, CHR 0xD6, CHR 0xD7,
haftmann@62678
   276
    CHR 0xD8, CHR 0xD9, CHR 0xDA, CHR 0xDB,
haftmann@62678
   277
    CHR 0xDC, CHR 0xDD, CHR 0xDE, CHR 0xDF,
haftmann@62678
   278
    CHR 0xE0, CHR 0xE1, CHR 0xE2, CHR 0xE3,
haftmann@62678
   279
    CHR 0xE4, CHR 0xE5, CHR 0xE6, CHR 0xE7,
haftmann@62678
   280
    CHR 0xE8, CHR 0xE9, CHR 0xEA, CHR 0xEB,
haftmann@62678
   281
    CHR 0xEC, CHR 0xED, CHR 0xEE, CHR 0xEF,
haftmann@62678
   282
    CHR 0xF0, CHR 0xF1, CHR 0xF2, CHR 0xF3,
haftmann@62678
   283
    CHR 0xF4, CHR 0xF5, CHR 0xF6, CHR 0xF7,
haftmann@62678
   284
    CHR 0xF8, CHR 0xF9, CHR 0xFA, CHR 0xFB,
haftmann@62678
   285
    CHR 0xFC, CHR 0xFD, CHR 0xFE, CHR 0xFF]"
haftmann@31484
   286
haftmann@49972
   287
definition
haftmann@49972
   288
  "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
haftmann@49972
   289
haftmann@49972
   290
definition
haftmann@49972
   291
  "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
haftmann@49972
   292
haftmann@62597
   293
lemma enum_char_unfold:
haftmann@62597
   294
  "Enum.enum = map char_of_nat [0..<256]"
haftmann@62597
   295
proof -
haftmann@62597
   296
  have *: "Suc (Suc 0) = 2" by simp
haftmann@62597
   297
  have "map nat_of_char Enum.enum = [0..<256]"
haftmann@62597
   298
    by (simp add: enum_char_def upt_conv_Cons_Cons *)
haftmann@62597
   299
  then have "map char_of_nat (map nat_of_char Enum.enum) =
haftmann@62597
   300
    map char_of_nat [0..<256]" by simp
haftmann@62597
   301
  then show ?thesis by (simp add: comp_def)
haftmann@62597
   302
qed
haftmann@51160
   303
haftmann@49972
   304
instance proof
haftmann@49972
   305
  show UNIV: "UNIV = set (Enum.enum :: char list)"
haftmann@62597
   306
    by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan)
haftmann@49972
   307
  show "distinct (Enum.enum :: char list)"
haftmann@62597
   308
    by (auto simp add: enum_char_unfold distinct_map intro: inj_onI)
haftmann@49972
   309
  show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
haftmann@49972
   310
    by (simp add: UNIV enum_all_char_def list_all_iff)
haftmann@49972
   311
  show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
haftmann@49972
   312
    by (simp add: UNIV enum_ex_char_def list_ex_iff)
haftmann@49972
   313
qed
haftmann@49972
   314
haftmann@49972
   315
end
haftmann@49972
   316
haftmann@62597
   317
lemma char_of_integer_code [code]:
haftmann@62597
   318
  "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
haftmann@62597
   319
  by (simp add: char_of_integer_def enum_char_unfold)
haftmann@49948
   320
haftmann@31051
   321
wenzelm@60758
   322
subsection \<open>Strings as dedicated type\<close>
bulwahn@39250
   323
wenzelm@49834
   324
typedef literal = "UNIV :: string set"
bulwahn@39250
   325
  morphisms explode STR ..
bulwahn@39250
   326
haftmann@59484
   327
setup_lifting type_definition_literal
haftmann@59484
   328
haftmann@59484
   329
lemma STR_inject' [simp]:
haftmann@59484
   330
  "STR s = STR t \<longleftrightarrow> s = t"
haftmann@59484
   331
  by transfer rule
Andreas@54594
   332
haftmann@57437
   333
definition implode :: "string \<Rightarrow> String.literal"
haftmann@57437
   334
where
haftmann@59484
   335
  [code del]: "implode = STR"
haftmann@59484
   336
  
bulwahn@39250
   337
instantiation literal :: size
bulwahn@39250
   338
begin
haftmann@31051
   339
bulwahn@39250
   340
definition size_literal :: "literal \<Rightarrow> nat"
bulwahn@39250
   341
where
wenzelm@61076
   342
  [code]: "size_literal (s::literal) = 0"
haftmann@31051
   343
bulwahn@39250
   344
instance ..
bulwahn@39250
   345
bulwahn@39250
   346
end
bulwahn@39250
   347
bulwahn@39250
   348
instantiation literal :: equal
bulwahn@39250
   349
begin
haftmann@31051
   350
Andreas@54594
   351
lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "op =" .
haftmann@31051
   352
Andreas@54594
   353
instance by intro_classes (transfer, simp)
bulwahn@39250
   354
bulwahn@39250
   355
end
haftmann@31051
   356
Andreas@54594
   357
declare equal_literal.rep_eq[code]
Andreas@54594
   358
haftmann@52365
   359
lemma [code nbe]:
haftmann@52365
   360
  fixes s :: "String.literal"
haftmann@52365
   361
  shows "HOL.equal s s \<longleftrightarrow> True"
haftmann@52365
   362
  by (simp add: equal)
haftmann@52365
   363
Andreas@55426
   364
lifting_update literal.lifting
Andreas@55426
   365
lifting_forget literal.lifting
Andreas@55426
   366
wenzelm@60758
   367
subsection \<open>Code generator\<close>
haftmann@31051
   368
wenzelm@48891
   369
ML_file "Tools/string_code.ML"
haftmann@31051
   370
haftmann@33237
   371
code_reserved SML string
haftmann@33237
   372
code_reserved OCaml string
haftmann@34886
   373
code_reserved Scala string
haftmann@33237
   374
haftmann@52435
   375
code_printing
haftmann@52435
   376
  type_constructor literal \<rightharpoonup>
haftmann@52435
   377
    (SML) "string"
haftmann@52435
   378
    and (OCaml) "string"
haftmann@52435
   379
    and (Haskell) "String"
haftmann@52435
   380
    and (Scala) "String"
haftmann@31051
   381
wenzelm@60758
   382
setup \<open>
haftmann@34886
   383
  fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
wenzelm@60758
   384
\<close>
haftmann@31051
   385
haftmann@52435
   386
code_printing
haftmann@52435
   387
  class_instance literal :: equal \<rightharpoonup>
haftmann@52435
   388
    (Haskell) -
haftmann@52435
   389
| constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
   390
    (SML) "!((_ : string) = _)"
haftmann@52435
   391
    and (OCaml) "!((_ : string) = _)"
haftmann@52435
   392
    and (Haskell) infix 4 "=="
haftmann@52435
   393
    and (Scala) infixl 5 "=="
haftmann@31051
   394
wenzelm@60758
   395
setup \<open>Sign.map_naming (Name_Space.mandatory_path "Code")\<close>
Andreas@52910
   396
Andreas@52910
   397
definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
Andreas@52910
   398
where [simp, code del]: "abort _ f = f ()"
Andreas@52910
   399
Andreas@54317
   400
lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
Andreas@54317
   401
by simp
Andreas@54317
   402
wenzelm@60758
   403
setup \<open>Sign.map_naming Name_Space.parent_path\<close>
Andreas@52910
   404
wenzelm@60758
   405
setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong})\<close>
Andreas@54317
   406
Andreas@52910
   407
code_printing constant Code.abort \<rightharpoonup>
Andreas@52910
   408
    (SML) "!(raise/ Fail/ _)"
Andreas@52910
   409
    and (OCaml) "failwith"
haftmann@59483
   410
    and (Haskell) "!(error/ ::/ forall a./ String -> (() -> a) -> a)"
Andreas@52910
   411
    and (Scala) "!{/ sys.error((_));/  ((_)).apply(())/ }"
Andreas@52910
   412
wenzelm@36176
   413
hide_type (open) literal
haftmann@31205
   414
haftmann@57437
   415
hide_const (open) implode explode
haftmann@57437
   416
bulwahn@39250
   417
end