6 Sample datatype definition. |
6 Sample datatype definition. |
7 It has four contructors, of arities 0-3, and two parameters A and B. |
7 It has four contructors, of arities 0-3, and two parameters A and B. |
8 *) |
8 *) |
9 |
9 |
10 structure Data = Datatype_Fun |
10 structure Data = Datatype_Fun |
11 (val thy = Univ.thy; |
11 (val thy = Univ.thy |
12 val rec_specs = |
12 val rec_specs = [("data", "univ(A Un B)", |
13 [("data", "univ(A Un B)", |
13 [(["Con0"], "i"), |
14 [(["Con0"], "i"), |
14 (["Con1"], "i=>i"), |
15 (["Con1"], "i=>i"), |
15 (["Con2"], "[i,i]=>i"), |
16 (["Con2"], "[i,i]=>i"), |
16 (["Con3"], "[i,i,i]=>i")])] |
17 (["Con3"], "[i,i,i]=>i")])]; |
17 val rec_styp = "[i,i]=>i" |
18 val rec_styp = "[i,i]=>i"; |
18 val ext = None |
19 val ext = None |
19 val sintrs = |
20 val sintrs = |
20 ["Con0 : data(A,B)", |
21 ["Con0 : data(A,B)", |
21 "[| a: A |] ==> Con1(a) : data(A,B)", |
22 "[| a: A |] ==> Con1(a) : data(A,B)", |
22 "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)", |
23 "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)", |
23 "[| a: A; b: B; d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"] |
24 "[| a: A; b: B; d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"]; |
24 val monos = [] |
25 val monos = []; |
|
26 val type_intrs = datatype_intrs |
25 val type_intrs = datatype_intrs |
27 val type_elims = datatype_elims); |
26 val type_elims = datatype_elims); |
28 |
27 |
29 |
28 |
30 (** Lemmas to justify using "data" in other recursive type definitions **) |
29 (** Lemmas to justify using "data" in other recursive type definitions **) |