src/HOL/Library/Enum.thy

--- a/src/HOL/Library/Enum.thy	Mon Jun 08 08:38:49 2009 +0200
+++ b/src/HOL/Library/Enum.thy	Mon Jun 08 08:38:50 2009 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Library/Enum.thy
-    Author:     Florian Haftmann, TU Muenchen
+(* Author: Florian Haftmann, TU Muenchen
 *)
 
 header {* Finite types as explicit enumerations *}
@@ -286,76 +285,9 @@
 definition
   [code del]: "enum = map (split Char) (product enum enum)"
 
-lemma enum_char [code]:
-  "enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
-  Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
-  Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
-  Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
-  Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
-  Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
-  Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
-  Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
-  Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
-  Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
-  Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
-  Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
-  Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
-  CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
-  CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
-  CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
-  CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
-  CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
-  CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
-  CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
-  CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
-  CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
-  CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
-  CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
-  CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
-  Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
-  Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
-  Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
-  Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
-  Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
-  Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
-  Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
-  Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
-  Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
-  Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
-  Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
-  Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
-  Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
-  Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
-  Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
-  Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
-  Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
-  Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
-  Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
-  Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
-  Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
-  Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
-  Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
-  Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
-  Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
-  Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
-  Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
-  Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
-  Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
-  Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
-  Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
-  Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
-  Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
-  Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
-  Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
-  Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
-  Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
-  Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
-  Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
-  Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
-  Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
-  Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
-  Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
-  unfolding enum_char_def enum_nibble_def by simp
+lemma enum_chars [code]:
+  "enum = chars"
+  unfolding enum_char_def chars_def enum_nibble_def by simp
 
 instance proof
 qed (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]