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