author | haftmann |
Tue, 19 Sep 2006 15:21:42 +0200 | |
changeset 20588 | c847c56edf0c |
parent 20523 | 36a59e5d0039 |
child 20798 | 3275b03e2fff |
permissions | -rw-r--r-- |
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
1 |
(* Title: HOL/Datatype.thy |
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
11954 | 3 |
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
4 |
*) |
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
5 |
|
12918 | 6 |
header {* Datatypes *} |
11954 | 7 |
|
15131 | 8 |
theory Datatype |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
9 |
imports Datatype_Universe |
15131 | 10 |
begin |
11954 | 11 |
|
20588 | 12 |
setup "DatatypeCodegen.setup2" |
13 |
||
11954 | 14 |
subsection {* Representing primitive types *} |
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
15 |
|
5759 | 16 |
rep_datatype bool |
11954 | 17 |
distinct True_not_False False_not_True |
18 |
induction bool_induct |
|
19 |
||
20 |
declare case_split [cases type: bool] |
|
21 |
-- "prefer plain propositional version" |
|
22 |
||
23 |
rep_datatype unit |
|
24 |
induction unit_induct |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
25 |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
26 |
rep_datatype prod |
11954 | 27 |
inject Pair_eq |
28 |
induction prod_induct |
|
29 |
||
12918 | 30 |
rep_datatype sum |
31 |
distinct Inl_not_Inr Inr_not_Inl |
|
32 |
inject Inl_eq Inr_eq |
|
33 |
induction sum_induct |
|
34 |
||
35 |
ML {* |
|
36 |
val [sum_case_Inl, sum_case_Inr] = thms "sum.cases"; |
|
37 |
bind_thm ("sum_case_Inl", sum_case_Inl); |
|
38 |
bind_thm ("sum_case_Inr", sum_case_Inr); |
|
39 |
*} -- {* compatibility *} |
|
40 |
||
41 |
lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)" |
|
42 |
apply (rule_tac s = s in sumE) |
|
43 |
apply (erule ssubst) |
|
44 |
apply (rule sum_case_Inl) |
|
45 |
apply (erule ssubst) |
|
46 |
apply (rule sum_case_Inr) |
|
47 |
done |
|
48 |
||
49 |
lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t" |
|
50 |
-- {* Prevents simplification of @{text f} and @{text g}: much faster. *} |
|
51 |
by (erule arg_cong) |
|
52 |
||
53 |
lemma sum_case_inject: |
|
54 |
"sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P" |
|
55 |
proof - |
|
56 |
assume a: "sum_case f1 f2 = sum_case g1 g2" |
|
57 |
assume r: "f1 = g1 ==> f2 = g2 ==> P" |
|
58 |
show P |
|
59 |
apply (rule r) |
|
60 |
apply (rule ext) |
|
14208 | 61 |
apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp) |
12918 | 62 |
apply (rule ext) |
14208 | 63 |
apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp) |
12918 | 64 |
done |
65 |
qed |
|
66 |
||
13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
67 |
constdefs |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
68 |
Suml :: "('a => 'c) => 'a + 'b => 'c" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
69 |
"Suml == (%f. sum_case f arbitrary)" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
70 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
71 |
Sumr :: "('b => 'c) => 'a + 'b => 'c" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
72 |
"Sumr == sum_case arbitrary" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
73 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
74 |
lemma Suml_inject: "Suml f = Suml g ==> f = g" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
75 |
by (unfold Suml_def) (erule sum_case_inject) |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
76 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
77 |
lemma Sumr_inject: "Sumr f = Sumr g ==> f = g" |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
78 |
by (unfold Sumr_def) (erule sum_case_inject) |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
79 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
80 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
81 |
subsection {* Finishing the datatype package setup *} |
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
82 |
|
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
83 |
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} |
18230 | 84 |
hide (open) const Push Node Atom Leaf Numb Lim Split Case Suml Sumr |
85 |
hide (open) type node item |
|
13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset
|
86 |
|
12918 | 87 |
|
88 |
subsection {* Further cases/induct rules for tuples *} |
|
11954 | 89 |
|
90 |
lemma prod_cases3 [case_names fields, cases type]: |
|
91 |
"(!!a b c. y = (a, b, c) ==> P) ==> P" |
|
92 |
apply (cases y) |
|
14208 | 93 |
apply (case_tac b, blast) |
11954 | 94 |
done |
95 |
||
96 |
lemma prod_induct3 [case_names fields, induct type]: |
|
97 |
"(!!a b c. P (a, b, c)) ==> P x" |
|
98 |
by (cases x) blast |
|
99 |
||
100 |
lemma prod_cases4 [case_names fields, cases type]: |
|
101 |
"(!!a b c d. y = (a, b, c, d) ==> P) ==> P" |
|
102 |
apply (cases y) |
|
14208 | 103 |
apply (case_tac c, blast) |
11954 | 104 |
done |
105 |
||
106 |
lemma prod_induct4 [case_names fields, induct type]: |
|
107 |
"(!!a b c d. P (a, b, c, d)) ==> P x" |
|
108 |
by (cases x) blast |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
109 |
|
11954 | 110 |
lemma prod_cases5 [case_names fields, cases type]: |
111 |
"(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P" |
|
112 |
apply (cases y) |
|
14208 | 113 |
apply (case_tac d, blast) |
11954 | 114 |
done |
115 |
||
116 |
lemma prod_induct5 [case_names fields, induct type]: |
|
117 |
"(!!a b c d e. P (a, b, c, d, e)) ==> P x" |
|
118 |
by (cases x) blast |
|
119 |
||
120 |
lemma prod_cases6 [case_names fields, cases type]: |
|
121 |
"(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P" |
|
122 |
apply (cases y) |
|
14208 | 123 |
apply (case_tac e, blast) |
11954 | 124 |
done |
125 |
||
126 |
lemma prod_induct6 [case_names fields, induct type]: |
|
127 |
"(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" |
|
128 |
by (cases x) blast |
|
129 |
||
130 |
lemma prod_cases7 [case_names fields, cases type]: |
|
131 |
"(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P" |
|
132 |
apply (cases y) |
|
14208 | 133 |
apply (case_tac f, blast) |
11954 | 134 |
done |
135 |
||
136 |
lemma prod_induct7 [case_names fields, induct type]: |
|
137 |
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" |
|
138 |
by (cases x) blast |
|
5759 | 139 |
|
12918 | 140 |
|
141 |
subsection {* The option type *} |
|
142 |
||
143 |
datatype 'a option = None | Some 'a |
|
144 |
||
18576 | 145 |
lemma not_None_eq[iff]: "(x ~= None) = (EX y. x = Some y)" |
146 |
by (induct x) auto |
|
147 |
||
148 |
lemma not_Some_eq[iff]: "(ALL y. x ~= Some y) = (x = None)" |
|
18447 | 149 |
by (induct x) auto |
150 |
||
18576 | 151 |
text{*Although it may appear that both of these equalities are helpful |
152 |
only when applied to assumptions, in practice it seems better to give |
|
153 |
them the uniform iff attribute. *} |
|
12918 | 154 |
|
18576 | 155 |
(* |
18447 | 156 |
lemmas not_None_eq_D = not_None_eq [THEN iffD1] |
157 |
declare not_None_eq_D [dest!] |
|
158 |
||
159 |
lemmas not_Some_eq_D = not_Some_eq [THEN iffD1] |
|
160 |
declare not_Some_eq_D [dest!] |
|
18576 | 161 |
*) |
12918 | 162 |
|
163 |
lemma option_caseE: |
|
164 |
"(case x of None => P | Some y => Q y) ==> |
|
165 |
(x = None ==> P ==> R) ==> |
|
166 |
(!!y. x = Some y ==> Q y ==> R) ==> R" |
|
167 |
by (cases x) simp_all |
|
168 |
||
169 |
||
170 |
subsubsection {* Operations *} |
|
171 |
||
172 |
consts |
|
173 |
the :: "'a option => 'a" |
|
174 |
primrec |
|
175 |
"the (Some x) = x" |
|
176 |
||
177 |
consts |
|
178 |
o2s :: "'a option => 'a set" |
|
179 |
primrec |
|
180 |
"o2s None = {}" |
|
181 |
"o2s (Some x) = {x}" |
|
182 |
||
183 |
lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x" |
|
184 |
by simp |
|
185 |
||
17876 | 186 |
ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *} |
12918 | 187 |
|
188 |
lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)" |
|
189 |
by (cases xo) auto |
|
190 |
||
191 |
lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)" |
|
192 |
by (cases xo) auto |
|
193 |
||
194 |
||
195 |
constdefs |
|
196 |
option_map :: "('a => 'b) => ('a option => 'b option)" |
|
197 |
"option_map == %f y. case y of None => None | Some x => Some (f x)" |
|
198 |
||
199 |
lemma option_map_None [simp]: "option_map f None = None" |
|
200 |
by (simp add: option_map_def) |
|
201 |
||
202 |
lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)" |
|
203 |
by (simp add: option_map_def) |
|
204 |
||
14187 | 205 |
lemma option_map_is_None[iff]: |
206 |
"(option_map f opt = None) = (opt = None)" |
|
207 |
by (simp add: option_map_def split add: option.split) |
|
208 |
||
12918 | 209 |
lemma option_map_eq_Some [iff]: |
210 |
"(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)" |
|
14187 | 211 |
by (simp add: option_map_def split add: option.split) |
212 |
||
213 |
lemma option_map_comp: |
|
214 |
"option_map f (option_map g opt) = option_map (f o g) opt" |
|
215 |
by (simp add: option_map_def split add: option.split) |
|
12918 | 216 |
|
217 |
lemma option_map_o_sum_case [simp]: |
|
218 |
"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)" |
|
219 |
apply (rule ext) |
|
220 |
apply (simp split add: sum.split) |
|
221 |
done |
|
222 |
||
19787 | 223 |
|
19817 | 224 |
subsubsection {* Codegenerator setup *} |
225 |
||
19787 | 226 |
consts |
227 |
is_none :: "'a option \<Rightarrow> bool" |
|
228 |
primrec |
|
229 |
"is_none None = True" |
|
230 |
"is_none (Some x) = False" |
|
231 |
||
20105 | 232 |
lemma is_none_none [code inline]: |
19787 | 233 |
"(x = None) = (is_none x)" |
20105 | 234 |
by (cases x) simp_all |
19787 | 235 |
|
17458
e42bfad176eb
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
wenzelm
parents:
15140
diff
changeset
|
236 |
lemmas [code] = imp_conv_disj |
e42bfad176eb
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
wenzelm
parents:
15140
diff
changeset
|
237 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
238 |
lemma [code func]: |
19138 | 239 |
"(\<not> True) = False" by (rule HOL.simp_thms) |
240 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
241 |
lemma [code func]: |
19138 | 242 |
"(\<not> False) = True" by (rule HOL.simp_thms) |
243 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
244 |
lemma [code func]: |
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
245 |
shows "(False \<and> x) = False" |
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
246 |
and "(True \<and> x) = x" |
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
247 |
and "(x \<and> False) = False" |
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
248 |
and "(x \<and> True) = x" by simp_all |
19138 | 249 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
250 |
lemma [code func]: |
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
251 |
shows "(False \<or> x) = x" |
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
252 |
and "(True \<or> x) = True" |
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
253 |
and "(x \<or> False) = x" |
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
254 |
and "(x \<or> True) = True" by simp_all |
19138 | 255 |
|
256 |
declare |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
257 |
if_True [code func] |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20453
diff
changeset
|
258 |
if_False [code func] |
19179
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
259 |
fst_conv [code] |
61ef97e3f531
changed and retracted change of location of code lemmas.
nipkow
parents:
19150
diff
changeset
|
260 |
snd_conv [code] |
19138 | 261 |
|
20105 | 262 |
lemma split_is_prod_case [code inline]: |
263 |
"split = prod_case" |
|
264 |
by (simp add: expand_fun_eq split_def prod.cases) |
|
265 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
266 |
code_type bool |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
267 |
(SML target_atom "bool") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
268 |
(Haskell target_atom "Bool") |
19138 | 269 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
270 |
code_const True and False and Not and "op &" and "op |" and If |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
271 |
(SML target_atom "true" and target_atom "false" and target_atom "not" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
272 |
and infixl 1 "andalso" and infixl 0 "orelse" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
273 |
and target_atom "(if __/ then __/ else __)") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
274 |
(Haskell target_atom "True" and target_atom "False" and target_atom "not" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
275 |
and infixl 3 "&&" and infixl 2 "||" |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
276 |
and target_atom "(if __/ then __/ else __)") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
277 |
|
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
278 |
code_type * |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
279 |
(SML infix 2 "*") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
280 |
(Haskell target_atom "(__,/ __)") |
19138 | 281 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
282 |
code_const Pair |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
283 |
(SML target_atom "(__,/ __)") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
284 |
(Haskell target_atom "(__,/ __)") |
18702 | 285 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
286 |
code_type unit |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
287 |
(SML target_atom "unit") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
288 |
(Haskell target_atom "()") |
19150 | 289 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
290 |
code_const Unity |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
291 |
(SML target_atom "()") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
292 |
(Haskell target_atom "()") |
19150 | 293 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
294 |
code_type option |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
295 |
(SML "_ option") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
296 |
(Haskell "Maybe _") |
19150 | 297 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
298 |
code_const None and Some |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
299 |
(SML target_atom "NONE" and target_atom "SOME") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20105
diff
changeset
|
300 |
(Haskell target_atom "Nothing" and target_atom "Just") |
19150 | 301 |
|
20588 | 302 |
code_instance option :: eq |
303 |
(Haskell -) |
|
304 |
||
305 |
code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool" |
|
306 |
(Haskell infixl 4 "==") |
|
307 |
||
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
308 |
end |