1 (* Title: ZF/ex/tf.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Trees & forests, a mutually recursive type definition. |
|
7 *) |
|
8 |
|
9 structure TF = Datatype_Fun |
|
10 (val thy = Univ.thy |
|
11 val rec_specs = [("tree", "univ(A)", |
|
12 [(["Tcons"], "[i,i]=>i")]), |
|
13 ("forest", "univ(A)", |
|
14 [(["Fnil"], "i"), |
|
15 (["Fcons"], "[i,i]=>i")])] |
|
16 val rec_styp = "i=>i" |
|
17 val ext = None |
|
18 val sintrs = |
|
19 ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)", |
|
20 "Fnil : forest(A)", |
|
21 "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"] |
|
22 val monos = [] |
|
23 val type_intrs = datatype_intrs |
|
24 val type_elims = datatype_elims); |
|
25 |
|
26 val [TconsI, FnilI, FconsI] = TF.intrs; |
|
27 |
|
28 (** tree_forest(A) as the union of tree(A) and forest(A) **) |
|
29 |
|
30 goalw TF.thy (tl TF.defs) "tree(A) <= tree_forest(A)"; |
|
31 by (rtac Part_subset 1); |
|
32 val tree_subset_TF = result(); |
|
33 |
|
34 goalw TF.thy (tl TF.defs) "forest(A) <= tree_forest(A)"; |
|
35 by (rtac Part_subset 1); |
|
36 val forest_subset_TF = result(); |
|
37 |
|
38 goalw TF.thy (tl TF.defs) "tree(A) Un forest(A) = tree_forest(A)"; |
|
39 by (rtac (TF.dom_subset RS Part_sum_equality) 1); |
|
40 val TF_equals_Un = result(); |
|
41 |
|
42 (** NOT useful, but interesting... **) |
|
43 |
|
44 (*The (refl RS conjI RS exI RS exI) avoids considerable search!*) |
|
45 val unfold_cs = sum_cs addSIs [PartI, refl RS conjI RS exI RS exI] |
|
46 addIs datatype_intrs |
|
47 addDs [TF.dom_subset RS subsetD] |
|
48 addSEs ([PartE] @ datatype_elims @ TF.free_SEs); |
|
49 |
|
50 goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}"; |
|
51 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1); |
|
52 by (rewrite_goals_tac TF.con_defs); |
|
53 by (rtac equalityI 1); |
|
54 by (fast_tac unfold_cs 1); |
|
55 by (fast_tac unfold_cs 1); |
|
56 val tree_unfold = result(); |
|
57 |
|
58 goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}"; |
|
59 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1); |
|
60 by (rewrite_goals_tac TF.con_defs); |
|
61 by (rtac equalityI 1); |
|
62 by (fast_tac unfold_cs 1); |
|
63 by (fast_tac unfold_cs 1); |
|
64 val forest_unfold = result(); |
|
65 |
|