author | blanchet |
Mon, 01 Sep 2014 16:17:46 +0200 | |
changeset 58112 | 8081087096ad |
parent 57634 | efc00b9b8680 |
child 58124 | c60617a84c1d |
permissions | -rw-r--r-- |
57634 | 1 |
(* Title: HOL/BNF_Examples/Compat.thy |
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
3 |
Copyright 2014 |
|
4 |
||
5 |
Tests for compatibility with the old datatype package. |
|
6 |
*) |
|
7 |
||
8 |
header {* Tests for Compatibility with the Old Datatype Package *} |
|
9 |
||
56454 | 10 |
theory Compat |
11 |
imports Main |
|
12 |
begin |
|
13 |
||
14 |
datatype_new 'a lst = Nl | Cns 'a "'a lst" |
|
15 |
datatype_compat lst |
|
16 |
||
56456 | 17 |
datatype_new 'b w = W | W' "'b w \<times> 'b list" |
56454 | 18 |
(* no support for sums of products |
19 |
datatype_compat w |
|
20 |
*) |
|
21 |
||
22 |
datatype_new ('c, 'b) s = L 'c | R 'b |
|
23 |
datatype_new 'd x = X | X' "('d x lst, 'd list) s" |
|
24 |
datatype_compat s |
|
25 |
datatype_compat x |
|
26 |
||
27 |
datatype_new 'a tttre = TTTre 'a "'a tttre lst lst lst" |
|
28 |
datatype_compat tttre |
|
29 |
||
30 |
datatype_new 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst" |
|
31 |
datatype_compat ftre |
|
32 |
||
33 |
datatype_new 'a btre = BTre 'a "'a btre lst" "'a btre lst" |
|
34 |
datatype_compat btre |
|
35 |
||
36 |
datatype_new 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo" |
|
37 |
datatype_compat foo bar |
|
38 |
||
39 |
datatype_new 'a tre = Tre 'a "'a tre lst" |
|
40 |
datatype_compat tre |
|
41 |
||
42 |
fun f_tre and f_tres where |
|
43 |
"f_tre (Tre a ts) = {a} \<union> f_tres ts" |
|
44 |
| "f_tres Nl = {}" |
|
45 |
| "f_tres (Cns t ts) = f_tres ts" |
|
46 |
||
47 |
datatype_new 'a f = F 'a and 'a g = G 'a |
|
48 |
datatype_new h = H "h f" | H' |
|
49 |
datatype_compat f g |
|
50 |
datatype_compat h |
|
51 |
||
52 |
datatype_new myunit = MyUnity |
|
53 |
datatype_compat myunit |
|
54 |
||
55 |
datatype_new mylist = MyNil | MyCons nat mylist |
|
56 |
datatype_compat mylist |
|
57 |
||
58 |
fun f_mylist where |
|
59 |
"f_mylist MyNil = 0" |
|
60 |
| "f_mylist (MyCons _ xs) = Suc (f_mylist xs)" |
|
61 |
||
62 |
datatype_new foo' = FooNil | FooCons bar' foo' and bar' = Bar |
|
63 |
datatype_compat bar' foo' |
|
64 |
||
65 |
fun f_foo and f_bar where |
|
66 |
"f_foo FooNil = 0" |
|
67 |
| "f_foo (FooCons bar foo) = Suc (f_foo foo) + f_bar bar" |
|
68 |
| "f_bar Bar = Suc 0" |
|
69 |
||
70 |
locale opt begin |
|
71 |
||
72 |
datatype_new 'a opt = Non | Som 'a |
|
73 |
datatype_compat opt |
|
74 |
||
75 |
end |
|
76 |
||
77 |
datatype funky = Funky "funky tre" | Funky' |
|
78 |
datatype fnky = Fnky "nat tre" |
|
79 |
||
80 |
datatype_new tree = Tree "tree foo" |
|
56488 | 81 |
datatype_compat tree |
56454 | 82 |
|
58112
8081087096ad
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents:
57634
diff
changeset
|
83 |
ML {* Old_Datatype_Data.get_info @{theory} @{type_name tree} *} |
56454 | 84 |
|
85 |
end |