src/HOL/String.thy
author wenzelm
Fri Mar 06 23:44:51 2015 +0100 (2015-03-06)
changeset 59631 34030d67afb9
parent 59621 291934bac95e
child 60758 d8d85a8172b5
permissions -rw-r--r--
clarified context;
     1 (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
     2 
     3 section {* 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 @{context} 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 char_of_nat_nibble_pair [simp]:
   323   "char_of_nat (nat_of_nibble a * 16 + nat_of_nibble b) = Char a b"
   324   by (simp add: nat_of_char_Char [symmetric])
   325 
   326 lemma inj_nat_of_char:
   327   "inj nat_of_char"
   328   by (rule inj_on_inverseI) (rule char_of_nat_of_char)
   329 
   330 lemma nat_of_char_eq_iff:
   331   "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
   332   by (rule inj_eq) (rule inj_nat_of_char)
   333 
   334 lemma nat_of_char_less_256:
   335   "nat_of_char c < 256"
   336 proof (cases c)
   337   case (Char x y)
   338   with nat_of_nibble_less_16 [of x] nat_of_nibble_less_16 [of y]
   339   show ?thesis by (simp add: nat_of_char_def)
   340 qed
   341 
   342 lemma char_of_nat_mod_256:
   343   "char_of_nat (n mod 256) = char_of_nat n"
   344 proof -
   345   from nibble_of_nat_mod_16 [of "n mod 256"]
   346   have "nibble_of_nat (n mod 256) = nibble_of_nat (n mod 256 mod 16)" by simp
   347   with nibble_of_nat_mod_16 [of n]
   348   have *: "nibble_of_nat (n mod 256) = nibble_of_nat n" by (simp add: mod_mod_cancel)
   349   have "n mod 256 = n mod (16 * 16)" by simp
   350   then have **: "n mod 256 = n div 16 mod 16 * 16 + n mod 16" by (simp only: mod_mult2_eq)
   351   show ?thesis
   352     by (simp add: char_of_nat_Char_nibbles *)
   353      (simp add: div_add1_eq nibble_of_nat_mod_16 [of "n div 16"] **)
   354 qed
   355 
   356 
   357 subsection {* Strings as dedicated type *}
   358 
   359 typedef literal = "UNIV :: string set"
   360   morphisms explode STR ..
   361 
   362 setup_lifting type_definition_literal
   363 
   364 lemma STR_inject' [simp]:
   365   "STR s = STR t \<longleftrightarrow> s = t"
   366   by transfer rule
   367 
   368 definition implode :: "string \<Rightarrow> String.literal"
   369 where
   370   [code del]: "implode = STR"
   371   
   372 instantiation literal :: size
   373 begin
   374 
   375 definition size_literal :: "literal \<Rightarrow> nat"
   376 where
   377   [code]: "size_literal (s\<Colon>literal) = 0"
   378 
   379 instance ..
   380 
   381 end
   382 
   383 instantiation literal :: equal
   384 begin
   385 
   386 lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "op =" .
   387 
   388 instance by intro_classes (transfer, simp)
   389 
   390 end
   391 
   392 declare equal_literal.rep_eq[code]
   393 
   394 lemma [code nbe]:
   395   fixes s :: "String.literal"
   396   shows "HOL.equal s s \<longleftrightarrow> True"
   397   by (simp add: equal)
   398 
   399 lifting_update literal.lifting
   400 lifting_forget literal.lifting
   401 
   402 subsection {* Code generator *}
   403 
   404 ML_file "Tools/string_code.ML"
   405 
   406 code_reserved SML string
   407 code_reserved OCaml string
   408 code_reserved Scala string
   409 
   410 code_printing
   411   type_constructor literal \<rightharpoonup>
   412     (SML) "string"
   413     and (OCaml) "string"
   414     and (Haskell) "String"
   415     and (Scala) "String"
   416 
   417 setup {*
   418   fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
   419 *}
   420 
   421 code_printing
   422   class_instance literal :: equal \<rightharpoonup>
   423     (Haskell) -
   424 | constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
   425     (SML) "!((_ : string) = _)"
   426     and (OCaml) "!((_ : string) = _)"
   427     and (Haskell) infix 4 "=="
   428     and (Scala) infixl 5 "=="
   429 
   430 setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *}
   431 
   432 definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
   433 where [simp, code del]: "abort _ f = f ()"
   434 
   435 lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
   436 by simp
   437 
   438 setup {* Sign.map_naming Name_Space.parent_path *}
   439 
   440 setup {* Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong}) *}
   441 
   442 code_printing constant Code.abort \<rightharpoonup>
   443     (SML) "!(raise/ Fail/ _)"
   444     and (OCaml) "failwith"
   445     and (Haskell) "!(error/ ::/ forall a./ String -> (() -> a) -> a)"
   446     and (Scala) "!{/ sys.error((_));/  ((_)).apply(())/ }"
   447 
   448 hide_type (open) literal
   449 
   450 hide_const (open) implode explode
   451 
   452 end