1 (* Title: HOL/ex/Simult |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 A simultaneous recursive type definition: trees & forests |
|
7 |
|
8 This is essentially the same data structure that on ex/term.ML, which is |
|
9 simpler because it uses list as a new type former. The approach in this |
|
10 file may be superior for other simultaneous recursions. |
|
11 |
|
12 The inductive definition package does not help defining this sort of mutually |
|
13 recursive data structure because it uses Inl, Inr instead of In0, In1. |
|
14 *) |
|
15 |
|
16 Simult = SList + |
|
17 |
|
18 types 'a tree |
|
19 'a forest |
|
20 |
|
21 arities tree,forest :: (term)term |
|
22 |
|
23 consts |
|
24 TF :: 'a item set => 'a item set |
|
25 FNIL :: 'a item |
|
26 TCONS,FCONS :: ['a item, 'a item] => 'a item |
|
27 Rep_Tree :: 'a tree => 'a item |
|
28 Abs_Tree :: 'a item => 'a tree |
|
29 Rep_Forest :: 'a forest => 'a item |
|
30 Abs_Forest :: 'a item => 'a forest |
|
31 Tcons :: ['a, 'a forest] => 'a tree |
|
32 Fcons :: ['a tree, 'a forest] => 'a forest |
|
33 Fnil :: 'a forest |
|
34 TF_rec :: ['a item, ['a item , 'a item, 'b]=>'b, |
|
35 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b |
|
36 tree_rec :: ['a tree, ['a, 'a forest, 'b]=>'b, |
|
37 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b |
|
38 forest_rec :: ['a forest, ['a, 'a forest, 'b]=>'b, |
|
39 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b |
|
40 |
|
41 defs |
|
42 (*the concrete constants*) |
|
43 TCONS_def "TCONS M N == In0(M $ N)" |
|
44 FNIL_def "FNIL == In1(NIL)" |
|
45 FCONS_def "FCONS M N == In1(CONS M N)" |
|
46 (*the abstract constants*) |
|
47 Tcons_def "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))" |
|
48 Fnil_def "Fnil == Abs_Forest(FNIL)" |
|
49 Fcons_def "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))" |
|
50 |
|
51 TF_def "TF(A) == lfp(%Z. A <*> Part Z In1 |
|
52 <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))" |
|
53 |
|
54 rules |
|
55 (*faking a type definition for tree...*) |
|
56 Rep_Tree "Rep_Tree(n): Part (TF(range Leaf)) In0" |
|
57 Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t" |
|
58 Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z" |
|
59 (*faking a type definition for forest...*) |
|
60 Rep_Forest "Rep_Forest(n): Part (TF(range Leaf)) In1" |
|
61 Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts" |
|
62 Abs_Forest_inverse |
|
63 "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z" |
|
64 |
|
65 |
|
66 defs |
|
67 (*recursion*) |
|
68 TF_rec_def |
|
69 "TF_rec M b c d == wfrec (trancl pred_sexp) |
|
70 (%g. Case (Split(%x y. b x y (g y))) |
|
71 (List_case c (%x y. d x y (g x) (g y)))) M" |
|
72 |
|
73 tree_rec_def |
|
74 "tree_rec t b c d == |
|
75 TF_rec (Rep_Tree t) (%x y r. b (inv Leaf x) (Abs_Forest y) r) |
|
76 c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)" |
|
77 |
|
78 forest_rec_def |
|
79 "forest_rec tf b c d == |
|
80 TF_rec (Rep_Forest tf) (%x y r. b (inv Leaf x) (Abs_Forest y) r) |
|
81 c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)" |
|
82 end |
|