src/HOL/String.thy
author haftmann
Sat Mar 12 22:04:52 2016 +0100 (2016-03-12)
changeset 62597 b3f2b8c906a6
parent 62580 7011429f44f9
child 62678 843ff6f1de38
permissions -rw-r--r--
model characters directly as range 0..255
* * *
operate on syntax terms rather than asts
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@62597
   209
haftmann@62597
   210
syntax
haftmann@62597
   211
  "_Char_ord" :: "num_const \<Rightarrow> char"     ("CHAR _")
haftmann@31051
   212
bulwahn@42163
   213
type_synonym string = "char list"
haftmann@31051
   214
haftmann@31051
   215
syntax
wenzelm@46483
   216
  "_String" :: "str_position => string"    ("_")
haftmann@31051
   217
wenzelm@48891
   218
ML_file "Tools/string_syntax.ML"
haftmann@31051
   219
haftmann@49972
   220
instantiation char :: enum
haftmann@49972
   221
begin
haftmann@49972
   222
haftmann@49972
   223
definition
haftmann@62597
   224
  "Enum.enum = [0, CHAR 0x01, CHAR 0x02, CHAR 0x03,
haftmann@62597
   225
    CHAR 0x04, CHAR 0x05, CHAR 0x06, CHAR 0x07,
haftmann@62597
   226
    CHAR 0x08, CHAR 0x09, CHR ''\<newline>'', CHAR 0x0B,
haftmann@62597
   227
    CHAR 0x0C, CHAR 0x0D, CHAR 0x0E, CHAR 0x0F,
haftmann@62597
   228
    CHAR 0x10, CHAR 0x11, CHAR 0x12, CHAR 0x13,
haftmann@62597
   229
    CHAR 0x14, CHAR 0x15, CHAR 0x16, CHAR 0x17,
haftmann@62597
   230
    CHAR 0x18, CHAR 0x19, CHAR 0x1A, CHAR 0x1B,
haftmann@62597
   231
    CHAR 0x1C, CHAR 0x1D, CHAR 0x1E, CHAR 0x1F,
haftmann@62597
   232
    CHR '' '', CHR ''!'', CHAR 0x22, CHR ''#'',
haftmann@62597
   233
    CHR ''$'', CHR ''%'', CHR ''&'', CHAR 0x27,
haftmann@62597
   234
    CHR ''('', CHR '')'', CHR ''*'', CHR ''+'',
haftmann@62597
   235
    CHR '','', CHR ''-'', CHR ''.'', CHR ''/'',
haftmann@62597
   236
    CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
haftmann@62597
   237
    CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'',
haftmann@62597
   238
    CHR ''8'', CHR ''9'', CHR '':'', CHR '';'',
haftmann@62597
   239
    CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'',
haftmann@62597
   240
    CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'',
haftmann@62597
   241
    CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'',
haftmann@62597
   242
    CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'',
haftmann@62597
   243
    CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
haftmann@62597
   244
    CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'',
haftmann@62597
   245
    CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'',
haftmann@62597
   246
    CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['',
haftmann@62597
   247
    CHAR 0x5C, CHR '']'', CHR ''^'', CHR ''_'',
haftmann@62597
   248
    CHAR 0x60, CHR ''a'', CHR ''b'', CHR ''c'',
haftmann@62597
   249
    CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'',
haftmann@62597
   250
    CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'',
haftmann@62597
   251
    CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'',
haftmann@62597
   252
    CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'',
haftmann@62597
   253
    CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
haftmann@62597
   254
    CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'',
haftmann@62597
   255
    CHR ''|'', CHR ''}'', CHR ''~'', CHAR 0x7F,
haftmann@62597
   256
    CHAR 0x80, CHAR 0x81, CHAR 0x82, CHAR 0x83,
haftmann@62597
   257
    CHAR 0x84, CHAR 0x85, CHAR 0x86, CHAR 0x87,
haftmann@62597
   258
    CHAR 0x88, CHAR 0x89, CHAR 0x8A, CHAR 0x8B,
haftmann@62597
   259
    CHAR 0x8C, CHAR 0x8D, CHAR 0x8E, CHAR 0x8F,
haftmann@62597
   260
    CHAR 0x90, CHAR 0x91, CHAR 0x92, CHAR 0x93,
haftmann@62597
   261
    CHAR 0x94, CHAR 0x95, CHAR 0x96, CHAR 0x97,
haftmann@62597
   262
    CHAR 0x98, CHAR 0x99, CHAR 0x9A, CHAR 0x9B,
haftmann@62597
   263
    CHAR 0x9C, CHAR 0x9D, CHAR 0x9E, CHAR 0x9F,
haftmann@62597
   264
    CHAR 0xA0, CHAR 0xA1, CHAR 0xA2, CHAR 0xA3,
haftmann@62597
   265
    CHAR 0xA4, CHAR 0xA5, CHAR 0xA6, CHAR 0xA7,
haftmann@62597
   266
    CHAR 0xA8, CHAR 0xA9, CHAR 0xAA, CHAR 0xAB,
haftmann@62597
   267
    CHAR 0xAC, CHAR 0xAD, CHAR 0xAE, CHAR 0xAF,
haftmann@62597
   268
    CHAR 0xB0, CHAR 0xB1, CHAR 0xB2, CHAR 0xB3,
haftmann@62597
   269
    CHAR 0xB4, CHAR 0xB5, CHAR 0xB6, CHAR 0xB7,
haftmann@62597
   270
    CHAR 0xB8, CHAR 0xB9, CHAR 0xBA, CHAR 0xBB,
haftmann@62597
   271
    CHAR 0xBC, CHAR 0xBD, CHAR 0xBE, CHAR 0xBF,
haftmann@62597
   272
    CHAR 0xC0, CHAR 0xC1, CHAR 0xC2, CHAR 0xC3,
haftmann@62597
   273
    CHAR 0xC4, CHAR 0xC5, CHAR 0xC6, CHAR 0xC7,
haftmann@62597
   274
    CHAR 0xC8, CHAR 0xC9, CHAR 0xCA, CHAR 0xCB,
haftmann@62597
   275
    CHAR 0xCC, CHAR 0xCD, CHAR 0xCE, CHAR 0xCF,
haftmann@62597
   276
    CHAR 0xD0, CHAR 0xD1, CHAR 0xD2, CHAR 0xD3,
haftmann@62597
   277
    CHAR 0xD4, CHAR 0xD5, CHAR 0xD6, CHAR 0xD7,
haftmann@62597
   278
    CHAR 0xD8, CHAR 0xD9, CHAR 0xDA, CHAR 0xDB,
haftmann@62597
   279
    CHAR 0xDC, CHAR 0xDD, CHAR 0xDE, CHAR 0xDF,
haftmann@62597
   280
    CHAR 0xE0, CHAR 0xE1, CHAR 0xE2, CHAR 0xE3,
haftmann@62597
   281
    CHAR 0xE4, CHAR 0xE5, CHAR 0xE6, CHAR 0xE7,
haftmann@62597
   282
    CHAR 0xE8, CHAR 0xE9, CHAR 0xEA, CHAR 0xEB,
haftmann@62597
   283
    CHAR 0xEC, CHAR 0xED, CHAR 0xEE, CHAR 0xEF,
haftmann@62597
   284
    CHAR 0xF0, CHAR 0xF1, CHAR 0xF2, CHAR 0xF3,
haftmann@62597
   285
    CHAR 0xF4, CHAR 0xF5, CHAR 0xF6, CHAR 0xF7,
haftmann@62597
   286
    CHAR 0xF8, CHAR 0xF9, CHAR 0xFA, CHAR 0xFB,
haftmann@62597
   287
    CHAR 0xFC, CHAR 0xFD, CHAR 0xFE, CHAR 0xFF]"
haftmann@31484
   288
haftmann@49972
   289
definition
haftmann@49972
   290
  "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
haftmann@49972
   291
haftmann@49972
   292
definition
haftmann@49972
   293
  "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
haftmann@49972
   294
haftmann@62597
   295
lemma enum_char_unfold:
haftmann@62597
   296
  "Enum.enum = map char_of_nat [0..<256]"
haftmann@62597
   297
proof -
haftmann@62597
   298
  have *: "Suc (Suc 0) = 2" by simp
haftmann@62597
   299
  have "map nat_of_char Enum.enum = [0..<256]"
haftmann@62597
   300
    by (simp add: enum_char_def upt_conv_Cons_Cons *)
haftmann@62597
   301
  then have "map char_of_nat (map nat_of_char Enum.enum) =
haftmann@62597
   302
    map char_of_nat [0..<256]" by simp
haftmann@62597
   303
  then show ?thesis by (simp add: comp_def)
haftmann@62597
   304
qed
haftmann@51160
   305
haftmann@49972
   306
instance proof
haftmann@49972
   307
  show UNIV: "UNIV = set (Enum.enum :: char list)"
haftmann@62597
   308
    by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan)
haftmann@49972
   309
  show "distinct (Enum.enum :: char list)"
haftmann@62597
   310
    by (auto simp add: enum_char_unfold distinct_map intro: inj_onI)
haftmann@49972
   311
  show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
haftmann@49972
   312
    by (simp add: UNIV enum_all_char_def list_all_iff)
haftmann@49972
   313
  show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
haftmann@49972
   314
    by (simp add: UNIV enum_ex_char_def list_ex_iff)
haftmann@49972
   315
qed
haftmann@49972
   316
haftmann@49972
   317
end
haftmann@49972
   318
haftmann@62597
   319
lemma char_of_integer_code [code]:
haftmann@62597
   320
  "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
haftmann@62597
   321
  by (simp add: char_of_integer_def enum_char_unfold)
haftmann@49948
   322
haftmann@31051
   323
wenzelm@60758
   324
subsection \<open>Strings as dedicated type\<close>
bulwahn@39250
   325
wenzelm@49834
   326
typedef literal = "UNIV :: string set"
bulwahn@39250
   327
  morphisms explode STR ..
bulwahn@39250
   328
haftmann@59484
   329
setup_lifting type_definition_literal
haftmann@59484
   330
haftmann@59484
   331
lemma STR_inject' [simp]:
haftmann@59484
   332
  "STR s = STR t \<longleftrightarrow> s = t"
haftmann@59484
   333
  by transfer rule
Andreas@54594
   334
haftmann@57437
   335
definition implode :: "string \<Rightarrow> String.literal"
haftmann@57437
   336
where
haftmann@59484
   337
  [code del]: "implode = STR"
haftmann@59484
   338
  
bulwahn@39250
   339
instantiation literal :: size
bulwahn@39250
   340
begin
haftmann@31051
   341
bulwahn@39250
   342
definition size_literal :: "literal \<Rightarrow> nat"
bulwahn@39250
   343
where
wenzelm@61076
   344
  [code]: "size_literal (s::literal) = 0"
haftmann@31051
   345
bulwahn@39250
   346
instance ..
bulwahn@39250
   347
bulwahn@39250
   348
end
bulwahn@39250
   349
bulwahn@39250
   350
instantiation literal :: equal
bulwahn@39250
   351
begin
haftmann@31051
   352
Andreas@54594
   353
lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "op =" .
haftmann@31051
   354
Andreas@54594
   355
instance by intro_classes (transfer, simp)
bulwahn@39250
   356
bulwahn@39250
   357
end
haftmann@31051
   358
Andreas@54594
   359
declare equal_literal.rep_eq[code]
Andreas@54594
   360
haftmann@52365
   361
lemma [code nbe]:
haftmann@52365
   362
  fixes s :: "String.literal"
haftmann@52365
   363
  shows "HOL.equal s s \<longleftrightarrow> True"
haftmann@52365
   364
  by (simp add: equal)
haftmann@52365
   365
Andreas@55426
   366
lifting_update literal.lifting
Andreas@55426
   367
lifting_forget literal.lifting
Andreas@55426
   368
wenzelm@60758
   369
subsection \<open>Code generator\<close>
haftmann@31051
   370
wenzelm@48891
   371
ML_file "Tools/string_code.ML"
haftmann@31051
   372
haftmann@33237
   373
code_reserved SML string
haftmann@33237
   374
code_reserved OCaml string
haftmann@34886
   375
code_reserved Scala string
haftmann@33237
   376
haftmann@52435
   377
code_printing
haftmann@52435
   378
  type_constructor literal \<rightharpoonup>
haftmann@52435
   379
    (SML) "string"
haftmann@52435
   380
    and (OCaml) "string"
haftmann@52435
   381
    and (Haskell) "String"
haftmann@52435
   382
    and (Scala) "String"
haftmann@31051
   383
wenzelm@60758
   384
setup \<open>
haftmann@34886
   385
  fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
wenzelm@60758
   386
\<close>
haftmann@31051
   387
haftmann@52435
   388
code_printing
haftmann@52435
   389
  class_instance literal :: equal \<rightharpoonup>
haftmann@52435
   390
    (Haskell) -
haftmann@52435
   391
| constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
haftmann@52435
   392
    (SML) "!((_ : string) = _)"
haftmann@52435
   393
    and (OCaml) "!((_ : string) = _)"
haftmann@52435
   394
    and (Haskell) infix 4 "=="
haftmann@52435
   395
    and (Scala) infixl 5 "=="
haftmann@31051
   396
wenzelm@60758
   397
setup \<open>Sign.map_naming (Name_Space.mandatory_path "Code")\<close>
Andreas@52910
   398
Andreas@52910
   399
definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
Andreas@52910
   400
where [simp, code del]: "abort _ f = f ()"
Andreas@52910
   401
Andreas@54317
   402
lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
Andreas@54317
   403
by simp
Andreas@54317
   404
wenzelm@60758
   405
setup \<open>Sign.map_naming Name_Space.parent_path\<close>
Andreas@52910
   406
wenzelm@60758
   407
setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong})\<close>
Andreas@54317
   408
Andreas@52910
   409
code_printing constant Code.abort \<rightharpoonup>
Andreas@52910
   410
    (SML) "!(raise/ Fail/ _)"
Andreas@52910
   411
    and (OCaml) "failwith"
haftmann@59483
   412
    and (Haskell) "!(error/ ::/ forall a./ String -> (() -> a) -> a)"
Andreas@52910
   413
    and (Scala) "!{/ sys.error((_));/  ((_)).apply(())/ }"
Andreas@52910
   414
wenzelm@36176
   415
hide_type (open) literal
haftmann@31205
   416
haftmann@57437
   417
hide_const (open) implode explode
haftmann@57437
   418
bulwahn@39250
   419
end