constant "chars" of all characters
authorhaftmann
Mon Jun 08 08:38:52 2009 +0200 (2009-06-08)
changeset 31484cabcb95fde29
parent 31483 88210717bfc8
child 31485 259a3c90016e
constant "chars" of all characters
src/HOL/String.thy
     1.1 --- a/src/HOL/String.thy	Mon Jun 08 08:38:51 2009 +0200
     1.2 +++ b/src/HOL/String.thy	Mon Jun 08 08:38:52 2009 +0200
     1.3 @@ -46,8 +46,6 @@
     1.4  primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
     1.5    "nibble_pair_of_char (Char n m) = (n, m)"
     1.6  
     1.7 -declare nibble_pair_of_char.simps [code del]
     1.8 -
     1.9  setup {*
    1.10  let
    1.11    val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
    1.12 @@ -82,6 +80,76 @@
    1.13  
    1.14  setup StringSyntax.setup
    1.15  
    1.16 +definition chars :: string where
    1.17 +  "chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
    1.18 +  Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
    1.19 +  Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
    1.20 +  Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
    1.21 +  Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
    1.22 +  Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
    1.23 +  Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
    1.24 +  Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
    1.25 +  Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
    1.26 +  Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
    1.27 +  Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
    1.28 +  Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
    1.29 +  Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
    1.30 +  CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
    1.31 +  CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
    1.32 +  CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
    1.33 +  CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
    1.34 +  CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
    1.35 +  CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
    1.36 +  CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
    1.37 +  CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
    1.38 +  CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
    1.39 +  CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
    1.40 +  CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
    1.41 +  CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
    1.42 +  Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
    1.43 +  Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
    1.44 +  Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
    1.45 +  Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
    1.46 +  Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
    1.47 +  Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
    1.48 +  Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
    1.49 +  Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
    1.50 +  Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
    1.51 +  Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
    1.52 +  Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
    1.53 +  Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
    1.54 +  Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
    1.55 +  Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
    1.56 +  Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
    1.57 +  Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
    1.58 +  Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
    1.59 +  Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
    1.60 +  Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
    1.61 +  Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
    1.62 +  Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
    1.63 +  Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
    1.64 +  Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
    1.65 +  Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
    1.66 +  Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
    1.67 +  Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
    1.68 +  Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
    1.69 +  Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
    1.70 +  Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
    1.71 +  Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
    1.72 +  Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
    1.73 +  Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
    1.74 +  Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
    1.75 +  Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
    1.76 +  Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
    1.77 +  Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
    1.78 +  Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
    1.79 +  Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
    1.80 +  Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
    1.81 +  Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
    1.82 +  Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
    1.83 +  Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
    1.84 +  Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
    1.85 +
    1.86  
    1.87  subsection {* Strings as dedicated datatype *}
    1.88