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