5 |
5 |
6 Trees & forests, a mutually recursive type definition. |
6 Trees & forests, a mutually recursive type definition. |
7 *) |
7 *) |
8 |
8 |
9 structure TF = Datatype_Fun |
9 structure TF = Datatype_Fun |
10 (val thy = Univ.thy; |
10 (val thy = Univ.thy |
11 val rec_specs = |
11 val rec_specs = [("tree", "univ(A)", |
12 [("tree", "univ(A)", |
12 [(["Tcons"], "[i,i]=>i")]), |
13 [(["Tcons"], "[i,i]=>i")]), |
13 ("forest", "univ(A)", |
14 ("forest", "univ(A)", |
14 [(["Fnil"], "i"), |
15 [(["Fnil"], "i"), |
15 (["Fcons"], "[i,i]=>i")])] |
16 (["Fcons"], "[i,i]=>i")])]; |
16 val rec_styp = "i=>i" |
17 val rec_styp = "i=>i"; |
17 val ext = None |
18 val ext = None |
18 val sintrs = |
19 val sintrs = |
19 ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)", |
20 ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)", |
20 "Fnil : forest(A)", |
21 "Fnil : forest(A)", |
21 "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"] |
22 "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"]; |
22 val monos = [] |
23 val monos = []; |
|
24 val type_intrs = datatype_intrs |
23 val type_intrs = datatype_intrs |
25 val type_elims = datatype_elims); |
24 val type_elims = datatype_elims); |
26 |
25 |
27 val [TconsI, FnilI, FconsI] = TF.intrs; |
26 val [TconsI, FnilI, FconsI] = TF.intrs; |
28 |
27 |