src/HOL/String.thy
author haftmann
Thu Feb 10 10:32:12 2011 +0100 (2011-02-10)
changeset 41750 2b4f7a29126f
parent 39557 fe5722fce758
child 42163 392fd6c4669c
permissions -rw-r--r--
reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space
     1 (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
     2 
     3 header {* Character and string types *}
     4 
     5 theory String
     6 imports List
     7 uses
     8   ("Tools/string_syntax.ML")
     9   ("Tools/string_code.ML")
    10 begin
    11 
    12 subsection {* Characters *}
    13 
    14 datatype nibble =
    15     Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
    16   | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
    17 
    18 lemma UNIV_nibble:
    19   "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
    20     Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
    21 proof (rule UNIV_eq_I)
    22   fix x show "x \<in> ?A" by (cases x) simp_all
    23 qed
    24 
    25 instance nibble :: finite
    26   by default (simp add: UNIV_nibble)
    27 
    28 datatype char = Char nibble nibble
    29   -- "Note: canonical order of character encoding coincides with standard term ordering"
    30 
    31 lemma UNIV_char:
    32   "UNIV = image (split Char) (UNIV \<times> UNIV)"
    33 proof (rule UNIV_eq_I)
    34   fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
    35 qed
    36 
    37 instance char :: finite
    38   by default (simp add: UNIV_char)
    39 
    40 lemma size_char [code, simp]:
    41   "size (c::char) = 0" by (cases c) simp
    42 
    43 lemma char_size [code, simp]:
    44   "char_size (c::char) = 0" by (cases c) simp
    45 
    46 primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
    47   "nibble_pair_of_char (Char n m) = (n, m)"
    48 
    49 setup {*
    50 let
    51   val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
    52   val thms = map_product
    53    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
    54       nibbles nibbles;
    55 in
    56   Global_Theory.note_thmss Thm.definitionK
    57     [((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
    58   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    59 end
    60 *}
    61 
    62 lemma char_case_nibble_pair [code, code_unfold]:
    63   "char_case f = split f o nibble_pair_of_char"
    64   by (simp add: fun_eq_iff split: char.split)
    65 
    66 lemma char_rec_nibble_pair [code, code_unfold]:
    67   "char_rec f = split f o nibble_pair_of_char"
    68   unfolding char_case_nibble_pair [symmetric]
    69   by (simp add: fun_eq_iff split: char.split)
    70 
    71 syntax
    72   "_Char" :: "xstr => char"    ("CHR _")
    73 
    74 
    75 subsection {* Strings *}
    76 
    77 types string = "char list"
    78 
    79 syntax
    80   "_String" :: "xstr => string"    ("_")
    81 
    82 use "Tools/string_syntax.ML"
    83 setup String_Syntax.setup
    84 
    85 definition chars :: string where
    86   "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
    87   Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
    88   Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
    89   Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
    90   Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
    91   Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
    92   Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
    93   Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
    94   Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
    95   Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
    96   Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
    97   Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
    98   Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
    99   CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
   100   CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
   101   CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
   102   CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
   103   CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
   104   CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
   105   CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
   106   CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
   107   CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
   108   CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
   109   CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
   110   CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
   111   Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
   112   Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
   113   Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
   114   Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
   115   Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
   116   Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
   117   Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
   118   Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
   119   Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
   120   Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
   121   Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
   122   Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
   123   Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
   124   Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
   125   Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
   126   Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
   127   Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
   128   Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
   129   Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
   130   Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
   131   Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
   132   Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
   133   Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
   134   Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
   135   Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
   136   Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
   137   Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
   138   Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
   139   Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
   140   Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
   141   Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
   142   Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
   143   Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
   144   Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
   145   Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
   146   Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
   147   Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
   148   Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
   149   Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
   150   Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
   151   Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
   152   Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
   153   Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
   154 
   155 
   156 subsection {* Strings as dedicated type *}
   157 
   158 typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
   159   morphisms explode STR ..
   160 
   161 instantiation literal :: size
   162 begin
   163 
   164 definition size_literal :: "literal \<Rightarrow> nat"
   165 where
   166   [code]: "size_literal (s\<Colon>literal) = 0"
   167 
   168 instance ..
   169 
   170 end
   171 
   172 instantiation literal :: equal
   173 begin
   174 
   175 definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
   176 where
   177   "equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
   178 
   179 instance
   180 proof
   181 qed (auto simp add: equal_literal_def explode_inject)
   182 
   183 end
   184 
   185 lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
   186 by(simp add: STR_inject)
   187 
   188 
   189 subsection {* Code generator *}
   190 
   191 use "Tools/string_code.ML"
   192 
   193 code_reserved SML string
   194 code_reserved OCaml string
   195 code_reserved Scala string
   196 
   197 code_type literal
   198   (SML "string")
   199   (OCaml "string")
   200   (Haskell "String")
   201   (Scala "String")
   202 
   203 setup {*
   204   fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
   205 *}
   206 
   207 code_instance literal :: equal
   208   (Haskell -)
   209 
   210 code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   211   (SML "!((_ : string) = _)")
   212   (OCaml "!((_ : string) = _)")
   213   (Haskell infix 4 "==")
   214   (Scala infixl 5 "==")
   215 
   216 types_code
   217   "char" ("string")
   218 attach (term_of) {*
   219 val term_of_char = HOLogic.mk_char o ord;
   220 *}
   221 attach (test) {*
   222 fun gen_char i =
   223   let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
   224   in (chr j, fn () => HOLogic.mk_char j) end;
   225 *}
   226 
   227 setup {*
   228 let
   229 
   230 fun char_codegen thy defs dep thyname b t gr =
   231   let
   232     val i = HOLogic.dest_char t;
   233     val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
   234       (fastype_of t) gr;
   235   in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
   236   end handle TERM _ => NONE;
   237 
   238 in Codegen.add_codegen "char_codegen" char_codegen end
   239 *}
   240 
   241 hide_type (open) literal
   242 
   243 end