author | hoelzl |
Mon, 03 Dec 2012 18:19:08 +0100 | |
changeset 50328 | 25b1e8686ce0 |
parent 49972 | f11f8905d9fd |
child 51160 | 599ff65b85e2 |
permissions | -rw-r--r-- |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
1 |
(* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
2 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
3 |
header {* Character and string types *} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
4 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
5 |
theory String |
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
6 |
imports List Enum |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
7 |
begin |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
8 |
|
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
9 |
subsection {* Characters and strings *} |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
10 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
11 |
datatype nibble = |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
12 |
Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7 |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
13 |
| Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
14 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
15 |
lemma UNIV_nibble: |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
16 |
"UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7, |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
17 |
Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
18 |
proof (rule UNIV_eq_I) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
19 |
fix x show "x \<in> ?A" by (cases x) simp_all |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
20 |
qed |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
21 |
|
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
22 |
lemma size_nibble [code, simp]: |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
23 |
"size (x::nibble) = 0" by (cases x) simp_all |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
24 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
25 |
lemma nibble_size [code, simp]: |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
26 |
"nibble_size (x::nibble) = 0" by (cases x) simp_all |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
27 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
28 |
instantiation nibble :: enum |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
29 |
begin |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
30 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
31 |
definition |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
32 |
"Enum.enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7, |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
33 |
Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
34 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
35 |
definition |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
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 |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
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" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
38 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
39 |
definition |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
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 |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
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" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
42 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
43 |
instance proof |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
44 |
qed (simp_all only: enum_nibble_def enum_all_nibble_def enum_ex_nibble_def UNIV_nibble, simp_all) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
45 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
46 |
end |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
47 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
48 |
lemma card_UNIV_nibble: |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
49 |
"card (UNIV :: nibble set) = 16" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
50 |
by (simp add: card_UNIV_length_enum enum_nibble_def) |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
51 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
52 |
datatype char = Char nibble nibble |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
53 |
-- "Note: canonical order of character encoding coincides with standard term ordering" |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
54 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
55 |
syntax |
46483 | 56 |
"_Char" :: "str_position => char" ("CHR _") |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
57 |
|
42163
392fd6c4669c
renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents:
41750
diff
changeset
|
58 |
type_synonym string = "char list" |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
59 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
60 |
syntax |
46483 | 61 |
"_String" :: "str_position => string" ("_") |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
62 |
|
48891 | 63 |
ML_file "Tools/string_syntax.ML" |
35123 | 64 |
setup String_Syntax.setup |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
65 |
|
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
66 |
lemma UNIV_char: |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
67 |
"UNIV = image (split Char) (UNIV \<times> UNIV)" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
68 |
proof (rule UNIV_eq_I) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
69 |
fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
70 |
qed |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
71 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
72 |
lemma size_char [code, simp]: |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
73 |
"size (c::char) = 0" by (cases c) simp |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
74 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
75 |
lemma char_size [code, simp]: |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
76 |
"char_size (c::char) = 0" by (cases c) simp |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
77 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
78 |
instantiation char :: enum |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
79 |
begin |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
80 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
81 |
definition |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
82 |
"Enum.enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2, |
31484 | 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 |
||
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
151 |
definition |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
152 |
"Enum.enum_all P \<longleftrightarrow> list_all P (Enum.enum :: char list)" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
153 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
154 |
definition |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
155 |
"Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
156 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
157 |
instance proof |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
158 |
have enum: "(Enum.enum :: char list) = map (split Char) (List.product Enum.enum Enum.enum)" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
159 |
by (simp add: enum_char_def enum_nibble_def) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
160 |
show UNIV: "UNIV = set (Enum.enum :: char list)" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
161 |
by (simp add: enum UNIV_char product_list_set enum_UNIV) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
162 |
show "distinct (Enum.enum :: char list)" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
163 |
by (auto intro: inj_onI simp add: enum distinct_map distinct_product enum_distinct) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
164 |
show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
165 |
by (simp add: UNIV enum_all_char_def list_all_iff) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
166 |
show "\<And>P. Enum.enum_ex P \<longleftrightarrow> Bex (UNIV :: char set) P" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
167 |
by (simp add: UNIV enum_ex_char_def list_ex_iff) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
168 |
qed |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
169 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
170 |
end |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
171 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
172 |
lemma card_UNIV_char: |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
173 |
"card (UNIV :: char set) = 256" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
174 |
by (simp add: card_UNIV_length_enum enum_char_def) |
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset
|
175 |
|
49972
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
176 |
primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
177 |
"nibble_pair_of_char (Char n m) = (n, m)" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
178 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
179 |
setup {* |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
180 |
let |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
181 |
val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16; |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
182 |
val thms = map_product |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
183 |
(fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps}) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
184 |
nibbles nibbles; |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
185 |
in |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
186 |
Global_Theory.note_thmss "" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
187 |
[((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])] |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
188 |
#-> (fn [(_, thms)] => fold_rev Code.add_eqn thms) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
189 |
end |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
190 |
*} |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
191 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
192 |
lemma char_case_nibble_pair [code, code_unfold]: |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
193 |
"char_case f = split f o nibble_pair_of_char" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
194 |
by (simp add: fun_eq_iff split: char.split) |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
195 |
|
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
196 |
lemma char_rec_nibble_pair [code, code_unfold]: |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
197 |
"char_rec f = split f o nibble_pair_of_char" |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
198 |
unfolding char_case_nibble_pair [symmetric] |
f11f8905d9fd
incorporated constant chars into instantiation proof for enum;
haftmann
parents:
49948
diff
changeset
|
199 |
by (simp add: fun_eq_iff split: char.split) |
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset
|
200 |
|
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
201 |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
202 |
subsection {* Strings as dedicated type *} |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
203 |
|
49834 | 204 |
typedef literal = "UNIV :: string set" |
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
205 |
morphisms explode STR .. |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
206 |
|
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
207 |
instantiation literal :: size |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
208 |
begin |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
209 |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
210 |
definition size_literal :: "literal \<Rightarrow> nat" |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
211 |
where |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
212 |
[code]: "size_literal (s\<Colon>literal) = 0" |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
213 |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
214 |
instance .. |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
215 |
|
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
216 |
end |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
217 |
|
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
218 |
instantiation literal :: equal |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
219 |
begin |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
220 |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
221 |
definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
222 |
where |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
223 |
"equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2" |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
224 |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
225 |
instance |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
226 |
proof |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
227 |
qed (auto simp add: equal_literal_def explode_inject) |
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
228 |
|
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
229 |
end |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
230 |
|
39274
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
39272
diff
changeset
|
231 |
lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)" |
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
39272
diff
changeset
|
232 |
by(simp add: STR_inject) |
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
39272
diff
changeset
|
233 |
|
b17ffa965223
fiddling with the correct setup for String.literal
bulwahn
parents:
39272
diff
changeset
|
234 |
|
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
235 |
subsection {* Code generator *} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
236 |
|
48891 | 237 |
ML_file "Tools/string_code.ML" |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
238 |
|
33237 | 239 |
code_reserved SML string |
240 |
code_reserved OCaml string |
|
34886 | 241 |
code_reserved Scala string |
33237 | 242 |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31176
diff
changeset
|
243 |
code_type literal |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
244 |
(SML "string") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
245 |
(OCaml "string") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
246 |
(Haskell "String") |
34886 | 247 |
(Scala "String") |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
248 |
|
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
249 |
setup {* |
34886 | 250 |
fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"] |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
251 |
*} |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
252 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37743
diff
changeset
|
253 |
code_instance literal :: equal |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
254 |
(Haskell -) |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
255 |
|
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37743
diff
changeset
|
256 |
code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool" |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
257 |
(SML "!((_ : string) = _)") |
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
258 |
(OCaml "!((_ : string) = _)") |
39272 | 259 |
(Haskell infix 4 "==") |
34886 | 260 |
(Scala infixl 5 "==") |
31051
4d9b52e0a48c
refined HOL string theories and corresponding ML fragments
haftmann
parents:
diff
changeset
|
261 |
|
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
35123
diff
changeset
|
262 |
hide_type (open) literal |
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31176
diff
changeset
|
263 |
|
39250
548a3e5521ab
changing String.literal to a type instead of a datatype
bulwahn
parents:
39198
diff
changeset
|
264 |
end |
49948
744934b818c7
moved quite generic material from theory Enum to more appropriate places
haftmann
parents:
49834
diff
changeset
|
265 |