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