src/HOL/String.thy
author blanchet
Sun May 04 18:14:58 2014 +0200 (2014-05-04)
changeset 56846 9df717fef2bb
parent 55969 8820ddb8f9f4
child 57247 8191ccf6a1bd
permissions -rw-r--r--
renamed 'xxx_size' to 'size_xxx' for old datatype package
     1 (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Character and string types *}
     4 
     5 theory String
     6 imports Enum
     7 begin
     8 
     9 subsection {* Characters and strings *}
    10 
    11 datatype nibble =
    12     Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    13   | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    14 
    15 lemma UNIV_nibble:
    16   "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
    17     Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
    18 proof (rule UNIV_eq_I)
    19   fix x show "x \<in> ?A" by (cases x) simp_all
    20 qed
    21 
    22 lemma size_nibble [code, simp]:
    23   "size_nibble (x::nibble) = 0"
    24   "size (x::nibble) = 0"
    25   by (cases x, simp_all)+
    26 
    27 instantiation nibble :: enum
    28 begin
    29 
    30 definition
    31   "Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
    32     Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
    33 
    34 definition
    35   "Enum.enum_all P \<longleftrightarrow> P Nibble0 \<and> P Nibble1 \<and> P Nibble2 \<and> P Nibble3 \<and> P Nibble4 \<and> P Nibble5 \<and> P Nibble6 \<and> P Nibble7
    36      \<and> P Nibble8 \<and> P Nibble9 \<and> P NibbleA \<and> P NibbleB \<and> P NibbleC \<and> P NibbleD \<and> P NibbleE \<and> P NibbleF"
    37 
    38 definition
    39   "Enum.enum_ex P \<longleftrightarrow> P Nibble0 \<or> P Nibble1 \<or> P Nibble2 \<or> P Nibble3 \<or> P Nibble4 \<or> P Nibble5 \<or> P Nibble6 \<or> P Nibble7
    40      \<or> P Nibble8 \<or> P Nibble9 \<or> P NibbleA \<or> P NibbleB \<or> P NibbleC \<or> P NibbleD \<or> P NibbleE \<or> P NibbleF"
    41 
    42 instance proof
    43 qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all)
    44 
    45 end
    46 
    47 lemma card_UNIV_nibble:
    48   "card (UNIV :: nibble set) = 16"
    49   by (simp add: card_UNIV_length_enum enum_nibble_def)
    50 
    51 primrec nat_of_nibble :: "nibble \<Rightarrow> nat"
    52 where
    53   "nat_of_nibble Nibble0 = 0"
    54 | "nat_of_nibble Nibble1 = 1"
    55 | "nat_of_nibble Nibble2 = 2"
    56 | "nat_of_nibble Nibble3 = 3"
    57 | "nat_of_nibble Nibble4 = 4"
    58 | "nat_of_nibble Nibble5 = 5"
    59 | "nat_of_nibble Nibble6 = 6"
    60 | "nat_of_nibble Nibble7 = 7"
    61 | "nat_of_nibble Nibble8 = 8"
    62 | "nat_of_nibble Nibble9 = 9"
    63 | "nat_of_nibble NibbleA = 10"
    64 | "nat_of_nibble NibbleB = 11"
    65 | "nat_of_nibble NibbleC = 12"
    66 | "nat_of_nibble NibbleD = 13"
    67 | "nat_of_nibble NibbleE = 14"
    68 | "nat_of_nibble NibbleF = 15"
    69 
    70 definition nibble_of_nat :: "nat \<Rightarrow> nibble" where
    71   "nibble_of_nat n = Enum.enum ! (n mod 16)"
    72 
    73 lemma nibble_of_nat_simps [simp]:
    74   "nibble_of_nat  0 = Nibble0"
    75   "nibble_of_nat  1 = Nibble1"
    76   "nibble_of_nat  2 = Nibble2"
    77   "nibble_of_nat  3 = Nibble3"
    78   "nibble_of_nat  4 = Nibble4"
    79   "nibble_of_nat  5 = Nibble5"
    80   "nibble_of_nat  6 = Nibble6"
    81   "nibble_of_nat  7 = Nibble7"
    82   "nibble_of_nat  8 = Nibble8"
    83   "nibble_of_nat  9 = Nibble9"
    84   "nibble_of_nat 10 = NibbleA"
    85   "nibble_of_nat 11 = NibbleB"
    86   "nibble_of_nat 12 = NibbleC"
    87   "nibble_of_nat 13 = NibbleD"
    88   "nibble_of_nat 14 = NibbleE"
    89   "nibble_of_nat 15 = NibbleF"
    90   unfolding nibble_of_nat_def by (simp_all add: enum_nibble_def)
    91 
    92 lemma nibble_of_nat_of_nibble [simp]:
    93   "nibble_of_nat (nat_of_nibble x) = x"
    94   by (cases x) (simp_all add: nibble_of_nat_def enum_nibble_def)
    95 
    96 lemma nat_of_nibble_of_nat [simp]:
    97   "nat_of_nibble (nibble_of_nat n) = n mod 16"
    98   by (cases "nibble_of_nat n")
    99      (simp_all add: nibble_of_nat_def enum_nibble_def nth_equal_first_eq nth_non_equal_first_eq, arith)
   100 
   101 lemma inj_nat_of_nibble:
   102   "inj nat_of_nibble"
   103   by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
   104 
   105 lemma nat_of_nibble_eq_iff:
   106   "nat_of_nibble x = nat_of_nibble y \<longleftrightarrow> x = y"
   107   by (rule inj_eq) (rule inj_nat_of_nibble)
   108 
   109 lemma nat_of_nibble_less_16:
   110   "nat_of_nibble x < 16"
   111   by (cases x) auto
   112 
   113 lemma nibble_of_nat_mod_16:
   114   "nibble_of_nat (n mod 16) = nibble_of_nat n"
   115   by (simp add: nibble_of_nat_def)
   116 
   117 datatype char = Char nibble nibble
   118   -- "Note: canonical order of character encoding coincides with standard term ordering"
   119 
   120 syntax
   121   "_Char" :: "str_position => char"    ("CHR _")
   122 
   123 type_synonym string = "char list"
   124 
   125 syntax
   126   "_String" :: "str_position => string"    ("_")
   127 
   128 ML_file "Tools/string_syntax.ML"
   129 setup String_Syntax.setup
   130 
   131 lemma UNIV_char:
   132   "UNIV = image (split Char) (UNIV \<times> UNIV)"
   133 proof (rule UNIV_eq_I)
   134   fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
   135 qed
   136 
   137 lemma size_char [code, simp]:
   138   "size_char (c::char) = 0"
   139   "size (c::char) = 0"
   140   by (cases c, simp)+
   141 
   142 instantiation char :: enum
   143 begin
   144 
   145 definition
   146   "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
   147   Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
   148   Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
   149   Char Nibble0 Nibble9, CHR ''\<newline>'', Char Nibble0 NibbleB,
   150   Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
   151   Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
   152   Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
   153   Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
   154   Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
   155   Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
   156   Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
   157   Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
   158   Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
   159   CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
   160   CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
   161   CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
   162   CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
   163   CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
   164   CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
   165   CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
   166   CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
   167   CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
   168   CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
   169   CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
   170   CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
   171   Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
   172   Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
   173   Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
   174   Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
   175   Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
   176   Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
   177   Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
   178   Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
   179   Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
   180   Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
   181   Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
   182   Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
   183   Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
   184   Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
   185   Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
   186   Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
   187   Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
   188   Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
   189   Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
   190   Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
   191   Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
   192   Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
   193   Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
   194   Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
   195   Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
   196   Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
   197   Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
   198   Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
   199   Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
   200   Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
   201   Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
   202   Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
   203   Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
   204   Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
   205   Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
   206   Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
   207   Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
   208   Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
   209   Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
   210   Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
   211   Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
   212   Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
   213   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
   214 
   215 definition
   216   "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
   217 
   218 definition
   219   "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
   220 
   221 lemma enum_char_product_enum_nibble:
   222   "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
   223   by (simp add: enum_char_def enum_nibble_def)
   224 
   225 instance proof
   226   show UNIV: "UNIV = set (Enum.enum :: char list)"
   227     by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV)
   228   show "distinct (Enum.enum :: char list)"
   229     by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
   230   show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
   231     by (simp add: UNIV enum_all_char_def list_all_iff)
   232   show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
   233     by (simp add: UNIV enum_ex_char_def list_ex_iff)
   234 qed
   235 
   236 end
   237 
   238 lemma card_UNIV_char:
   239   "card (UNIV :: char set) = 256"
   240   by (simp add: card_UNIV_length_enum enum_char_def)
   241 
   242 definition nat_of_char :: "char \<Rightarrow> nat"
   243 where
   244   "nat_of_char c = (case c of Char x y \<Rightarrow> nat_of_nibble x * 16 + nat_of_nibble y)"
   245 
   246 lemma nat_of_char_Char:
   247   "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y"
   248   by (simp add: nat_of_char_def)
   249 
   250 setup {*
   251 let
   252   val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
   253   val simpset =
   254     put_simpset HOL_ss @{context}
   255       addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
   256   fun mk_code_eqn x y =
   257     Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
   258     |> simplify simpset;
   259   val code_eqns = map_product mk_code_eqn nibbles nibbles;
   260 in
   261   Global_Theory.note_thmss ""
   262     [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
   263   #> snd
   264 end
   265 *}
   266 
   267 declare nat_of_char_simps [code]
   268 
   269 lemma nibble_of_nat_of_char_div_16:
   270   "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
   271   by (cases c)
   272     (simp add: nat_of_char_def add_commute nat_of_nibble_less_16)
   273 
   274 lemma nibble_of_nat_nat_of_char:
   275   "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
   276 proof (cases c)
   277   case (Char x y)
   278   then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
   279     by (simp add: nibble_of_nat_mod_16)
   280   then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
   281     by (simp only: nibble_of_nat_mod_16)
   282   with Char show ?thesis by (simp add: nat_of_char_def add_commute)
   283 qed
   284 
   285 code_datatype Char -- {* drop case certificate for char *}
   286 
   287 lemma case_char_code [code]:
   288   "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
   289   by (cases c)
   290     (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
   291 
   292 lemma [code]:
   293   "rec_char = case_char"
   294   by (simp add: fun_eq_iff split: char.split)
   295 
   296 definition char_of_nat :: "nat \<Rightarrow> char" where
   297   "char_of_nat n = Enum.enum ! (n mod 256)"
   298 
   299 lemma char_of_nat_Char_nibbles:
   300   "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
   301 proof -
   302   from mod_mult2_eq [of n 16 16]
   303   have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
   304   then show ?thesis
   305     by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble
   306       card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add_commute)
   307 qed
   308 
   309 lemma char_of_nat_of_char [simp]:
   310   "char_of_nat (nat_of_char c) = c"
   311   by (cases c)
   312     (simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char)
   313 
   314 lemma nat_of_char_of_nat [simp]:
   315   "nat_of_char (char_of_nat n) = n mod 256"
   316 proof -
   317   have "n mod 256 = n mod (16 * 16)" by simp
   318   then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq)
   319   then show ?thesis
   320     by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
   321 qed
   322 
   323 lemma inj_nat_of_char:
   324   "inj nat_of_char"
   325   by (rule inj_on_inverseI) (rule char_of_nat_of_char)
   326 
   327 lemma nat_of_char_eq_iff:
   328   "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
   329   by (rule inj_eq) (rule inj_nat_of_char)
   330 
   331 lemma nat_of_char_less_256:
   332   "nat_of_char c < 256"
   333 proof (cases c)
   334   case (Char x y)
   335   with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
   336   show ?thesis by (simp add: nat_of_char_def)
   337 qed
   338 
   339 lemma char_of_nat_mod_256:
   340   "char_of_nat (n mod 256) = char_of_nat n"
   341 proof -
   342   from nibble_of_nat_mod_16 [of "n mod 256"]
   343   have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp
   344   with nibble_of_nat_mod_16 [of n]
   345   have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel)
   346   have "n mod 256 = n mod (16 * 16)" by simp
   347   then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq)
   348   show ?thesis
   349     by (simp add: char_of_nat_Char_nibbles *)
   350      (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **)
   351 qed
   352 
   353 
   354 subsection {* Strings as dedicated type *}
   355 
   356 typedef literal = "UNIV :: string set"
   357   morphisms explode STR ..
   358 
   359 setup_lifting (no_code) type_definition_literal
   360 
   361 instantiation literal :: size
   362 begin
   363 
   364 definition size_literal :: "literal \<Rightarrow> nat"
   365 where
   366   [code]: "size_literal (s\<Colon>literal) = 0"
   367 
   368 instance ..
   369 
   370 end
   371 
   372 instantiation literal :: equal
   373 begin
   374 
   375 lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "op =" .
   376 
   377 instance by intro_classes (transfer, simp)
   378 
   379 end
   380 
   381 declare equal_literal.rep_eq[code]
   382 
   383 lemma [code nbe]:
   384   fixes s :: "String.literal"
   385   shows "HOL.equal s s \<longleftrightarrow> True"
   386   by (simp add: equal)
   387 
   388 lemma STR_inject' [simp]:
   389   "STR xs = STR ys \<longleftrightarrow> xs = ys"
   390   by (simp add: STR_inject)
   391 
   392 lifting_update literal.lifting
   393 lifting_forget literal.lifting
   394 
   395 subsection {* Code generator *}
   396 
   397 ML_file "Tools/string_code.ML"
   398 
   399 code_reserved SML string
   400 code_reserved OCaml string
   401 code_reserved Scala string
   402 
   403 code_printing
   404   type_constructor literal \<rightharpoonup>
   405     (SML) "string"
   406     and (OCaml) "string"
   407     and (Haskell) "String"
   408     and (Scala) "String"
   409 
   410 setup {*
   411   fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
   412 *}
   413 
   414 code_printing
   415   class_instance literal :: equal \<rightharpoonup>
   416     (Haskell) -
   417 | constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
   418     (SML) "!((_ : string) = _)"
   419     and (OCaml) "!((_ : string) = _)"
   420     and (Haskell) infix 4 "=="
   421     and (Scala) infixl 5 "=="
   422 
   423 setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *}
   424 
   425 definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
   426 where [simp, code del]: "abort _ f = f ()"
   427 
   428 lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
   429 by simp
   430 
   431 setup {* Sign.map_naming Name_Space.parent_path *}
   432 
   433 setup {* Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong}) *}
   434 
   435 code_printing constant Code.abort \<rightharpoonup>
   436     (SML) "!(raise/ Fail/ _)"
   437     and (OCaml) "failwith"
   438     and (Haskell) "error"
   439     and (Scala) "!{/ sys.error((_));/  ((_)).apply(())/ }"
   440 
   441 hide_type (open) literal
   442 
   443 end