src/HOL/String.thy
author wenzelm
Wed Oct 29 15:07:53 2014 +0100 (2014-10-29)
changeset 58822 90a5e981af3e
parent 58310 91ea607a34d8
child 58889 5b7a9633cfa8
permissions -rw-r--r--
modernized setup;
     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 
   130 lemma UNIV_char:
   131   "UNIV = image (split Char) (UNIV \<times> UNIV)"
   132 proof (rule UNIV_eq_I)
   133   fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
   134 qed
   135 
   136 lemma size_char [code, simp]:
   137   "size_char (c::char) = 0"
   138   "size (c::char) = 0"
   139   by (cases c, simp)+
   140 
   141 instantiation char :: enum
   142 begin
   143 
   144 definition
   145   "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
   146   Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
   147   Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
   148   Char Nibble0 Nibble9, CHR ''\<newline>'', Char Nibble0 NibbleB,
   149   Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
   150   Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
   151   Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
   152   Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
   153   Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
   154   Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
   155   Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
   156   Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
   157   Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
   158   CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
   159   CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
   160   CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
   161   CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
   162   CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
   163   CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
   164   CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
   165   CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
   166   CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
   167   CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
   168   CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
   169   CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
   170   Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
   171   Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
   172   Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
   173   Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
   174   Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
   175   Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
   176   Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
   177   Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
   178   Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
   179   Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
   180   Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
   181   Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
   182   Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
   183   Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
   184   Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
   185   Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
   186   Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
   187   Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
   188   Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
   189   Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
   190   Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
   191   Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
   192   Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
   193   Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
   194   Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
   195   Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
   196   Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
   197   Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
   198   Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
   199   Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
   200   Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
   201   Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
   202   Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
   203   Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
   204   Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
   205   Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
   206   Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
   207   Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
   208   Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
   209   Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
   210   Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
   211   Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
   212   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
   213 
   214 definition
   215   "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
   216 
   217 definition
   218   "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
   219 
   220 lemma enum_char_product_enum_nibble:
   221   "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
   222   by (simp add: enum_char_def enum_nibble_def)
   223 
   224 instance proof
   225   show UNIV: "UNIV = set (Enum.enum :: char list)"
   226     by (simp add: enum_char_product_enum_nibble UNIV_char enum_UNIV)
   227   show "distinct (Enum.enum :: char list)"
   228     by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
   229   show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
   230     by (simp add: UNIV enum_all_char_def list_all_iff)
   231   show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
   232     by (simp add: UNIV enum_ex_char_def list_ex_iff)
   233 qed
   234 
   235 end
   236 
   237 lemma card_UNIV_char:
   238   "card (UNIV :: char set) = 256"
   239   by (simp add: card_UNIV_length_enum enum_char_def)
   240 
   241 definition nat_of_char :: "char \<Rightarrow> nat"
   242 where
   243   "nat_of_char c = (case c of Char x y \<Rightarrow> nat_of_nibble x * 16 + nat_of_nibble y)"
   244 
   245 lemma nat_of_char_Char:
   246   "nat_of_char (Char x y) = nat_of_nibble x * 16 + nat_of_nibble y"
   247   by (simp add: nat_of_char_def)
   248 
   249 setup {*
   250 let
   251   val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
   252   val simpset =
   253     put_simpset HOL_ss @{context}
   254       addsimps @{thms nat_of_nibble.simps mult_0 mult_1 add_0 add_0_right arith_simps numeral_plus_one};
   255   fun mk_code_eqn x y =
   256     Drule.instantiate' [] [SOME x, SOME y] @{thm nat_of_char_Char}
   257     |> simplify simpset;
   258   val code_eqns = map_product mk_code_eqn nibbles nibbles;
   259 in
   260   Global_Theory.note_thmss ""
   261     [((@{binding nat_of_char_simps}, []), [(code_eqns, [])])]
   262   #> snd
   263 end
   264 *}
   265 
   266 declare nat_of_char_simps [code]
   267 
   268 lemma nibble_of_nat_of_char_div_16:
   269   "nibble_of_nat (nat_of_char c div 16) = (case c of Char x y \<Rightarrow> x)"
   270   by (cases c)
   271     (simp add: nat_of_char_def add.commute nat_of_nibble_less_16)
   272 
   273 lemma nibble_of_nat_nat_of_char:
   274   "nibble_of_nat (nat_of_char c) = (case c of Char x y \<Rightarrow> y)"
   275 proof (cases c)
   276   case (Char x y)
   277   then have *: "nibble_of_nat ((nat_of_nibble y + nat_of_nibble x * 16) mod 16) = y"
   278     by (simp add: nibble_of_nat_mod_16)
   279   then have "nibble_of_nat (nat_of_nibble y + nat_of_nibble x * 16) = y"
   280     by (simp only: nibble_of_nat_mod_16)
   281   with Char show ?thesis by (simp add: nat_of_char_def add.commute)
   282 qed
   283 
   284 code_datatype Char -- {* drop case certificate for char *}
   285 
   286 lemma case_char_code [code]:
   287   "case_char f c = (let n = nat_of_char c in f (nibble_of_nat (n div 16)) (nibble_of_nat n))"
   288   by (cases c)
   289     (simp only: Let_def nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char char.case)
   290 
   291 lemma [code]:
   292   "rec_char = case_char"
   293   by (simp add: fun_eq_iff split: char.split)
   294 
   295 definition char_of_nat :: "nat \<Rightarrow> char" where
   296   "char_of_nat n = Enum.enum ! (n mod 256)"
   297 
   298 lemma char_of_nat_Char_nibbles:
   299   "char_of_nat n = Char (nibble_of_nat (n div 16)) (nibble_of_nat n)"
   300 proof -
   301   from mod_mult2_eq [of n 16 16]
   302   have "n mod 256 = 16 * (n div 16 mod 16) + n mod 16" by simp
   303   then show ?thesis
   304     by (simp add: char_of_nat_def enum_char_product_enum_nibble card_UNIV_nibble
   305       card_UNIV_length_enum [symmetric] nibble_of_nat_def product_nth add.commute)
   306 qed
   307 
   308 lemma char_of_nat_of_char [simp]:
   309   "char_of_nat (nat_of_char c) = c"
   310   by (cases c)
   311     (simp add: char_of_nat_Char_nibbles nibble_of_nat_of_char_div_16 nibble_of_nat_nat_of_char)
   312 
   313 lemma nat_of_char_of_nat [simp]:
   314   "nat_of_char (char_of_nat n) = n mod 256"
   315 proof -
   316   have "n mod 256 = n mod (16 * 16)" by simp
   317   then have "n div 16 mod 16 * 16 + n mod 16 = n mod 256" by (simp only: mod_mult2_eq)
   318   then show ?thesis
   319     by (cases "char_of_nat n") (auto simp add: nat_of_char_def char_of_nat_Char_nibbles)
   320 qed
   321 
   322 lemma inj_nat_of_char:
   323   "inj nat_of_char"
   324   by (rule inj_on_inverseI) (rule char_of_nat_of_char)
   325 
   326 lemma nat_of_char_eq_iff:
   327   "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
   328   by (rule inj_eq) (rule inj_nat_of_char)
   329 
   330 lemma nat_of_char_less_256:
   331   "nat_of_char c < 256"
   332 proof (cases c)
   333   case (Char x y)
   334   with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
   335   show ?thesis by (simp add: nat_of_char_def)
   336 qed
   337 
   338 lemma char_of_nat_mod_256:
   339   "char_of_nat (n mod 256) = char_of_nat n"
   340 proof -
   341   from nibble_of_nat_mod_16 [of "n mod 256"]
   342   have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp
   343   with nibble_of_nat_mod_16 [of n]
   344   have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel)
   345   have "n mod 256 = n mod (16 * 16)" by simp
   346   then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq)
   347   show ?thesis
   348     by (simp add: char_of_nat_Char_nibbles *)
   349      (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **)
   350 qed
   351 
   352 
   353 subsection {* Strings as dedicated type *}
   354 
   355 typedef literal = "UNIV :: string set"
   356   morphisms explode STR ..
   357 
   358 setup_lifting (no_code) type_definition_literal
   359 
   360 definition implode :: "string \<Rightarrow> String.literal"
   361 where
   362   "implode = STR"
   363 
   364 instantiation literal :: size
   365 begin
   366 
   367 definition size_literal :: "literal \<Rightarrow> nat"
   368 where
   369   [code]: "size_literal (s\<Colon>literal) = 0"
   370 
   371 instance ..
   372 
   373 end
   374 
   375 instantiation literal :: equal
   376 begin
   377 
   378 lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "op =" .
   379 
   380 instance by intro_classes (transfer, simp)
   381 
   382 end
   383 
   384 declare equal_literal.rep_eq[code]
   385 
   386 lemma [code nbe]:
   387   fixes s :: "String.literal"
   388   shows "HOL.equal s s \<longleftrightarrow> True"
   389   by (simp add: equal)
   390 
   391 lemma STR_inject' [simp]:
   392   "STR xs = STR ys \<longleftrightarrow> xs = ys"
   393   by (simp add: STR_inject)
   394 
   395 lifting_update literal.lifting
   396 lifting_forget literal.lifting
   397 
   398 subsection {* Code generator *}
   399 
   400 ML_file "Tools/string_code.ML"
   401 
   402 code_reserved SML string
   403 code_reserved OCaml string
   404 code_reserved Scala string
   405 
   406 code_printing
   407   type_constructor literal \<rightharpoonup>
   408     (SML) "string"
   409     and (OCaml) "string"
   410     and (Haskell) "String"
   411     and (Scala) "String"
   412 
   413 setup {*
   414   fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
   415 *}
   416 
   417 code_printing
   418   class_instance literal :: equal \<rightharpoonup>
   419     (Haskell) -
   420 | constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
   421     (SML) "!((_ : string) = _)"
   422     and (OCaml) "!((_ : string) = _)"
   423     and (Haskell) infix 4 "=="
   424     and (Scala) infixl 5 "=="
   425 
   426 setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *}
   427 
   428 definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
   429 where [simp, code del]: "abort _ f = f ()"
   430 
   431 lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
   432 by simp
   433 
   434 setup {* Sign.map_naming Name_Space.parent_path *}
   435 
   436 setup {* Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong}) *}
   437 
   438 code_printing constant Code.abort \<rightharpoonup>
   439     (SML) "!(raise/ Fail/ _)"
   440     and (OCaml) "failwith"
   441     and (Haskell) "error"
   442     and (Scala) "!{/ sys.error((_));/  ((_)).apply(())/ }"
   443 
   444 hide_type (open) literal
   445 
   446 hide_const (open) implode explode
   447 
   448 end