|
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 = |
|
12 [("tree", "univ(A)", |
|
13 [(["Tcons"], "[i,i]=>i")]), |
|
14 ("forest", "univ(A)", |
|
15 [(["Fnil"], "i"), |
|
16 (["Fcons"], "[i,i]=>i")])]; |
|
17 val rec_styp = "i=>i"; |
|
18 val ext = None |
|
19 val sintrs = |
|
20 ["[| a:A; tf: forest(A) |] ==> Tcons(a,tf) : tree(A)", |
|
21 "Fnil : forest(A)", |
|
22 "[| t: tree(A); tf: forest(A) |] ==> Fcons(t,tf) : forest(A)"]; |
|
23 val monos = []; |
|
24 val type_intrs = data_typechecks |
|
25 val type_elims = []); |
|
26 |
|
27 val [TconsI, FnilI, FconsI] = TF.intrs; |
|
28 |
|
29 (** tree_forest(A) as the union of tree(A) and forest(A) **) |
|
30 |
|
31 goalw TF.thy (tl TF.defs) "tree(A) <= tree_forest(A)"; |
|
32 by (rtac Part_subset 1); |
|
33 val tree_subset_TF = result(); |
|
34 |
|
35 goalw TF.thy (tl TF.defs) "forest(A) <= tree_forest(A)"; |
|
36 by (rtac Part_subset 1); |
|
37 val forest_subset_TF = result(); |
|
38 |
|
39 goalw TF.thy (tl TF.defs) "tree(A) Un forest(A) = tree_forest(A)"; |
|
40 by (rtac (TF.dom_subset RS Part_sum_equality) 1); |
|
41 val TF_equals_Un = result(); |
|
42 |
|
43 (** NOT useful, but interesting... **) |
|
44 |
|
45 goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}"; |
|
46 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1); |
|
47 by (rewrite_goals_tac TF.con_defs); |
|
48 by (rtac equalityI 1); |
|
49 by (fast_tac (ZF_cs addIs [PartI] addSEs (PartE::TF.free_SEs)) 1); |
|
50 by (fast_tac (ZF_cs addIs ([PartI,InlI,InrI] @ [TF.dom_subset RS subsetD] |
|
51 @ data_typechecks) |
|
52 addSEs (PartE::TF.free_SEs)) 1); |
|
53 val tree_unfold = result(); |
|
54 |
|
55 goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}"; |
|
56 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1); |
|
57 by (rewrite_goals_tac TF.con_defs); |
|
58 by (rtac equalityI 1); |
|
59 by (fast_tac (ZF_cs addIs [PartI,InlI,InrI] |
|
60 addSEs (PartE::TF.free_SEs)) 1); |
|
61 by (fast_tac (ZF_cs addIs ([PartI,InlI,InrI] @ [TF.dom_subset RS subsetD] |
|
62 @ data_typechecks) |
|
63 addSEs ([PartE, sumE] @ TF.free_SEs)) 1); |
|
64 val forest_unfold = result(); |
|
65 |