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 |
|
|
83 |
ML {* Datatype_Data.get_info @{theory} @{type_name tree} *}
|
|
84 |
|
|
85 |
end
|