src/HOL/String.thy
author haftmann
Sat Oct 20 09:12:16 2012 +0200 (2012-10-20)
changeset 49948 744934b818c7
parent 49834 b27bbb021df1
child 49972 f11f8905d9fd
permissions -rw-r--r--
moved quite generic material from theory Enum to more appropriate places
     1 (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Character and string types *}
     4 
     5 theory String
     6 imports List
     7 begin
     8 
     9 subsection {* Characters *}
    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 instance nibble :: finite
    23   by default (simp add: UNIV_nibble)
    24 
    25 datatype char = Char nibble nibble
    26   -- "Note: canonical order of character encoding coincides with standard term ordering"
    27 
    28 lemma UNIV_char:
    29   "UNIV = image (split Char) (UNIV \<times> UNIV)"
    30 proof (rule UNIV_eq_I)
    31   fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
    32 qed
    33 
    34 instance char :: finite
    35   by default (simp add: UNIV_char)
    36 
    37 lemma size_char [code, simp]:
    38   "size (c::char) = 0" by (cases c) simp
    39 
    40 lemma char_size [code, simp]:
    41   "char_size (c::char) = 0" by (cases c) simp
    42 
    43 primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
    44   "nibble_pair_of_char (Char n m) = (n, m)"
    45 
    46 setup {*
    47 let
    48   val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
    49   val thms = map_product
    50    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
    51       nibbles nibbles;
    52 in
    53   Global_Theory.note_thmss ""
    54     [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
    55   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    56 end
    57 *}
    58 
    59 lemma char_case_nibble_pair [code, code_unfold]:
    60   "char_case f = split f o nibble_pair_of_char"
    61   by (simp add: fun_eq_iff split: char.split)
    62 
    63 lemma char_rec_nibble_pair [code, code_unfold]:
    64   "char_rec f = split f o nibble_pair_of_char"
    65   unfolding char_case_nibble_pair [symmetric]
    66   by (simp add: fun_eq_iff split: char.split)
    67 
    68 syntax
    69   "_Char" :: "str_position => char"    ("CHR _")
    70 
    71 
    72 subsection {* Strings *}
    73 
    74 type_synonym string = "char list"
    75 
    76 syntax
    77   "_String" :: "str_position => string"    ("_")
    78 
    79 ML_file "Tools/string_syntax.ML"
    80 setup String_Syntax.setup
    81 
    82 definition chars :: string where
    83   "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
    84   Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
    85   Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
    86   Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
    87   Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
    88   Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
    89   Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
    90   Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
    91   Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
    92   Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
    93   Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
    94   Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
    95   Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
    96   CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
    97   CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
    98   CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
    99   CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
   100   CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
   101   CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
   102   CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
   103   CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
   104   CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
   105   CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
   106   CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
   107   CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
   108   Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
   109   Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
   110   Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
   111   Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
   112   Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
   113   Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
   114   Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
   115   Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
   116   Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
   117   Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
   118   Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
   119   Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
   120   Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
   121   Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
   122   Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
   123   Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
   124   Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
   125   Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
   126   Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
   127   Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
   128   Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
   129   Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
   130   Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
   131   Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
   132   Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
   133   Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
   134   Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
   135   Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
   136   Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
   137   Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
   138   Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
   139   Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
   140   Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
   141   Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
   142   Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
   143   Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
   144   Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
   145   Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
   146   Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
   147   Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
   148   Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
   149   Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
   150   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
   151 
   152 lemma UNIV_set_chars:
   153   "UNIV = set chars"
   154   by (simp only: UNIV_char UNIV_nibble) code_simp
   155 
   156 lemma distinct_chars:
   157   "distinct chars"
   158   by code_simp
   159 
   160 
   161 subsection {* Strings as dedicated type *}
   162 
   163 typedef literal = "UNIV :: string set"
   164   morphisms explode STR ..
   165 
   166 instantiation literal :: size
   167 begin
   168 
   169 definition size_literal :: "literal \<Rightarrow> nat"
   170 where
   171   [code]: "size_literal (s\<Colon>literal) = 0"
   172 
   173 instance ..
   174 
   175 end
   176 
   177 instantiation literal :: equal
   178 begin
   179 
   180 definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
   181 where
   182   "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
   183 
   184 instance
   185 proof
   186 qed (auto simp add: equal_literal_def explode_inject)
   187 
   188 end
   189 
   190 lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
   191 by(simp add: STR_inject)
   192 
   193 
   194 subsection {* Code generator *}
   195 
   196 ML_file "Tools/string_code.ML"
   197 
   198 code_reserved SML string
   199 code_reserved OCaml string
   200 code_reserved Scala string
   201 
   202 code_type literal
   203   (SML "string")
   204   (OCaml "string")
   205   (Haskell "String")
   206   (Scala "String")
   207 
   208 setup {*
   209   fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
   210 *}
   211 
   212 code_instance literal :: equal
   213   (Haskell -)
   214 
   215 code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   216   (SML "!((_ : string) = _)")
   217   (OCaml "!((_ : string) = _)")
   218   (Haskell infix 4 "==")
   219   (Scala infixl 5 "==")
   220 
   221 hide_type (open) literal
   222 
   223 end
   224