src/HOL/String.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 49972 f11f8905d9fd
child 51160 599ff65b85e2
permissions -rw-r--r--
introduce order topology
     1 (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Character and string types *}
     4 
     5 theory String
     6 imports List 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 datatype char = Char nibble nibble
    53   -- "Note: canonical order of character encoding coincides with standard term ordering"
    54 
    55 syntax
    56   "_Char" :: "str_position => char"    ("CHR _")
    57 
    58 type_synonym string = "char list"
    59 
    60 syntax
    61   "_String" :: "str_position => string"    ("_")
    62 
    63 ML_file "Tools/string_syntax.ML"
    64 setup String_Syntax.setup
    65 
    66 lemma UNIV_char:
    67   "UNIV = image (split Char) (UNIV \<times> UNIV)"
    68 proof (rule UNIV_eq_I)
    69   fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
    70 qed
    71 
    72 lemma size_char [code, simp]:
    73   "size (c::char) = 0" by (cases c) simp
    74 
    75 lemma char_size [code, simp]:
    76   "char_size (c::char) = 0" by (cases c) simp
    77 
    78 instantiation char :: enum
    79 begin
    80 
    81 definition
    82   "Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
    83   Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
    84   Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
    85   Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
    86   Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
    87   Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
    88   Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
    89   Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
    90   Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
    91   Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
    92   Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
    93   Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
    94   Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
    95   CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
    96   CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
    97   CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
    98   CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
    99   CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
   100   CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
   101   CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
   102   CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
   103   CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
   104   CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
   105   CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
   106   CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
   107   Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
   108   Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
   109   Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
   110   Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
   111   Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
   112   Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
   113   Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
   114   Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
   115   Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
   116   Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
   117   Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
   118   Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
   119   Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
   120   Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
   121   Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
   122   Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
   123   Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
   124   Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
   125   Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
   126   Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
   127   Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
   128   Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
   129   Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
   130   Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
   131   Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
   132   Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
   133   Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
   134   Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
   135   Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
   136   Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
   137   Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
   138   Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
   139   Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
   140   Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
   141   Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
   142   Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
   143   Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
   144   Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
   145   Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
   146   Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
   147   Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
   148   Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
   149   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
   150 
   151 definition
   152   "Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)"
   153 
   154 definition
   155   "Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
   156 
   157 instance proof
   158   have enum: "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)"
   159     by (simp add: enum_char_def enum_nibble_def)
   160   show UNIV: "UNIV = set (Enum.enum :: char list)"
   161     by (simp add: enum UNIV_char product_list_set enum_UNIV)
   162   show "distinct (Enum.enum :: char list)"
   163     by (auto intro: inj_onI simp add: enum distinct_map distinct_product enum_distinct)
   164   show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"
   165     by (simp add: UNIV enum_all_char_def list_all_iff)
   166   show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P"
   167     by (simp add: UNIV enum_ex_char_def list_ex_iff)
   168 qed
   169 
   170 end
   171 
   172 lemma card_UNIV_char:
   173   "card (UNIV :: char set) = 256"
   174   by (simp add: card_UNIV_length_enum enum_char_def)
   175 
   176 primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
   177   "nibble_pair_of_char (Char n m) = (n, m)"
   178 
   179 setup {*
   180 let
   181   val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
   182   val thms = map_product
   183    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
   184       nibbles nibbles;
   185 in
   186   Global_Theory.note_thmss ""
   187     [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
   188   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
   189 end
   190 *}
   191 
   192 lemma char_case_nibble_pair [code, code_unfold]:
   193   "char_case f = split f o nibble_pair_of_char"
   194   by (simp add: fun_eq_iff split: char.split)
   195 
   196 lemma char_rec_nibble_pair [code, code_unfold]:
   197   "char_rec f = split f o nibble_pair_of_char"
   198   unfolding char_case_nibble_pair [symmetric]
   199   by (simp add: fun_eq_iff split: char.split)
   200 
   201 
   202 subsection {* Strings as dedicated type *}
   203 
   204 typedef literal = "UNIV :: string set"
   205   morphisms explode STR ..
   206 
   207 instantiation literal :: size
   208 begin
   209 
   210 definition size_literal :: "literal \<Rightarrow> nat"
   211 where
   212   [code]: "size_literal (s\<Colon>literal) = 0"
   213 
   214 instance ..
   215 
   216 end
   217 
   218 instantiation literal :: equal
   219 begin
   220 
   221 definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
   222 where
   223   "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
   224 
   225 instance
   226 proof
   227 qed (auto simp add: equal_literal_def explode_inject)
   228 
   229 end
   230 
   231 lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
   232 by(simp add: STR_inject)
   233 
   234 
   235 subsection {* Code generator *}
   236 
   237 ML_file "Tools/string_code.ML"
   238 
   239 code_reserved SML string
   240 code_reserved OCaml string
   241 code_reserved Scala string
   242 
   243 code_type literal
   244   (SML "string")
   245   (OCaml "string")
   246   (Haskell "String")
   247   (Scala "String")
   248 
   249 setup {*
   250   fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
   251 *}
   252 
   253 code_instance literal :: equal
   254   (Haskell -)
   255 
   256 code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   257   (SML "!((_ : string) = _)")
   258   (OCaml "!((_ : string) = _)")
   259   (Haskell infix 4 "==")
   260   (Scala infixl 5 "==")
   261 
   262 hide_type (open) literal
   263 
   264 end
   265