1 (* Title: HOL/BNF_Examples/Misc_Datatype.thy |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Andrei Popescu, TU Muenchen |
|
4 Author: Jasmin Blanchette, TU Muenchen |
|
5 Copyright 2012, 2013 |
|
6 |
|
7 Miscellaneous datatype definitions. |
|
8 *) |
|
9 |
|
10 header {* Miscellaneous Datatype Definitions *} |
|
11 |
|
12 theory Misc_Datatype |
|
13 imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/FSet" |
|
14 begin |
|
15 |
|
16 datatype_new (discs_sels) simple = X1 | X2 | X3 | X4 |
|
17 |
|
18 datatype_new (discs_sels) simple' = X1' unit | X2' unit | X3' unit | X4' unit |
|
19 |
|
20 datatype_new (discs_sels) simple'' = X1'' nat int | X2'' |
|
21 |
|
22 datatype_new (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist") |
|
23 |
|
24 datatype_new (discs_sels) ('b, 'c :: ord, 'd, 'e) some_passive = |
|
25 SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e |
|
26 |
|
27 datatype_new (discs_sels) hfset = HFset "hfset fset" |
|
28 |
|
29 datatype_new (discs_sels) lambda = |
|
30 Var string | |
|
31 App lambda lambda | |
|
32 Abs string lambda | |
|
33 Let "(string \<times> lambda) fset" lambda |
|
34 |
|
35 datatype_new (discs_sels) 'a par_lambda = |
|
36 PVar 'a | |
|
37 PApp "'a par_lambda" "'a par_lambda" | |
|
38 PAbs 'a "'a par_lambda" | |
|
39 PLet "('a \<times> 'a par_lambda) fset" "'a par_lambda" |
|
40 |
|
41 (* |
|
42 ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 |
|
43 ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 |
|
44 *) |
|
45 |
|
46 datatype_new (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2" |
|
47 and 'a I2 = I21 | I22 "'a I1" "'a I2" |
|
48 |
|
49 datatype_new (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest" |
|
50 and 'a forest = FNil | FCons "'a tree" "'a forest" |
|
51 |
|
52 datatype_new (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" |
|
53 and 'a branch = Branch 'a "'a tree'" |
|
54 |
|
55 datatype_new (discs_sels) 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist" |
|
56 |
|
57 datatype_new (discs_sels) ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" |
|
58 and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" |
|
59 and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" |
|
60 |
|
61 datatype_new (discs_sels) 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree" |
|
62 |
|
63 datatype_new (discs_sels) ('a, 'b, 'c) some_killing = |
|
64 SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" |
|
65 and ('a, 'b, 'c) in_here = |
|
66 IH1 'b 'a | IH2 'c |
|
67 |
|
68 datatype_new (discs_sels) 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b |
|
69 datatype_new (discs_sels) 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list" |
|
70 datatype_new (discs_sels) 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset" |
|
71 datatype_new (discs_sels) 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list" |
|
72 |
|
73 (* |
|
74 datatype_new (discs_sels) 'b fail = F "'b fail" 'b "'b fail" "'b list" |
|
75 datatype_new (discs_sels) 'b fail = F "'b fail" 'b "'b fail" 'b |
|
76 datatype_new (discs_sels) 'b fail = F1 "'b fail" 'b | F2 "'b fail" |
|
77 datatype_new (discs_sels) 'b fail = F "'b fail" 'b |
|
78 *) |
|
79 |
|
80 datatype_new (discs_sels) l1 = L1 "l2 list" |
|
81 and l2 = L21 "l1 fset" | L22 l2 |
|
82 |
|
83 datatype_new (discs_sels) kk1 = KK1 kk2 |
|
84 and kk2 = KK2 kk3 |
|
85 and kk3 = KK3 "kk1 list" |
|
86 |
|
87 datatype_new (discs_sels) t1 = T11 t3 | T12 t2 |
|
88 and t2 = T2 t1 |
|
89 and t3 = T3 |
|
90 |
|
91 datatype_new (discs_sels) t1' = T11' t2' | T12' t3' |
|
92 and t2' = T2' t1' |
|
93 and t3' = T3' |
|
94 |
|
95 (* |
|
96 datatype_new (discs_sels) fail1 = F1 fail2 |
|
97 and fail2 = F2 fail3 |
|
98 and fail3 = F3 fail1 |
|
99 |
|
100 datatype_new (discs_sels) fail1 = F1 "fail2 list" fail2 |
|
101 and fail2 = F2 "fail2 fset" fail3 |
|
102 and fail3 = F3 fail1 |
|
103 |
|
104 datatype_new (discs_sels) fail1 = F1 "fail2 list" fail2 |
|
105 and fail2 = F2 "fail1 fset" fail1 |
|
106 *) |
|
107 |
|
108 (* SLOW |
|
109 datatype_new (discs_sels) ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" |
|
110 and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" |
|
111 and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" |
|
112 and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" |
|
113 and ('a, 'c) D5 = A5 "('a, 'c) D6" |
|
114 and ('a, 'c) D6 = A6 "('a, 'c) D7" |
|
115 and ('a, 'c) D7 = A7 "('a, 'c) D8" |
|
116 and ('a, 'c) D8 = A8 "('a, 'c) D1 list" |
|
117 *) |
|
118 |
|
119 (* fail: |
|
120 datatype_new (discs_sels) tt1 = TT11 tt2 tt3 | TT12 tt2 tt4 |
|
121 and tt2 = TT2 |
|
122 and tt3 = TT3 tt4 |
|
123 and tt4 = TT4 tt1 |
|
124 *) |
|
125 |
|
126 datatype_new (discs_sels) k1 = K11 k2 k3 | K12 k2 k4 |
|
127 and k2 = K2 |
|
128 and k3 = K3 k4 |
|
129 and k4 = K4 |
|
130 |
|
131 datatype_new (discs_sels) tt1 = TT11 tt3 tt2 | TT12 tt2 tt4 |
|
132 and tt2 = TT2 |
|
133 and tt3 = TT3 tt1 |
|
134 and tt4 = TT4 |
|
135 |
|
136 (* SLOW |
|
137 datatype_new (discs_sels) s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2 |
|
138 and s2 = S21 s7 s5 | S22 s5 s4 s6 |
|
139 and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5 |
|
140 and s4 = S4 s5 |
|
141 and s5 = S5 |
|
142 and s6 = S61 s6 | S62 s1 s2 | S63 s6 |
|
143 and s7 = S71 s8 | S72 s5 |
|
144 and s8 = S8 nat |
|
145 *) |
|
146 |
|
147 datatype_new (discs_sels) 'a deadbar = DeadBar "'a \<Rightarrow> 'a" |
|
148 datatype_new (discs_sels) 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option" |
|
149 datatype_new (discs_sels) ('a, 'b) bar = Bar "'b \<Rightarrow> 'a" |
|
150 datatype_new (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a" |
|
151 datatype_new (discs_sels) 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a" |
|
152 |
|
153 datatype_new (discs_sels) 'a dead_foo = A |
|
154 datatype_new (discs_sels) ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" |
|
155 |
|
156 datatype_new (discs_sels) d1 = D |
|
157 datatype_new (discs_sels) d1' = is_D: D |
|
158 |
|
159 datatype_new (discs_sels) d2 = D nat |
|
160 datatype_new (discs_sels) d2' = is_D: D nat |
|
161 |
|
162 datatype_new (discs_sels) d3 = D | E |
|
163 datatype_new (discs_sels) d3' = D | is_E: E |
|
164 datatype_new (discs_sels) d3'' = is_D: D | E |
|
165 datatype_new (discs_sels) d3''' = is_D: D | is_E: E |
|
166 |
|
167 datatype_new (discs_sels) d4 = D nat | E |
|
168 datatype_new (discs_sels) d4' = D nat | is_E: E |
|
169 datatype_new (discs_sels) d4'' = is_D: D nat | E |
|
170 datatype_new (discs_sels) d4''' = is_D: D nat | is_E: E |
|
171 |
|
172 datatype_new (discs_sels) d5 = D nat | E int |
|
173 datatype_new (discs_sels) d5' = D nat | is_E: E int |
|
174 datatype_new (discs_sels) d5'' = is_D: D nat | E int |
|
175 datatype_new (discs_sels) d5''' = is_D: D nat | is_E: E int |
|
176 |
|
177 instance simple :: countable |
|
178 by countable_datatype |
|
179 |
|
180 instance simple'' :: countable |
|
181 by countable_datatype |
|
182 |
|
183 instance mylist :: (countable) countable |
|
184 by countable_datatype |
|
185 |
|
186 instance some_passive :: (countable, "{countable,ord}", countable, countable) countable |
|
187 by countable_datatype |
|
188 |
|
189 (* TODO: Enable once "fset" is registered as countable: |
|
190 |
|
191 instance hfset :: countable |
|
192 by countable_datatype |
|
193 |
|
194 instance lambda :: countable |
|
195 by countable_datatype |
|
196 |
|
197 instance par_lambda :: (countable) countable |
|
198 by countable_datatype |
|
199 *) |
|
200 |
|
201 instance I1 and I2 :: (countable) countable |
|
202 by countable_datatype |
|
203 |
|
204 instance tree and forest :: (countable) countable |
|
205 by countable_datatype |
|
206 |
|
207 instance tree' and branch :: (countable) countable |
|
208 by countable_datatype |
|
209 |
|
210 instance bin_rose_tree :: (countable) countable |
|
211 by countable_datatype |
|
212 |
|
213 instance exp and trm and factor :: (countable, countable) countable |
|
214 by countable_datatype |
|
215 |
|
216 instance nofail1 :: (countable) countable |
|
217 by countable_datatype |
|
218 |
|
219 instance nofail2 :: (countable) countable |
|
220 by countable_datatype |
|
221 |
|
222 (* TODO: Enable once "fset" is registered as countable: |
|
223 |
|
224 instance nofail3 :: (countable) countable |
|
225 by countable_datatype |
|
226 |
|
227 instance nofail4 :: (countable) countable |
|
228 by countable_datatype |
|
229 |
|
230 instance l1 and l2 :: countable |
|
231 by countable_datatype |
|
232 *) |
|
233 |
|
234 instance kk1 and kk2 :: countable |
|
235 by countable_datatype |
|
236 |
|
237 instance t1 and t2 and t3 :: countable |
|
238 by countable_datatype |
|
239 |
|
240 instance t1' and t2' and t3' :: countable |
|
241 by countable_datatype |
|
242 |
|
243 instance k1 and k2 and k3 and k4 :: countable |
|
244 by countable_datatype |
|
245 |
|
246 instance tt1 and tt2 and tt3 and tt4 :: countable |
|
247 by countable_datatype |
|
248 |
|
249 instance d1 :: countable |
|
250 by countable_datatype |
|
251 |
|
252 instance d1' :: countable |
|
253 by countable_datatype |
|
254 |
|
255 instance d2 :: countable |
|
256 by countable_datatype |
|
257 |
|
258 instance d2' :: countable |
|
259 by countable_datatype |
|
260 |
|
261 instance d3 :: countable |
|
262 by countable_datatype |
|
263 |
|
264 instance d3' :: countable |
|
265 by countable_datatype |
|
266 |
|
267 instance d3'' :: countable |
|
268 by countable_datatype |
|
269 |
|
270 instance d3''' :: countable |
|
271 by countable_datatype |
|
272 |
|
273 instance d4 :: countable |
|
274 by countable_datatype |
|
275 |
|
276 instance d4' :: countable |
|
277 by countable_datatype |
|
278 |
|
279 instance d4'' :: countable |
|
280 by countable_datatype |
|
281 |
|
282 instance d4''' :: countable |
|
283 by countable_datatype |
|
284 |
|
285 instance d5 :: countable |
|
286 by countable_datatype |
|
287 |
|
288 instance d5' :: countable |
|
289 by countable_datatype |
|
290 |
|
291 instance d5'' :: countable |
|
292 by countable_datatype |
|
293 |
|
294 instance d5''' :: countable |
|
295 by countable_datatype |
|
296 |
|
297 datatype_compat simple |
|
298 datatype_compat simple' |
|
299 datatype_compat simple'' |
|
300 datatype_compat mylist |
|
301 datatype_compat some_passive |
|
302 datatype_compat I1 I2 |
|
303 datatype_compat tree forest |
|
304 datatype_compat tree' branch |
|
305 datatype_compat bin_rose_tree |
|
306 datatype_compat exp trm factor |
|
307 datatype_compat ftree |
|
308 datatype_compat nofail1 |
|
309 datatype_compat kk1 kk2 kk3 |
|
310 datatype_compat t1 t2 t3 |
|
311 datatype_compat t1' t2' t3' |
|
312 datatype_compat k1 k2 k3 k4 |
|
313 datatype_compat tt1 tt2 tt3 tt4 |
|
314 datatype_compat deadbar |
|
315 datatype_compat deadbar_option |
|
316 datatype_compat bar |
|
317 datatype_compat foo |
|
318 datatype_compat deadfoo |
|
319 datatype_compat dead_foo |
|
320 datatype_compat use_dead_foo |
|
321 datatype_compat d1 |
|
322 datatype_compat d1' |
|
323 datatype_compat d2 |
|
324 datatype_compat d2' |
|
325 datatype_compat d3 |
|
326 datatype_compat d3' |
|
327 datatype_compat d3'' |
|
328 datatype_compat d3''' |
|
329 datatype_compat d4 |
|
330 datatype_compat d4' |
|
331 datatype_compat d4'' |
|
332 datatype_compat d4''' |
|
333 datatype_compat d5 |
|
334 datatype_compat d5' |
|
335 datatype_compat d5'' |
|
336 datatype_compat d5''' |
|
337 |
|
338 end |
|