author | oheimb |
Wed, 03 Apr 2002 10:21:13 +0200 | |
changeset 13076 | 70704dd48bd5 |
parent 12918 | bca45be2d25b |
child 13635 | c41e88151b54 |
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 |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
5 |
*) |
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
6 |
|
12918 | 7 |
header {* Datatypes *} |
11954 | 8 |
|
9 |
theory Datatype = Datatype_Universe: |
|
10 |
||
12918 | 11 |
subsection {* Finishing the datatype package setup *} |
12 |
||
12029 | 13 |
text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *} |
11954 | 14 |
hide const Node Atom Leaf Numb Lim Funs Split Case |
15 |
hide type node item |
|
16 |
||
17 |
||
18 |
subsection {* Representing primitive types *} |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
19 |
|
5759 | 20 |
rep_datatype bool |
11954 | 21 |
distinct True_not_False False_not_True |
22 |
induction bool_induct |
|
23 |
||
24 |
declare case_split [cases type: bool] |
|
25 |
-- "prefer plain propositional version" |
|
26 |
||
27 |
rep_datatype unit |
|
28 |
induction unit_induct |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
29 |
|
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
30 |
rep_datatype prod |
11954 | 31 |
inject Pair_eq |
32 |
induction prod_induct |
|
33 |
||
12918 | 34 |
rep_datatype sum |
35 |
distinct Inl_not_Inr Inr_not_Inl |
|
36 |
inject Inl_eq Inr_eq |
|
37 |
induction sum_induct |
|
38 |
||
39 |
ML {* |
|
40 |
val [sum_case_Inl, sum_case_Inr] = thms "sum.cases"; |
|
41 |
bind_thm ("sum_case_Inl", sum_case_Inl); |
|
42 |
bind_thm ("sum_case_Inr", sum_case_Inr); |
|
43 |
*} -- {* compatibility *} |
|
44 |
||
45 |
lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)" |
|
46 |
apply (rule_tac s = s in sumE) |
|
47 |
apply (erule ssubst) |
|
48 |
apply (rule sum_case_Inl) |
|
49 |
apply (erule ssubst) |
|
50 |
apply (rule sum_case_Inr) |
|
51 |
done |
|
52 |
||
53 |
lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t" |
|
54 |
-- {* Prevents simplification of @{text f} and @{text g}: much faster. *} |
|
55 |
by (erule arg_cong) |
|
56 |
||
57 |
lemma sum_case_inject: |
|
58 |
"sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P" |
|
59 |
proof - |
|
60 |
assume a: "sum_case f1 f2 = sum_case g1 g2" |
|
61 |
assume r: "f1 = g1 ==> f2 = g2 ==> P" |
|
62 |
show P |
|
63 |
apply (rule r) |
|
64 |
apply (rule ext) |
|
65 |
apply (cut_tac x = "Inl x" in a [THEN fun_cong]) |
|
66 |
apply simp |
|
67 |
apply (rule ext) |
|
68 |
apply (cut_tac x = "Inr x" in a [THEN fun_cong]) |
|
69 |
apply simp |
|
70 |
done |
|
71 |
qed |
|
72 |
||
73 |
||
74 |
subsection {* Further cases/induct rules for tuples *} |
|
11954 | 75 |
|
76 |
lemma prod_cases3 [case_names fields, cases type]: |
|
77 |
"(!!a b c. y = (a, b, c) ==> P) ==> P" |
|
78 |
apply (cases y) |
|
79 |
apply (case_tac b) |
|
80 |
apply blast |
|
81 |
done |
|
82 |
||
83 |
lemma prod_induct3 [case_names fields, induct type]: |
|
84 |
"(!!a b c. P (a, b, c)) ==> P x" |
|
85 |
by (cases x) blast |
|
86 |
||
87 |
lemma prod_cases4 [case_names fields, cases type]: |
|
88 |
"(!!a b c d. y = (a, b, c, d) ==> P) ==> P" |
|
89 |
apply (cases y) |
|
90 |
apply (case_tac c) |
|
91 |
apply blast |
|
92 |
done |
|
93 |
||
94 |
lemma prod_induct4 [case_names fields, induct type]: |
|
95 |
"(!!a b c d. P (a, b, c, d)) ==> P x" |
|
96 |
by (cases x) blast |
|
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
97 |
|
11954 | 98 |
lemma prod_cases5 [case_names fields, cases type]: |
99 |
"(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P" |
|
100 |
apply (cases y) |
|
101 |
apply (case_tac d) |
|
102 |
apply blast |
|
103 |
done |
|
104 |
||
105 |
lemma prod_induct5 [case_names fields, induct type]: |
|
106 |
"(!!a b c d e. P (a, b, c, d, e)) ==> P x" |
|
107 |
by (cases x) blast |
|
108 |
||
109 |
lemma prod_cases6 [case_names fields, cases type]: |
|
110 |
"(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P" |
|
111 |
apply (cases y) |
|
112 |
apply (case_tac e) |
|
113 |
apply blast |
|
114 |
done |
|
115 |
||
116 |
lemma prod_induct6 [case_names fields, induct type]: |
|
117 |
"(!!a b c d e f. P (a, b, c, d, e, f)) ==> P x" |
|
118 |
by (cases x) blast |
|
119 |
||
120 |
lemma prod_cases7 [case_names fields, cases type]: |
|
121 |
"(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P" |
|
122 |
apply (cases y) |
|
123 |
apply (case_tac f) |
|
124 |
apply blast |
|
125 |
done |
|
126 |
||
127 |
lemma prod_induct7 [case_names fields, induct type]: |
|
128 |
"(!!a b c d e f g. P (a, b, c, d, e, f, g)) ==> P x" |
|
129 |
by (cases x) blast |
|
5759 | 130 |
|
12918 | 131 |
|
132 |
subsection {* The option type *} |
|
133 |
||
134 |
datatype 'a option = None | Some 'a |
|
135 |
||
136 |
lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)" |
|
137 |
by (induct x) auto |
|
138 |
||
139 |
lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)" |
|
140 |
by (induct x) auto |
|
141 |
||
142 |
lemma option_caseE: |
|
143 |
"(case x of None => P | Some y => Q y) ==> |
|
144 |
(x = None ==> P ==> R) ==> |
|
145 |
(!!y. x = Some y ==> Q y ==> R) ==> R" |
|
146 |
by (cases x) simp_all |
|
147 |
||
148 |
||
149 |
subsubsection {* Operations *} |
|
150 |
||
151 |
consts |
|
152 |
the :: "'a option => 'a" |
|
153 |
primrec |
|
154 |
"the (Some x) = x" |
|
155 |
||
156 |
consts |
|
157 |
o2s :: "'a option => 'a set" |
|
158 |
primrec |
|
159 |
"o2s None = {}" |
|
160 |
"o2s (Some x) = {x}" |
|
161 |
||
162 |
lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x" |
|
163 |
by simp |
|
164 |
||
165 |
ML_setup {* claset_ref() := claset() addSD2 ("ospec", thm "ospec") *} |
|
166 |
||
167 |
lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)" |
|
168 |
by (cases xo) auto |
|
169 |
||
170 |
lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)" |
|
171 |
by (cases xo) auto |
|
172 |
||
173 |
||
174 |
constdefs |
|
175 |
option_map :: "('a => 'b) => ('a option => 'b option)" |
|
176 |
"option_map == %f y. case y of None => None | Some x => Some (f x)" |
|
177 |
||
178 |
lemma option_map_None [simp]: "option_map f None = None" |
|
179 |
by (simp add: option_map_def) |
|
180 |
||
181 |
lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)" |
|
182 |
by (simp add: option_map_def) |
|
183 |
||
184 |
lemma option_map_eq_Some [iff]: |
|
185 |
"(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)" |
|
186 |
by (simp add: option_map_def split add: option.split) |
|
187 |
||
188 |
lemma option_map_o_sum_case [simp]: |
|
189 |
"option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)" |
|
190 |
apply (rule ext) |
|
191 |
apply (simp split add: sum.split) |
|
192 |
done |
|
193 |
||
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset
|
194 |
end |