1signature patriciaSyntax =
2sig
3
4  include Abbrev
5
6  val mk_ptree_type   : hol_type -> hol_type
7  val dest_ptree_type : hol_type -> hol_type
8  val is_ptree_type   : hol_type -> bool
9
10  val empty_tm           : term
11  val leaf_tm            : term
12  val branch_tm          : term
13  val peek_tm            : term
14  val find_tm            : term
15  val add_tm             : term
16  val add_list_tm        : term
17  val remove_tm          : term
18  val traverse_tm        : term
19  val keys_tm            : term
20  val transform_tm       : term
21  val every_leaf_tm      : term
22  val exists_leaf_tm     : term
23  val size_tm            : term
24  val depth_tm           : term
25  val is_ptree_tm        : term
26  val in_ptree_tm        : term
27  val insert_ptree_tm    : term
28  val branching_bit_tm   : term
29  val ptree_of_numset_tm : term
30  val numset_of_ptree_tm : term
31
32  val mk_empty           : hol_type -> term
33  val mk_leaf            : term * term -> term
34  val mk_branch          : term * term * term * term -> term
35  val mk_peek            : term * term -> term
36  val mk_find            : term * term -> term
37  val mk_add             : term * term -> term
38  val mk_add_list        : term * term -> term
39  val mk_remove          : term * term -> term
40  val mk_traverse        : term -> term
41  val mk_keys            : term -> term
42  val mk_transform       : term * term -> term
43  val mk_every_leaf      : term * term -> term
44  val mk_exists_leaf     : term * term -> term
45  val mk_size            : term -> term
46  val mk_depth           : term -> term
47  val mk_is_ptree        : term -> term
48  val mk_in_ptree        : term * term -> term
49  val mk_insert_ptree    : term * term -> term
50  val mk_branching_bit   : term * term -> term
51  val mk_ptree_of_numset : term * term -> term
52  val mk_numset_of_ptree : term -> term
53
54  val dest_leaf            : term -> term * term
55  val dest_branch          : term -> term * term * term * term
56  val dest_peek            : term -> term * term
57  val dest_find            : term -> term * term
58  val dest_add             : term -> term * term
59  val dest_add_list        : term -> term * term
60  val dest_remove          : term -> term * term
61  val dest_traverse        : term -> term
62  val dest_keys            : term -> term
63  val dest_transform       : term -> term * term
64  val dest_every_leaf      : term -> term * term
65  val dest_exists_leaf     : term -> term * term
66  val dest_size            : term -> term
67  val dest_depth           : term -> term
68  val dest_is_ptree        : term -> term
69  val dest_in_ptree        : term -> term * term
70  val dest_insert_ptree    : term -> term * term
71  val dest_branching_bit   : term -> term * term
72  val dest_ptree_of_numset : term -> term * term
73  val dest_numset_of_ptree : term -> term
74
75  val is_empty           : term -> bool
76  val is_leaf            : term -> bool
77  val is_branch          : term -> bool
78  val is_peek            : term -> bool
79  val is_find            : term -> bool
80  val is_add             : term -> bool
81  val is_add_list        : term -> bool
82  val is_remove          : term -> bool
83  val is_traverse        : term -> bool
84  val is_keys            : term -> bool
85  val is_transform       : term -> bool
86  val is_every_leaf      : term -> bool
87  val is_exists_leaf     : term -> bool
88  val is_size            : term -> bool
89  val is_depth           : term -> bool
90  val is_is_ptree        : term -> bool
91  val is_in_ptree        : term -> bool
92  val is_insert_ptree    : term -> bool
93  val is_branching_bit   : term -> bool
94  val is_ptree_of_numset : term -> bool
95  val is_numset_of_ptree : term -> bool
96
97end
98